hyperoperation rw not rewriting properly

Stream: maths

[Mark Andrew Gerads]

Can anyone tell me why the commented rw is not rewriting, and what work-around there might be?

import algebra.group_with_zero.defs

def hyperoperation : ℕ → ℕ → ℕ → ℕ
| 0 _ b := 1 + b
| 1 a 0 := a
| 2 _ 0 := 0
| _ _ 0 := 1
| (n + 1) a (b + 1) := hyperoperation n a (hyperoperation (n + 1) a b)

lemma hyperoperation_1_addition (a b : ℕ) : hyperoperation 1 a b = a + b :=
begin
  induction b with bn bih,
  rw [nat_add_zero a, hyperoperation],
  {
    rw hyperoperation,
    have h1 : 0 + 1 = 1,
    exact rfl,
    rw [h1,bih],
    -- rw hyperoperation, --should work; does not work
    sorry,
  },
end

[Alex J. Best]

I guess the issue is somehow caused by having all these overlapping patterns, maybe lean gives up generating all the equation lemmas or something:
If I change your definition like this I think it means the same thing and lean is now happy to rewrite, but of course you should make sure the function still does what you intend

import algebra.group_with_zero.defs

def hyperoperation : ℕ → ℕ → ℕ → ℕ
| 0 _ b := 1 + b
| 1 a 0 := a
| 2 _ 0 := 0
| (a + 3) _ 0 := 1
| (n + 1) a (b + 1) := hyperoperation n a (hyperoperation (n + 1) a b)

lemma hyperoperation_1_addition (a b : ℕ) : hyperoperation 1 a b = a + b :=
begin
  induction b with bn bih,
  rw [nat_add_zero a, hyperoperation],
  {
    rw hyperoperation,
    have h1 : 0 + 1 = 1,
    exact rfl,
    rw [h1,bih],
    rw [hyperoperation],
  },
end

[Eric Wieser]

You can have a look at the rewrite rules it generated with #print prefix hyperoperation

[Mark Andrew Gerads]

I found another case where it does not rewrite correctly.

import algebra.group_with_zero.defs
import tactic

def hyperoperation : ℕ → ℕ → ℕ → ℕ
| 0 _ b := b + 1
| 1 a 0 := a
| 2 _ 0 := 0
| (n + 3) _ 0 := 1
| (n + 1) a (b + 1) := hyperoperation n a (hyperoperation (n + 1) a b)

lemma hyperoperation_1_addition (a b : ℕ) : hyperoperation 1 a b = a + b :=
begin
  induction b with bn bih,
  rw [nat_add_zero a, hyperoperation],
  {
    rw hyperoperation,
    rw (show 0 + 1 = 1, by refl),
    rw bih,
    rw hyperoperation,
    rw (show bn.succ = bn + 1, by refl),
    exact nat.add_assoc a bn 1,
  },
end

lemma hyperoperation_2_multiplication (a b : ℕ) : hyperoperation 2 a b = a * b :=
begin
  induction b with bn bih,
  {
    rw hyperoperation,
    exact (nat.mul_zero a).symm,
  },
  {
    rw [hyperoperation,hyperoperation_1_addition],
    rw (show 1 + 1 = 2, by refl),
    rw bih,
    ring,
  },
end

lemma hyperoperation_succn_2_2_eq_4 (n : ℕ) : hyperoperation (n + 1) 2 2 = 4 :=
begin
  induction n with nn nih,
  {
    rw (show 0 + 1 = 1, by refl),
    rw hyperoperation_1_addition,
  },
  {
    rw (show nn.succ + 1 = nn + 2, by refl),
    -- rw hyperoperation, --should work, fails to work
    sorry,
  },
end

[Scott Morrison]

I would recommend adding an intermediate layer of lemmas, that explicitly state the equation lemmas you are expecting/hoping the equation compiler is going to produce for you, and rewrite via those rather than by hyperoperation directly. That will hopefully be easier to debug and more stable to changes to the definition / moving to Lean 4.

[Mark Andrew Gerads]

I added all the intermediate lemmas, yet 1 of them (the one I need) stubbornly resists my attempt to unsorry it.

import algebra.group_with_zero.defs
import tactic

def hyperoperation : ℕ → ℕ → ℕ → ℕ
| 0 _ b := b + 1
| 1 a 0 := a
| 2 _ 0 := 0
| (n + 3) _ 0 := 1
| (n + 1) a (b + 1) := hyperoperation n a (hyperoperation (n + 1) a b)

-- Basic hyperoperation lemmas

lemma hyperoperation_0ab_b.succ (a b : ℕ) : hyperoperation 0 a b = b + 1 :=
begin
  rw hyperoperation,
end

lemma hyperoperation_1a0_a (a : ℕ) : hyperoperation 1 a 0 = a :=
begin
  rw hyperoperation,
end

lemma hyperoperation_2a0_0 (a : ℕ) : hyperoperation 2 a 0 = 0 :=
begin
  rw hyperoperation,
end

lemma hyperoperation_n3a0_1 (n a : ℕ) : hyperoperation (n + 3) a 0 = 1 :=
begin
  rw hyperoperation,
end

lemma hyperoperation_n1ab1_recurse (n a b : ℕ) :
  hyperoperation (n + 1) a (b + 1) = hyperoperation n a (hyperoperation (n + 1) a b) :=
begin
  -- rw hyperoperation, -- does not work; should work
  sorry,
