Skip to content

Instantly share code, notes, and snippets.

@amintimany
Last active December 10, 2021 00:02
Show Gist options
  • Save amintimany/798a096e2f2ff0582b36 to your computer and use it in GitHub Desktop.
Save amintimany/798a096e2f2ff0582b36 to your computer and use it in GitHub Desktop.
Facts stating equivalence of axioms K, URIP, UIP, eq_rect_eq, projT_2_eq and JMeq_eq in Coq.
Require Import Coq.Logic.JMeq.
Definition JMeq_eq := forall (A : Type) (x y : A), JMeq x y -> x = y.
Section Eq_Facts.
Variable A : Type.
Definition K := forall (x : A) (P : x = x -> Prop), P eq_refl -> forall (eq : x = x), P eq.
Definition URIP := forall (x : A) (eq : x = x), eq = eq_refl.
Definition UIP := forall (x y : A) (eq eq' : x = y), eq = eq'.
Definition eq_rect_eq := forall (x : A) (P : A -> Type) (eq : x = x) (p : P x), p = eq_rect x P p x eq.
Definition projT2_eq := forall (x : A) (P : A -> Type) (p q : P x), existT P x p = existT P x q -> p = q.
Lemma K_URIP : K -> URIP.
Proof.
intros k x eq.
apply (k _ (fun p => p = eq_refl) eq_refl).
Qed.
Lemma UIP_UIP : URIP -> UIP.
Proof.
intros urip x y eq eq'.
destruct eq'.
apply urip.
Qed.
Theorem UIP_eq_rect_eq : UIP -> eq_rect_eq.
Proof.
intros uip x P eq p.
rewrite (uip _ _ eq eq_refl); trivial.
Qed.
Theorem eq_rect_eq_projT2_eq : eq_rect_eq -> projT2_eq.
Proof.
intros ere x P p q H.
set (proj1_eq := fun (v : sigT P) (H : existT P x p = v) => match H in _ = z return projT1 (existT P x p) = projT1 z with eq_refl => eq_refl end).
assert (H' : match (proj1_eq (existT P x q) H) in _ = u return P u with eq_refl => projT2 (existT P x p) end = projT2 (existT P x q)).
{
destruct H; trivial.
}
cbv in ere.
rewrite <- (ere _ _ (proj1_eq _ H)) in H'; trivial.
Qed.
Theorem projT2_eq_k : projT2_eq -> K.
Proof.
intros p2 x P H eq.
cut (eq = eq_refl); [intros H'; rewrite H'; trivial|].
apply p2; destruct eq; trivial.
Qed.
Section Dec.
Hypothesis A_dec : forall a b : A, {a = b} + {a <> b}.
Definition make_eq {a b : A} (eq : a = b) : a = b.
Proof.
destruct (A_dec a b) as [H|H].
+ exact H.
+ exact (False_rect _ (H eq)).
Defined.
Theorem make_eq_const : forall {a b : A} (eq eq' : a = b), make_eq eq = make_eq eq'.
Proof.
intros a b eq eq'.
cbv.
destruct A_dec as [H|H]; trivial.
destruct (H eq).
Qed.
Theorem make_eq_com_sym : forall {a b : A} (eq : a = b), eq_trans (eq_sym (make_eq (eq_refl a))) (make_eq eq) = eq.
Proof.
intros a b eq.
destruct eq.
destruct (make_eq eq_refl); trivial.
Qed.
Theorem k : K.
Proof.
intros x P H eq.
rewrite <- make_eq_com_sym in H.
rewrite <- make_eq_com_sym.
replace (make_eq eq) with (make_eq (eq_refl x)); trivial.
apply make_eq_const.
Qed.
End Dec.
End Eq_Facts.
Theorem projT2_eq_JMeq_eq : (forall A, projT2_eq A) <-> JMeq_eq.
Proof.
split.
{
intros p2 A x y H.
inversion H as [H1 H2].
exact (p2 Type _ _ _ _ H2).
}
{
intros je A x P p q H.
apply je.
change (JMeq (projT2 (existT P x p)) (projT2 (existT P x q))).
rewrite H.
exact JMeq_refl.
}
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment