(0: ℕ).succ workaround?

Stream: lean4

[Chris Lovett]

(deleted)

[Chris Lovett]

Lean3 I can write this, but not in Lean4 is there a workaround?

notation "ℕ" => Nat
axiom one_eq_succ_zero : 1 = (0: ℕ).succ

I get this error:

function expected at
  Nat.succ 0
term has type
  ℕ

[Floris van Doorn]

Do you get the same error when you paste this in an empty file?
It is likely that something on the next line causes this error, because Lean thinks you're applying (0: ℕ).succ to whatever is on the next line.

[Chris Lovett]

Oh wow, you are right, thanks. I had lots of fun with the Natural Number Game and now I'm trying to port my answers to Lean 4... and my follow on syntax for a lemma is incorrect. This bogus error on previous line thing is not very friendly... can that be fixed?

[Mario Carneiro]

lean will often be able to catch this due to whitespace sensitivity, but you have to be in a context that introduces a colGt scope, like by

[Mario Carneiro]

in other words, if you inserted by exact before the type, it would probably not get confused like this

[Chris Lovett]

Harumph. Sounds like the answer is "it's hard" because of the lean language syntax. By the way what is the lean4 equivalent of this?

lemma zero_add (n : ℕ) : 0 + n = n :=
  induction n with d h,
  rw add_zero,
  rw add_succ,
  rw h

[Mario Carneiro]

theorem zero_add (n : ℕ) : 0 + n = n := by
  induction n with
  | zero => rw add_zero
  | succ d h =>
    rw add_succ
    rw h

[Mario Carneiro]

Chris Lovett said:

Harumph. Sounds like the answer is "it's hard" because of the lean language syntax.

Actually, it's closer to "it used to be impossible, now it is possible but requires specific accomodation in the grammar"

[Mario Carneiro]

In lean 3, the main mechanism for avoiding this is command keywords like theorem or lemma, which always end the previous definition no matter where it is written. I'm guessing that you discovered that lemma is no longer a command keyword in lean 4; if you use mathlib4 then lemma will be a command keyword

[Chris Lovett]

I'm getting a syntax error on add_zero, is my add_zero axoim correct?

notation "ℕ" => Nat
axiom add_zero (x : ℕ) : x + 0 = x
axiom add_succ (a d : ℕ) : a + d.succ = (a + d).succ

image.png

[Leonardo de Moura]

@Chris Lovett

notation "ℕ" => Nat
axiom add_zero (x : ℕ) : x + 0 = x
axiom add_succ (a d : ℕ) : a + d.succ = (a + d).succ

theorem zero_add (n : ℕ) : 0 + n = n := by
  induction n with
  | zero => rw [add_zero]
  | succ d h => rw [add_succ, h]