(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*                              Hurkens.v                               *)
(************************************************************************)

(** Exploiting Hurkens's paradox [[Hurkens95]] for system U- so as to
    derive various contradictory contexts.

    The file is devided in various sub-modules which all follow the
    same structure: a section introduce the contradictory hypotheses
    and a theorem named [paradox] concludes the module with a proof of
    [False].

    - The [Generic] module contains the actual Hurkens's paradox for a
      postulated shallow encoding of system U- in Coq. This is an
      adaptation by Arnaud Spiwack of a previous, more restricted
      implementation by Herman Geuvers. It is used to derive every
      other special cases of the paradox in this file.

    - The [NoRetractToImpredicativeUniverse] module contains a simple
      and effective formulation by Herman Geuvers [[Geuvers01]] of a
      result by Thierry Coquand [[Coquand90]]. It states that no
      impredicative sort can contain a type of which it is a
      retract. This result implies that Coq with classical logic
      stated in impredicative Set is inconsistent and that classical
      logic stated in Prop implies proof-irrelevance (see
      [ClassicalFacts.v])

    - The [NoRetractFromSmallPropositionToProp] module is a
      specialisation of the [NoRetractToImpredicativeUniverse] module
      to the case where the impredicative sort is [Prop].

    - The [NoRetractFromTypeToProp] module proves that [Prop] cannot
      be a retract of a larger type.

    - The [Prop_neq_Type] module proves that [Prop] is different from
      any larger [Type].

    References:

    - [[Coquand90]] T. Coquand, "Metamathematical Investigations of a
      Calculus of Constructions", Proceedings of Logic in Computer
      Science (LICS'90), 1990.

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

    - [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type
      Theory", 2001, revised 2007
      (see http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz).
*)

(* Pleasing coqdoc! *)


Set Universe Polymorphism.

(** A modular proof of Hurkens's paradox. It relies on an
    axiomatisation of a shallow embedding of system U- (i.e.  types of
    U- are interepreted by types of Coq). The universes are encoding
    in a style, due to Martin-Löf, where they are given with a set of
    name and a family [El:Name->Type] which interprets each name into
    a type. This allows the encoding of universe to be decoupled from
    Coq's universes. Dependent products and abstractions are similarly
    postulated rather than encoded as Coq's dependent products and
    abstractions. *)

Module Generic.

(** Notations used in the proof. *)

Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity).
Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200).
Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity).
Reserved Notation "f '·₁' x" (at level 5, left associativity).
Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity).
Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity).
Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity).
Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity).
Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200).
Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity).
Reserved Notation "f '·₀' x" (at level 5, left associativity).
Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity).
Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity).
Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity).

Section Paradox.

(* arnaud: do some Coqdoc formatting *)
(** Axiomatisation of impredicative universes in a Martin-Löf style *)

(** System U- has two impredicative universes. In the proof of the
    paradox they are slightly asymetric (in particular the reduction
    rules of the small universe are not needed).  Therefore, the
    axioms are duplicated allowing for a weaker requirement than the
    actual system U-. *)


(** Large universe *)
Variable U1 : Type.
Variable El1 : U1 -> Type.
(** Closure by small product *)
Variable Forall1 : forall u:U1, (El1 u -> U1) -> U1.
  Notation "'∀₁' x : A , B" := (Forall1 A (fun x => B)).
  Notation "A '⟶₁' B" := (Forall1 A (fun _ => B)).
Variable lam1 : forall u B, (forall x:El1 u, El1 (B x)) -> El1 (∀₁ x:u, B x).
  Notation "'λ₁' x , u" := (lam1 _ _ (fun x => u)).
Variable app1 : forall u B (f:El1 (Forall1 u B)) (x:El1 u), El1 (B x).
  Notation "f '·₁' x" := (app1 _ _ f x).
Variable beta1 : forall u B (f:forall x:El1 u, El1 (B x)) x,
                   (λ₁ y, f y) ·₁ x = f x.
(** Closure by large products ([U1] only needs to quantify over itself) *)
Variable ForallU1 : (U1->U1) -> U1.
  Notation "'∀₂' A , F" := (ForallU1 (fun A => F)).
