# Zulip Chat Archive

## Stream: general

### Topic: int numerals -> nat

#### Jeremy Avigad (Feb 14 2021 at 20:56):

Does anyone know how to prove this with `rw`

or `simp`

or some other tactic?

```
example : (5 : int).to_nat = 5 := rfl
```

(In my application, I have such expressions buried in a more complicated expression.)

#### Ruben Van de Velde (Feb 14 2021 at 21:06):

I think the only way I've seen is to turn `(5 : int)`

into `((5 : nat) : int)`

first

#### Eric Wieser (Feb 14 2021 at 21:46):

I don't understand the question, since you already have a proof - is `rw [(show (5 : int).to_nat = 5, from rfl)]`

an answer to your question?

#### Jeremy Avigad (Feb 14 2021 at 21:51):

I was hoping there might be a method that doesn't require doing that manually, and separately for each numeral. But if not, I'll manage. Thanks for the responses.

#### Eric Wieser (Feb 14 2021 at 21:52):

`norm_num`

can probably be taught to solve that

#### Eric Wieser (Feb 14 2021 at 21:55):

Alternatively - is there a simp lemma that says `(bit0 x).to_nat = bit0 (x.to_nat)`

? I think then simp could solve it

#### Jeremy Avigad (Feb 14 2021 at 22:10):

Alas, the `bit1`

version is false when `x`

is negative.

#### Yakov Pechersky (Feb 14 2021 at 22:17):

Does norm_num not solve this, or solve the goals you had upstream that lead to this state?

#### Jeremy Avigad (Feb 15 2021 at 00:46):

`norm_num`

does not currently solve this.

#### Mario Carneiro (Feb 15 2021 at 01:16):

There is definitely space for a norm_num extension with support for all the wacky int functions

#### Mario Carneiro (Feb 15 2021 at 01:33):

```
import tactic.norm_num
section end
namespace norm_num
open tactic
theorem int_to_nat_pos (a : ℕ) (b : ℤ)
(h : (by haveI := @nat.cast_coe ℤ; exact a : ℤ) = b) :
b.to_nat = a := by rw ← h; simp
theorem int_to_nat_neg (a : ℤ) (h : 0 < a) : (-a).to_nat = 0 :=
by simp [int.to_nat_zero_of_neg, h]
@[norm_num] meta def eval_int_to_nat : expr → tactic (expr × expr)
| `(int.to_nat %%e) := do
n ← e.to_int,
ic ← mk_instance_cache `(ℤ),
if n ≥ 0 then do
nc ← mk_instance_cache `(ℕ),
(_, _, a, p) ← prove_nat_uncast ic nc e,
pure (a, `(int_to_nat_pos).mk_app [a, e, p])
else do
a ← match_neg e,
(_, p) ← prove_pos ic a,
pure (`(0:ℤ), `(int_to_nat_neg).mk_app [a, p])
| _ := failed
end norm_num
example (p : ℤ → Prop) (h : p 5) : p (5 : int).to_nat := by norm_num; exact h
```

#### Mario Carneiro (Feb 15 2021 at 01:34):

@Jeremy Avigad

#### Mario Carneiro (Feb 15 2021 at 02:47):

Last updated: May 13 2021 at 22:15 UTC