3
$\begingroup$

In 3. Interlude of the Functional Programming in Lean book, one of the exercises asks the reader to prove by simp some few theorems, one of them is "Hello, ".append "world" = "Hello, world". However, when I write

theorem appendHelloWorld : "Hello, ".append "world" = "Hello, world" := by simp

I get an error message telling that simp made no progress. How should I write the theorem to solve the exercise?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ I agree, by simp doesn’t work in the current version of Lean. by rfl does work however. I would make an issue on the book’s GitHub or reach out to the author. $\endgroup$
    – Jason Rute
    Commented Apr 28 at 0:57

1 Answer 1

Reset to default
4
$\begingroup$

Perhaps you need to tell Lean what to simplify.

theorem appendHelloWorld : "Hello, ".append "world" = "Hello, world" := by simp [String.append]

I think it is a bug. It seems like a commit caused this regression.

Lean changed the default behavior of simp since 4.3.0

The current default is that simp will call decide to discharge goals. This is a change from Lean 3, potentially expensive, and not relied on by anything in this repository (i.e. CI passes here). Could we consider changing the default to decide := false.

See also this.

Improve this answer
$\endgroup$
4
  • $\begingroup$ A regression in the book or in Lean? $\endgroup$
    – Jason Rute
    Commented Apr 28 at 0:59
  • $\begingroup$ I thought previously Lean’s simp would run rfl at the end (unlike Coq’s simplify), but now it doesn’t seem to do that. I wonder if that is intended behavior? $\endgroup$
    – Jason Rute
    Commented Apr 28 at 1:11
  • $\begingroup$ The behavior of simp was changed since 4.3.0 (I tested on my computer). I noticed the change related to simp is chore: change simp default to decide := false by @collares in #2722 $\endgroup$
    – Hiroki Chen
    Commented Apr 28 at 1:17
  • $\begingroup$ @JasonRute github.com/leanprover/lean4/pull/1888 says that the default behavior of simp that uses the decidable instances to discard goals seems expensive so they just disabled the default one. $\endgroup$
    – Hiroki Chen
    Commented Apr 28 at 1:22

Not the answer you're looking for? Browse other questions tagged or ask your own question.