(** * Church Numerals *) Definition Nat : Prop := forall X : Prop, (X -> X) -> X -> X. Definition zero : Nat := fun X f x => x. Definition succ : Nat -> Nat := fun n X f x => f (n X f x). Definition N : nat -> Nat := fun n => nat_iter n succ zero. Lemma NS n : N (S n) = succ (N n). Proof. reflexivity. Qed. Compute (N 5). Fixpoint pow (x y : nat) : nat := match y with | 0 => 1 | S y' => x * pow x y' end. (** Dedekind version of addition, multiplication, and exponentiation. Does not require Coq's eta-conversion. *) Module AME. Definition add : Nat -> Nat -> Nat := fun m => m Nat succ. Definition mul : Nat -> Nat -> Nat := fun m n => m Nat (add n) (N 0). Definition exp : Nat -> Nat -> Nat := fun m n => n Nat (mul m) (N 1). Lemma add_correct m n : add (N m) (N n) = N (m + n). Proof. induction m; simpl. - reflexivity. - change (add (N (S m)) (N n)) with (succ (add (N m) (N n))). now rewrite IHm. Qed. Lemma mul_correct m n : mul (N m) (N n) = N (m * n). Proof. induction m; simpl. - reflexivity. - change (mul _ _) with (add (N n) (mul (N m) (N n))). now rewrite IHm, add_correct. Qed. Lemma exp_correct m n : exp (N m) (N n) = N (pow m n). Proof. induction n; simpl. - reflexivity. - change (exp _ _) with (mul (N m) (exp (N m) (N n))). now rewrite IHn, mul_correct. Qed. End AME. (** Church's version of addition, multiplication, and exponentiation. Exploits Coq's eta-conversion. *) Module AME_Church. Definition add : Nat -> Nat -> Nat := fun m n X f x => m X f (n X f x). Definition mul : Nat -> Nat -> Nat := fun m n X f => m X (n X f). Definition exp : Nat -> Nat -> Nat := fun m n X => n (X -> X) (m X). Compute exp (N 2) (N 3). Lemma add_correct m n : N (m + n) = add (N m) (N n). Proof. induction m; simpl. - reflexivity. - change (N (S (m+n))) with (succ (N (m+n))). now rewrite IHm. Qed. Lemma mul_correct m n : N (m * n) = mul (N m) (N n). Proof. induction m; simpl. - reflexivity. - now rewrite add_correct, IHm. Qed. Lemma exp_correct m n : N (pow m n) = exp (N m) (N n). Proof. induction n; simpl. - reflexivity. - now rewrite mul_correct, IHn. Qed. End AME_Church. (** Pairs *) Set Implicit Arguments. Definition Prod (X Y : Prop) : Prop := forall Z : Prop, (X -> Y -> Z) -> Z. Definition pair (X Y : Prop) : X -> Y -> Prod X Y := fun x y Z f => f x y. Definition fst (X Y : Prop) : Prod X Y -> X := fun p => p X (fun x y => x). Definition snd (X Y : Prop) : Prod X Y -> Y := fun p => p Y (fun x y => y). Lemma fst_correct (X Y : Prop) (x : X) (y : Y) : fst (pair x y) = x. Proof. cbv. reflexivity. Qed. (** The eta-law for pairs [pair (fst p) (snd p) = p] cannot be shown. *) (** Primitive recursion *) Section Prec. Variable X : Prop. Variable x : X. Variable f : Nat -> X -> X. Definition P := Prod Nat X. Definition a : P := pair (N 0) x. Definition step (p : P) : P := pair (succ (fst p)) (f (fst p) (snd p)). Definition prec (n : Nat) : X := snd (n P step a). Lemma precO : prec (N 0) = x. Proof. reflexivity. Qed. Lemma precS' n : (N (S n)) P step a = pair (N (S n)) (f (N n) (snd (N n P step a))). Proof. induction n. - reflexivity. - change (N (S (S n)) P step a) with (step (N (S n) P step a)). rewrite IHn. reflexivity. Qed. Lemma precS n : prec (N (S n)) = f (N n) (prec (N n)). Proof. unfold prec. now rewrite precS'. Qed. End Prec. (** Predecessor *) Definition pre : Nat -> Nat := prec (N 0) (fun n' _ => n'). Lemma pre_correct n : pre (N n) = N (pred n). Proof. destruct n. - reflexivity. - unfold pre. now rewrite precS. Qed.