Zulip Chat Archive

Stream: new members

Topic: Eliminating coercions


Sandy Maguire (Jan 11 2021 at 20:28):

I have the following context

nd: 
x': n ^ 2 = 2 * d ^ 2
 n ^ 2 = 2 * d ^ 2

where the coe on n and d are both at \R. how can i prove the goal from x'?

Kevin Buzzard (Jan 11 2021 at 20:29):

Try assumption_mod_cast.

Sandy Maguire (Jan 11 2021 at 20:29):

that does it. how could i have found this for myself?

Kevin Buzzard (Jan 11 2021 at 20:29):

Just keep asking.

Kevin Buzzard (Jan 11 2021 at 20:30):

The cast tactics are probably mentioned in the API documentation

Sandy Maguire (Jan 11 2021 at 20:30):

happy to continue asking, tho i feel like a bit of a burden!!

Kevin Buzzard (Jan 11 2021 at 20:30):

The one you need to know in this case is norm_cast at x'.

Kevin Buzzard (Jan 11 2021 at 20:31):

There's a relatively small number of techniques and if you keep trying to prove stuff then eventually you see them all

Sandy Maguire (Jan 11 2021 at 20:32):

that's helpful. thank you!

Bryan Gin-ge Chen (Jan 11 2021 at 20:37):

tactic#norm_cast mentions assumption_mod_cast and the other *_mod_cast tactics.

Kevin Buzzard (Jan 11 2021 at 20:40):

I used to think it was kind of hopeless trying to keep up with the new tactics, but actually over the last few months there are not so many new ones which have appeared, partly because we now have most of the ones we were desperate for (like assumption_mod_cast) and partly because I suspect the tactic writers are reluctant to work hard on Lean 3 now Lean 4 is here. Mathematically we're still missing a Groebner basis tactic, which I don't think anyone is working on ( :-( ), our omega tactic to solve stuff on nat is quite buggy, and some people want more general automation tactics because they're jealous of tactics in other provers. Gabriel was working on a hammer tactic but again I'm unclear about whether this will happen before Lean 4. Maybe just browsing the tactics in the API docs might be useful to you, I remember doing this quite a bit when I was learning.

Patrick Massot (Jan 11 2021 at 20:58):

Sandy, if you are serious about this you can also watch the full Lean for the curious mathematician series on Youtube (except the meta-programming part). This is not so long since most of the week were exercises sessions that are not recorded. This covers the norm_cast family of tactics.


Last updated: Dec 20 2023 at 11:08 UTC