Variable lamU1 : forall F, (forall A:U1, El1 (F A)) -> El1 (∀₂ A, F A).
  Notation "'λ₂' x , u" := (lamU1 _ (fun x => u)).
Variable appU1 : forall F (f:El1(∀₂ A,F A)) (A:U1), El1 (F A).
  Notation "f '·₁' [ A ]" := (appU1 _ f A).
Variable betaU1 : forall F (f:forall A:U1, El1 (F A)) A,
                    (λ₂ x, f x) ·₁ [ A ] = f A.

(** Small universe *)
(** The small universe is an element of the large one. *)
Variable u0 : U1.
Notation U0 := (El1 u0).
Variable El0 : U0 -> Type.
(** Closure by small product, [U0] does not need reduction rules *)
Variable Forall0 : forall u:U0, (El0 u -> U0) -> U0.
  Notation "'∀₀' x : A , B" := (Forall0 A (fun x => B)).
  Notation "A '⟶₀' B" := (Forall0 A (fun _ => B)).
Variable lam0 : forall u B, (forall x:El0 u, El0 (B x)) -> El0 (∀₀ x:u, B x).
  Notation "'λ₀' x , u" := (lam0 _ _ (fun x => u)).
Variable app0 : forall u B (f:El0 (Forall0 u B)) (x:El0 u), El0 (B x).
  Notation "f '·₀' x" := (app0 _ _ f x).
(** Closure by large products *)
Variable ForallU0 : forall u:U1, (El1 u->U0) -> U0.
  Notation "'∀₀¹' A : U , F" := (ForallU0 U (fun A => F)).
Variable lamU0 : forall U F, (forall A:El1 U, El0 (F A)) -> El0 (∀₀¹ A:U, F A).
  Notation "'λ₀¹' x , u" := (lamU0 _ _ (fun x => u)).
Variable appU0 : forall U F (f:El0(∀₀¹ A:U,F A)) (A:El1 U), El0 (F A).
  Notation "f '·₀' [ A ]" := (appU0 _ _ f A).

(** Automating the rewrite rules of our encoding. *)
Local Ltac simplify :=
  (* spiwack: ideally we could use [rewrite_strategy] here, but I am a tad
     scared of the idea of depending on setoid rewrite in such a simple
     file. *)
  (repeat rewrite ?beta1, ?betaU1);
  lazy beta.

Local Ltac simplify_in h :=
  (repeat rewrite ?beta1, ?betaU1 in h);
  lazy beta in h.


