The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

Attached is a proof relying on Hurkens' paradox (not without pain)!

Hugo

On Thu, Nov 15, 2012 at 12:16:52AM +0100, Andreas Abel wrote:
> You could try to adopt Hurkens' Paradox (inconsistency of Prop :
> Prop).  I do not know whether it will work, because under the
> assumption
> 
>   H : Type = Prop
> 
> you only get something like
> 
>   cast H Prop : Prop
> 
> but it might work nevertheless.
> 
> Andreas
> 
> On 14.11.12 4:15 PM, Daniel Schepler wrote:
> >On Tue, Nov 13, 2012 at 4:54 PM, Jonas Oberhauser 
> ><s9joober AT gmail.com>
> > wrote:
> >>Can I prove
> >>
> >>Goal Prop <> Type.
> >>
> >>In coq?
> >>
> >>Kind regards,
> >>Jonas
> >
> >Well, Prop has impredicative constructions, which in Type would lead
> >to contradictions.  That's where I'd start looking for something to
> >distinguish between the two.  Though I couldn't immediately think of
> >any way to exploit this...
> >
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel AT ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
(** A proof of the inconsistency of Prop=Type (for some fixed Type) in Coq 
using 
    Hurkens' paradox for system Type:Type.

    Adapted from an initial formulation by Herman Geuvers (this formulation 
was used 
    to show the inconsistency in the pure calculus of constructions of a 
retract from 
    Prop into a small type).

    A. J. Hurkens, "A simplification of Girard's paradox",
    Proceedings of the 2nd international conference Typed Lambda-Calculi
    and Applications (TLCA'95), 1995.
*)

Section Paradox.

Definition Type2 := Type.
Definition Type1 := Type : Type2.

(** Preliminary *)

Notation "'rew2' <- H 'in' H'" := (@eq_rect_r Type2 _ (fun X : Type2 => X) H' 
_ H)
    (at level 10, H' at level 10).
Notation "'rew2' H 'in' H'" := (@eq_rect Type2 _ (fun X : Type2 => X) H' _ H)
    (at level 10, H' at level 10).
Notation "'rew1' <- H 'in' H'" := (@eq_rect_r Type1 _ (fun X : Type1 => X) H' 
_ H)
    (at level 10, H' at level 10).
Notation "'rew1' H 'in' H'" := (@eq_rect Type1 _ (fun X : Type1 => X) H' _ H)
    (at level 10, H' at level 10).

Lemma rew_rew : forall (A B:Type1) (H:B=A) (x:A), rew1 H in rew1 <- H in x = 
x.
Proof.
intros.
destruct H.
reflexivity.
Defined. 

(** Main assumption and proof *)

Variable Heq : Prop = Type1 :> Type2.

Definition down : Type1 -> Prop := fun A => rew2 <- Heq in A.
Definition up : Prop -> Type1 := fun A => rew2 Heq in A.

Lemma up_down : forall (A:Type1), up (down A) = A :> Type1.
Proof.
unfold down, up. rewrite Heq. reflexivity.
Defined.

Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up 
A -> Prop.
Definition U : Type1 := V -> Prop.

Definition forth (a:U) : up (down U) := rew1 <- (up_down U) in a.
Definition back (x:up (down U)) : U := rew1 (up_down U) in x. 

Definition sb (z:V) : V := fun A r a => r (z A r) a.
Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v 
A r a)).
Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U 
=> i (forth a)) (back x).
Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i 
x).
Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth 
a))).
Definition I (x:U) : Prop :=
  (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' 
(forth x)))) -> False.

Lemma back_forth (a:U) : back (forth a) = a.
Proof.
apply rew_rew.
Defined.

Lemma Omega : forall i:U -> Prop, induct i -> up (i WF).
Proof.
intros i y.
apply y.
unfold le, WF, induct.
rewrite up_down.
intros x H0.
apply y.
unfold sb, le', le.
rewrite back_forth.
exact H0.
Qed.

Lemma lemma1 : induct (fun u => down (I u)).
Proof.
unfold induct.
intros x p.
rewrite up_down.
intro q.
generalize (q (fun u => down (I u)) p).
rewrite up_down.
intro r.
apply r.
intros i j.
unfold le, sb, le', le in j |-.
rewrite back_forth in j.
specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth y))).
apply q.
exact j.
Qed.

Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False.
Proof.
intro x.
generalize (x (fun u => down (I u)) lemma1).
rewrite up_down.
intro r. apply r.
intros i H0.
apply (x (fun y => i (fun v => sb v (down U) le' (forth y)))).
unfold le, WF in H0.
rewrite up_down in H0.
exact H0.
Qed.

Theorem paradox : False.
Proof.
exact (lemma2 Omega).
Qed.

End Paradox.