Topic: int numerals -> nat
Jeremy Avigad (Feb 14 2021 at 20:56):
Does anyone know how to prove this with
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):
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):
Mario Carneiro (Feb 15 2021 at 02:47):
Last updated: May 13 2021 at 22:15 UTC