The Coq mailing list

["Stefan O'Rear" <stefanor AT cox.net>]

On Sat, Sep 29, 2007 at 02:18:20PM +0100, Sean Wilson wrote:
> forall (p:Prop), p->p=True.
> 
> In Coq, none of the automated tactics do anything if you try to prove this 
> theorem and I really can't see any useful steps forward. I assume it isn't 
> true but I can't explain why. If it isn't true, does anyone have a good 
> explanation as to why it isn't true in Coq but it is in other logics?

Suppose that was true.  Then it has a proof-term; call it GP.

(GP (True -> True) (fun x:True => x)) is a form of type  True -> True =
True; call it P.

Let P' be the normal form of P.  This exists, due to strong
normalization (a prerequisite of consistency, and we hope Coq is
consistent).  By subject reduction, it also has type True -> True =
True.

In Coq, all normal forms of inductive type have the form (C a b c..),
where C is a constructor.  Thus, since the only constructor of eq is
refl_eq, P' has form (eq_refl TY) for some TY.  By the typing rules for
CIC, TY is β-convertable to both True and True -> True, and thus True
and True -> True are themselves β-convertable (transitivity).

But True and True -> True are distinct β-normal forms, so by
Church-Rosser they are not β-convertable.

QED


The story changes radically if you modify the logic by the introduction
of axioms.

Axiom prepositional_extensionality: forall (P1 P2: Prop), (P1 <-> P2) ->
P1 = P2.

Goal forall P: Prop, P -> P = True.
intros P t.
apply prepositional_extensionality.
tauto.
Qed.

Stefan

Attachment: signature.asc
Description: Digital signature