2
$\begingroup$

I don't understand LEAN well enough, but from my rough understanding that tactics delete old pairs of conditions and goals and create new pairs of conditions and goals, it seems all tactics are applying some form of theorem. For instance, 'refl' applies the theorem 'x=x' for all x. 'apply' applies a theoremm to reduce proving the current goal to proving other goals. 'cases' splits a goal into subcases, which could be understood as applying a theorem classifying the goal w.r.t. some criteria. Are there counter-examples to this claim? Are there more precise statement that says something about classifying all tactics?

$\endgroup$
5
  • 3
    $\begingroup$ Kyle Miller gave a good answer below, but as a matter of general knowledge about logic, let me just say that not every step in a proof is an application of a theorem. It can also be an axiom, or an inference rule of logic. For example, if from an assumption $A$ you proved $B$, then you can apply the rule of inference called "implication introduction" to conclude $A \Rightarrow B$. $\endgroup$ Commented Nov 13, 2023 at 19:53
  • $\begingroup$ @AndrejBauer isn't a rule of inference also a theorem? $\endgroup$ Commented Nov 23, 2023 at 0:49
  • 2
    $\begingroup$ @DanielDonnelly: Most rules of inference have corresponding theorems, for example the rule that $\vdash A$ and $\vdash B$ entail $\vdash A \land B$ has the corresponding theorem $\vdash A \Rightarrow B \Rightarrow A \land B$, see deduction theorem. However, we cannot eliminate all rules of inference, because then we would never be able to make any reasoning steps. In particular, we could never apply any theorems, as that (in typicaly cases) requires $\forall$-elimination or $\Rightarrow$-elimination. $\endgroup$ Commented Nov 23, 2023 at 18:38
  • $\begingroup$ @AndrejBauer Do you know if there are a minimal set of logical inference rules one need to conduct proofs? Do one need anything besides $\forall$-elimination/introduction and $\Rightarrow$-elimination/introduction? $\endgroup$
    – 12121
    Commented Dec 6, 2023 at 19:45
  • 1
    $\begingroup$ That depends on what sort of system you use. In a Hilbert system there are just two rules of inference, namely modus ponens and generalization. In natural deduction each connective has introduction and elimination rules, so there are many. However, let me say that a formal system is not inherently better just because it has fewer rules. Different ways of setting up logic have different goals and applications. $\endgroup$ Commented Dec 6, 2023 at 19:49

1 Answer 1

3
$\begingroup$

Here's the model:

  • A metavariable is a "hole" in an expression that must eventually be filled to get a complete expression. A metavariable has a type, a local context, and, optionally, an assigned value that fills it in. The local context consists of a list of local variables, their types, and, if they are local definitions, their values.
  • The tactic state is a list of metavariables, called goals. The "tactic state" window in VS Code displays each metavariable's local context and type.
  • The by ... syntax creates a fresh metavariable and sets up a tactic state with that single metavariable.
  • Each tactic operates by assigning expressions to metavariables. Those expressions themselves might contain new metavariables, in which case the tactic is sure to place those new metavariables into the tactic state.

For example, the constructor tactic in Lean 4 assigns a constructor expression to the first goal, applying enough metavariable arguments to make it well-typed. In the following example, we start with a single goal, and then the constructor tactic assigns And.intro ?left ?right, where ?left and ?right are new metavariables. (These names are reflected in the case tags.)

example (p q : Prop) : p ∧ q := by
  /-
  p q : Prop
  ⊢ p ∧ q
  -/
  constructor
  /-
  case left
  p q : Prop
  ⊢ p

  case right
  p q : Prop
  ⊢ q
  -/

Indeed, we can verify this by using the Std library's show_term tactic, which shows you what the current goal's metavariable is assigned to immediately after the tactic is executed.

import Std.Tactic.ShowTerm

set_option pp.structureInstances false

example (p q : Prop) : p ∧ q := by
  show_term constructor
  -- refine And.intro ?left ?right

(I set pp.structureInstances to false to get it to show And.intro rather than some { ... } structure expression.)

I could go into more examples, but every single tactic works in a similar way, with varying levels of complexity. With Lean 4 in VS Code, you can right click on a tactic and do "Go to definition" to see its implementation. You might need to do import Lean at the beginning to ensure the source position information is loaded.

$\endgroup$
2
  • $\begingroup$ TL;DR, is that a yes or a no? $\endgroup$ Commented Nov 23, 2023 at 0:48
  • 1
    $\begingroup$ @DanielDonnelly Technically "no" since they can assign non-theorem terms like lambdas, foralls, Sort*, etc. too, but essentially "yes" because every tactic operates by assigning ("applying") terms to the goal. There's also the wrinkle of how tactics such as intro manage to create the correct tactic state (that would get into delayed assignment metavariables, implementing what Andrej mentioned about implication introduction, but these aren't intro's responsibility per se). $\endgroup$ Commented Nov 23, 2023 at 4:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.