The Coq mailing list

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

On Dec 6, 2007 1:55 PM, Brandon Moore 
<brandon_m_moore AT yahoo.com>
 wrote:
> 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.

I see.  This is a more "interesting" situation.  I was able to write a
tactic that does not use existential variables, but it is (as written)
much slower than yours.  I also wrote another version that is
fundamentally the same as yours but relies on a lemma (in the manner
of Frederic's).  I find it as a slight improvement on a purely
subjective basis.  I don't know how to answer your questions about
existential variables, but perhaps my versions of the tactics will
give you some ideas on how to avoid those situations.

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

I think they are somewhat unpredictable (and your original message is
a case in point), and thus I would worry about the robustness of the
tactic.  Moreover, I suspected that their use could not add anything
over other ways of writing tactics.  This situation at hand, however,
would seem to indicate that they can be used for writing more
efficient tactics in some special cases.

-Aaron

Lemma contrapositive : forall P Q : Prop,
  (P -> Q) -> ~ Q -> ~ P.
Proof. tauto. Qed.

Ltac infer_neg1 Hneg lem :=
  match goal with
  | |- _ =>
    pose proof (contrapositive _ _ lem Hneg);
    try clear lem
  | a : _ |- _ =>
    let lem' := fresh in
    pose proof (lem a) as lem';
    try clear lem;
    infer_neg1 Hneg lem'
  end.

Lemma contrapositive_strengthening : forall P Q R : Prop,
  ((P -> Q) -> (~ Q -> ~ P) -> R) ->
  (P -> Q) -> R.
Proof. tauto. Qed.

Ltac infer_neg2 Hneg lem :=
  generalize Hneg;
  let H := fresh in
  intros H; eapply contrapositive_strengthening; [
    let J := fresh in
    intros _ J; apply J in H; clear J
  | apply lem ].

Parameter A : Set.
Parameters P Q : A -> A -> A -> Prop.
Parameters f : A -> A -> A.
Hypothesis lem : forall w x y z, P x y z -> Q (f w x) y z.

Lemma foo : forall a b c d,
  ~ Q (f a b) c d ->
  ~ P b c d.
Proof.
  intros ? ? ? ? H.
  infer_neg1 H lem.
  infer_neg2 H lem.
  auto.
Qed.