The Coq mailing list

[Josh Berdine <berdine AT dcs.qmul.ac.uk>]

Hi Coq-club,

I'm new to coq and having trouble automating a class of proof steps.  
I'm hoping someone will be able to suggest a way to get coq to do what 
I want.  For a distilled version of my problem, consider the coq code 
(I'm using coq v7.4):

Axiom exp : Set.
Axiom nil : exp.

Inductive app : Set := eeq : exp -> exp -> app.
Hint app_constr := Constructors app.

Inductive entl : Set := entlI : app -> app -> entl.
Hint entl_constr := Constructors entl.

Inductive ps : entl -> Prop :=
  axiom : (P:?) (ps (entlI P (eeq nil nil)))
| subst : (E,X,x:?)
          (ps (entlI (eeq x E) (X E)))
       -> (ps (entlI (eeq x E) (X x)))
.
Hint ps_constr := Constructors ps.

Now I want to prove things like:

Goal (E:?) (ps (entlI (eeq E nil) (eeq E nil))).

which I can like so:

  Proof.
    Change (E:?) (ps (entlI (eeq E nil) ([E:?](eeq E nil) E))).
    Auto.
  Qed.

Using Change here to beta-expand seems necessary since trying "Intro; 
Apply subst" reveals that the unification algorithm isn't complete 
enough, but once the beta-expansion is done unification is happy.

Now I would _really_ like to be able to automate these sort of steps, 
but can't figure out how.  I tried doing things like:

Tactic Definition Beta_ex_1 :=
  Match Context With [ |- (ps (entlI (eeq E ?1) ?2))] ->
  (Change (ps (entlI (eeq E ?1) ([E:?]?2 E)))).

but this is no good since E is unbound.  An attempted fix:

Tactic Definition Beta_ex_2 :=
  Match Context With [ |- (E:?) (ps (entlI (eeq E ?1) ?2))] ->
  (Change (E:?) (ps (entlI (eeq E ?1) ([E:?]?2 E)))).

is also no good since the pattern never matches, in fact even:

Match Context With [ |- (E:?) ?1] -> Try Assumption.

fails to match the above Goal.  Another attempted fix:

Tactic Definition Beta_ex_3 :=
  Match Context With [E:? |- (ps (entlI (eeq E ?1) ?2))] ->
  (Change (ps (entlI (eeq E ?1) ([E:?]?2 E)))).

also leaves E unbound.  I also considered:

Tactic Definition Beta_ex_4 :=
  Match Context With [?3:? |- (ps (entlI (eeq ?3 ?1) ?2))] ->
  (Change (ps (entlI (eeq ?3 ?1) ([?3:?]?2 ?3)))).

but this isn't even syntactically well-formed.

Is what I'm trying to do nonsensical?  Any ideas on how to accomplish 
it?  Do I need to go all the way to writing a tactic in caml?  Would 
switching to coq v8 help?

Cheers,  Josh