simp and nat lits

Stream: lean4

[François G. Dorais]

I've been noticing some instances where simp occasionally fails to simplify 0+n to n such as here:

example (n : Nat) : 1 + n = Nat.succ n := by simp [Nat.succ_add] -- fails!

I found this unusual since Nat.zero_add is a simp lemma! I figured that this was because Nat.zero_add uses the notation 0 instead of Nat.zero, as illustrated by

example (n : Nat) : Nat.succ 0 + n = Nat.succ n := by simp [Nat.succ_add] -- works!

So I added this simp lemma:

@[simp] theorem Nat.zero_add' (n : Nat) : Nat.zero + n = n := Nat.zero_add n

Now everything works swimmingly but something about the original issue that still bothers me.

Although, Nat.zero_add only hooks on the notation 0, there is the simp lemma Nat.zero_Eq: Nat.zero = 0 to work around that. For example:

example (n : Nat) : Nat.zero + n = n := by simp only [Nat.zero_add, eqSelf] -- fails (expected)
example (n : Nat) : Nat.zero + n = n := by simp only [Nat.zero_add, Nat.zero_Eq, eqSelf] -- works (expected)

However, Nat.zero_Eq doesn't always trigger as expected as illustrated by these examples:

example (n : Nat) : Nat.succ 0 + n = Nat.succ n := by simp only [Nat.succ_add, Nat.zero_add, eqSelf] -- works (expected)
example (n : Nat) : Nat.succ Nat.zero + n = Nat.succ n := by simp only [Nat.succ_add, Nat.zero_add, eqSelf] -- fails (expected)
example (n : Nat) : Nat.succ Nat.zero + n = Nat.succ n := by simp only [Nat.succ_add, Nat.zero_add, Nat.zero_Eq, eqSelf] -- works (expected)
example (n : Nat) : 1 + n = Nat.succ n := by simp only [Nat.succ_add, Nat.zero_add, Nat.zero_Eq, eqSelf] -- fails (unexpected!)

So it seems that some intermediate form of zero is generated when unifying 1 with Nat.succ _ and that intermediate form doesn't trigger Nat.zero_Eq.

Interestingly, there are no issues at all when using Nat.zero_add' instead of Nat.zero_add (and Nat.zero_Eq is no longer needed anywhere).

example (n : Nat) : 0 + n = n := by simp only [Nat.zero_add', eqSelf] -- works!
example (n : Nat) : Nat.succ Nat.zero + n = Nat.succ n := by simp only [Nat.succ_add, Nat.zero_add', eqSelf] -- works!
example (n : Nat) : Nat.succ 0 + n = Nat.succ n := by simp only [Nat.succ_add, Nat.zero_add', eqSelf] -- works!
example (n : Nat) : 1 + n = Nat.succ n := by simp only [Nat.succ_add, Nat.zero_add', eqSelf] -- works!

What is really going on here?

[François G. Dorais]

PS: This also works like the above:

theorem Nat.zero_add' (n : Nat) : no_index 0 + n = n := Nat.zero_add n

[François G. Dorais]

Weirdly interesting...

attribute [-simp] Nat.zero_Eq
@[simp] theorem Nat.zero_eq : no_index 0 = 0 := rfl
example (n : Nat) : 1 + n = n.succ := by simp [Nat.succ_add] -- works!

[François G. Dorais]

Apparently the intermediate form is a raw nat literal which doesn't match Nat.zero nor 0. I submitted an issue.