has_zero

Stream: new members

[Guilherme Kunigami]

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 :=
begin
induction n with d hd,

-- base
--  rw zero_is_nat,
rw add_zero,

-- inductive step
rw add_succ,
rw hd,
end

[Alex J. Best]

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]

Thanks for the pointers!

There does seem to be some customization here:
https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/tactic/modded.lean#L73-L78

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]

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]

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]

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

[Eric Wieser]

Then you could use induction n using that_nat_recursor

[Guilherme Kunigami]

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]

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

[Patrick Massot]

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

[Guilherme Kunigami]

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]

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

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

[Patrick Massot]

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]

@Eric Rodriguez could we add this to the FAQ?

[Eric Rodriguez]

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