Load "geuvers-coquand".
Implicit Arguments On.
Section Orderings.
Variable U:Type.
 
Definition Relation := U -> U ->  Prop.
Variable R:Relation.
 
Definition Reflexive := (x : U)  (R x x).
 
Definition Transitive := (x, y, z : U) (R x y) -> (R y z) ->  (R x z).
 
Definition Symmetric := (x, y : U) (R x y) ->  (R y x).
 
Definition Antisymmetric := (x, y : U) (R x y) -> (R y x) ->  x == y.
 
Definition Contains := [R, R' : Relation] (x, y : U) (R' x y) ->  (R x y).
 
Record Partial_equivalence : Prop := {
   Prf_trans: Transitive;
   Prf_sym: Symmetric }.
 
Record Equivalence : Prop := {
   Prf_refl: Reflexive;
   Prf_pequiv:> Partial_equivalence }.
End Orderings.
Section Quotients.
 
Definition comp :=
   [E, F, G : Type] [g : F ->  G] [f : E ->  F] [x : E]  (g (f x)).
 
Definition compatible :=
   [E, F : Type]
   [R : (Relation E)] [f : E ->  F] (x, y : E) (R x y) ->  (f x) == (f y).
 
Record type_quotient [E : Type; R : (Relation E); p : (Equivalence R)] : Type := {
   quo:> Type;
   class:> E ->  quo;
   quo_comp: (x, y : E) (R x y) ->  (class x) == (class y);
   quo_comp_rev: (x, y : E) (class x) == (class y) ->  (R x y);
   quo_lift: (F : Type) (f : E ->  F) (compatible R f) -> quo ->  F;
   quo_lift_prop:
     (F : Type)
     (f : E ->  F) (H : (compatible R f))  (comp (quo_lift F f H) class) == f;
   quo_ind: (P : quo ->  Prop) ((x : E)  (P (class x))) -> (y : quo)  (P y) }.
 
Axiom
   quotient :
   (E : Type) (R : (Relation E)) (p : (Equivalence R))  (type_quotient p).
Variable E:Type.
Variable R:(Relation E).
Variable p:(Equivalence R).
Variable F:Type.
 
Definition S : (Relation F ->  E) := [f, g : F ->  E] (x : F)  (R (f x) (g x)).
 
Lemma Sequiv: (Equivalence S).
Split; Try Red; Try Split; Try Red.
Intros x x0; Apply (Prf_refl p).
Unfold S.
Intros x y z; Try Assumption.
Intros H H0 x0; Apply (Prf_trans p) with y := (y x0); Auto.
Unfold S; Intros; Apply (Prf_sym p); Auto.
Qed.
 
Axiom
   Extensionality :
   (F, G : Type) (f, g : F ->  G) ((x : F)  (f x) == (g x)) ->  f == g.
 
Lemma ps: (compatible S [f : F ->  E]  (comp (class (quotient p)) f)).
Red.
Unfold S comp.
Intros x y H; Try Assumption.
Apply Extensionality.
Intros x0; Try Assumption.
Apply (quo_comp (quotient p)); Auto.
Qed.
 
Axiom
   theta_surj :
   (f : F ->  (quotient p))
    (!exT
     (quotient Sequiv)
     [g : (quotient Sequiv)]
      ((!quo_lift ? ? ? (quotient Sequiv) ? ? ps) g) == f).
 
Definition Id := [E : Type] [x : E]  x.
 
Definition P1 :=
   [f : (quo (quotient p)) ->  (quo (quotient p))]
    (!exT
     (quo (quotient p)) ->  E
     [s : (quo (quotient p)) ->  E]  (comp (class (quotient p)) s) == f).
End Quotients.
Section Q2.
Variable E:Type.
Variable R:(Relation E).
Variable p:(Equivalence R).
Variable F:Type.
 
Lemma step0:
 (f : (quotient p) ->  (quotient p))
  (!exT
   (quo (quotient p)) ->  E
   [s : (quo (quotient p)) ->  E]  (comp (class (quotient p)) s) == f).
Intros f.
Generalize (theta_surj f).
Intros H; Try Assumption.
Elim H; Intros g H0; Clear H; Try Exact H0.
Rewrite <- H0.
Apply (!quo_ind ? ? ? (quotient (!Sequiv ? ? p (quotient p))))
     with
      P :=
      [g : (quotient (!Sequiv ? ? p (quotient p)))]
       (exT
        (quotient p) ->  E
        [s : (quotient p) ->  E]
         (comp (quotient p) s) == (quo_lift (!ps ? ? p (quotient p)) g)).
