Zulip Chat Archive

Stream: general

Topic: int numerals -> nat


view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 14 2021 at 21:52):

norm_num can probably be taught to solve that

view this post on Zulip 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

view this post on Zulip Jeremy Avigad (Feb 14 2021 at 22:10):

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

view this post on Zulip 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?

view this post on Zulip Jeremy Avigad (Feb 15 2021 at 00:46):

norm_num does not currently solve this.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 15 2021 at 01:34):

@Jeremy Avigad

view this post on Zulip Mario Carneiro (Feb 15 2021 at 02:47):

#6235


Last updated: May 13 2021 at 22:15 UTC