Tactics for goals containing "exists"

[Sean Wilson]

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

[Andrew McCreight]

Hi,

econstructor

followed by reflexivity does what you want.

-Andrew

Post by Sean Wilson
Hi,
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

[Arnaud Spiwack]

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

Post by Sean Wilson
Hi,
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