Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/nat_by_j.v

Last active November 4, 2025 14:08
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save EduardoRFS/8ba5eebda8ae9d52f98801e7f6d925ee to your computer and use it in GitHub Desktop.
Download ZIP
Raw
nat_by_j.v
(* TODO: this file was not cleaned and is currently
using the builtin or, that can be replaced by
https://gist.github.com/EduardoRFS/8fb6ecbe7b34b78e772b1bc207ad3395 *)
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 ap {A B x y} (f : A -> B) (H : x = y) : f x = f y :=
match H in (_ = z) return f x = f z with
| eq_refl => eq_refl
end.
Lemma transport_ap {A B x y} (f : A -> B) P v (H : x = y) :
match ap f H in (_ = z) return P z with
| eq_refl => v
end = match H in (_ = z) return P (f z) with
| eq_refl => v
end.
destruct H; reflexivity.
Defined.
Definition Bad {A : Prop} (x y : A) := x = y ->
forall (A : Prop) (t f : A), t = f.
Definition Cmp_f {A : Prop} (f : A -> A) :=
forall (x y : A), f x = f y \/ Bad (f x) (f y).
Definition cmp_I {A : Prop} {x y} f (I : f (f x) = f y)
(f_cmp : forall (x y : A), f x = f y \/ Bad (f x) (f y))
: f (f x) = f y.
destruct (f_cmp (f x) y) as [H1 | H1].
destruct (f_cmp y y) as [H2 | H2].
exact (
match eq_sym H2 in (_ = z) return f (f x) = z with
| eq_refl => H1
end
).
exact I.
exact I.
Defined.
Definition Wrap (A : Prop) (f : A -> A) := {x : A | f x = x}.
(* TODO: maybe f_cmp could be only for the current elements *)
Definition wrap {A f} (f_cmp : Cmp_f f) (w : Wrap A f) : Wrap A f :=
exist _ (f (proj1_sig w)) (cmp_I f (ap f (proj2_sig w)) f_cmp).
Lemma wrap_elim {A : Prop} {f}
(f_cmp : forall (x y : A), f x = f y \/ Bad (f x) (f y))
(w : Wrap A f) : wrap f_cmp w = w.
destruct w as [x H1]; unfold wrap; simpl.
apply (sig_ext (exist _ _ _) (exist _ _ _) H1).
refine (match H1 with | eq_refl => _ end H1); clear H1; intros H1.
unfold eq_rect; simpl.
assert (
match f_cmp (f x) (f x) with
| or_introl H3 =>
match H3 in (_ = z) return (z = f x) with
| eq_refl =>
match f_cmp (f x) (f x) with
| or_introl H4 =>
match eq_sym H4 in (_ = z) return (z = f x) with
| eq_refl => H1
end
| or_intror H4 => H4 eq_refl A (f (f x)) (f x)
end
end
| or_intror _ =>
match H1 in (_ = a) return (f a = a) with
| eq_refl => cmp_I f (ap f H1) f_cmp
end
end = H1
) as H2.
destruct (f_cmp (f x) (f x)) as [H2 | H2].
rewrite H2; reflexivity.
apply H2; reflexivity.
refine (
match H2 in (_ = H3) return
match H1 in (_ = a) return (f a = a) with
| eq_refl => cmp_I f (ap f H1) f_cmp
end = H3 with
| eq_refl => _
end
); clear H2.
refine (
match cmp_I f H1 f_cmp in (_ = y) return
forall (H2 : f (f x) = y),
match H2 in (_ = a) return (f a = a) with
| eq_refl => cmp_I f (ap f H1) f_cmp
end =
match f_cmp (f x) y with
| or_introl H3 =>
match H3 in (_ = z) return (z = y) with
| eq_refl =>
match f_cmp (f x) (f x) with
| or_introl H4 =>
match eq_sym H4 in (_ = z) return (z = y) with
| eq_refl => H2
end
| or_intror H4 => H4 eq_refl _ _ _
end
end
| or_intror H3 =>
match H2 in (_ = a) return (f a = a) with
| eq_refl => cmp_I f (ap f H1) f_cmp
end
end
with
| eq_refl => _
end H1
).
intros H2.
destruct H2.
destruct H1.
simpl.
unfold cmp_I.
destruct (f_cmp (f (f x)) (f (f x))).
assert (
match eq_sym e in (_ = z) return (f (f (f x)) = z) with
| eq_refl => e
end = eq_refl
).
destruct e; reflexivity.
rewrite H; clear H.
assert (
match e in (_ = z) return (z = f (f (f x))) with
| eq_refl =>
match eq_sym e in (_ = z) return (z = f (f (f x))) with
| eq_refl => eq_refl
end
end = eq_refl
).
destruct e; reflexivity.
rewrite H; reflexivity.
reflexivity.
Defined.
Lemma wrap_mod {A : Prop} {f}
(f_cmp : forall (x y : A), f x = f y \/ Bad (f x) (f y))
x H1 H2 : (exist _ x H1 : Wrap A f) = (exist _ x H2 : Wrap A f).
destruct (wrap_elim f_cmp (exist _ x H1)).
destruct (wrap_elim f_cmp (exist _ x H2)).
unfold wrap; simpl in *.
unfold cmp_I.
destruct (f_cmp (f x) x).
destruct (f_cmp x x); auto.
apply b; rewrite H1; exact H1.
Defined.
Lemma wrap_mod2 {A : Prop} {f}
(f_cmp : forall (x y : A), f x = f y \/ Bad (f x) (f y))
x y (H1 : x = y) H2 H3 :
(exist _ x H2 : Wrap A f) = (exist _ y H3 : Wrap A f).
destruct H1.
apply (wrap_mod f_cmp).
Defined.
(* bool *)
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.
(* nat *)
Definition C_Nat : Prop := forall A, A -> (A -> A) -> A.
Definition c_zero : C_Nat := fun A z s => z.
Definition c_succ (c_n : C_Nat) : C_Nat :=
fun A z s => s (c_n A z s).
Lemma c_zero_neq_c_succ c_n : Bad c_zero (c_succ c_n).
intros H A t f.
exact (
match H in (_ = c_n) return t = c_n _ t (fun _ => f) with
| eq_refl => eq_refl
end
).
Defined.
Definition I_Nat (c_n : C_Nat) : Prop :=
forall P, P c_zero ->
(forall c_n, P c_n -> P (c_succ c_n)) -> P c_n.
Definition i_zero : I_Nat c_zero := fun P z s => z.
Definition i_succ (c_n : C_Nat) (i_n : I_Nat c_n) : I_Nat (c_succ c_n) :=
fun P z s => s c_n (i_n P z s).
Definition W_Nat : Prop := {c_n : C_Nat | I_Nat c_n}.
Definition w_zero : W_Nat := exist _ c_zero i_zero.
Definition w_succ (w_n : W_Nat) : W_Nat :=
exist _ (c_succ (proj1_sig w_n)) (i_succ _ (proj2_sig w_n)).
Definition c_next (c_n : C_Nat) : C_Nat :=
proj1_sig (c_n W_Nat w_zero w_succ).
Definition c_next_ind (c_n : C_Nat) :
forall (P : C_Nat -> Prop),
P c_zero ->
(forall c_n, P c_n -> P (c_succ c_n)) ->
P (c_next c_n).
intros P z s; unfold c_next.
exact (proj2_sig (c_n W_Nat w_zero w_succ) P z s).
Defined.
Definition c_next_I c_n : c_next (c_next c_n) = c_next c_n.
apply (c_next_ind c_n); clear c_n.
reflexivity.
intros c_n IH; exact (ap c_succ IH).
Defined.
Definition c_pred_and_is_zero (c_n : C_Nat) :=
c_n (C_Nat * C_Bool : Prop) (c_zero, c_true) (fun p =>
let (c_n_pred, is_zero) := p in
is_zero _ (c_n_pred, c_false) (c_succ c_n_pred, c_false)).
Definition c_pred (c_n : C_Nat) := fst (c_pred_and_is_zero c_n).
Lemma c_pred_and_is_zero_c_succ_next c_n
: c_pred_and_is_zero (c_succ (c_next c_n)) = (c_next c_n, c_false).
apply (c_next_ind c_n); clear c_n.
reflexivity.
intros c_n_pred IH.
unfold c_pred in *.
unfold c_pred_and_is_zero, c_succ at 1; simpl.
fold (c_pred_and_is_zero (c_succ c_n_pred)).
rewrite IH; reflexivity.
Defined.
Lemma c_pred_c_succ_next c_n
: c_pred (c_succ (c_next c_n)) = c_next c_n.
unfold c_pred; rewrite c_pred_and_is_zero_c_succ_next; reflexivity.
Defined.
Lemma c_succ_next_inj {l_c_n r_c_n} (w : c_succ l_c_n = c_succ r_c_n) :
c_next l_c_n = c_next r_c_n.
destruct (c_pred_c_succ_next r_c_n).
refine (
match ap c_next w in (_ = c_n) return c_next l_c_n = c_pred c_n with
| eq_refl => _
end
).
unfold c_next; simpl; fold (c_next l_c_n).
rewrite (c_pred_c_succ_next l_c_n).
reflexivity.
Defined.
Definition c_next_dec (l_c_n r_c_n : C_Nat) :
c_next l_c_n = c_next r_c_n \/
Bad (c_next l_c_n) (c_next r_c_n).
destruct (c_next_I l_c_n), (c_next_I r_c_n).
revert r_c_n; apply (c_next_ind l_c_n); clear l_c_n.
-
intros r_c_n; apply (c_next_ind r_c_n); clear r_c_n.
left; reflexivity.
intros c_n_pred IHr; clear IHr.
right; intros H; apply (c_zero_neq_c_succ _ H).
-
intros l_c_n IHl r_c_n; apply (c_next_ind r_c_n); clear r_c_n.
right; intros H; apply (c_zero_neq_c_succ _ (eq_sym H)).
intros r_c_n IHr; clear IHr.
destruct (IHl r_c_n) as [H1 | H1]; rewrite (c_next_I r_c_n) in H1.
left; exact (ap c_succ H1).
right; intros H2; apply H1.
destruct (c_next_I l_c_n), (c_next_I r_c_n).
exact (c_succ_next_inj H2).
Defined.
Definition Nat : Prop := Wrap C_Nat c_next.
Definition zero : Nat := exist _ c_zero eq_refl.
Definition succ (n : Nat) : Nat :=
exist _ (c_next (c_succ (proj1_sig n)))
(ap c_succ (cmp_I c_next (ap c_next (proj2_sig n)) c_next_dec)).
Theorem ind (n : Nat) :
forall P : Nat -> Prop, P zero ->
(forall n, P n -> P (succ n)) -> P n.
intros P z s.
destruct n as [c_n H1].
refine (match H1 with | eq_refl => _ end H1); clear H1; intros H1.
revert H1; destruct (c_next_I c_n); intros H1.
rewrite (wrap_mod c_next_dec _ H1 (c_next_I _)); clear H1.
apply (c_next_ind c_n); clear c_n.
exact z.
intros c_n IH.
unfold succ in s.
assert (
succ (exist _ (c_next c_n) (c_next_I _)) =
exist _ (c_next (c_succ c_n)) (c_next_I _)
); unfold succ; simpl.
apply (wrap_mod2 c_next_dec
(c_next (c_succ (c_next c_n)))
(c_succ (c_next c_n)) (c_next_I (c_succ c_n))).
destruct H.
exact (s _ IH).
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment