## 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