subtraction on church numerals in Coq

subtract_church.v

(* subtraction on church numerals in Coq *)
Set Printing Universes.
  
(* we always use universe polymorphism, which is later required to define subtraction *)
Polymorphic Definition church : Type := forall X:Type, (X->X) -> (X->X).

Polymorphic Definition zero : church := fun X s z => z.
Polymorphic Definition suc : church -> church := fun n X s z => s (n X s z).

(* as usual *)
Polymorphic Definition add : church -> church -> church :=
  fun m n X s z => m X s (n X s z).
Polymorphic Definition mult : church -> church -> church := 
  fun m n X s z => m X (n X s) z.
Polymorphic Definition exp : church -> church -> church := 
  fun m n X => n (X->X) (m X).

(* helper function to record 'previous' value *)
Definition church_ : Type -> Type := fun (X:Type) => (X->X) -> (X->X).
Polymorphic Definition next : forall X, church_ X * church_ X -> church_ X * church_ X :=
  fun X tup => 
    let suc_ := fun n s z => s (n s z) in
    match tup with (x,_) => (suc_ x, x) end.

Polymorphic Definition pred : church -> church :=
  fun n X => snd (n (church_ X * church_ X)%type (next X) (zero X, zero X)).

(* subtraction. we need a church numeral in a higher universe *)
Definition sub : church -> church -> church :=
  fun n m => m church pred n. 

Polymorphic Definition one := suc zero.
Polymorphic Definition two := suc (suc zero).
Polymorphic Definition three := add two one.
Polymorphic Definition four := add three one.
Polymorphic Definition five := add two three.
Polymorphic Definition six := mult three two.
Polymorphic Definition seven := add three four.

(* To print them, it needs to be projected into some actual data type (of Prop). *)
Inductive mynat : Type := Z : mynat | S : mynat -> mynat.

(* check it *)
Eval compute in one mynat S Z.
Eval compute in three mynat S Z.
Eval compute in four mynat S Z.
Eval compute in five mynat S Z.
Eval compute in six mynat S Z.
Eval compute in seven mynat S Z.
Eval compute in pred seven mynat S Z.

Eval compute in exp three two mynat S Z.
Eval compute in exp one seven mynat S Z.
Eval compute in exp seven zero mynat S Z.

(* to use sub, we must redefine our church numerals in a higher universe *)
Eval compute in sub five three mynat S Z.
Eval compute in sub seven one mynat S Z.