The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, this is a rather typical use of the "esplit" tactic. It is a 
variation of "eapply" for inductive types with a single constructor 
type. It simply destruct the constructor in the goal generating 
metavariables where dependencies are needed.

A bit of action :

Require Import List.
Axiom A : Set.

Goal forall (h:A) (t:list A) (o:list A), exists f : list A, f ++ o = 
h::t ++o.
intros.
esplit.
change (h::t++o) with ((h::t)++o).
reflexivity.
Qed.



As you can see while running the proof, unification is done at the time 
of the "reflexivity". I haven't figured a way to go around the "change" 
though, since "h::t++o" is in normal form where "(h::t)++o" is not. Coq 
unification is very first order.


Arnaud Spiwack

Sean Wilson a écrit :
> Hi,
>
> I'm working with goals containing existential quantifiers like the following:
>
> h : A
> t : list A
> o : list A
> ______________________________________(1/1)
> exists f : list A, f ++ o = h :: t ++ o
>
> To progress, I must call "exists h::t", which you can work out by unification 
> of the two sides of the equality. Does Coq have any way of inferring this and 
> solving the goal automatically? Also, are there any other tactics 
> besides "exists" that let me manipulate goals like this in useful ways?
>
> Regards,
>
> Sean
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>
>