Zulip Chat Archive

Stream: new members

Topic: Using 0 with has zero doesn't quite work


Ben (Nov 05 2022 at 17:19):

I am trying some things out (apologise for the lengthiness)

inductive my_nat : Type
| zero
| succ (n: my_nat)

def my_nat.add : my_nat  my_nat  my_nat
| a  my_nat.zero     := a
| a  (my_nat.succ b) := my_nat.succ (my_nat.add a b)

instance : has_add my_nat := my_nat.add
instance : has_zero my_nat := my_nat.zero

-- It works when I replace 0 here with `my_nat .zero`
lemma add_zero (a: my_nat) : a + 0 = a := rfl
lemma add_succ (a b: my_nat) : a + my_nat.succ b = my_nat.succ (a + b) := rfl

lemma succ_add (a b: my_nat) : my_nat.succ a + b = my_nat.succ (a + b) := begin
  induction b,
  repeat { rw add_zero },
  rw add_succ at b_ih,
  rw [b_ih, add_succ],
end

The succ_add lemma only checks when add_zero refers to my_nat .zero rather than the 0 symbol. The hypothesises in induction are written in terms of my_nat.zero rather with the 0 symbol. Any ideas how to rewrite 0 <-> my_nat.zero ?

Alex J. Best (Nov 05 2022 at 17:25):

The fact that 0 = my_nat.zero is true by definition, so you could either make a lemma stating that my_nat.zero = 0 (proved by rfl) and rewrite with it, or you could use tactic#change or something similar to substitute the definitionally equal term you want, e.g. with

  change my_nat.zero with 0,

Patrick Johnson (Nov 05 2022 at 17:38):

I guess the question is why doing induction on nat leaves literal 0 in the base case, while doing induction on my_nat leaves my_nat.zero in the base case, despite both nat and my_nat have defined has_zero and has_add.

Patrick Johnson (Nov 05 2022 at 17:38):

It probably has something to do with nat being in the core and gets special treatment by the pp.

Eric Wieser (Nov 05 2022 at 18:23):

You're right, this does seem to be a pretty-printer thing

Eric Wieser (Nov 05 2022 at 18:23):

Note that if you hover over the 0 in the widget goal view, you can tell the difference between nat.zero and has_zero.zero.

Yaël Dillies (Nov 05 2022 at 18:42):

Yes, it is the pretty printer. See the stupid-looking docs#nat.nat_zero_eq_zero

Kyle Miller (Nov 05 2022 at 20:00):

The special treatment for nats in the pretty printer is specifically this line of pp.cpp. I think it's set_option pp.nat_numerals false to turn it off.

Kyle Miller (Nov 05 2022 at 20:04):

Other numerals are decoded here. That's for pretty printing bit0/bit1/has_zero.zero/has_one.one/has_neg.neg expressions.

Kevin Buzzard (Nov 05 2022 at 21:52):

In the natural number game I had real problems with this, which I fixed by hacking the induction tactic so that after every time it ran it changed all mynat.zeros to 0 with a rewrite -- I wrote the rewrite lemma myself and proved it with refl and hid it from the user.


Last updated: Dec 20 2023 at 11:08 UTC