## Stream: new members

### Topic: conceptual mathematical primer for tactics?

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

#### Jalex Stark (Jun 16 2020 at 06:29):

tactics are programs that build proof terms

#### 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

#### Jalex Stark (Jun 16 2020 at 06:30):

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

#### 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 .

#### 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