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

Revisions

  1. EduardoRFS revised this gist Oct 28, 2025. 1 changed file with 119 additions and 156 deletions.
    275 changes: 119 additions & 156 deletions nat_by_j.v
    View file
    Original file line number Diff line number Diff line change
    @@ -1,6 +1,3 @@
    (* 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.
    @@ -24,168 +21,105 @@ 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 Wrap (A : Prop) (f : A -> A) := {x : A | f x = x}.

    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].
    Definition wrap_I {A : Prop} {f x}
    (f_eq : forall (x y : A) (H : f x = y), f x = f y)
    (H : f x = x) : f (f x) = f x.
    exact (
    match eq_sym H2 in (_ = z) return f (f x) = z with
    | eq_refl => H1
    end
    eq_sym (f_eq x (f x)
    match H in (_ = y) return f y = f x with
    | eq_refl => ap f H
    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.
    Definition wrap {A : Prop} {f} (f_eq : forall (x y : A) (H : f x = y), f x = f y)
    (w : Wrap A f) : Wrap A f :=
    exist _ (f (proj1_sig w)) (wrap_I f_eq (proj2_sig w)).

    (* f_eq is half of a decidable quality,
    this avoids the requirement for either *)
    Lemma wrap_elim {A : Prop} {f} (f_eq : forall (x y : A) (H : f x = y), f x = f y)
    (f_eq_refl : forall (x : A) (H : f x = x), eq_refl = f_eq x x H)
    (w : Wrap A f) : wrap f_eq 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
    enough (
    match H1 in (_ = a) return (f a = a) with
    | eq_refl => wrap_I f_eq H1
    end =
    match f_eq x x H1 in (_ = a) return (a = x) with
    | eq_refl => H1
    end
    ) 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.
    rewrite H2; clear H2.
    destruct (f_eq_refl x H1).
    reflexivity.

    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

    match H1 as H2 in (_ = y) return
    match H2 in (_ = a) return (f a = a) with
    | eq_refl => wrap_I f_eq H1
    end =
    match f_eq x y H2 in (_ = a) return (a = y) with
    | eq_refl => H2
    end
    with
    | eq_refl => _
    end H1
    end
    ).
    intros H2.
    destruct H2.
    unfold wrap_I.
    destruct H1.
    unfold eq_sym.
    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))
    (f_eq : forall (x y : A) (H : f x = y), f x = f y)
    (f_eq_refl : forall (x : A) (H : f x = x), eq_refl = f_eq x x H)
    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.
    destruct (wrap_elim f_eq f_eq_refl (exist _ x H1)).
    destruct (wrap_elim f_eq f_eq_refl (exist _ x H2)).
    unfold wrap, wrap_I; simpl in *.
    rewrite H1, H2; reflexivity.
    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 *)
    (* helpers *)
    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 C_Either (A B : Prop) : Prop :=
    forall C, (A -> C) -> (B -> C) -> C.
    Definition c_inl {A B} (a : A) : C_Either A B := fun C l r => l a.
    Definition c_inr {A B} (b : B) : C_Either A B := fun C f r => r b.

    Definition I_Either A B (e : C_Either A B) : Prop :=
    forall P, (forall a, P (c_inl a)) -> (forall b, P (c_inr b)) -> P e.
    Definition i_inl {A B} (a : A) : I_Either A B (c_inl a) :=
    fun P l r => l a.
    Definition i_inr {A B} (b : B) : I_Either A B (c_inr b) :=
    fun P l r => r b.

    Definition W_Either A B : Prop :=
    {e : C_Either A B | I_Either A B e}.
    Definition w_inl {A B} (a : A) : W_Either A B :=
    exist _ (c_inl a) (i_inl a).
    Definition w_inr {A B} (b : B) : W_Either A B :=
    exist _ (c_inr b) (i_inr b).

    Definition Neq {A : Prop} (x y : A) := x = y ->
    forall (A : Prop) (t f : A), t = 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.
    @@ -214,6 +148,15 @@ Definition c_next_I c_n : c_next (c_next c_n) = c_next c_n.
    intros c_n IH; exact (ap c_succ IH).
    Defined.

    (* decidable equality *)
    Lemma c_zero_neq_c_succ c_n : Neq 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 c_pred_and_is_zero (c_n : C_Nat) :=
    c_n (C_Nat * C_Bool : Prop) (c_zero, c_true) (fun p =>
    @@ -248,32 +191,59 @@ Lemma c_succ_next_inj {l_c_n r_c_n} (w : c_succ l_c_n = c_succ r_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).
    W_Either (c_next l_c_n = c_next r_c_n)
    (Neq (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.
    apply w_inl; reflexivity.
    intros c_n_pred IHr; clear IHr.
    right; intros H; apply (c_zero_neq_c_succ _ H).
    apply w_inr; 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)).
    apply w_inr; 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.
    apply (IHl r_c_n); intros H1; rewrite (c_next_I r_c_n) in H1.
    apply w_inl; exact (ap c_succ H1).
    apply w_inr; intros H2; apply H1.
    destruct (c_next_I l_c_n), (c_next_I r_c_n).
    exact (c_succ_next_inj H2).
    Defined.

    (* back to the ritual *)
    Definition c_next_eq (l_c_n r_c_n : C_Nat) (H1 : c_next l_c_n = r_c_n)
    : c_next l_c_n = c_next r_c_n.
    apply (proj1_sig (c_next_dec l_c_n r_c_n)); intros H2.
    apply (proj1_sig (c_next_dec r_c_n r_c_n)); intros H3.
    refine (
    match eq_sym H3 in (_ = c_n) return c_next l_c_n = c_n with
    | eq_refl => _
    end
    ).
    refine (
    match H2 in (_ = c_n) return c_next l_c_n = c_n with
    | eq_refl => eq_refl
    end
    ).
    (* refute *)
    exact H2.
    destruct H1; exact (eq_sym (c_next_I l_c_n)).
    Defined.

    Definition c_next_eq_refl c_n (H : c_next c_n = c_n)
    : eq_refl = c_next_eq c_n c_n H.
    unfold c_next_eq; apply (proj2_sig (c_next_dec c_n c_n)); intros H1.
    unfold c_inl; destruct H1; reflexivity.
    apply H1; reflexivity.
    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)).
    exist _ (c_succ (proj1_sig n)) (ap c_succ (proj2_sig n)).

    Theorem ind (n : Nat) :
    forall P : Nat -> Prop, P zero ->
    @@ -282,18 +252,11 @@ Theorem ind (n : Nat) :
    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.
    rewrite (wrap_mod c_next_eq c_next_eq_refl _ H1 (c_next_I _)).
    clear H1; apply (c_next_ind c_n); clear c_n; auto.
    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).
    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_mod c_next_eq c_next_eq_refl _ _).
    destruct H; exact (s _ IH).
    Defined.
  2. EduardoRFS revised this gist Oct 28, 2025. 1 changed file with 299 additions and 1 deletion.
    300 changes: 299 additions & 1 deletion nat_by_j.v
    View file
    Original file line number Diff line number Diff line change
    @@ -1 +1,299 @@
    (*
    (* 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.
  3. EduardoRFS created this gist Oct 28, 2025.
    1 change: 1 addition & 0 deletions nat_by_j.v
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1 @@
    (*