The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

> You could also just do this:

> assert (~ P a) by auto.

That's a great suggestions for manual use, but I don't see
how to use it for my script.

I  was trying to make a tactic that works with lemmas with
with arbitrary numbers of dependent arguments. I should
have given another example. A case I'm actually using has four,

union_l : forall bound_l bound_r x y,
 in_rect bound_l x y -> in_rect (union bound_l bound_r) x y

Given that, the main problem in coming up with the tactic
turns out to be calculating P in the first place.

My final script only makes one existential variable, so I can
use assert before knowing P, and resolve P once it is exposed
by applying the lemma in the subgoal.

(I also experimented with examining the type of the lemma
by applying it to existential variables, which was much more
complicated)

> 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.

Is that because you can do everything with existing tactics that
encapsulate them, because they make scripts harder to understand,
or because they are hard to use?

Thanks for the suggestions

Brandon

(sorry for the duplicate, I accidentally replied directly)

---

Never miss a thing.   Make Yahoo your homepage.