Trouble with a `rw`

Stream: lean4

[Mac]

So I have been toying around with Nat.add that is not left or right recursive and while trying to prove add_succ I ran into the following problem, which I think may be an bug in Lean, but I am not sure.

open Nat (zero succ)

def add : Nat → Nat → Nat
| 0, 0 => 0
| succ n, 0 => succ n
| 0, succ n => succ n
| succ m, succ n => succ (succ (add m n))

infixl:65 (priority := high) " + " => add

instance : Add Nat := ⟨add⟩ -- removing this fixes the theorem error

@[simp] theorem succ_zero : succ 0 = 1 := rfl

@[simp] theorem zero_add_zero : 0 + 0 = 0 := rfl

@[simp] theorem add_zero : n + 0 = n := by cases n; repeat rfl
@[simp] theorem zero_add : 0 + n = n := by cases n; repeat rfl

theorem succ_add_succ : succ m + succ n = succ (succ (m + n)) := rfl

@[simp] theorem add_one : n + 1 = succ n := by
  cases n with | zero => rfl | succ n => rw [succ_add_succ, add_zero]

@[simp] theorem one_add : 1 + n = succ n := by
  cases n with | zero => rfl | succ => rw [succ_add_succ, zero_add]

-- error: theorem fails despite goals accomplished
theorem add_succ {m n : Nat} : m + succ n = succ (m + n) := by
  revert m
  induction n with
  | zero => simp
  | succ n ih =>
    intro m
    cases m with
    | zero => simp
    | succ m =>
      rw [succ_add_succ, succ_add_succ] -- produces an `n + 1` for some reason
      show succ (succ (m + succ n)) = succ (succ (succ (m + n)))
      rw [@ih m]

The error on add_succ is as follows:

application type mismatch
  @Eq.ndrec Nat (succ m + succ (n + 1))
    (fun _a => (succ m + succ (succ n) = succ (succ m + succ n)) = (_a = succ (succ m + succ n)))
    (Eq.refl (succ m + succ (succ n) = succ (succ m + succ n)))
argument has type
  (succ m + succ (succ n) = succ (succ m + succ n)) = (succ m + succ (succ n) = succ (succ m + succ n))
but function has type
  (fun _a => (succ m + succ (succ n) = succ (succ m + succ n)) = (_a = succ (succ m + succ n)))
      (succ m + succ (n + 1)) →
    ∀ {b : Nat},
      succ m + succ (n + 1) = b →
        (fun _a => (succ m + succ (succ n) = succ (succ m + succ n)) = (_a = succ (succ m + succ n))) b

I am very confused as to why the n + 1 is introduced during rewriting. I am also curious as to why removing the Add instance fixes the error (and why the n + 1 still appears even then). Is this some weird bug in rw (or show) or are there details I am missing?

[Mario Carneiro]

Here's a minimized version:

open Nat

def add : Nat → Nat → Nat
| 0, 0 => 0
| succ n, 0 => succ n
| 0, succ n => succ n
| succ m, succ n => succ (succ (add m n))

instance : Add Nat := ⟨add⟩ -- removing this fixes the theorem error

theorem succ_add_succ : succ m + succ n = succ (succ (m + n)) := rfl

theorem add_succ : succ m + succ (succ n) = 0 := by
  rw [succ_add_succ]
  sorry

This is certainly a bug, and my guess is that it is caused by something that has a hardcoded match on Add.add Nat thinking that it's surely Nat.add and your alternate definition is confusing it. (Lean 3 simp has the same problem with numerals encoded using nonstandard instances of standard typeclasses)

[Kevin Buzzard]

So the problem should go away if you try this on a custom nat'?

[James Gallicchio]

I seem to have run into this bug trying to simplify a definition not involving Nat. I'll try to minimize but it's pretty deep in LeanSAT's propositional theory.

[James Gallicchio]

ok, removed all of our library imports, now it just has one mathlib import. if someone else has time I'd appreciate help reducing further:

import Mathlib.Data.Set.Finite

abbrev PropFun (ν : Type u) := (ν → Bool) → Bool

namespace PropFun

variable [DecidableEq ν]

def semVars' (φ : PropFun ν) : Set ν :=
  { x | ∀ (τ : ν → Bool), φ (Function.update τ x false) }

instance semVars'_finite (φ : PropFun ν) : Set.Finite φ.semVars' := sorry

noncomputable def semVars (φ : PropFun ν) : Finset ν :=
  Set.Finite.toFinset φ.semVars'_finite

def invImage [DecidableEq ν'] (f : ν ↪ ν')
      (vs : Finset ν) (φ : PropFun ν')
      (h : φ.semVars ⊆ vs.map f) : PropFun ν :=
  sorry

end PropFun

abbrev Cnf (L : Type u) := Array (Array L)

namespace Cnf

def toPropFun (φ : Cnf L) : PropFun L := sorry

def addClause (C : Array L) (f : Cnf L) : Cnf L := f.push C

theorem toPropFun_addClause (C : Array L) (f : Cnf L)
  : (f.addClause C).toPropFun = f.toPropFun
  := sorry

noncomputable def interp [DecidableEq L] (s : Cnf L) : PropFun L :=
  s.toPropFun.invImage sorry sorry sorry

theorem interp_addClause [DecidableEq L]
        (C : Array L) (s : Cnf L)
  : interp (addClause C s) = sorry := by
  ext τ
  unfold addClause
  unfold interp
  simp [Array.push]
  sorry

[Kim Morrison]

Presumably the problem here is with a instance resynthesisation: some non-canonical instance is being replaced by simp / rw with a canonical instance inappropriately.

[James Gallicchio]

I see -- so is the "bug" here is just an unclear error message? Or is the re-synthesizing behavior not intended?

[Kim Morrison]

No, Mario's example above definitely counts as a bug to me. The aggressive resynthesisation of instances is new in Lean 4. So far I've been surprised how unproblematic it is, but I think this is an example of it causing problems.