conceptual mathematical primer for tactics?

Stream: new members

[Chris M]

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 ...."?

[Jalex Stark]

tactics are programs that build proof terms

[Jalex Stark]

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

[Jalex Stark]

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

[Utensil Song]

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 .

[Matt Earnshaw]

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