The Coq mailing list

[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