Proving with auxiliary lemmas

By now your proofs chain a fair number of by steps. Real developments get bigger still — and the cure is the same one you’d reach for in any program: pull a self-contained piece out, give it a name, and reuse it. In Algae that piece is a lemma, and the payoff is direct:

Once a lemma’s qed checks, it becomes a fact — you invoke it by name with by, exactly like an axiom or an inference rule.

Its parameters become the arguments you pass; its goal becomes the conclusion it discharges. Because a proved lemma has nothing left to prove, applying it closes the goal outright — zero subgoals, just like an axiom.

A proof becomes a fact

Here’s a small helper — conjunction is commutative — and a second lemma that uses it:

import core(and_intro, and_left, and_right, implication_intro);

lemma and_comm(A B : Prop, both := A ∧ B)
  ⊢ B ∧ A;
proof
  by and_intro(B, A) cases
    case ⊢ B; by and_right(A, B) then ⊢ A ∧ B; by both; qed;
    case ⊢ A; by and_left(A, B) then ⊢ A ∧ B; by both; qed;
  qed;
qed;

lemma and_comm_imp(A B : Prop)
  ⊢ (A ∧ B) ⇒ (B ∧ A);
proof
  by implication_intro(A ∧ B, B ∧ A)
  then P := A ∧ B ⊢ B ∧ A;
  by and_comm(A, B, P);
qed;

Look at the last line. and_comm’s signature is (A B : Prop, both := A ∧ B), so invoking it takes three arguments: the two propositions A and B, and a proof of A ∧ B — here the hypothesis P that implication_intro just handed us. The lemma’s conclusion, B ∧ A, matches the goal, so by and_comm(A, B, P) finishes the branch on its own. A term parameter takes a term; a := parameter takes a proof; a proved lemma behaves like any other rule with zero premises.

Prove once, reuse forever

The real reason to factor a lemma out is that some facts are expensive to prove. The natural-number fact ∀ n. n + 0 = n needs a full induction (you met it in Induction and friends); it lives, already proved, in nat.alg as add_zero_right. You never want to redo that induction. Instead, import it and instantiate it at whatever point you need:

import nat;
import core(forall_elim);

lemma add_zero_at(a : Nat)
  ⊢ a + 0 = a;
proof
  by forall_elim(Nat, _ + 0 = _, a)
  then ⊢ ∀ (n : Nat) st n + 0 = n;
  by add_zero_right;
qed;

add_zero_right takes no arguments — it’s a closed universal fact — so by add_zero_right; discharges the ∀ goal directly, and forall_elim peels it down to the instance a + 0 = a. The whole stdlib is built this way: each module’s harder theorems lean on the simpler lemmas below them.

Note

Order doesn’t matter within a unit. The checker reads every declaration in the file before it checks any proof, so a lemma may cite one defined further down (or a mutually-useful pair may cite each other). Idiomatic style is still bottom-up — helpers first — because it reads like the dependency order.

Your turn

Disjunction is commutative too — and it’s already proved for you below as or_comm. Use it to prove that A ∨ B implies B ∨ A.

import core(or_elim, or_intro_left, or_intro_right, implication_intro);

lemma or_comm(A B : Prop, d := A ∨ B)
  ⊢ B ∨ A;
proof
  by or_elim(A, B, B ∨ A) cases
    case ⊢ A ∨ B; by d; qed;
    case P := A ⊢ B ∨ A; by or_intro_right(B, A) then ⊢ A; by P; qed;
    case Q := B ⊢ B ∨ A; by or_intro_left(B, A) then ⊢ B; by Q; qed;
  qed;
qed;

lemma or_comm_imp(A B : Prop)
  ⊢ (A ∨ B) ⇒ (B ∨ A);
proof
  by wip(?goal);
wip;

Hint

Mirror and_comm_imp. Start with by implication_intro(A ∨ B, B ∨ A), which leaves then P := A ∨ B ⊢ B ∨ A;. Now or_comm’s conclusion is exactly B ∨ A — feed it the two propositions and your hypothesis: by or_comm(A, B, P);.

That’s the whole trick. A lemma is a proof you get to name and a fact you get to reuse — the same duality that makes the standard library, and any development you build on top of it, scale.