Let's Learn Lean : Basics-II

03 Dec, 2025

The first chapter of Software Foundations is pretty intense and contains a lot of stuff. Therefore, to keep things digestible, I decided to split the explanation in two parts.

In the first part we learnt about defining Data Types, Tuples, Natural Numbers, writing functions using pattern matching, and verified simple equalities using the rfl tactic.

This part will be a continuation to the previous information and we are going to learn Proof by Simplification(simp), Proof by Rewriting(rw) and Proof by Case Analysis(cases) .

But before all that, I just wanna explain a small topic about how Lean handles recursion differently from Coq.

Fixpoint vs def

If anyone has tried writing Coq, they would notice that we only have def in Lean as compared to Definition and Fixpoint in Coq.

In Coq, we define any recursive function using the Fixpoint keyword which basically tells Coq to keep a check on the function as it is calling itself and make sure it terminates. Coq uses Structural Recursion. It means that one of the arguments must get syntactically smaller in every recursive call (e.g., n becomes n-1). If Coq can't "see" the argument shrinking, it rejects the function.

(* Coq *)
Fixpoint even (n:nat) : bool := ...

In Lean 4, we simply use def. Why ? Because Lean uses Well-Founded Recursion. When you define a function, Lean first checks for structural recursion. If that fails, it does not immediately reject the code. Instead, it attempts to find a well-founded relation (a "measure" like the size of an argument) and prove termination automatically. And even after this, if Lean cannot figure out, we can use termination_by to provide a proof of termination manually.

-- Lean
def even (n : Nat) : Bool := ...

Perfect, now we move ahead with our normal flow.

Proof by Simplification

In Basics-I, we used example to claim that a function behaves a certain way on specific inputs.

example : nextWorkingDay (nextWorkingDay Day.saturday) = Day.tuesday := by
  rfl

The proof was simply rfl (reflexivity). This tactic checks if both sides of the equation are definitionally equal—meaning, if we run the computation on both sides, do they result in the exact same value?

Universal Properties

0 is a "neutral element" for addition on the right. This means n + 0 = n for every natural number n.

In logical terms, we use the Universal Quantifier (∀ : forall).

theorem plus_n_0 : forall n : Nat, n + 0 = n := by
  intro n
  rfl

There is a fundamental difference in how addition is defined in Lean as compared to Coq.

The add function is Coq is :

Fixpoint add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m        (* Base case: if 1st arg is 0, return 2nd arg *)
  | S p => S (add p m)
  end.

But in Lean, the recursion happens on the 2nd argument :

def add (n k : Nat) : Nat :=
  match k with
  | 0 => n        (* Base case: if 2nd arg is 0, return 1st arg *)
  | succ k' => succ (add n k')

So, therefore the theorem plus_n_0 i.e. n+0=n in Lean would translate to theorem plus_0_n in Coq i.e. 0+n=n.

What about the case 0+n=n in Lean ? We will discuss how this works later, as the proof for this requires much more knowledge that just a simple rfl.

You can also use simp if the step just requires simplification, but we will mostly focus on using rfl.

theorem plus_n_0' : forall n : Nat, n + 0 = n := by
  intro n
  simp
-- This works as well

We can prove similar theorems with the same pattern :

theorem plus_r_1 : forall n : Nat, n + 1 = Nat.succ n := by
  intro n
  rfl

theorem mult_r_0 : forall n : Nat, n*0=0 := by
  intro n
  rfl

The r prefix in the names of these theorems is pronounced on the right.

Proof by Rewriting

Let's take a look at the following theorem :

theorem plus_id_example : forall n m : Nat,
  n = m -> n + n = m + m

Here we are not making any universal claim. But instead, this theorem holds iff n=m. The -> is pronounced implies.

As we did earlier, we use intro n m assuming we are given such numbers n and m. We also need to assume the hypothesis n=m. The intro tactic will serve to move these from the goal into assumptions in the current context.

Since n and m are arbitrary numbers, we can't just use simplification (rfl) to prove this theorem. Instead, we prove it by observing that, if we are assuming n = m, then we can replace n with m in the goal statement and obtain an equality with the same expression on both sides. The tactic that tells Lean to perform this replacement is called rw (short for rewrite).

theorem plus_id_example : forall n m : Nat,
  n = m -> n + n = m + m := by
  intro n m
  intro h
  rw [h]

