## Stream: new members

### Topic: typecasting

#### Jalex Stark (May 13 2020 at 22:04):

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

(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

why?

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

isn't there a button to delete your post? I think that does the auto-replace to (deleted)

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

where's the delete post button? I have been clicking edit and then selecting all the text and deleting

#### Mario Carneiro (May 13 2020 at 23:28):

maybe it's just me (i'm an admin)

#### Matt Earnshaw (May 13 2020 at 23:30):

if int.coe_nat_eq were tagged with norm_cast then the OP would go through... don't know if there's a case to be made for doing or not doing so

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

it's plausibly better to tag it with simp?

Last updated: May 08 2021 at 19:11 UTC