Intros h; Try Assumption.
Generalize
 (!quo_lift_prop
  ? ? ? (quotient (!Sequiv ? ? p (quotient p))) ? ? (!ps ? ? p (quotient p))).
Intros H; Try Assumption.
Cut
 ((comp (quo_lift (ps p 4!(quotient p))) (quotient (Sequiv p (quotient p)))) h) ==
 (comp (quotient p) h).
Intros H1; Try Assumption.
Unfold 1 comp in H1.
Rewrite H1.
Exists h; Auto.
Rewrite H; Auto.
Qed.
End Q2.
Section P3.
 
Inductive P2 : Type :=
  p1: Prop ->  P2
 | p2: Prop ->  P2 .
 
Inductive RP2 : P2 -> P2 ->  Prop :=
  RP4_12: (x, y : Prop) x -> y ->  (RP2 (p1 x) (p2 y))
 | RP4_21: (x, y : Prop) x -> y ->  (RP2 (p2 x) (p1 y))
 | RP4_11: (x, y : Prop) (iff x y) ->  (RP2 (p1 x) (p1 y))
 | RP4_22: (x, y : Prop) (iff x y) ->  (RP2 (p2 x) (p2 y)) .
Hints Resolve RP4_12 RP4_21 RP4_11 RP4_22 :P4base.
 
Lemma coupdepouceaauto: (P, Q : Prop) (iff P Q) ->  (iff Q P).
Intros P Q H; Try Assumption.
Elim H; Intros; Split; Auto with *.
Qed.
Hints Immediate coupdepouceaauto :P4base.
 
Lemma RP4equiv: (Equivalence RP2).
Split; Try Red; Try Split; Try Red.
Intros.
Case x; Intros P; [Apply RP4_11 | Apply RP4_22]; Split; Auto with *.
Intros x y z; Try Assumption.
2:Intros x y H; Try Assumption.
2:Inversion H; Auto with *.
Intros H H0; Try Assumption.
Inversion H; Inversion H0; Try (Rewrite <- H4 in H7; Inversion H7);
 Try (Rewrite <- H4 in H6; Inversion H6);
 Try (Rewrite <- H3 in H6; Inversion H6);
 Try (Rewrite <- H3 in H5; Inversion H5); Auto with *.
Apply RP4_11; Split; Auto with *.
Apply RP4_12; Elim H5; Rewrite <- H9 in H2; Intros; Auto with *.
Apply RP4_22; Split; Auto with *.
Apply RP4_21; Elim H5; Rewrite <- H9 in H2; Intros; Auto with *.
Apply RP4_12; Intros; Rewrite H9 in H4; Elim H1; Auto with *.
Apply RP4_11; Elim H1; Elim H4; (Intros; Split); Auto with *.
Intros x00; Apply H7; Rewrite H8; Apply H10; Exact x00.
Intros y11; Apply H11; Rewrite <- H8; Apply H9; Exact y11.
Apply RP4_21; Elim H1; Intros.
Apply H10; Rewrite <- H9; Exact H4.
Try Exact H5.
Apply RP4_22; Split; Auto with *.
Elim H4; Elim H1; Auto.
Intros H7 H9 H10 H11 H12; Try Assumption.
Apply H10; Rewrite H8; Apply H7; Exact H12.
Intros y11.
Elim H4; Elim H1; Intros.
Apply H9; Rewrite <- H8; Apply H11; Exact y11.
Qed.
 
Definition height : P2 ->  bool :=
   [x : P2]  Cases x of (p1 p) => true | (p2 p) => false end.
 
Definition down : P2 ->  bool := [x : P2]  (negb (height x)).
 
Tactic Definition CaseEq x :=
 Generalize (refl_eqT ? x); Pattern -1 x; Case x.
 
Lemma P21: (P, Q : Prop) (RP2 (p2 P) (p1 Q)) ->  P.
Intros P Q H; Try Assumption.
Inversion H.
Exact H2.
Qed.
 
Lemma P12: (P, Q : Prop) (RP2 (p1 P) (p2 Q)) ->  P.
Intros P Q H; Try Assumption.
Inversion H.
Exact H2.
Qed.
 
Lemma P12_2: (P, Q : Prop) (RP2 (p1 P) (p2 Q)) ->  Q.
Intros P Q H; Try Assumption.
Inversion H.
Exact H3.
Qed.
 
Lemma P21_2: (P, Q : Prop) (RP2 (p2 P) (p1 Q)) ->  Q.
Intros P Q H; Try Assumption.
Inversion H.
Exact H3.
Qed.
 
Lemma existence_decision:
 (!exT ? [f : Prop ->  bool] (P : Prop)  (iff P (f P) = true)).
