int numerals -> nat

Stream: general

[Jeremy Avigad]

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]

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

[Eric Wieser]

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]

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]

norm_num can probably be taught to solve that

[Eric Wieser]

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]

Alas, the bit1 version is false when x is negative.

[Yakov Pechersky]

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

[Jeremy Avigad]

norm_num does not currently solve this.

[Mario Carneiro]

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

[Mario Carneiro]

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]

@Jeremy Avigad

[Mario Carneiro]

#6235