nat_by_j.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 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.

Definition Wrap (A : Prop) (f : A -> A) := {x : A | f x = x}.

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 (
    eq_sym (f_eq x (f x)
      match H in (_ = y) return f y = f x with
      | eq_refl => ap f H
      end)
  ).
Defined.

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).
  unfold eq_rect; simpl.
  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.
  rewrite H2; clear H2.
  destruct (f_eq_refl x H1).
  reflexivity.

  refine (
    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
  ).
  unfold wrap_I.
  destruct H1.
  unfold eq_sym.
  simpl.
  reflexivity.
Defined.

Lemma wrap_mod {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)
  x H1 H2 : (exist _ x H1 : Wrap A f) = (exist _ x H2 : Wrap A f).
  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.

(* 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).
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.

(* 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 =>
    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) :
  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.
    apply w_inl; reflexivity.
    intros c_n_pred IHr; clear IHr.
    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.
    apply w_inr; intros H; apply (c_zero_neq_c_succ _ (eq_sym H)).
    intros r_c_n IHr; clear IHr.
    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_succ (proj1_sig n)) (ap c_succ (proj2_sig n)).

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_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.
  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.