Skip to content

Instantly share code, notes, and snippets.

@fluiddynamics
Last active Nov 4, 2019
Embed
What would you like to do?
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.
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment