Issue with simp?

Stream: lean4

[Arien Malec]

I would think this should close via simp?

example: a * c + b * c + (a + b) = a * c + a + (b * c + b) := by simp

gets the helpful message

typeclass instance problem is stuck, it is often due to metavariables
  HAdd ?m.188 ?m.189 ?m.190

[Jireh Loreaux]

Two questions:

1. what are the types of a,b,c? This is not an #mwe
2. why do you think simp should be able to solve this? (ring would make more sense to me, if you have Mathlib4 imported)

[Arien Malec]

Good point -- poor typing on the example.

example (a b c: Nat): a * c + b * c + (a + b) = a * c + a + (b * c + b) := by simp

now just fails to close.

my expectation from previous work with the NNG is that simp closes goals that can be solved via associativity and commutitivty

[Jireh Loreaux]

Sorry, I had to step away. Aha, you are working with NNG, which one? There are now a few of these floating around and you seem to be on a Lean 4 version (given that you typed Nat and not nat)? No, simp does not in general close goals involving associativity and commutativity. This is because such lemmas are generally not tagged with the simp attribute.

A lemma will generally be a simp lemma if it is an equality (or an ↔) for which the left-hand side is "more complicated" than the right-hand side, and for which you almost always want to replace the left-hand side with the right-hand side wherever you find it.

So, a lemma like zero_add (x : Nat) : 0 + x = x should be a simp lemma. On the other hand, add_comm (x y : Nat) : x + y = y + x should not be a simp lemma because both sides are equally complicated, and similarly for add_assoc. A tactic that deals with associativity and commutativity would be tactic#ac_refl, but this is a Lean 3 tactic, I'm not sure if it exists in Lean 4 or if you have access to it in NNG.

[Arien Malec]

Gotcha -- yeah, I'm learning Lean4 tactics from TPIL, and practicing by re-deriving the NNG work following the TPIL work. Back to figuring out the magic combination of rewrites.

[Arien Malec]

The quote that I was leaning on was from NNG multiplication world 7 "If your goal looks like a+(b+c)=c+b+a or something, don't mess around doing it explicitly with add_comm and add_assoc, just try simp." -- maybe @Kevin Buzzard tagged those in the context of NNG?

[Chris Lovett]

Arien, I got that one working in lean4 already, so if you get stuck in your learning process you can go here for the lean4 answers:
https://github.com/leanprover/lean4-samples/tree/main/NaturalNumbers
See Level 9, the trick is registering things with simp using this:

attribute [simp] mul_assoc mul_comm mul_left_comm

[Arien Malec]

Yep, I'm doing a custom thing building my own definition of mul but relying on Nat's built in definition. @Kevin Buzzard/NNG must mark the relevant add version of assoc and comm as simp as well.

[Arien Malec]

anyway

conv =>
      rhs
      rw [Nat.add_assoc, Nat.add_comm a, Nat.add_assoc, ←Nat.add_assoc, Nat.add_comm b]

closes this goal.

[Arien Malec]

Just verifying that the lean3 equivalents are also not marked as simp

[Kevin Buzzard]

Back in the day, add_comm was tagged simp, and ring didn't exist, but times change. The ring tactic is now the appropriate tactic to solve lemmas such as this.