Skip to content

1.19 Term Mode vs Tactic Mode

Lean proofs are terms.

lean proof-assistant type-theory functional-programming

Lean proofs are terms. Tactic mode is a way to construct those terms incrementally. Term mode writes the final object directly. Both styles produce the same kernel-checked result. The choice affects readability, locality of reasoning, and how easily a proof evolves.

Problem

You want to decide when to write a proof as a term, when to use tactics, and how to translate between the two styles.

Solution

Recognize that every tactic proof has a corresponding term proof. Use term mode for small, compositional proofs and tactic mode for stepwise transformations.

Example: Identity

Term mode:

theorem id_term (P : Prop) : P -> P :=
  fun h => h

Tactic mode:

theorem id_tactic (P : Prop) : P -> P := by
  intro h
  exact h

Both have the same type:

#check id_term
#check id_tactic

Reading Tactic Proofs as Terms

A tactic script corresponds to nested function applications and lambda abstractions.

theorem mp_tactic (P Q : Prop) (hp : P) (hpq : P -> Q) : Q := by
  exact hpq hp

Term version:

theorem mp_term (P Q : Prop) (hp : P) (hpq : P -> Q) : Q :=
  hpq hp

The tactic exact t inserts the term t.

Building Structure: Conjunction

Term mode:

theorem and_intro_term (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
  And.intro hp hq

Tactic mode:

theorem and_intro_tactic (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  · exact hp
  · exact hq

The constructor And.intro is applied explicitly in term mode and implicitly by constructor in tactic mode.

Case Analysis: Disjunction

Term mode:

theorem or_comm_term (P Q : Prop) : P ∨ Q -> Q ∨ P :=
  fun h =>
    Or.elim h
      (fun hp => Or.inr hp)
      (fun hq => Or.inl hq)

Tactic mode:

theorem or_comm_tactic (P Q : Prop) : P ∨ Q -> Q ∨ P := by
  intro h
  cases h with
  | inl hp =>
      right
      exact hp
  | inr hq =>
      left
      exact hq

The eliminator Or.elim corresponds to cases.

Intermediate Results

Term mode often uses let or nested functions.

theorem chain_term (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R :=
  fun hp => hqr (hpq hp)

Tactic mode uses have:

theorem chain_tactic (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R := by
  intro hp
  have hq : Q := hpq hp
  have hr : R := hqr hq
  exact hr

Both express the same data flow. Tactic mode names intermediate steps; term mode composes functions.

Rewriting

Term mode:

theorem rw_term (a b : Nat) (h : a = b) : a + 1 = b + 1 :=
  Eq.subst h rfl

Tactic mode:

theorem rw_tactic (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]

The tactic hides the underlying substitution term.

Function Extensionality

Term mode:

theorem fun_eq_term :
    (fun n : Nat => n + 0) = (fun n => n) :=
  funext (fun n => by simp)

Tactic mode:

theorem fun_eq_tactic :
    (fun n : Nat => n + 0) = (fun n => n) := by
  funext n
  simp

funext introduces an arbitrary input and reduces function equality to pointwise equality.

When to Use Term Mode

Use term mode when:

  • the proof is a single expression
  • the structure is clear from function composition
  • you want compact, compositional code
  • the proof resembles a direct computation

Example:

theorem const_term {α β : Type} (x : α) (y : β) : α :=
  x

When to Use Tactic Mode

Use tactic mode when:

  • the proof has many steps
  • you need case analysis or induction
  • intermediate results help readability
  • you want to inspect goals interactively

Example:

theorem and_comm_tactic (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left

Mixing Styles

You can mix styles within a single proof.

theorem mixed_example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  exact And.intro hp hq

Or use term fragments inside tactics:

theorem mixed_example2 (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  · exact hp
  · exact hq

Both are valid. Choose the style that keeps the proof readable.

Inspecting the Generated Term

Lean can show the term produced by a tactic proof.

#print id_tactic

This reveals the underlying lambda term. Reading such output helps connect tactic steps with term structure.

Common Pitfalls

If a tactic proof becomes long, consider rewriting it as a term or splitting it into lemmas.

If a term proof becomes unreadable, switch to tactic mode and name intermediate steps.

If a tactic hides too much detail, replace it with explicit terms or smaller tactics.

If a term uses complex nested lambdas, introduce local definitions or use tactic mode.

Recipe: Translate Between Styles

Start with a tactic proof:

theorem ex (P Q : Prop) (hp : P) (hq : Q) : Q ∧ P := by
  constructor
  · exact hq
  · exact hp

Translate to term mode:

theorem ex_term (P Q : Prop) (hp : P) (hq : Q) : Q ∧ P :=
  And.intro hq hp

Then compare with #check or #print.

This exercise builds intuition for both styles.

Takeaway

Term mode and tactic mode are two interfaces to the same underlying system. Term mode emphasizes direct construction and compositional clarity. Tactic mode emphasizes stepwise reasoning and local control. Effective Lean code uses both, choosing the style that best matches the structure of the argument.