The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

Hello

I have been trying to define a tactic to compose a negated hypothesis like ~(Q a)
and a lemma with dependent arguments like forall x, P x -> Q x into a new
hypothesis ~(P a). To get from a goal of false to a goal of P a just
requires apply H; apply lem. Constructively, I then expect to be able to
prove ~(P a), but I took a while to build the tactic, mostly
trying to get existential variables instantiated.

I eventually arrived at this fairly simple script

Ltac strech H lem :=
 let a := fresh "a" in
 evar (a:Prop); assert (~a);
 [let H1 := fresh "H" in intro H1; unfold a in H1; apply H; apply lem; apply H1
 | subst a].

I'm hoping for advice on the problems I ran into, and maybe some improvements
to the tactic.

Basically, the problem was that I found no was to instantiate existential variables
except apply.

Trying to resolve "a" above with instantiate failed with an error like
"the term is not well-typed in the environment of ?1720", whenever the term
was at all calculated, even just as in let g := *term* in instantiate (1:=g) in (Value of a).
It worked as instantiate (1:=*term*) in (Value of a), and even introducing a new
definition equal to the term I wanted to instantiate with did not help, so I'm not
sure what's wrong.

Other things I tried were matching against nonlinear patterns (which just failed),
and applying functions with existential variables in their types to arguments
with specific types (which complained that the types were not convertible).
instantiate doesn't seem suitable for automated use, except maybe in special
cases like evar variables. Is there any other way to resolve variables?

Thanks

Brandon

---

Never miss a thing.   Make Yahoo your homepage.