Zulip Chat Archive

At this point in the proof, the goal is an inequality between ints, all of which are explicitly int.of_nat n for some n. I feel like I should be able to say norm_cast or push_cast in order to get a goal that's just about natural numbers. Why am I wrong?

import tactic
import data.nat.basic
import data.int.basic

example (x : ℕ) : 2 ≤ int.of_nat (1 + x) + int.of_nat (1 + x) :=
begin
lift (2 : ℤ) to ℕ,
end

Jalex Stark (May 13 2020 at 22:06):

I feel like I want a tactic work_in which takes a type as an argument and tries to coerce or lift things in your goal to that type

Jalex Stark (May 13 2020 at 22:06):

work_in (zmod 24) would be nice for some number theory kata

Jalex Stark (May 13 2020 at 22:09):

(of course, I don't know how to implement this without magic, the tactic has to break up the goal into "atoms" and "glue" --- you don't want to lift (+) to a nat, you want it to stay has_add.add for whatever you're changing the stuff around it to)

Kevin Buzzard (May 13 2020 at 23:05):

The canonical map from nat to int is probably coe rather than int.of_nat

Kevin Buzzard (May 13 2020 at 23:06):

Does linarith do it?

Kevin Buzzard (May 13 2020 at 23:07):

(away from lean right now)

Mario Carneiro (May 13 2020 at 23:07):

You should rewrite int.of_nat to coe, then use norm_cast as normal

Mario Carneiro (May 13 2020 at 23:08):

example (x : ℕ) : 2 ≤ int.of_nat (1 + x) + int.of_nat (1 + x) :=
begin
  simp only [int.of_nat_eq_coe], norm_cast,
end

works great

Jalex Stark (May 13 2020 at 23:13):

i see. the int.of_nat came from cases on integers

Mario Carneiro (May 13 2020 at 23:14):

protip: if you use the equation compiler to write a proof by cases, you can give the case as | (n : nat) := and then you won't see of_nat

Jalex Stark (May 13 2020 at 23:15):

(deleted)

Jalex Stark (May 13 2020 at 23:16):

okay, the last several times i attempted to use the equation compiler i got errors I didn't understand. I guess I can go out and find some examples

Jalex Stark (May 13 2020 at 23:22):

today I learned that if you delete all of the text in a post, it gets auto-replaced by (deleted), but I have been manually entering that string a bunch