Lean v4.3.0 change to simp defaults breaks proofs

[coproduct]

In Lean v4.3.0, "simp will no longer try to use Decidable instances to rewrite terms" by default (release notes). This change broke these proofs in chapter 3:

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := by simp

with unsolved goal ⊢ String.append "Str" "ing" = "String" and

#eval third woodlandCritters (by simp)

with simp made no progress.

These can be fixed with the decide config option like so:

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := (by simp (config := {decide := true}))

#eval third woodlandCritters (by simp (config := {decide := true}))

Thanks for the book! If I find other instances of this breakage, would you rather I comment on this issue or make new ones?

[david-christiansen]

Thanks!

Comments here are fine. But the book's CI will catch it when I do the next version bump, so please don't feel like you need to find everything by hand.

[medovina]

Note that in the fixes above, instead of (by simp (config := {decide := true})) you could just write (by decide).

[Aphexus]

Still a problem.