The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Quoting Lionel Elie Mamane 
<lionel AT mamane.lu>:



>
> H is not applied to Q; "Apply" is being smarter than you (and I)
> expect it to be.


Well, when I was young, I used to help "apply" to get the correct
intantiation of "P". This was done using the tactic "pattern".

Here is the proof in that style :

Set Implicit Arguments.
Definition leibniz (A:Set)(a b:A):= forall P:A->Prop, P a -> P b.

Theorem leibniz_sym : forall (A:Set)( a b:A), leibniz  a b -> leibniz b a.
Proof.
 unfold leibniz at 2;intros A a b H P.
 (*
  A : Set
  a : A
  b : A
  H : leibniz a b
  P : A -> Prop
  ============================
   P b -> P a
 *)
 pattern b.
 (*
  A : Set
  a : A
  b : A
  H : leibniz a b
  P : A -> Prop
  ============================
   (fun a0 : A => P a0 -> P a) b
 *)
 apply H.
 (*
 1 subgoal

  A : Set
  a : A
  b : A
  H : leibniz a b
  P : A -> Prop
  ============================
   P a -> P a
 *)
 trivial.
Qed.


Now, it seems that "apply" is smarter than it was, or that we thought it was).
There remain some cases in which "pattern" is useful, so, you can try
to use "apply" directly, and use "pattern" in case of difficulty.

"pattern" is also very useful for using rewrite or elimination tactics,
and in general when what you need is not the default behaviour.


Pierre




-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.