Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/coherence_either.v

Created October 23, 2025 19:23
Show Gist options
  • Save EduardoRFS/8fb6ecbe7b34b78e772b1bc207ad3395 to your computer and use it in GitHub Desktop.
Save EduardoRFS/8fb6ecbe7b34b78e772b1bc207ad3395 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coherence_either.v
Definition sig_fst {A B} {p q : {x : A | B x}} (H : p = q)
: proj1_sig p = proj1_sig q :=
eq_rect _ (fun z => proj1_sig p = proj1_sig z) eq_refl _ H.
Definition sig_snd {A B} {p q : {x : A | B x}} (H : p = q)
: eq_rect _ B (proj2_sig p) _ (sig_fst H) = proj2_sig q :=
match H with
| eq_refl => eq_refl
end.
Lemma sig_ext {A B} (p q : {x : A | B x})
(H1 : proj1_sig p = proj1_sig q)
(H2 : eq_rect _ B (proj2_sig p) _ H1 = proj2_sig q)
: p = q.
destruct p, q; simpl in *.
destruct H1, H2; simpl in *.
reflexivity.
Defined.
Definition sigT_fst {A B} {p q : {x : A & B x}} (H : p = q)
: projT1 p = projT1 q :=
eq_rect _ (fun z => projT1 p = projT1 z) eq_refl _ H.
Definition sigT_snd {A B} {p q : {x : A & B x}} (H : p = q)
: eq_rect _ B (projT2 p) _ (sigT_fst H) = projT2 q :=
match H with
| eq_refl => eq_refl
end.
Lemma sigT_ext {A B} (p q : {x : A & B x})
(H1 : projT1 p = projT1 q)
(H2 : eq_rect _ B (projT2 p) _ H1 = projT2 q)
: p = q.
destruct p, q; simpl in *.
destruct H1, H2; simpl in *.
reflexivity.
Defined.
(* bool *)
Definition C_Bool : Type := forall A : Type, A -> A -> A.
Definition c_true : C_Bool := fun A t f => t.
Definition c_false : C_Bool := fun A t f => f.
Definition I_Bool (c_b : C_Bool) : Type :=
forall P, P c_true -> P c_false -> P c_b.
Definition i_true : I_Bool c_true := fun P t f => t.
Definition i_false : I_Bool c_false := fun P t f => f.
Definition W_Bool : Type := {c_b : C_Bool & I_Bool c_b}.
Definition w_true : W_Bool := existT _ c_true i_true.
Definition w_false : W_Bool := existT _ c_false i_false.
Definition Bool : Type := {w_b : W_Bool &
projT1 w_b _ (w_true = w_b) (w_false = w_b)}.
Definition true : Bool := existT _ w_true eq_refl.
Definition false : Bool := existT _ w_false eq_refl.
Module Bool.
Lemma weak_ind (w_b : W_Bool) :
forall P : W_Bool -> Prop,
(forall i_b, P (existT _ c_true i_b)) ->
(forall i_b, P (existT _ c_false i_b)) -> P w_b.
intros P t f; destruct w_b as [c_b i_b]; simpl in *.
refine (i_b (fun c_b => forall i_b, P (existT _ c_b i_b))
_ _ i_b); clear i_b; intros i_b.
apply t.
apply f.
Defined.
Lemma w_true_next_w {w_b} (w : w_true = w_b) : w_true = w_b.
induction w_b using weak_ind; simpl.
exact (
match w in (_ = w_b) return (
projT1 w_b _ (w_true = w_b) (w_false = w_b)
) with
| eq_refl => eq_refl
end
).
exact w.
Defined.
Lemma w_false_next_w {w_b} (w : w_false = w_b) : w_false = w_b.
induction w_b using weak_ind; simpl.
exact w.
exact (
match w in (_ = w_b) return (
projT1 w_b _ (w_true = w_b) (w_false = w_b)
) with
| eq_refl => eq_refl
end
).
Defined.
Lemma contr_true w : true = existT _ w_true w.
apply (sigT_ext true (existT _ _ _) w).
simpl in *; unfold eq_rect, c_true in *.
exact (
match w in (_ = w_b) return w_true_next_w w = w with
| eq_refl => eq_refl
end
).
Defined.
Lemma contr_false w : false = existT _ w_false w.
apply (sigT_ext false (existT _ _ _) w).
simpl in *; unfold eq_rect, c_false in *.
exact (
match w in (_ = w_b) return w_false_next_w w = w with
| eq_refl => eq_refl
end
).
Defined.
Lemma contr_c_true i_b w : true = existT _ (existT I_Bool c_true i_b) w.
simpl in *; unfold c_true in w; fold c_true in w.
exact (
match w in (_ = w_b) return
forall w, true = existT _ w_b w
with
| eq_refl => fun w => contr_true w
end w
).
Defined.
Lemma contr_c_false i_b w : false = existT _ (existT I_Bool c_false i_b) w.
simpl in *; unfold c_false in w; fold c_false in w.
exact (
match w in (_ = w_b) return
forall w, false = existT _ w_b w
with
| eq_refl => fun w => contr_false w
end w
).
Defined.
Lemma ind_prop b : forall P : Bool -> Prop, P true -> P false -> P b.
intros P t f; destruct b as [w_b w]; simpl in *.
induction w_b using weak_ind; simpl in *.
unfold c_true in w; fold c_true in w.
rewrite (contr_c_true i_b w) in t; exact t.
rewrite (contr_c_false i_b w) in f; exact f.
Defined.
Definition case (b : Bool) : C_Bool := projT1 (projT1 b).
Lemma ind_type b : forall P : Bool -> Type, P true -> P false -> P b.
destruct b as [[c_b i_b] w]; simpl in *.
intros P t f.
(* TODO: this is really ugly *)
assert (c_b Type (P true) (P false) = P (existT _ (existT _ c_b i_b) w)).
refine (
i_b (fun i_c_b => i_c_b = c_b ->
i_c_b _ (P true) (P false) = P (existT _ (existT _ c_b i_b) w)
) _ _ eq_refl
); intros H; destruct H.
rewrite (contr_c_true i_b w); reflexivity.
rewrite (contr_c_false i_b w); reflexivity.
epose (i_b (fun c_b => c_b _ (P true) (P false)) t f); simpl in *.
rewrite H in p; exact p.
Defined.
End Bool.
(* either *)
Definition Either_Tag (A B K : Prop) : Prop := exists (b : Bool),
Bool.case b Prop (A = K) (B = K).
Definition inl_tag {A B} : Either_Tag A B A :=
ex_intro _ true eq_refl.
Definition inr_tag {A B} : Either_Tag A B B :=
ex_intro _ false eq_refl.
Definition Either A B : Prop := exists K, {tag : Either_Tag A B K | K}.
Definition inl {A B} (v : A) : Either A B :=
ex_intro _ A (exist _ inl_tag v).
Definition inr {A B} (v : B) : Either A B :=
ex_intro _ B (exist _ inr_tag v).
Definition ind_tag {A B K} (e : Either_Tag A B K) :
forall P : forall K, Either_Tag A B K -> Prop,
P A inl_tag -> P B inr_tag -> P K e.
intros P l r.
destruct e as [b w].
destruct b using Bool.ind_type.
destruct w; exact l.
destruct w; exact r.
Defined.
Definition ind {A B} (e : Either A B) :
forall P : Either A B -> Prop,
(forall v, P (inl v)) -> (forall v, P (inr v)) -> P e.
intros P l r.
destruct e as [K [tag v]].
refine (
ind_tag tag (fun K tag => forall v, P (ex_intro _ K (exist _ tag v)))
_ _ v
); clear v tag.
intros v; apply l.
intros v; apply r.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment