Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/bool_by_j_cc.v

Last active October 24, 2025 16:55
Show Gist options
  • Save EduardoRFS/3562d2d3daeb1f605499e4e1a58c0e07 to your computer and use it in GitHub Desktop.
Save EduardoRFS/3562d2d3daeb1f605499e4e1a58c0e07 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
bool_by_j_cc.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 C_Bool : Prop := 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 T_Bool := Prop -> Prop -> Prop.
Definition t_true : T_Bool := fun t f => t.
Definition t_false : T_Bool := fun t f => f.
Definition I_Bool (t_b : T_Bool) : Prop :=
forall P, P t_true -> P t_false -> P t_b.
Definition i_true : I_Bool t_true := fun P t f => t.
Definition i_false : I_Bool t_false := fun P t f => f.
Definition W_Bool := {t_b : T_Bool | I_Bool t_b}.
Definition w_true : W_Bool := exist _ t_true i_true.
Definition w_false : W_Bool := exist _ t_false i_false.
Definition weak_ind w_b :
forall P : W_Bool -> Prop,
(forall i_b, P (exist _ t_true i_b)) ->
(forall i_b, P (exist _ t_false i_b)) -> P w_b.
intros P t f; destruct w_b as [t_b i_b]; simpl in *.
refine (i_b (fun t_b => forall i_b, _) _ _ i_b); auto.
Defined.
Definition Bool :=
{w_b : W_Bool | proj1_sig w_b (w_true = w_b) (w_false = w_b)}.
Definition true : Bool := exist _ w_true eq_refl.
Definition false : Bool := exist _ w_false eq_refl.
Definition true_next_eq {w_b : W_Bool} (w : w_true = w_b) : w_true = w_b.
induction w_b using weak_ind.
exact (
match w in (_ = w_b) return
(proj1_sig w_b (w_true = w_b) (w_false = w_b))
with
| eq_refl => eq_refl
end
).
exact w.
Defined.
Definition false_next_eq {w_b : W_Bool} (w : w_false = w_b) : w_false = w_b.
induction w_b using weak_ind.
exact w.
exact (
match w in (_ = w_b) return
(proj1_sig w_b (w_true = w_b) (w_false = w_b))
with
| eq_refl => eq_refl
end
).
Defined.
Lemma true_eq w : true = exist _ w_true w.
apply (sig_ext true (exist _ _ _) w).
unfold eq_rect; simpl.
exact (
match w in (_ = w_b) return true_next_eq w = w with
| eq_refl => eq_refl
end
).
Defined.
Lemma false_eq w : false = exist _ w_false w.
apply (sig_ext false (exist _ _ _) w).
unfold eq_rect; simpl.
exact (
match w in (_ = w_b) return false_next_eq w = w with
| eq_refl => eq_refl
end
).
Defined.
Definition case (b : Bool) : Prop -> Prop -> Prop :=
proj1_sig (proj1_sig b).
Definition ind (b : Bool)
: 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.
refine (
match w in (_ = w_b) return
forall w, P (exist _ w_b w) with
| eq_refl => _
end w
); clear w; intros w.
rewrite <- (true_eq w); exact t.
refine (
match w in (_ = w_b) return
forall w, P (exist _ w_b w) with
| eq_refl => _
end w
); clear w; intros w.
rewrite <- (false_eq w); exact f.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment