Zulip Chat Archive

Stream: new members

Topic: conceptual mathematical primer for tactics?

view this post on Zulip Chris M (Jun 16 2020 at 04:10):

I haven't used tactics yet in Lean, and starting to. Looking at the tutorial, some of them seem unnatural to me, and it's not "clicking" yet for me. Can you point to a practice that mathematicians perform within informal mathematical proofs, to which tactics are analogous? Is it possible to say "tactics are the formal version of ...."?

view this post on Zulip Jalex Stark (Jun 16 2020 at 06:29):

tactics are programs that build proof terms

view this post on Zulip Jalex Stark (Jun 16 2020 at 06:29):

in informal math we don't build proof terms, we argue that we could build a proof term if we tried

view this post on Zulip Jalex Stark (Jun 16 2020 at 06:30):

norm_num is a like a mathematician's a short calculation shows...

view this post on Zulip Utensil Song (Jun 16 2020 at 07:18):

I think it's a good idea to have such conceptual mathematical primer for tactics, I'll try to merge this idea into the cheat sheet idea here .

view this post on Zulip Matt Earnshaw (Jun 16 2020 at 15:52):

you may find it worthwhile to read at least the intro of Milner's paper that introduced the tactic idea, which gives a nice informal explanation https://royalsocietypublishing.org/doi/10.1098/rsta.1984.0067
If there are specific tactics that trouble you, feel free to ask about them. Some perhaps too obvious examples would be apply as recognising that when A -> B and we want to prove B then it suffices to prove A, and intro as introducing an arbitrary x : X when we want to prove a forall x : X

Last updated: May 13 2021 at 00:41 UTC