Bug in Lean 4.7.0 or FPIL sect 3?

Stream: general

[mars0i]

FPIL section 3 says:

Replacing A and B with concrete propositions, it is possible to prove 1 + 1 = 2 ∧ "Str".append "ing" = "String" with And.intro rfl rfl.

That works for me.

Of course, simp is also powerful enough to find this proof:

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

This doesn't work with my setup, Lean (version 4.7.0-rc2, x86_64-apple-darwin21.6.0, commit 6fce8f7d5cd1, Release). The error is:

▶ 69:69-69:76: error:
unsolved goals
p q r : Prop
⊢ String.append "Str" "ing" = "String"

I'm not sure whether this is supposed to work, and it's an error in FPIL, or whether there's a bug in Lean 4.7.0-rc2, or something I've done wrong (the most likely given my level of experience, but I can't see what it would be).

[Notification Bot]

A message was moved here from #general > FPIL and TPIL with internal tables of contents? by mars0i.

[Edward van de Meent]

could it be the case that you are missing some imports or opens?

[mars0i]

Oh, right, that's the other alternative. Thanks @Edward van de Meent. I did consider that earlier, I recall now, but I don't see any mention of an import or open in this section of the book. This section is labeled as an "interlude", so it's not really a continuation of earlier sections. I think it's the first place where simp or theorem is mentioned, or at least seriously presented, so I think it's unlikely that the relevant import is to be carried over from an earlier section.

[Ruben Van de Velde]

It's also possible that this is a result of simp getting weaker relatively recently: it used to try decide but doesn't anymore