(** Hurkens's paradox. *)

(** An inhabitant of [U0] standing for [False]. *)
Variable F:U0.

(** Preliminary definitions *)

Definition V : U1 := ∀₂ A, ((A ⟶₁ u0) ⟶₁ A ⟶₁ u0) ⟶₁ A ⟶₁ u0.
Definition U : U1 := V ⟶₁ u0.

Definition sb (z:El1 V) : El1 V := λ₂ A, λ₁ r, λ₁ a, r ·₁ (z·₁[A]·₁r) ·₁ a.

Definition le (i:El1 (U⟶₁u0)) (x:El1 U) : U0 :=
  x ·₁ (λ₂ A, λ₁ r, λ₁ a, i ·₁ (λ₁ v, (sb v) ·₁ [A] ·₁ r ·₁ a)).
Definition le' : El1 ((U⟶₁u0) ⟶₁ U ⟶₁ u0) := λ₁ i, λ₁ x, le i x.
Definition induct (i:El1 (U⟶₁u0)) : U0 :=
  ∀₀¹ x:U, le i x ⟶₀ i ·₁ x.

Definition WF : El1 U := λ₁ z, (induct (z·₁[U] ·₁ le')).
Definition I (x:El1 U) : U0 :=
  (∀₀¹ i:U⟶₁u0, le i x ⟶₀ i ·₁ (λ₁ v, (sb v) ·₁ [U] ·₁ le' ·₁ x)) ⟶₀ F
.

(** Proof *)

Lemma Omega : El0 (∀₀¹ i:U⟶₁u0, induct i ⟶₀ i ·₁ WF).
Proof.
  refine (λ₀¹ i, λ₀ y, _).
  refine (y·₀[_]·₀_).
  unfold le,WF,induct. simplify.
  refine (λ₀¹ x, λ₀ h0, _). simplify.
  refine (y·₀[_]·₀_).
  unfold le. simplify.
  unfold sb at 1. simplify.
  unfold le' at 1. simplify.
  exact h0.
Qed.

Lemma lemma1 : El0 (induct (λ₁ u, I u)).
Proof.
  unfold induct.
  refine (λ₀¹ x, λ₀ p, _). simplify.
  refine (λ₀ q,_).
  assert (El0 (I (λ₁ v, (sb v)·₁[U]·₁le'·₁x))) as h.
  { generalize (q·₀[λ₁ u, I u]·₀p). simplify.
    intros q'.
    exact q'. }
  refine (h·₀_).
  refine (λ₀¹ i,_).
  refine (λ₀ h', _).
  generalize (q·₀[λ₁ y, i ·₁ (λ₁ v, (sb v)·₁[U] ·₁ le' ·₁ y)]). simplify.
  intros q'.
  refine (q'·₀_). clear q'.
  unfold le at 1 in h'. simplify_in h'.
  unfold sb at 1 in h'. simplify_in h'.
  unfold le' at 1 in h'. simplify_in h'.
  exact h'.
Qed.

Lemma lemma2 : El0 ((∀₀¹i:U⟶₁u0, induct i ⟶₀ i·₁WF) ⟶₀ F).
Proof.
  refine (λ₀ x, _).
  assert (El0 (I WF)) as h.
  { generalize (x·₀[λ₁ u, I u]·₀lemma1). simplify.
    intros q.
    exact q. }
  refine (h·₀_). clear h.
  refine (λ₀¹ i, λ₀ h0, _).
  generalize (x·₀[λ₁ y, i·₁(λ₁ v, (sb v)·₁[U]·₁le'·₁y)]). simplify.
  intros q.
  refine (q·₀_). clear q.
  unfold le in h0. simplify_in h0.
  unfold WF in h0. simplify_in h0.
  exact h0.
Qed.

Theorem paradox : El0 F.
Proof.
  exact (lemma2·₀Omega).
Qed.

End Paradox.

Ltac paradox h :=
  refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1.

End Generic.

(** There can be no retract to an impredicative Coq universe from a
    smaller type. In this version of the proof, the impredicativity of
    the universe is postulated with a pair of functions from the
    universe to its type and back which commute with dependent product
    in an appropriate way. *)

Module NoRetractToImpredicativeUniverse.

Section Paradox.

Let      U2    := Type.
Let      U1:U2 := Type.
Variable U0:U1.

(** [U1] is impredicative *)
Variable u22u1 : U2 -> U1.
Hypothesis u22u1_unit   : forall (c:U2), c -> u22u1 c.
(** [u22u1_counit] and [u22u1_coherent] only apply to dependent
    product so that the equations happen in the smaller [U1] rather
    than [U2].  Indeed, it is not generally the case that one can
    project from a large universe to an impredicative universe and
    then get back the original type again. It would be too strong a
    hypothesis to require (in particular, it is not true of
    [Prop]). The formulation is reminiscent of the monadic
    characteristic of the projection from a large type to [Prop].*)
Hypothesis u22u1_counit : forall (F:U1->U1), u22u1 (forall A,F A) -> (forall A,F A).
Hypothesis u22u1_coherent : forall (F:U1 -> U1) (f:forall x:U1, F x) (x:U1), 
                              u22u1_counit _ (u22u1_unit _ f) x = f x.

(** [U0] is a retract of [U1] *)
Variable u02u1 : U0 -> U1.
Variable u12u0 : U1 -> U0.
Hypothesis u12u0_unit   : forall (b:U1), b -> u02u1 (u12u0 b).
Hypothesis u12u0_counit : forall (b:U1), u02u1 (u12u0 b) -> b.

(** Paradox *)

Theorem paradox : forall F:U1, F.
Proof.
  intros F.
  Generic.paradox h.
  (** Large universe *)
  + exact U1.
  + exact (fun X => X).
  + cbn. exact (fun u F => forall x:u, F x).
  + cbn. exact (fun _ _ x => x).
  + cbn. exact (fun _ _ x => x).
  + cbn. easy.
  + cbn. exact (fun F => u22u1 (forall x, F x)).
  + cbn. exact (fun _ x => u22u1_unit _ x).
  + cbn. exact (fun _ x => u22u1_counit _ x).
  + cbn. intros **. now rewrite u22u1_coherent.
  (** Small universe *)
  + exact U0.
  (** The interpretation of the small universe is the image of
      [U0] in [U1]. *)
  + cbn. exact (fun X => u02u1 X).
  + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))).
  + cbn. intros * x. exact (u12u0_unit _ x).
  + cbn. intros * x. exact (u12u0_counit _ x).
  + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))).
  + cbn. intros * x. exact (u12u0_unit _ x).
  + cbn. intros * x. exact (u12u0_counit _ x).
  + cbn. exact (u12u0 F).
  + cbn in h.
    exact (u12u0_counit _ h).
Qed.

End Paradox.

End NoRetractToImpredicativeUniverse.


(** * Inconsistency of the existence in the pure Calculus of Constructions of a retract from Prop into a small type of Prop *)

Module NoRetractFromSmallPropositionToProp.

Section Paradox.

(** Assumption of a retract from Prop to a small type in Prop, using *)
(*     equivalence as the equality on propositions *)

Variable bool : Prop.
Variable p2b : Prop -> bool.
Variable b2p : bool -> Prop.
Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).

Theorem paradox : forall B:Prop, B.
Proof.
  intros B.
  pose proof
      (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P.
  refine (P _ _ _ _ _ _ _ _ _ _);clear P.
  + exact bool.
  + exact (fun x => forall P:Prop, (x->P)->P).
  + cbn. exact (fun _ x P k => k x).
  + cbn. intros F P x.
    apply P.
    intros f.
    exact (f x).
  + cbn. easy.
  + exact b2p.
  + exact p2b.
  + exact p2p2.
  + exact p2p1.
Qed.

End Paradox.

End NoRetractFromSmallPropositionToProp.

(** * Inconsistency of the existence in the Calculus of Constructions with universes of a retract from some Type universe into Prop. *)

(** Note: Assuming the context [down:Type->Prop; up:Prop->Type; forth:
      forall (A:Type), A -> up (down A); back: forall (A:Type), up
      (down A) -> A; H: forall (A:Type) (P:A->Type) (a:A),
      P (back A (forth A a)) -> P a] is probably enough.  *)

Module NoRetractFromTypeToProp.

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

Section Paradox.

(** Assumption of a retract from Type into Prop *)

Variable down : Type1 -> Prop.
Variable up : Prop -> Type1.
Hypothesis up_down : forall (A:Type1), up (down A) = A :> Type1.

Theorem paradox : forall P:Prop, P.
Proof.
  intros P.
  Generic.paradox h.
  (** Large universe. *)
  + exact Type1.
  + exact (fun X => X).
  + cbn. exact (fun u F => forall x, F x).
  + cbn. exact (fun _ _ x => x).
  + cbn. exact (fun _ _ x => x).
  + cbn. easy.
  + exact (fun F => forall A:Prop, F(up A)).
  + cbn. exact (fun F f A => f (up A)).
  + cbn.
    intros F f A.
    specialize (f (down A)).
    rewrite up_down in f.
    exact f.
  + cbn.
    intros F f A.
    destruct (up_down A). cbn.
    reflexivity.
  + exact Prop.
  + cbn. exact (fun X => X).
  + cbn. exact (fun A P => forall x:A, P x).
  + cbn. exact (fun _ _ x => x).
  + cbn. exact (fun _ _ x => x).
  + cbn. exact (fun A P => forall x:A, P x).
  + cbn. exact (fun _ _ x => x).
  + cbn. exact (fun _ _ x => x).
  + cbn. exact P.
  + exact h.
Qed.

End Paradox.

End NoRetractFromTypeToProp.

(** Application: Prop<>Type for some given Type *)

Module PropNeqType.

Import NoRetractFromTypeToProp.

Section Paradox.

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).

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 up, down. rewrite Heq. reflexivity.
Defined.

Theorem paradox : False.
Proof.
apply paradox with down up.
apply up_down.
Qed.

End Paradox.

End PropNeqType.