The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Thomas,

> I was then told that I could use inductives, to do the same job.
> <--
> Inductive mem_spec_ind : elt -> t -> bool -> Type :=
>    | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
>    | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
> Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.
> -->
>
> Unfortunately, "destruct"-ing mem_eq in a Goal can lead to the
> forgetting of useful informations. I have to remember some pieces of
> information by hand, while everything is smoother using the
> rewrite-destruct scheme.

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)))).
   reflexivity.
   setdec.
 Qed.

Even with the 'wrong' definition you can also use inversion(_clear)
instead of destruct and you won't lose any information, but
unfortunately you'd have to explictely introduce the hypothesis to be
inverted. I'd like it a lot, actually, if the inversion tactic were to
work on arbitrary constructions instead of just hypotheses
identifiers.

On a more specific note, in your particular goal here, I'd rather use
existing lemmas and proceed without case split at all : rewrite twice
using EqProps.add_mem_3 and then EqProps.singleton_mem_1. If I can
give a direct proof, I tend to do it.

Cheers,

Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06