Zulip Chat Archive

Stream: general

Topic: Tactic mode to term mode


view this post on Zulip Ashvni Narayanan (Aug 18 2020 at 19:41):

I am trying to convert a tactic mode proof into a term mode proof. It is quite confusing. I tried using show_term, but that did not work out too well. Is there any online guide/reference regarding this? Thank you!

view this post on Zulip Mario Carneiro (Aug 18 2020 at 19:47):

that's pretty broad. What tactics are you using?

view this post on Zulip Mario Carneiro (Aug 18 2020 at 19:49):

Here's a small listing of simple tactics and their term mode equivalents: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20building.20block.20tactics/near/189275113

view this post on Zulip Ashvni Narayanan (Aug 18 2020 at 19:50):

Mario Carneiro said:

that's pretty broad. What tactics are you using?

rintros, apply, split, cases, use, and simp. I tried to do away with as many simps as possible.

view this post on Zulip Mario Carneiro (Aug 18 2020 at 19:53):

you can often use calc in place of simp, to make the rewrites explicit

view this post on Zulip Mario Carneiro (Aug 18 2020 at 19:54):

but it's generally best to leave rewrites as by rw thm even in term mode proofs because the elaboration is more controlled than what you get with eq.rec_on thm

view this post on Zulip Mario Carneiro (Aug 18 2020 at 19:55):

everything else is easy term mode stuff

view this post on Zulip Mario Carneiro (Aug 18 2020 at 19:56):

especially if you cheat and use let <x, y, z> := or match in place of cases and rintros

view this post on Zulip Ashvni Narayanan (Aug 18 2020 at 20:37):

Thank you very much, I will give it another go.


Last updated: May 13 2021 at 21:12 UTC