Zulip Chat Archive

Stream: new members

Topic: has_zero

Guilherme Kunigami (Jan 25 2022 at 01:11):

I'm writing down some of https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ into a single standalone code and trying to run it in https://leanprover.github.io/live/latest.

I have this code: https://tinyurl.com/2p9afvwh

When I try to prove the zero_add lemma, I'm required to explicitly rewrite zero as 0 (via the zero_is_nat axiom), whereas in the game it seems like this inference happens automatically. Am I missing something?

instance : has_zero Nat := ⟨zero⟩    
axiom zero_is_nat : zero = 0
axiom add_zero (n : Nat) : n + 0 = n
lemma zero_add (n : Nat) : 0 + n = n :=
induction n with d hd,

-- base
--  rw zero_is_nat,
rw add_zero,

-- inductive step
rw add_succ,
rw hd,

Alex J. Best (Jan 25 2022 at 01:25):

You aren't missing anything, there are a few differences between the game and the environment you are running in.
The first is that the natural number game is tweaked for teaching purposes to make some things more intuitive, I believe the behaviour of induction is one of those things.
The second is that the game runs on a more recent but not the most recent version of lean, the web editor you are using is actually very old, we recommend you use the more recent one at https://leanprover-community.github.io/lean-web-editor/

Guilherme Kunigami (Jan 25 2022 at 03:15):

Thanks for the pointers!

There does seem to be some customization here:

Is there any way to "alias" Nat.zero to 0?

So when declaring a lemma like this

lemma zero_add (n : Nat) : 0 + n = n :=

It really means

lemma zero_add (n : Nat) : add zero n = n :=


Alex J. Best (Jan 25 2022 at 11:43):

Thats what declaring has_zero Nat does, it makes lean interpret 0 : Nat using Nat.zero, the two should be definitionally equal but displayed differently

Kevin Buzzard (Jan 25 2022 at 12:04):

Yes, induction had the irritating behaviour that it would use nat.zero which was definitionally but not syntactically has_zero.zero so I did some hackery with induction to make this not happen

Eric Wieser (Jan 25 2022 at 15:16):

Do we have a recursor for nat that expresses things in terms of 0 and +1?

Eric Wieser (Jan 25 2022 at 15:17):

Then you could use induction n using that_nat_recursor

Guilherme Kunigami (Jan 25 2022 at 17:53):

Another confusing bit is that rw zero_is_nat rewrites both zeros to 0:

 -- 0 + zero = zero
 rw zero_is_nat
 -- 0 + 0 = 0

Whereas in other scenarios rw seems to only re-write the first occurrence. I'm assuming the second zero turned into 0 via some type inference?

Yaël Dillies (Jan 25 2022 at 17:54):

No, it finds the first occurrence to figure out the correct arguments, then rewrites it everywhere.

Patrick Massot (Jan 25 2022 at 18:00):

Guilherme, see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20rw.20tactic

Guilherme Kunigami (Jan 25 2022 at 18:01):

Yaël Dillies said:

No, it finds the first occurrence to figure out the correct arguments, then rewrites it everywhere.

ohh! thanks for the clarification :)

Guilherme Kunigami (Jan 25 2022 at 18:03):

Thanks for the link Patrick, Kevin's answer explains the rw in more detail:


Patrick Massot (Jan 25 2022 at 18:04):

I don't know whether we have this explanation somewhere on the community website, but we should. This is a very natural question and people ask about it pretty often.

Bhavik Mehta (Jan 25 2022 at 20:18):

@Eric Rodriguez could we add this to the FAQ?

Eric Rodriguez (Jan 26 2022 at 13:04):

done, and also added something about nat.zero. https://github.com/ericrbg/leanFAQ/wiki/Tactics if someone can check this would be appreciated as I'm really not sure about my writing here

Last updated: Dec 20 2023 at 11:08 UTC