The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Hi,

I think yours ideas show a way how to linearize the propositional
disjunction so that the proof unicity holds. They will be useful in
many situations.

Thanks a lot.

Gyesik


2010/10/13 Jean-Francois Monin 
<jean-francois.monin AT imag.fr>:
> Hello,
>
> There is a simple solution without bool.
>
> Fixpoint VarInk (t:toto) : Prop -> Prop :=
>  fun A =>
>  match t with
>    | Var        => True
>    | Unit       => A
>    | Plus t0 t1 => (VarInk t0 (VarInk t1 A))
>  end.
>
> What you want is (VarInk t False).
>
> Proving
>
> Lemma VarInk_unicity :
>  forall (t : toto) (A: Prop), unicity A -> unicity (VarInk t A).
>
> is a piece of cake.
>
> Of course
> Definition unicity (P:Prop) := forall (p q: P), p=q.
>
>
> If you need the equivalence with your
> original definition, just prove (rather simple):
>
> Lemma varin_varink : forall t A, VarIn t \/ A -> VarInk t A.
> Lemma varink_varin : forall t A, VarInk t A -> VarIn t \/ A.
>
> Hope this helps,
> JF
>
> On Tue, Oct 12, 2010 at 02:40:28AM +0900, Gyesik Lee wrote:
>> Hi,
>>
>> I am not sure if the title of the message is adequate, so I apologize
>> in advance for any possible confusion.
>>
>> ========================
>>
>> (* Consider the following inductive definition.*)
>>
>> Inductive toto : Type :=
>>   Var   : toto
>> | Unit  : toto
>> | Plus  : toto -> toto -> toto.
>>
>> (* Now I would like to check if a (t : toto) contains [Var] or not.
>> One possible definition is as follows *)
>>
>> Fixpoint VarIn (t:toto) : Prop :=
>>   match r with
>>     | Var        => True
>>     | Unit       => False
>>     | Plus t0 t1 => (VarIn t0) \/ (VarIn t1)
>>   end.
>>
>> (* What I don't like with this definition is that I don't have the
>> proof unicity without using proof-irrelevance.
>> This doesn't mean that I don't like proof-irrelevance.
>>
>> Lemma VarIn_unicity : forall (t : toto) (p q : VarIn t), p = q.
>>
>>
>
> --
> Jean-Francois Monin
> CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1
>
> Office 3-605, FIT, Tsinghua University
> Haidian District, Beijing 100084, CHINA
> Tel: +86 10 62 79 69 79 ext 605
> Fax@LIAMA:
>  +86 10 6264 7458
>