The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Jan 13, 2005 at 10:55:01AM +0530, Param Jyothi Reddy wrote:
> Hi all, I was trying to understand how in intutionistic logic 
>      (forall P)(P(x)->P(y)) |- (forall P)(P(y)->P(x))
> is true.

> So i took a look at how Coq proves this.
> (http://www.labri.fr/Perso/~casteran/CoqArt/depprod/SRC/leibniz.v)

> leibniz_sym < intros a b H Q.
> 1 subgoal
> 
>   A : Set
>   a : A
>   b : A
>   H : forall P : A -> Prop, P a -> P b
>   Q : A -> Prop
>   ============================
>    Q b -> Q a
> 
> leibniz_sym < apply H.
> 1 subgoal
> 
>   A : Set
>   a : A
>   b : A
>   H : forall P : A -> Prop, P a -> P b
>   Q : A -> Prop
>   ============================
>    Q a -> Q a
 
> I am unable to understand how apply H resulted in Q a-> Q a. (My
> expectation was H applied to Q would be Q a -> Q b)

H is not applied to Q; "Apply" is being smarter than you (and I)
expect it to be. The P of H is not being unified with "Q", but with
something else. Indeed, if you try "Apply (H Q)." instead of just
"Apply.", you'll see that this doesn't work (it doesn't unify).

If you finish the proof and look at the lambda-term directly (with
"Print"), you'll see that the P of H is unified with
  (fun c : A => Q c -> Q a)

thus (P b) is (Q b -> Q a), our whole goal, and the application
generates as subgoal (P a), i.e. (Q a -> Q a).

-- 
Lionel