Bespoke nats and algorithms

Stream: general

[Kevin Buzzard]

In the tutorial world of NNG4 I force people to prove 2+2=4 by unfolding numerals and rewriting add_zero and add_succ. I'm now adding an "algorithm world", an optional world where people who care more about the CS side of things can prove things like 20 + 20 = 40.

I was surprised by several things in the experiment below.
1) You can prove 100+200=300 in MyNat with rfl quickly. Is this Lean just doing tens of thousands of manipulations quickly or is something cleverer going on?
2) But you can't prove 1000+2000=3000 with rfl on MyNat, although you can with Nat. So there is special support for Nat in rfl?
3) simp uses decide and norm_num uses simp? Is that right?
4) But decide on MyNat is worse than rfl?? (it can't do 100+200=300) Can I write a better decide?
5) I am assuming that norm_num is doing something clever. How much hard work is it to make norm_num work on MyNat? Does this involve making binary nats? Can someone prove 1000+2000=3000 for MyNat? (without the hack of bijecting it with Nat, doing it there, and then moving back?) Can I teach this in NNG4?

import Mathlib.Tactic

/-! Define bespoke naturals -/

inductive MyNat : Type
| zero : MyNat
| succ : MyNat → MyNat

namespace MyNat

/-! Get numerals working -/

def myNatFromNat (x : Nat) : MyNat :=
  match x with
  | Nat.zero   => MyNat.zero
  | Nat.succ b => MyNat.succ (myNatFromNat b)

instance ofNat {n : Nat} : OfNat MyNat n where
  ofNat := myNatFromNat n

/-! Get addition working -/

def add : MyNat → MyNat → MyNat
  | a, MyNat.zero  => a
  | a, MyNat.succ b => MyNat.succ (MyNat.add a b)

instance : Add MyNat where
  add := MyNat.add

/-! `rfl` experiments -/

example : (10 : MyNat) + 20 = 30 := rfl -- OK

example : (100 : MyNat) + 200 = 300 := rfl -- how the heck does this work so quickly???

-- example : (1000 : MyNat) + 2000 = 3000 := rfl -- max recursion depth has been reached

example : (1000 : ℕ) + 2000 = 3000 := rfl -- ℕ not MyNat

/-! `simp` experiments -/

-- example : (10 : MyNat) + 20 = 30 := by simp -- simp made no progress

/-! Get decidability working -/

instance instDecidableEq : DecidableEq MyNat
| 0, 0 => isTrue <| rfl
| succ m, 0 => isFalse <| by rintro ⟨⟩
| 0, succ n => isFalse <| by rintro ⟨⟩
| succ m, succ n => match instDecidableEq m n with
  | isTrue (h : m = n) => isTrue <| by rw [h]
  | isFalse (h : m ≠ n) => isFalse <| by rintro ⟨h⟩; exact h rfl

/-! `decide` experiments -/

example : (10 : MyNat) + 20 = 30 := by decide -- OK

-- example : (100 : MyNat) + 200 = 300 := by decide -- max recursion depth

/-! `simp` again -/

example : (10 : MyNat) + 20 = 30 := by simp -- now works?!

-- example : (100 : MyNat) + 200 = 300 := by simp -- simp made no progress

/-! What about `norm_num`? -/

example : (10 : MyNat) + 20 = 30 := by norm_num -- presumably it tried `simp`?

-- example : (100 : MyNat) + 200 = 300 := by norm_num  -- unsolved goals `100 + 200 = 300`

[Eric Rodriguez]

for 2), as far as I know, Nat operations are reduced with GMP in the kernel, and therefore are much faster.

[Arthur Adjedj]

for 4), that's to be expected, rfl will check for decidable equality between the two terms, looking at their shape after reduction. decide on the other hand, is a function in your language, and will pattern-match on the two terms, and reduce iteratively, creating new terms and doing heavier computations. Note also that native_decide handles bigger numbers with no issue, though it still causes a stack-overflow on numbers too big:

example : (5000 : MyNat) + 2000 = 7000 := by native_decide -- works

[Kevin Buzzard]

Oh thanks Arthur! So both algorithms reduce but then one of them starts cancelling and the other one just goes "yes they are the same".

[Arthur Adjedj]

rfl reduces the two numbers and checks them syntactically. decide has to reduce the comparison function you gave as a DecidableEq instance, applied to your two arguments, doing heavier computations along the way, before checking whether the value is isTrue of isFalse.

[Jannis Limperg]

With a more efficient tail-recursive equality check, we can push decide a bit farther. But it still can't do 7000; apparently the interpreter has some internal recursion limit even for tail-recursive functions.

inductive MyNat : Type
| zero : MyNat
| succ : MyNat → MyNat

namespace MyNat

def myNatFromNat (x : Nat) : MyNat :=
  match x with
  | Nat.zero   => MyNat.zero
  | Nat.succ b => MyNat.succ (myNatFromNat b)

instance ofNat {n : Nat} : OfNat MyNat n where
  ofNat := myNatFromNat n

def add : MyNat → MyNat → MyNat
  | a, MyNat.zero  => a
  | a, MyNat.succ b => MyNat.succ (MyNat.add a b)

instance : Add MyNat where
  add := MyNat.add

def beq : MyNat → MyNat → Bool
  | 0, 0 => true
  | 0, succ _ => false
  | succ _, 0 => false
  | succ m, succ n => beq m n

theorem beq_eq : ∀ {n m}, beq n m → n = m
  | 0, 0, _ => rfl
  | succ _, succ _, h => congrArg _ (beq_eq h)

theorem beq_refl : ∀ n, beq n n
  | 0 => rfl
  | succ n => beq_refl n

theorem eq_beq (h : m = n) : beq m n := by
  rw [h]; exact beq_refl _

instance instDecidableEq : DecidableEq MyNat := λ m n =>
  if h : beq m n then
    isTrue $ beq_eq h
  else
    isFalse λ contra => h (eq_beq contra)

example : (10 : MyNat) + 20 = 30 := by decide -- OK

example : (100 : MyNat) + 200 = 300 := by decide -- OK

example : (5000 : MyNat) + 2000 = 7000 := by decide -- max recursion depth

[Reid Barton]

For 1), isn't it only something like 600 operations?

[Reid Barton]

Computers are fast, e.g., this below runs in <1 second in the interpreter ghci, which is doing something vaguely analogous to kernel reduction:

myReplicate :: Integer -> a -> [a]
myReplicate 0 x = []
myReplicate n x = x : myReplicate (n-1) x

myEq :: Eq a => [a] -> [a] -> Bool
myEq [] [] = True
myEq (x:xs) (y:ys) = if x == y then myEq xs ys else False
myEq _ _ = False

myConcat :: [a] -> [a] -> [a]
myConcat [] ys = ys
myConcat (x:xs) ys = x : myConcat xs ys

main = print $
  myEq
    (myConcat (myReplicate 100000 ()) (myReplicate 200000 ()))
    (myReplicate 300000 ())

[Kevin Buzzard]

So then why does 1000+2000 fail?

[Mario Carneiro]

@Reid Barton I think GHC will have bounded stack size for this implementation, but it is very unlikely that the kernel will have this property. I can check using lean4lean if you are interested, but my guess is that it's not strictly lazy evaluating, and a term of size 300000*<term size of some relatively large intermediate> is actually produced at some point during the computation.

Improving kernel reduction has been something I've been looking into with Leo. There are a lot of low hanging fruits. In fact, if you (or anyone else) has examples of proofs that require a lot of kernel reduction, it would be helpful to send them to me so that I can demonstrate progress on them. I don't think the lean 4 test suite has much in this area.