Church_sol.v

Definition num := forall X : Prop, (X -> X) -> X -> X.

Polymorphic Definition zero : num := fun X s z => z.
Polymorphic Definition succ : num -> num := fun n X s z => s (n X s z).

Fixpoint from_nat n : num :=
  match n with
  | 0 => zero
  | S n => succ (from_nat n)
  end.

(* Definition to_nat (n : num) : nat := n nat S 0. *)

Definition add : num -> num -> num :=
  fun n m X s z => n X s (m X s z).

(* Compute (to_nat (add (from_nat 8) (from_nat 5))). *)

Definition mul : num -> num -> num :=
  fun n m X s z => n X (m X s) z.

Definition exp : num -> num -> num :=
  fun n m X => m _ (n X).

Lemma add_from_nat n m :
  add (from_nat n) (from_nat m) = from_nat (n + m).
Proof.
  induction n; simpl.
  - reflexivity.
  - rewrite <- IHn. reflexivity.
Qed.

Lemma mul_from_nat n m :
  mul (from_nat n) (from_nat m) = from_nat (n * m).
Proof.
  induction n; simpl.
  - reflexivity.
  - rewrite <- add_from_nat. rewrite <- IHn. reflexivity.
Qed.

Lemma exp_from_nat n m :
  exp (from_nat n) (from_nat m) = from_nat (Nat.pow n m).
Proof.
  induction m; simpl.
  - reflexivity.
  - rewrite <- mul_from_nat. rewrite <- IHm. reflexivity.
Qed.

Definition pred' : num -> num * num :=
  fun n => (n (num * num)%type (fun p => (snd p, succ (snd p))) (zero, zero)).
Definition pred : num -> num :=
  fun n => fst (pred' n).

Lemma pred'_from_nat n :
  pred' (from_nat n) = (from_nat (Nat.pred n), from_nat n).
Proof.
  induction n.
  - reflexivity.
  - simpl. unfold pred' in *. simpl.
    unfold succ at 1. rewrite IHn. reflexivity.
Qed.

Lemma pred_from_nat n :
  pred (from_nat n) = from_nat (Nat.pred n).
Proof.
  unfold pred.
  rewrite pred'_from_nat.
  reflexivity.
Qed.