The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Stéphane Lescuyer a écrit :

> You should just be careful writing the inductive spec : uniform
> parameters are not the same thing as variables introduced in the
> constructors. In that case, you should have written :
>
> Inductive mem_spec_ind x s : bool -> Type :=
> | mem_spec_1 : In x s -> mem_spec_ind x s true
> | mem_spec_2 : ~In x s -> mem_spec_ind x s false.
> Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.
>
> and then destructing (mem_eq t1 t2) does not 'erase' t1 and t2, and
> everything goes fine :
>
>  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1 else 2)= 
> 1.
>    intros.
>    destruct (mem_eq z (add x (add y (singleton z)))).

Stephane's solution is correct. I would just like to point that there is 
a better tactic than "destruct" for this kind of inductives:

  case mem_eq. (* No arguments! Coq infers them when using "case". *)

Best regards,

Guillaume