Zulip Chat Archive

Stream: lean4

Topic: (0: ℕ).succ workaround?


Chris Lovett (Aug 26 2021 at 01:04):

(deleted)

Chris Lovett (Aug 26 2021 at 01:06):

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 (Aug 26 2021 at 01:47):

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 (Aug 26 2021 at 21:50):

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 (Aug 26 2021 at 21:52):

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 (Aug 26 2021 at 21:53):

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

Chris Lovett (Aug 26 2021 at 21:57):

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 (Aug 26 2021 at 22:00):

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 (Aug 26 2021 at 22:02):

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 (Aug 26 2021 at 22:15):

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 (Aug 27 2021 at 02:21):

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 (Aug 27 2021 at 03:06):

@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]

Last updated: Dec 20 2023 at 11:08 UTC