Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/bool_by_j_pure_pred.v

Created November 19, 2025 21:24
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save EduardoRFS/0fead2fefac87e93b8d0b738ebda0fc1 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save EduardoRFS/0fead2fefac87e93b8d0b738ebda0fc1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
bool_by_j_pure_pred.v
Inductive t_eq {A} (x : A) : A -> Type :=
| t_refl : t_eq x x.
Definition coe {A} {x y : A} (C : A -> Type) (p : t_eq x y) (H : C x) : C y :=
match p in (t_eq _ z) return C z with | t_refl _ => H end.
Definition sym {A} {x y : A} (p : t_eq x y) : t_eq y x :=
coe (fun z => t_eq z x) p (t_refl x).
Definition ap {A B x y} (f : A -> B) (H : t_eq x y) : t_eq (f x) (f y) :=
coe (fun z => t_eq (f x) (f z)) H (t_refl (f x)).
Definition coe_inj {A} {x y : A} (C : A -> Type)
(p : t_eq x y) {H1 H2} (H : t_eq (coe C p H1) (coe C p H2)) : t_eq H1 H2.
destruct p; exact H.
Defined.
Lemma sig_ext {A B} (p q : {x : A & B x})
(H1 : t_eq (projT1 p) (projT1 q))
(H2 : t_eq (coe B H1 (projT2 p)) (projT2 q)) : t_eq p q.
destruct p, q; cbn in *.
destruct H1, H2; cbn in *.
reflexivity.
Defined.
Definition C_False : Type := forall A, A.
Definition C_Unit : Type := forall A, A -> A.
Definition c_unit : C_Unit := fun A x => x.
Definition C_Either (A B : Type) : Type :=
forall (C : Type), (A -> C) -> (B -> C) -> C.
Definition c_inl {A B} (a : A) : C_Either A B :=
fun C f g => f a.
Definition c_inr {A B} (b : B) : C_Either A B :=
fun C f g => g b.
Definition I_Either A B (c_e : C_Either A B) : Type :=
forall (P : C_Either A B -> Type),
(forall a, P (c_inl a)) ->
(forall b, P (c_inr b)) ->
P c_e.
Definition i_inl A B (a : A) : I_Either A B (c_inl a) :=
fun P f g => f a.
Definition i_inr A B (b : B) : I_Either A B (c_inr b) :=
fun P f g => g b.
Definition W_Either A B : Type :=
{c_e : C_Either A B & I_Either A B c_e}.
Definition w_inl A B (a : A) : W_Either A B :=
existT _ (c_inl a) (i_inl A B a).
Definition w_inr A B (b : B) : W_Either A B :=
existT _ (c_inr b) (i_inr A B b).
Definition Dec_f A (f : A -> A) : Type :=
forall x y, W_Either (t_eq (f x) (f y)) (t_eq (f x) (f y) -> C_False).
Definition f_dec_eq {A f} (f_dec : Dec_f A f)
x y (H1 : t_eq (f x) (f y)) : t_eq (f x) (f y).
apply (projT1 (f_dec x y)); intros H2.
apply (projT1 (f_dec x x)); intros H3.
exact (coe (fun z => t_eq (f x) z) H2 (sym H3)).
apply (H3 (t_refl _)).
apply (H2 H1).
Defined.
Definition f_dec_eq_refl {A f} (f_dec : Dec_f A f)
x (H1 : t_eq (f x) (f x)) : t_eq (f_dec_eq f_dec x x H1) (t_refl _).
unfold f_dec_eq; apply (projT2 (f_dec x x)).
intros H2; unfold c_inl; destruct H2; reflexivity.
intros H2; apply (H2 (t_refl _)).
Defined.
Definition f_dec_uip {A f} (f_dec : Dec_f A f)
x y (H1 H2 : t_eq x y) : t_eq (ap f H1) (ap f H2).
destruct H2; cbn.
destruct (f_dec_eq_refl f_dec x (ap f H1)).
destruct H1.
exact (sym (f_dec_eq_refl f_dec x (t_refl _))).
Defined.
Definition fix_f {A f} (x : A) (p : t_eq (f x) x) :
t_eq (existT (fun x => t_eq (f x) x) (f x) (ap f p)) (existT _ x p).
apply (sig_ext (existT _ _ _) (existT _ _ _) p); cbn.
apply (coe_inj (fun z => t_eq (f z) x) (sym p)).
refine (match p with | t_refl _ => _ end); cbn.
refine (match p with | t_refl _ => _ end); cbn.
reflexivity.
Defined.
Definition fix_I {A f} (f_dec : Dec_f A f)
(f_I : forall x, t_eq (f (f x)) (f x)) (x : A) (p : t_eq (f x) x) :
t_eq (existT (fun x => t_eq (f x) x) (f x) (f_I x)) (existT _ x p).
destruct (fix_f (f x) (f_I x)).
destruct (fix_f x p), (fix_f (f x) (ap f p)).
destruct (f_dec_uip f_dec (f (f x)) (f x) (f_I x) (ap f p)).
reflexivity.
Defined.
(* bool *)
(* specific instances *)
Definition C_Bool : Type := forall A, 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 H_Bool : Type := forall A, A -> A -> A.
Definition h_true : H_Bool := fun A t f => t.
Definition h_false : H_Bool := fun A t f => f.
(* axioms usage starts here *)
Axiom lift_c_bool : C_Bool -> H_Bool.
Axiom lift_c_true : t_eq (lift_c_bool c_true) h_true.
Axiom lift_c_false : t_eq (lift_c_bool c_false) h_false.
Definition c_to_w (c_b : C_Bool) : W_Bool :=
lift_c_bool c_b _ w_true w_false.
Definition c_next (c_b : C_Bool) : C_Bool :=
projT1 (c_to_w c_b).
Definition c_next_ind c_b : I_Bool (c_next c_b) :=
projT2 (c_to_w c_b).
Definition c_next_I c_b : t_eq (c_next (c_next c_b)) (c_next c_b).
apply (c_next_ind c_b); clear c_b.
unfold c_next, c_to_w; rewrite lift_c_true; reflexivity.
unfold c_next, c_to_w; rewrite lift_c_false; reflexivity.
Defined.
(* axioms usage ends here *)
Definition c_true_neq_c_false : t_eq c_true c_false -> C_False :=
fun H1 => @coe C_Bool _ _ (fun c_b => c_b Type C_Unit C_False) H1 c_unit.
Definition c_next_dec : Dec_f C_Bool c_next.
intros l_c_b r_c_b.
apply (c_next_ind l_c_b); apply (c_next_ind r_c_b).
apply w_inl; reflexivity.
apply w_inr; intros H; exact (c_true_neq_c_false H).
apply w_inr; intros H; exact (c_true_neq_c_false (sym H)).
apply w_inl; reflexivity.
Defined.
Definition Bool : Type := { c_b : C_Bool & t_eq (c_next c_b) c_b }.
Definition true : Bool := existT _ (c_next c_true) (c_next_I c_true).
Definition false : Bool := existT _ (c_next c_false) (c_next_I c_false).
Definition next (b : Bool) : Bool :=
existT _ (c_next (projT1 b)) (c_next_I (projT1 b)).
Definition ind_next b : forall P, P true -> P false -> P (next b).
intros P t f; destruct b as [c_b H1]; unfold next; cbn; destruct H1.
apply (c_next_ind c_b); auto.
Defined.
Definition mod_next b : t_eq (next b) b.
destruct b as [c_b H1]; unfold next; cbn.
apply (fix_I c_next_dec c_next_I).
Defined.
Definition ind b : forall P, P true -> P false -> P b.
destruct (mod_next b); exact (ind_next b).
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment