Let's Learn Lean : Tactics

17 Dec, 2025

Welcome back to the sixth installment of our series porting Software Foundations to Lean 4.

In the previous article, Polymorphism and Higher-Order Functions, we unlocked more expressive programming patterns in Lean.

So far, we’ve been getting by with a small set of tactics: rfl, simp, rw, …

In this article, we are going to learn the essential tactics that bridge the gap:

1. The apply Tactic: Reasoning backward.
2. Injection and Discriminate: Handling constructors.
3. Symmetry and Transitivity: Working with equality without the standard library tactics.
4. Congruence: Proving functions equal.
5. Varying the Induction Hypothesis: Generalized induction.

Let's dive in.

1. The apply Tactic

We often encounter situations where the goal we are trying to prove matches the conclusion of a hypothesis.

In Coq, the apply tactic is the go-to tool for this. In Lean 4, we also use apply.

Basic Application and Backward Reasoning

If we have a hypothesis h : n = m and our goal is n = m, we can simply apply it:

theorem silly1 : forall (n m : Nat), n = m -> n = m := by
  intro n m eq
  apply eq

However, apply is much more useful when we reason backwards. If we have an implication eq2 : n = m -> [n,o] = [m,p], it tells us:

"If you can prove n = m, then I can give you a proof of [n,o] = [m,p]."

When our goal is the conclusion ([n,o] = [m,p]), using apply transforms the goal into the premise (n = m).

theorem silly2 : forall (n m o p : Nat),
  n = m -> (n = m -> [n,o] = [m,p]) -> [n,o] = [m,p] := by
  intro n m o p eq1 eq2
  apply eq2
  apply eq1

What happens here:

1. Our goal was [n, o] = [m, p].
2. apply eq2 matched the goal with the right side of eq2.
3. It replaced the goal with the required input for eq2, which is n = m.
4. We solved that new goal with apply eq1.

Applying with Hypotheses

We can also use apply with conditional hypotheses involving nested implications. In the following example, eq2 demands a proof that q = r implies [q] = [r].

theorem silly2a : forall (n m : Nat),
  (n,n) = (m,m) ->
  (forall (q r : Nat), (q,q) = (r,r) -> [q] = [r]) ->
  [n] = [m] := by
  intro n m eq1 eq2
  apply eq2
  apply eq1

2. Injection and Discriminate

Recall from Basics that inductive constructors (like succ or ::) have two special properties:

1. Injectivity: If succ n = succ m, then n = m.
2. Disjointness: succ n can never equal 0.

In Coq, we rely on two specific tactics, injection and discriminate, to handle these cases.

In Lean 4, we can actually handle both of these using the powerful cases tactic.

Injection (The cases upgrade)

When we have an equality between two identical constructors, like succ n = succ m, we want to "peel off" the constructors to get to the variables inside.

In Lean, using cases on such a hypothesis performs this peeling automatically.

theorem S_injective' : forall (n m : Nat),
  Nat.succ n = Nat.succ m ->
  n = m := by
  intro n m h
  cases h
  rfl

If we have a more complex structure, like lists, cases works exactly the same way. It matches the corresponding head and tail of the list.

theorem injection_ex1 : forall (n m o : Nat),
  [n, m] = [o, o] ->
  n = m := by
  intro n m o h
  cases h
  rfl

For slightly deeper structures, we might need to case split multiple times to extract every equality.

theorem injection_ex3 :
  forall (X : Type) (x y z : X) (l j : List X),
    x :: y :: l = z :: j ->
    j = z :: l ->
    x = y := by
  intro X x y z l j h hj
  cases h
  -- now z := x and j := y :: l
  -- hj : y :: l = x :: l
  cases hj
  rfl

Discriminate

The discriminate tactic in Coq is used to prove that two different constructors (like true and false, or succ and zero) cannot be equal. If a hypothesis claims they are equal, it's a contradiction.

In Lean 4, cases handles this too! If you try to case split on an equality like succ n = 0, Lean realizes there are no matching constructors and immediately solves the goal (technically using nomatch or contradiction).

theorem discriminate_ex1 : forall (n m : Nat),
  (false = true) ->
  n = m := by
  intro n m h
  cases h

Here is another example with natural numbers. Since succ n can never be 0, the hypothesis h is false, and the goal is solved instantly.

theorem discriminate_ex2 : forall (n : Nat),
  Nat.succ n = 0 ->
  2 + 2 = 5 := by
  intro n h
  cases h

3. Symmetry and Transitivity

In standard Coq, symmetry and transitivity are tactics available in the global namespace.

In Lean 4, these are often part of the Mathlib library. Since we are sticking to Core Lean to understand the basics, we will use the underlying properties of equality directly: Eq.symm and Eq.trans.

Transitivity

Transitivity tells us that if a = b and b = c, then a = c. We can apply the theorem Eq.trans to chain these equalities together.

theorem trans_eq_exercise : forall (n m o p : Nat),
  m = minustwo o ->
  (n + p) = m ->
  (n + p) = minustwo o := by
  intro n m o p h hm
  apply Eq.trans hm h

We can also wrap this in our own theorem if we want to mimic the Coq style of providing arguments explicitly.

theorem trans_eq : forall (X : Type) (x y z : X),
  x = y -> y = z -> x = z := by
  intro X x y z h1 h2
  rw [h1]
  exact h2

theorem trans_eq_example' : forall (a b c d e f : Nat),
  [a, b] = [c, d] ->
  [c, d] = [e, f] ->
  [a, b] = [e, f] := by
  intro a b c d e f h1 h2
  apply trans_eq (y := [c, d])
  exact h1
  exact h2

4. Congruence (f_equal)

A fundamental property of functions is that if x = y, then f x = f y. In Coq, the f_equal tactic is used to strip away the function f to prove the arguments are equal (or conversely, to add f to both sides).

In Lean, we can often just use rw to replace x with y. However, we can also define f_equal ourselves to see how it works under the hood.

theorem f_equal :
  forall {A B : Type} (f : A -> B) (x y : A),
    x = y -> f x = f y := by
  intro A B f x y h
  rw [h]
  rfl

Now we can use this theorem to prove that if n = m, then succ n = succ m.

theorem eq_implies_succ_equal : forall (n m : Nat),
  n = m -> Nat.succ n = Nat.succ m := by
  intro n m h
  apply f_equal
  exact h

Alternatively, Lean provides a congr tactic (and congrArg theorem) that automates this congruence reasoning.

theorem eq_implies_succ_equal' : forall (n m : Nat),
  n = m -> Nat.succ n = Nat.succ m := by
  intro n m h
  exact congrArg Nat.succ h

5. Varying the Induction Hypothesis

Sometimes, the variable you are inducting on appears in the goal or hypotheses in a way that makes the Induction Hypothesis (IH) too specific to be useful.

In Coq, we use the generalize dependent tactic to pull a variable back into the "forall" quantifier of the goal before starting induction.

In Lean 4, the induction tactic has a built-in generalizing keyword that makes this much cleaner.

The Problem

Consider double_injective. If we introduce both n and m into the context and then perform induction on n, our IH will say: "If double n' = double m, then n' = m." Notice that m is fixed.

When we reach the inductive step, we might need the IH to hold for m', but our IH is stuck on m.

The Lean Solution

We use induction n generalizing m. This tells Lean: "I am doing induction on n, but please keep m general in the induction hypothesis."

theorem double_injective_take2 : forall n m, double n = double m -> n = m := by
  intro n m h
  -- generalizing m replaces "generalize dependent m"
  induction n generalizing m with
  | zero =>
    cases m
    · rfl
    · contradiction
  | succ n' ih =>
    cases m with
    | zero => contradiction
    | succ m' =>
      -- 1. Force unfold (double (succ x) -> succ (succ ...))
      dsimp [double] at h
      -- 2. Peel constructors
      injection h with h
      injection h with h
      -- 3. Apply IH directly
      -- Since we used "generalizing m", 'ih' works for 'm'', not just 'm'
      specialize ih m' h
      rw [ih]

Concluding and Moving Ahead

We now have a robust set of tools to manipulate proofs like apply,exact, cases, generalizing etc. Let's put a stop to this article here. You can find all the source code in this repo.

In the next article, we will enter the world of Logic and learn how to define propositions, conjunctions, and logical connectives in Lean.

See you there!

Main Reference : Software Foundations