The Coq mailing list

[Remi Vanicat <remi.vanicat AT gmail.com>]

On Thu, 13 Jan 2005 10:55:01 +0530, Param Jyothi Reddy 
<paramr AT gmail.com>
 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. In classical logic this follows from (not P->not Q |- P->Q)
> 
> So i took a look at how Coq proves this.
> (http://www.labri.fr/Perso/~casteran/CoqArt/depprod/SRC/leibniz.v)
> 
> i got
> 
> 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)

Well, we have for all P, P a -> P b
let P be (fun x => Q x -> Q a)

then we have P a -> P b

that is (Q a -> Q a) -> (Q b -> Q a)

It is what coq has done when you apply H to the Q b -> Q a goal.