The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

You could also just do this:

assert (~ P a) by auto.

I don't think I would ever introduce existential variables in an Ltac
script unless the script was intended to ultimately solve the goal
with eauto.

-Aaron

On Dec 5, 2007 2:56 PM, Brandon Moore 
<brandon_m_moore AT yahoo.com>
 wrote:
>
> 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.