Church numeral subtraction

Stream: general

[Bob Rubbens]

Hi all, I'm trying to define subtraction with church numerals in lean 4. I've come up with the following:

import Mathlib.Data.Nat.Notation

def ChurchNat.{u} := (α : Type u) → (α → α) → α → α

def succ : ChurchNat → ChurchNat :=
  fun n => fun α =>
  fun f a => f (n α f a)

def succ_hist : ChurchNat × ChurchNat → ChurchNat × ChurchNat
| (m, _m_pred) => (succ m, m)

def pred (c : ChurchNat) : ChurchNat :=
  (c (ChurchNat × ChurchNat) succ_hist (/- error at this c -/ c, c)).snd

I get an error on the marked c:

Application type mismatch: The argument
  c
has type
  ChurchNat.{?u.200 + 1}
of sort `Type (?u.200 + 2)` but is expected to have type
  ChurchNat.{?u.200}
of sort `Type (?u.200 + 1)` in the application
  Prod.mk c

Intuitively I understand why this is a problem: I'm applying c to itself here, and possibly, c is sercetly a y-combinator, meaning the resulting term would not terminate if executed, so the type system is preventing me from doing this. My questions are:

• Can I change my pred definition to make this typecheck? I tried adding a universe explicitly, but that didn't help, and I'm not experienced enough to know what more I can do.
• Should I maybe change my ChurchNat definition to make this typecheck?
• Or should I use the alternate definition for subtraction from wikipedia? I've heard that that one does typecheck, but I find it a lot harder to understand than this one, so I'm not so confident since I can't even get this one to typecheck. I prefer using one that I do understand, but if it cannot be made to work then I can obviously try something else.
• Or is this definition simply not type-checkable because of some other property of church numerals? Maybe someone else has written about this so I can learn?

Any helpful pointers are appreciated!

[Kenny Lau]

@Bob Rubbens you're getting "universe issue"'d. add universes to see the problem explicitly:

import Mathlib.Data.Nat.Notation

universe u

def ChurchNat : Type (u+1) := (α : Type u) → (α → α) → α → α

def succ : ChurchNat.{u} → ChurchNat.{u} :=
  fun n => fun α =>
  fun f a => f (n α f a)

def succ_hist : ChurchNat.{u} × ChurchNat.{u} → ChurchNat.{u} × ChurchNat.{u}
| (m, _m_pred) => (succ m, m)

def pred (c : ChurchNat.{u+1}) : ChurchNat.{u+1} :=
  (c (ChurchNat.{u} × ChurchNat.{u}) succ_hist.{u} (/- error at this c -/ c, c)).snd

[Kenny Lau]

you're trying to apply c to c and there's no universe where you can do that

[Bob Rubbens]

Ok, so the only option is to try the formulation of pred as described on wikipedia. Too bad! I liked the pair-based formulation.

[Alexander Bentkamp]

Maybe you meant to write:

def pred (c : ChurchNat) : ChurchNat :=
  (c (ChurchNat × ChurchNat) succ_hist (fun _ _ x => x, fun _ _ x => x)).snd

?

[Bob Rubbens]

Wow, I see what you mean. I have no clue how that typo snuck in there, but that's definitely on me. Already in notes going back some time when I started playing with this I make the mistake of not starting with zero... Thanks!