Proof-step vs tactic

Stream: new members

[Chandan Sah]

Can anyone help me? What is the difference between proof-step and a tactic?

[Chandan Sah]

Or send here an article that answers it?

[Marcus Rossel]

(deleted)

[Marcus Rossel]

From #tpil chapter 5:

In this chapter, we describe an alternative approach to constructing proofs, using tactics. A proof term is a representation of a mathematical proof; tactics are commands, or instructions, that describe how to build such a proof.

[Marcus Rossel]

I guess one could then say that a tactic is a tool that allows you to perform a proof step by generating (part of) a proof term. For example the intro tactic allows you to introduce hypotheses by generating the appropriate proof term required for this.

[Jason Rute]

A “proof step” is a generic term roughly meaning one step of a proof. Some logical calculii like Hilbert-style deduction in FOL have very clear atomic proof steps in a linear step-by-step proof and often the steps of a proof are numbered. Other logics like Lean’s term proof language make it a little mirkier what a single proof step would be. First, Lean’s term proofs are terms, so to turn them into individual steps you need a way to break up the proofs into steps which would mean building a term one step at a time. Second, there is a form of automation built into Lean’s logic so one can prove say 100 * 100 = 10000 with a one token proof, refl even though the proof may take a long time to finish.

Also term proofs are just one way to construct proofs in Lean. Tactics are meta programs which build a partial term proof. Each tactic fills in more and more of the proof until it is complete. A simple tactic proof will look like a list of tactics and it would make sense to call each tactic a “proof step”. A more complicated tactic proof would be made up of a tree of tactics, and some tactics might be combined together to make other larger tactics. For example repeat { intro , refl } is a single tactic, but it uses a tactic combinator to wrap other tactics. So you could think of this a single large proof step, but you could also think of the sub tactics as their own mini proof steps. In Lean 4, the tactic language is even more combinatorial where you can have tactics inside tactics and it is sometimes hard to know where a single tactic begins and ends.

TL;DR Proof step is a vague term without a well defined meaning, but it roughly means one step of the proof. Tactics are a specific concept in Lean and other ITPs, but even then it is sometimes hard to decide what a single tactic proof step would be since the proofs aren’t linear.