[Bug] Leam version over 4.1.0 may not clost the proof when using `by simp`

[edwardzcn-decade]

Please quote the text that is incorrect:

E.g., the fowlloing two theoremspo are copied from Chap4 Indexing.lean

theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by simp
theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by simp

MISTAKE GOES HERE

It works well on the website (using the writer’s setup), but if your Lean version is over 4.10, you cannot run it on your own computer without encountering an error related to unsolved goals.

There are a lot of common problems because of the widely used simpl tactic.

e.g. In Chap 3. Chap 5

what way is this incorrect?

This is INCORRECT for users using Lean version > 4.10. People can not closing the proof as expected.

Personnaly

Personally, I don’t think this is a bug that could be solved by our community. I’ve listed it here to resolve confusion for subsequent learners using Lean, as suggested in the Hitchhiker’s Guide to Logical Verification. :)

Reference

chore: change simp default to decide := false

Alternative

Just replace by simpl with by decide. Or you can use (by simp (config := {decide := true})). Given by leanprover/fp-lean#152 (comment)