Confusion about use of "definitional equality" in FPIL

Stream: new members

[mars0i]

From FPIL section 8.5:

def Nat.plusR : Nat → Nat → Nat
  | n, 0 => n
  | n, k + 1 => plusR n k + 1

and

def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
  | 0 => by rfl
  | k + 1 => _

Then the book says:

The second placeholder is a bit trickier. The expression Nat.plusR 0 k + 1 is definitionally equal to Nat.plusR 0 (k + 1). This means that the goal could also be written k + 1 = Nat.plusR 0 k + 1:

def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
  | 0 => by rfl
  | k + 1 => (_ : k + 1 = Nat.plusR 0 k + 1)

My question is just about the claim that "Nat.plusR 0 k + 1 is definitionally equal to Nat.plusR 0 (k + 1)." If these are definitionally equal, why can't we just write by rfl in the rhs of the last line? I thought that's the kind of case that rfl is for. But replacing the rhs of the last line with by rfl produces:

tactic 'rfl' failed, the left-hand side
  k + 1
is not definitionally equal to the right-hand side
  Nat.plusR 0 (k + 1)
k : Nat
⊢ k + 1 = Nat.plusR 0 (k + 1)

The error message mentions Nat.plusR 0 (k + 1) rather than Nat.plusR 0 k + 1. I assume that's because rfl sees those as definitionally equal, but modulo that, it's saying that the definitional equality claimed in the text doesn't exist, right?

Is there something I don't understand? Or is this a typo in FPIL? (If so I can report it, but I wanted to check first whether there's something I misunderstand--which is likely.)

[Henrik Böving]

k + 1 = Nat.plusR 0 k + 1 is provable with induction but not by definitional equality. The definitional equality here can only reduce further if the k argument is a + 1 or a 0 which it isn't, it's k. So you are stuck at this point if you only rely on defeq

[Kyle Miller]

It's true that Nat.plusR 0 k + 1 is definitionally equal to Nat.plusR 0 (k + 1). You can verify that with

example (k : Nat) : Nat.plusR 0 k + 1 = Nat.plusR 0 (k + 1) := rfl

Since rfl doesn't work for k + 1 = Nat.plusR 0 (k + 1), the conclusion you should draw is that k + 1 is not definitionally equal to Nat.plusR 0 (k + 1).

Notice that in

def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
  | 0 => by rfl
  | k + 1 => (by rfl : k + 1 = Nat.plusR 0 k + 1)

the error reports Nat.plusR 0 k + 1. All rfl does is report the LHS and RHS of what it sees. It won't reduce anything in the report.

[mars0i]

Thanks very much @Kyle Miller, @Henrik Böving for the patient explanations. I see now that I was confused, and not paying attention to details that were there in front of me.

I hadn't seen the syntax for adding a type signature to a by expression. That's very helpful. (I'd also forgotten about example.)

[Kyle Miller]

It turns out to be the same general type ascription syntax. Remember that by blah is itself a term, so you can put it in place of e in (e : ty).

[mars0i]

OK, I see. And in (by rw [Nat.add_comm]; rfl), I'd add the colon and type just before the closing parenthesis. I hadn't been sure about how to think about the full implications of the by syntax.