Generalize (!step0 P2 RP2 RP4equiv (!Id (quotient RP4equiv))).
Intros H; Try Assumption.
Elim H; Intros s H0; Clear H; Try Exact H0.
Exists Cases (height (s (class (quotient RP4equiv) (p2 True)))) of
         true => [p : Prop]  (height (s (class (quotient RP4equiv) (p2 p))))
        | false => [p : Prop]  (down (s (class (quotient RP4equiv) (p1 p))))
       end.
Intros P; Try Assumption.
Split.
(CaseEq '(height (s ((quotient RP4equiv) (p2 True))))).
Intros hp2T.
Intros H1; Try Assumption.
Unfold height in hp2T.
Unfold height.
Cut ((quotient RP4equiv) (p2 P)) == ((quotient RP4equiv) (p2 True)).
Intros H2; Try Assumption.
Rewrite H2.
Generalize hp2T.
(CaseEq '(s ((quotient RP4equiv) (p2 True)))); Auto with *.
Intros a b c; Inversion c.
Apply (!quo_comp ? ? ? (quotient RP4equiv)).
Apply RP4_22; Split; Auto with *.
2:(CaseEq '(height (s ((quotient RP4equiv) (p2 True))))).
2:Intros hp2T.
2:Unfold height.
2:(CaseEq '(s ((quotient RP4equiv) (p2 P)))).
2:Intros P0 H H1; Try Assumption.
2:Apply P21 with Q := P0.
2:Apply (!quo_comp_rev ? ? ? (quotient RP4equiv)).
2:Change
   ((!Id (quotient RP4equiv)) ((quotient RP4equiv) (p2 P))) ==
   ((!Id (quotient RP4equiv)) ((quotient RP4equiv) (p1 P0))).
2:Transitivity ((comp (quotient RP4equiv) s) ((quotient RP4equiv) (p2 P))).
2:Rewrite <- H0; Reflexivity.
2:Unfold comp Id.
2:Apply (!congr_eqT ? ? (class (quotient RP4equiv))).
2:Try Exact H.
2:Intros P0 H H1; Inversion H1.
Intros hp2T.
Intros P0.
Unfold height in hp2T.
Unfold down negb height; Simpl.
Cut ((quotient RP4equiv) (p1 P)) == ((quotient RP4equiv) (p1 True)).
Intros H2; Try Assumption.
Rewrite H2.
Cut ((quotient RP4equiv) (p1 True)) == ((quotient RP4equiv) (p2 True)).
Intros hypenplus.
Rewrite hypenplus.
Generalize hp2T.
(CaseEq '(s ((quotient RP4equiv) (p2 True)))); Auto with *.
Intros a H3 H4; Inversion H4.
Apply (!quo_comp ? ? ? (quotient RP4equiv)).
Apply RP4_12; Split; Auto with *.
Apply (!quo_comp ? ? ? (quotient RP4equiv)).
Apply RP4_11; Split; Auto with *.
Intros hp2T.
Unfold down; Unfold negb.
(CaseEq '(s ((quotient RP4equiv) (p1 P)))).
Intros a b c; Inversion c.
Intros P0 H H1; Try Assumption.
Simpl in H1.
Apply P12 with Q := P0.
Apply (!quo_comp_rev ? ? ? (quotient RP4equiv)).
Change
 ((!Id (quotient RP4equiv)) ((quotient RP4equiv) (p1 P))) ==
 ((!Id (quotient RP4equiv)) ((quotient RP4equiv) (p2 P0))).
Transitivity ((comp (quotient RP4equiv) s) ((quotient RP4equiv) (p1 P))).
Rewrite <- H0; Reflexivity; Unfold comp Id;
 Apply (!congr_eqT ? ? (class (quotient RP4equiv))); Try Exact H.
Unfold comp Id.
Apply (!congr_eqT ? ? (class (quotient RP4equiv))).
Exact H.
Qed.
 
Lemma problem: False.
Generalize existence_decision.
Intros yH.
Elim yH; Intros f H; Clear yH.
Cut (P : Prop)  {P}+{~ P}.
Exact par.
Intros P.
Generalize (refl_equal ? (f P)); Pattern -1 (f P); Case (f P).
Intros H0.
Case (H P).
Intros H1 H2.
Left; Exact (H2 H0).
Intros hyp; Right.
Unfold not; Intros p.
Case (H P).
Intros H0 H1.
Rewrite (H0 p) in hyp; Inversion hyp.
Qed.
 
Lemma EM: (P : Prop)  P \/ ~ P.
Generalize existence_decision.
Intros yH.
Elim yH; Intros f H; Clear yH.
Intros P; Try Assumption.
Generalize (H P); Case (f P); Intros H0; (Elim H0; Intros; Intuition).
Qed.
End P3.