Zulip Chat Archive

Stream: new members

Topic: typecasting


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

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

view this post on Zulip Jalex Stark (May 13 2020 at 22:06):

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

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 23:05):

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 23:06):

Does linarith do it?

view this post on Zulip Kevin Buzzard (May 13 2020 at 23:07):

(away from lean right now)

view this post on Zulip Mario Carneiro (May 13 2020 at 23:07):

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

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

view this post on Zulip Jalex Stark (May 13 2020 at 23:13):

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

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

view this post on Zulip Jalex Stark (May 13 2020 at 23:15):

(deleted)

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

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

view this post on Zulip Mario Carneiro (May 13 2020 at 23:23):

why?

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

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

view this post on Zulip Mario Carneiro (May 13 2020 at 23:28):

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

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

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