# 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.zero`

s 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