The first line of the proof moves the universally quantified variables n and m into the context. The second moves the hypothesis n = m into the context and gives it the name h. The third tells Lean to rewrite the current goal (n + n = m + m) by replacing the left side of the equality hypothesis h with the right side.

Note on Direction: By default, rw [h] rewrites from left to right (replacing n with m). To rewrite from right to left (replacing m with n), you use the left-arrow symbol inside the brackets: rw [← h].

The #check command that we learnt earlier can also be used to examine the statements of previously declared lemmas and theorems. The two examples below are lemmas about multiplication that are proved in the standard library. ( We will prove them in the next blog.)

#check Nat.zero_mul
-- Nat.zero_mul (n : Nat) : 0 * n = 0
#check Nat.mul_succ
-- Nat.mul_succ (n m : Nat) : n * m.succ = n * m + n

We can use rw tactic with previously proved theorem instead of hypothesis from the context.

theorem mult_0_p_0_q : forall p q : Nat,
  0*p + 0*q = 0 := by
  intro p q
  rw[Nat.zero_mul]
  rw[Nat.zero_mul]

Proof by Case Analysis

Not everything can be proven by simple calculation (rfl) or rewriting (rw). Often, unknown values block computation because their definition depends on which "shape" the value takes. To proceed, we must split the proof into separate cases for each possible shape.

In Lean, the primary tools for this are the cases tactic and pattern matching via match.

cases

The cases tactic splits an inductive variable (like a natural number or boolean) into its constructors.

Example: Boolean Negation

Consider proving that boolean negation is its own inverse: !(!b) = b.

We cannot prove this directly because b is unknown. We must consider the cases where b is true and where b is false.

theorem negb_involutive (b : Bool) : !(!b) = b := by
  cases b with
  | true => rfl
  | false =>  rfl

Key syntax:

cases b: Tells Lean to destruct the variable b.
with: Begins the structured case block.
| constructor =>: Defines the proof for a specific constructor (e.g., true or false).

Handling Variables in Cases

When splitting types like Nat (natural numbers), some constructors carry data (like succ n). You can name these variables in the case line.

theorem plus_1_neq_0 (n : Nat) : ((n + 1) == 0) = false := by
  cases n with
  | zero => rfl
  | succ n' => rfl

Note: cases is sufficient here because simp and rfl might get stuck on n, but once n is split into zero or succ n', the definition of + and == can proceed.

match

In some proofs, you need to destruct multiple variables. Using nested cases blocks works but leads to deep indentation and poor readability. The idiomatic Lean solution is to use match, which allows you to pattern match on multiple variables at once.

Example: Commutativity of AND

Prove that b && c = c && b.

Bad Style (Nested Cases):

theorem andb_commutative_bad (b c : Bool) : (b && c) = (c && b) := by
  cases b with
  | true =>
      cases c with
      | true => rfl
      | false => rfl
  | false =>
      cases c with
      | true => rfl
      | false => rfl

Good Style (Pattern Matching):

theorem andb_commutative (b c : Bool) : (b && c) = (c && b) := by
  match b, c with
  | true, true   => rfl
  | true, false  => rfl
  | false, true  => rfl
  | false, false => rfl

This "truth table" style is concise, readable, and essentially standard functional programming syntax used within a proof.

Remembering Assumptions (`eqn:` equivalent)

Sometimes simply splitting a variable isn't enough; you need to remember what the variable was in the context of the proof.

To do this, we use the cases h : x syntax. This creates a hypothesis h asserting that x equals the current constructor.

def isZero (n : Nat) : Bool :=
  match n with
  | 0   => true
  | _   => false

theorem check_isZero (n : Nat) :
    isZero n = true → n = 0 := by
  intro h_eq
  cases h_n : n with
  | zero => simp
  | succ n' => rw [h_n] at h_eq
               simp [isZero] at h_eq

Conclusion and Moving Forward...

So this was all about the Basics of Software Foundations, which we have actually been able to learn in Lean. We are gonna stop here. You can find all the source code in this repo. The code for this particular article can be found in the Basics2.lean file. Do give a try to the exercises in the file as well.

In the next article, we focus on learning Proof by Induction which will be a highly used method throughout our journey. See you there !

Main Reference : Software Foundations