end

[Junyan Xu]

You simply need to do some cases; since (n+1) overlaps with other cases where n = 1 or 2, Lean breaks equations into multiple cases, which you can see using #print prefix hyperoperation.

lemma hyperoperation_n1ab1_recurse (n a b : ℕ) :
  hyperoperation (n + 1) a (b + 1) = hyperoperation n a (hyperoperation (n + 1) a b) :=
begin
  cases n,
  rw hyperoperation,
  cases n;
  rw hyperoperation,
end

[Junyan Xu]

The relevant ones used in the above proof are

hyperoperation.equations._eqn_3 : ∀ (a b : ℕ), hyperoperation (0 + 1) a (b + 1) = hyperoperation 0 a (hyperoperation (0 + 1) a b)
hyperoperation.equations._eqn_5 : ∀ (a b : ℕ), hyperoperation (1 + 1) a (b + 1) = hyperoperation 1 a (hyperoperation (1 + 1) a b)
hyperoperation.equations._eqn_7 : ∀ (n a b : ℕ),
  hyperoperation (n.succ.succ + 1) a (b + 1) = hyperoperation n.succ.succ a (hyperoperation (n.succ.succ + 1) a b)

[Mark Andrew Gerads]

Okay, thank you. I think I have all the interesting hyperoperation lemmas now.
Any help or advice on getting it added to mathlib would be appreciated. I do not know what would be the best place to add the file (maybe data.nat.hyperoperation ?), for example, and I am unsure how to make the branch for the pull request. Also, I do not know if my lemma names are good enough.
Here is the completed hyperoperation file:

import tactic

def hyperoperation : ℕ → ℕ → ℕ → ℕ
| 0 _ b := b + 1
| 1 a 0 := a
| 2 _ 0 := 0
| (n + 3) _ 0 := 1
| (n + 1) a (b + 1) := hyperoperation n a (hyperoperation (n + 1) a b)

-- Basic hyperoperation lemmas

lemma hyperoperation_0ab_b.succ (a b : ℕ) : hyperoperation 0 a b = b + 1 :=
begin
  rw hyperoperation,
end

lemma hyperoperation_1a0_a (a : ℕ) : hyperoperation 1 a 0 = a :=
begin
  rw hyperoperation,
end

lemma hyperoperation_2a0_0 (a : ℕ) : hyperoperation 2 a 0 = 0 :=
begin
  rw hyperoperation,
end

lemma hyperoperation_n3a0_1 (n a : ℕ) : hyperoperation (n + 3) a 0 = 1 :=
begin
  rw hyperoperation,
end

lemma hyperoperation_n1ab1_recurse (n a b : ℕ) :
  hyperoperation (n + 1) a (b + 1) = hyperoperation n a (hyperoperation (n + 1) a b) :=
begin
  cases n,
  rw hyperoperation,
  cases n;
  rw hyperoperation,
end

-- Interesting hyperoperation lemmas

lemma hyperoperation_1_addition (a b : ℕ) : hyperoperation 1 a b = a + b :=
begin
  induction b with bn bih,
  {
    rw [nat_add_zero a, hyperoperation_1a0_a],
  },
  {
    rw [hyperoperation_n1ab1_recurse,bih,hyperoperation_0ab_b.succ],
    exact nat.add_assoc a bn 1,
  },
end

lemma hyperoperation_2_multiplication (a b : ℕ) : hyperoperation 2 a b = a * b :=
begin
  induction b with bn bih,
  {
    rw hyperoperation_2a0_0,
    exact (nat.mul_zero a).symm,
  },
  {
    rw [hyperoperation_n1ab1_recurse,hyperoperation_1_addition,bih],
    ring,
  },
end

lemma hyperoperation_3_exponentiation (a b : ℕ) : hyperoperation 3 a b = a ^ b :=
begin
  induction b with bn bih,
  {
    rw hyperoperation_n3a0_1,
    exact (pow_zero a).symm,
  },
  {
    rw [hyperoperation_n1ab1_recurse,hyperoperation_2_multiplication,bih],
    exact (pow_succ a bn).symm,
  },
end

lemma hyperoperation_n2a1_a (n a : ℕ) : hyperoperation (n + 2) a 1 = a :=
begin
  induction n with nn nih,
  {
    rw hyperoperation_2_multiplication,
    ring,
  },
  {
    rw [hyperoperation_n1ab1_recurse,hyperoperation_n3a0_1,nih],
  },
end

lemma hyperoperation_succn_2_2_eq_4 (n : ℕ) : hyperoperation (n + 1) 2 2 = 4 :=
begin
  induction n with nn nih,
  {
    rw hyperoperation_1_addition,
  },
  {
    rw [hyperoperation_n1ab1_recurse,hyperoperation_n2a1_a,nih],
  },
end

[Mark Andrew Gerads]

After reading https://leanprover-community.github.io/contribute/style.html , I supposed I should replace a and b with m and k.

[Junyan Xu]

I think the next challenge is to show monotone and strict_mono w.r.t. the three arguments, whenever applicable. And the relationship with the Ackermann function which is already in mathlib as docs#ack. There's also relationship with Knuth's up-arrow and Conway's chained arrow notation, which however aren't in mathlib yet. (Personally, I have some computation using Knuth's arrows that I may formalize sometime ...)

[Mark Andrew Gerads]

PR now awaiting review.
https://github.com/leanprover-community/mathlib/pull/18116