proof irrelevance.v

Inductive X : Prop :=  
  | A : X
  | B : X.

Definition proof_irrelevant := forall (P:Prop) (p1 p2:P), p1 = p2.

Goal A=B -> proof_irrelevant.
Proof.
intros H P p1 p2.
pose (fun x => match x with A => p1 | B => p2 end).
assert (p1 = p A). reflexivity.
assert (p2 = p B). reflexivity.
rewrite H0. rewrite H1. now rewrite H.
Qed.

Goal X <-> True.
split. auto. intros. exact A.
Qed.

Definition U := forall P:Prop, P -> X.

Definition not_X x := match x with A => B | B => A end.
Definition Raux (u:U) : X := not_X (u U u).

Section use_g.

Variable g : (U->X) -> U.
Variable g_eq : forall (a:U->X) (u:U), g a U u= a u.

Definition R : U := g Raux.

Lemma not_has_fixpoint : R U R = not_X (R U R).
Proof.
unfold R. apply g_eq.
Qed.

Theorem classical_proof_irrelevance : A=B.
Proof.
assert (R U R = A \/ R U R = B).
destruct (R U R). now left. now right.
destruct H; rewrite <- H; rewrite not_has_fixpoint; now rewrite H.
Qed.

End use_g.

Section use_em1.  (* うまくいかない方法 *)

Hypothesis EM : forall P:Prop, P \/ ~ P.

Definition g1 : (U->X) -> U.
Proof.
intros. intros P.
destruct (EM (P=U)); intros.
 - rewrite H0 in H1. exact (H H1).
 - exact A.
Defined.

Goal forall (a:U->X) (u:U), g1 a U u= a u.
Proof.
intros. unfold g1. unfold eq_ind.
destruct (EM (U=U)).
Admitted.

End use_em1.

Section use_em2.

Record retract (P1 P2: Prop) :=
  {i : P1 -> P2; j : P2 -> P1; inv : forall a:P1, j (i a) = a}.
Check retract.
Print retract.
Check Build_retract.

Theorem retract_id A : retract A A.
Proof. now refine {| i := (fun x => x) ; j := (fun x => x)  |}. Defined.

Hypothesis EM : forall P:Prop, P \/ ~ P.

Definition g (h: U -> X) :U.
unfold U. intros P.
destruct (EM (retract (P -> X) (U -> X))) as [H1|H1].
 - destruct (EM (retract (U-> X) (U -> X))) as [H2|H2].
   + exact (j _ _ H1 (i _ _ H2 h)).
   + elim H2. apply retract_id.
  - intros. exact A.
Defined.

Theorem g_eq : forall h x, g h U x= h x.
intros. unfold g.
destruct (EM (retract (U->X) (U->X))).
 - now rewrite (inv _ _ r).
 - contradiction n. apply retract_id.
Qed.

Goal proof_irrelevant.
apply Unnamed_thm.
apply (classical_proof_irrelevance g g_eq).
Qed.

(* 以下、うまくいかない方法 *)

Goal forall h x, g h U x= h x.
intros. unfold g.
pose (retract_id (U->X)).
Admitted. (* 等式の証明の中でEMをdestructしないといけない *)

Definition g2 (h: U -> X) :U.
unfold U. intros P.
destruct (EM ((P -> X) = (U -> X))).
 - rewrite <- H in h. exact h.
 - intros. exact A.
Defined.

Goal forall h x, g2 h U x= h x.
intros. unfold g2.
destruct (EM  ((U->X) = (U->X))).
 - unfold eq_ind_r. unfold eq_ind. unfold eq_sym.
Admitted. (* eqではうまくいかない *)

Definition g3 (h: U -> X) :U.
unfold U. intros P.
destruct (EM (retract (P -> X) (U -> X))).
 - exact (j _ _ H h).
 - intros. exact A.
Defined.

Goal forall h x, g3 h U x= h x.
intros. unfold g3.
destruct (EM (retract (U -> X) (U -> X))).
Admitted. (* gの定義でiとj両方使わないとうまくいかない *)

Definition g4 (h: U -> X) :U.
unfold U. intros P.
destruct (EM (retract (P -> X) (U -> X))).
  - pose (retract_id (U -> X)).
    exact (j _ _ H (i _ _ r h)).
  - intros. exact A.
Defined.

Goal forall h x, g4 h U x= h x.
Proof.
intros. unfold g4. unfold retract_id. simpl.
destruct (EM (retract (U->X) (U->X))).
 -
Admitted. (* gの定義でEMを1回しか使わないとうまくいかない *)

Definition g5 (h: U -> X) :U.
unfold U. intros P.
destruct (EM (retract (U -> X) (P -> X))).
  - destruct (EM (retract (P -> X) (P -> X))).
      + exact (j _ _ H0 (i _ _ H h)).
      + elim H0. apply retract_id.
  - intros. exact A.
Defined.

Goal forall h x, g5 h U x= h x.
Proof.
intros. unfold g5.
destruct (EM (retract (U->X) (U->X))).
  - now rewrite (inv _ _ r).
  - elim n. apply retract_id.
Qed. (* g5はうまくいく *)

End use_em2.

proofirrelevance.pdf