why doesn't simp use provided lemma

Stream: new members

[Michael George]

I'm having some trouble understanding why simp is not finishing a goal even though explicitly rewriting and then using simp does. I have

lemma add_1 [Add R] (x y : AdjoinSqrt R n) : (x + y).a₁ = x.a₁ + y.a₁ := by rfl
lemma zero_1 [Zero R] : (0 : AdjoinSqrt R n).a₁ = 0 := by rfl

Writing rw [add_1, zero_1]; simp solves my goal, but simp [add_1, zero_1] does not. Looking at the trace (with set_option trace.Debug.Meta.Tactic.simp) shows "no theorems found for pre-rewriting (0 + a).a₁", but it seems to me like add_1 should apply here (and rw seems to agree).

I'm not sure what I'm missing, any suggestions?

[Michael George]

Curiously, it seems to work if my proof is not in the context of the instance I'm trying to provide. Here's an MWE:

-- Numbers of the form a₁ + aₙ√n
@[ext] structure AdjoinSqrt (R : Type u) (n : R) where
  a₁ : R
  aₙ : R

instance [Zero R] : Zero (AdjoinSqrt R n) where
  zero := ⟨0,0⟩

@[simp] lemma zero_1 [Zero R] : (0 : AdjoinSqrt R n).a₁ = 0 := rfl
@[simp] lemma zero_n [Zero R] : (0 : AdjoinSqrt R n).aₙ = 0 := rfl

instance [Add R] : Add (AdjoinSqrt R n) where
  add x y := ⟨ x.a₁ + y.a₁, x.aₙ + y.aₙ ⟩

@[simp] lemma add_1 [Add R] (x y : AdjoinSqrt R n) : (x+y).a₁ = x.a₁ + y.a₁ := by rfl
@[simp] lemma add_n [Add R] (x y : AdjoinSqrt R n) : (x+y).aₙ = x.aₙ + y.aₙ := by rfl

instance [AddSemigroup R]: AddSemigroup (AdjoinSqrt R n) where
  add_assoc := by intros; ext <;> apply add_assoc

-- set_option trace.Debug.Meta.Tactic.simp true

theorem sqrt_zero_add [AddMonoid R] (a : AdjoinSqrt R n) : 0 + a = a := by
  ext <;> simp

instance [AddMonoid R]: AddMonoid (AdjoinSqrt R n) where
  -- works: zero_add := sqrt_zero_add
  zero_add := by
    intros a; ext
    -- fails: simp
    -- fails: simp [add_1, zero_1]
    -- succeeds:
    rw [add_1, zero_1]; simp
    rw [add_n, zero_n]; simp

Note that simp works fine in the proof of sqrt_zero_add, which I think is exactly the same as zero_add.

[Michael George]

Even more curiously, the simp works if I don't import one of my other files, the following class seems to be the issue:

class SignedRing (R : Type) extends Ring R, Signed R where
  sign_zero : sign 0 = 0
  sign_one  : sign 1 = 1
  sign_mul  : ∀ (a b : R), sign (a * b) = sign a * sign b
  zero_sign : ∀ (a : R), sign a = 0 → a = 0
  sign_neg  : ∀ (a : R), sign (-a) = -sign a
  sign_plus : ∀ (a b : R), sign a ≠ .neg → sign b ≠ .neg → sign (a + b) ≠ .neg

I'm continuing to investigate.

[Michael George]

This seems quite bizarre to me; here is a complete MWE with imports. Commenting out Foo allows the proof of zero_add to succeed:

import Mathlib.Algebra.Ring.Basic

-- commenting this out lets the proof go through, but currently it fails with `simp made no progress`:
class Foo (R : Type) extends Ring R where

-- Numbers of the form a₁ + aₙ√n
@[ext] structure AdjoinSqrt (R : Type u) (n : R) where
  a₁ : R
  aₙ : R

@[simps] instance [Zero R] : Zero (AdjoinSqrt R n) where
  zero := ⟨0,0⟩

@[simps] instance [Add R] : Add (AdjoinSqrt R n) where
  add x y := ⟨ x.a₁ + y.a₁, x.aₙ + y.aₙ ⟩

instance [AddSemigroup R]: AddSemigroup (AdjoinSqrt R n) where
  add_assoc := by intros; ext <;> apply add_assoc

instance [AddMonoid R]: AddMonoid (AdjoinSqrt R n) where
  -- fails with "simp made no progress" unless `Foo` is commented out:
  zero_add := by intros a; ext <;> simp

[Michael Stoll]

This works regardless of the presence of Foo:

instance [AddMonoid R]: AddMonoid (AdjoinSqrt R n) where
  zero_add := by intros a; ext <;> simp
  add_zero := by intros a; ext <;> simp
  nsmul := nsmulRec

(Your version produces errors because fileds are missing.)

[Kevin Buzzard]

Yes, it looks like the errors you're seeing are caused by things like tactics failing to solve goals which you've not explicitly solved and hence are being auto-solved by algorithms which can't solve them.

[Michael George]

Copying in your version still gave me the same problem:

./././Greeting/Roots.lean:29:35: error: simp made no progress
./././Greeting/Roots.lean:29:35: error: simp made no progress
./././Greeting/Roots.lean:29:14: error: unsolved goals

(as before, commenting out Foo let it build).

[Kevin Buzzard]

Are you not using an IDE? The issue is that your code has errors and you're unable to see what's causing them. Just to be clear, you've used your code and then replaced the instance with Michael's code? That also worked fine for me. Are you on some old version of mathlib or something?

[Michael George]

I'm using nvim (but I built with lake to check that my editor wasn't in some inconsistent state). You're correct - I got those errors by replacing my instance with Michael's. I don't think there's anything strange about my version of mathlib - I haven't updated it in a few weeks probably. How can I check that I have a reasonable one?

[Michael George]

That must have been it - I ran lake update and everything went through

[Michael George]

Thanks for your help

[Kevin Buzzard]

Yeah mathlib moves fast :-)