Zulip Chat Archive

I am working through the examples and exercises in Theorem Proving in Lean 4 chapter 7 on inductive types. There is a proof of zero_add about halfway through which looks reasonable and syntactic to me, but which doesn't parse when I put it in my buffer.

Is there some weird setting I accidently toggled?

Note if I change the rfl on the fist line of the calc block to a by rfl then it works fine. I guess there's something related to term mode vs tactic mode?

image.png

Kevin Buzzard (May 03 2023 at 18:49):

Can you post code rather than a screenshot? See #mwe for more details. I can't cut and paste a screenshot so I'm less likely to think about your question.

Ryan McCorvie (May 03 2023 at 18:51):

Sure, here is the code, which is generated from the "copy" button in a code block in TPIL4

-- try it
namespace Hidden
open Nat

theorem zero_add (n : Nat) : 0 + n = n :=
  Nat.recOn (motive := fun x => 0 + x = x)
   n
   (show 0 + 0 = 0 from rfl)
   (fun (n : Nat) (ih : 0 + n = n) =>
    show 0 + succ n = succ n from
    calc
      0 + succ n = succ (0 + n) := rfl
               _ = succ n       := by rw [ih])
end Hidden

Kyle Miller (May 03 2023 at 18:58):

I think the syntax for calc has changed a little bit in the meantime, and now the _ has to line up with the previous equation:

theorem zero_add (n : Nat) : 0 + n = n :=
  Nat.recOn (motive := fun x => 0 + x = x)
   n
   (show 0 + 0 = 0 from rfl)
   (fun (n : Nat) (ih : 0 + n = n) =>
    show 0 + succ n = succ n from
    calc
      0 + succ n = succ (0 + n) := rfl
      _          = succ n       := by rw [ih])