# 1.19 Term Mode vs Tactic Mode

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:

```lean id="a1xk8h"
theorem id_term (P : Prop) : P -> P :=
  fun h => h
```

Tactic mode:

```lean id="k9y3ps"
theorem id_tactic (P : Prop) : P -> P := by
  intro h
  exact h
```

Both have the same type:

```lean id="q4v7mn"
#check id_term
#check id_tactic
```

## Reading Tactic Proofs as Terms

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

```lean id="j7t2ra"
theorem mp_tactic (P Q : Prop) (hp : P) (hpq : P -> Q) : Q := by
  exact hpq hp
```

Term version:

```lean id="v3c9zq"
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:

```lean id="n2m4uf"
theorem and_intro_term (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
  And.intro hp hq
```

Tactic mode:

```lean id="z8s0dw"
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:

```lean id="e6qk2h"
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:

```lean id="t9w5mx"
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.

```lean id="k3d1pb"
theorem chain_term (P Q R : Prop)
    (hpq : P -> Q) (hqr : Q -> R) : P -> R :=
  fun hp => hqr (hpq hp)
```

Tactic mode uses `have`:

```lean id="y1o6fw"
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:

```lean id="d8u2ne"
theorem rw_term (a b : Nat) (h : a = b) : a + 1 = b + 1 :=
  Eq.subst h rfl
```

Tactic mode:

```lean id="p4z7ys"
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:

```lean id="b6c0xn"
theorem fun_eq_term :
    (fun n : Nat => n + 0) = (fun n => n) :=
  funext (fun n => by simp)
```

Tactic mode:

```lean id="s9q2le"
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:

```lean id="x5n8dw"
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:

```lean id="u3m4qk"
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.

```lean id="r2k1sh"
theorem mixed_example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  exact And.intro hp hq
```

Or use term fragments inside tactics:

```lean id="g8w3py"
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.

```lean id="x8j5az"
#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:

```lean id="p7m6qd"
theorem ex (P Q : Prop) (hp : P) (hq : Q) : Q ∧ P := by
  constructor
  · exact hq
  · exact hp
```

Translate to term mode:

```lean id="c4t8wj"
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.