Using 0 with has zero doesn't quite work

Stream: new members

[Ben]

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]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Kyle Miller]

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]

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

[Kevin Buzzard]

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.