Building proofs

One rule application is a single step. A proof is many of them fitted together, and it helps to picture how.

Proofs are dominoes

Think of the rules as pieces in a game of dominoes. Each piece has a top (its conclusion) and a bottom (its premises), and you can lay one piece against another only where they line up: a premise you still owe on one piece is answered by the conclusion of the next.

You start by laying down a piece whose top matches your goal. That piece may leave one open end (a single premise) that you extend with another piece, or it may branch into several open ends (several premises) — one for each subgoal. You keep laying pieces down each open end until every end is capped. And you cap an end with an axiom or an assumption — a piece with no bottom, nothing left to answer. When every branch is capped, the chain is complete and the proof closes.

That’s why the number of premises drives everything: a one-premise rule extends a single line (then), a many-premise rule forks it (cases), and a zero-premise fact caps the line it’s on.

Because each step hangs its subgoals beneath it and every branch ends in a cap, the finished structure is a tree: the goal at the root, rule applications for nodes, and axioms or assumptions for leaves. This is the proof tree, and it’s the thing the kernel actually checks. A proof written in Algae is just that tree, laid out in text.

A branching proof, end to end

Let’s prove that conjunction doesn’t care about order: from a proof of A ∧ B we build B ∧ A. This uses all three conjunction rules at once — a nice domino chain that forks and then caps each branch. We spell the rules out in the buffer instead of import-ing them, so you can see exactly what each by step is matching against:

rule and_intro(P Q : Prop)
  ⊢ P;
  ⊢ Q
  ────────────────────────
  ⊢ P ∧ Q
end;

rule and_left(P Q : Prop)
  ⊢ P ∧ Q
  ────────────────────────
  ⊢ P
end;

rule and_right(P Q : Prop)
  ⊢ P ∧ Q
  ────────────────────────
  ⊢ Q
end;

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;

Follow the dominoes:

  • The goal is ⊢ B ∧ A. Lay down and_intro — its conclusion P ∧ Q matches with P = B, Q = A, so by and_intro(B, A). It has two premises, so the line forks into ⊢ B and ⊢ A — hence cases.

  • Left branch, ``⊢ B``. Lay and_right (conclusion ⊢ Q, matched with Q = B). Its single premise is ⊢ A ∧ B, so we extend with then ⊢ A ∧ B; — and cap that end with our assumption, by both.

  • Right branch, ``⊢ A``. Symmetric: and_left (conclusion ⊢ P, with P = A) leaves ⊢ A ∧ B, capped again by both.

Both branches capped, both cases closed, qed. Notice how both := A ∧ B — the whole conjunction we were handed — caps both branches; it’s evidence we can cite as many times as we like.

Draw the same proof as a tree and its shape jumps out — the goal at the root, each by a node that hangs its subgoals below, and every leaf an assumption that caps its branch:

⊢ B ∧ A                              (the goal — root of the tree)
└─ by and_intro(B, A)                two premises → the tree forks
   ├─ ⊢ B
   │  └─ by and_right(A, B)          one premise
   │     └─ ⊢ A ∧ B
   │        └─ by both               leaf: assumption caps the branch
   └─ ⊢ A
      └─ by and_left(A, B)           one premise
         └─ ⊢ A ∧ B
            └─ by both               leaf: assumption caps the branch

Read top to bottom it’s the proof you wrote; read bottom to top it’s the logical argument — every branch climbs from the goal up to a fact you already hold. That tree is the proof; the proof … qed text is just one way of writing it down.

What the checker actually checks

The kernel (algae-kernel) is deliberately dim: it does not search for proofs, and it will not fill anything in for you. For every by step it performs exactly two checks:

  1. The rule fits the goal. It instantiates the rule’s conclusion with your arguments and confirms it matches the current goal. (and_intro(B, A) has conclusion B ∧ A — that had better be the goal.)

  2. You accounted for the premises. It instantiates the rule’s premises the same way and confirms the subgoals you continue with — your then goal, or your case goals — are exactly those premises. (and_intro(B, A) demands premises ⊢ B and ⊢ A; your two cases must be precisely those.)

Get either wrong and the step is rejected, pointing at the mismatch. There is no third, hidden step where the checker “runs” anything or guesses — a proof is correct only when every domino lines up under those two checks, all the way down.

Everything is explicit — on purpose

Unlike Lean 4 or Rocq (Coq), Algae keeps all the proof information in the syntax, and that was a deliberate design decision. Rocq, for example, drives proofs with a macro/tactic language that generates proof terms — which enables proof search, automation, and a great deal of power. That power comes at two costs: it is harder to learn, and you cannot read the proof off the source. (Rocq can print the underlying term, but it was never meant to be read.) Algae is built on two principles instead: be simple, and be explicit — the context, the goal, and the rule being applied are all deliberately required in the syntax, right where you can see them.

Why so strict?

Because a checker that guesses is a checker you can’t trust. Every gap is one you must close explicitly, which is exactly what makes a passing proof mean something. When you don’t know the next piece, that’s what holes are for — drop a by wip(?goal), check, and let the kernel tell you the open end it’s still waiting on.

Your turn

Disjunction has the mirror shape: or_intro_left proves A ∨ B from just A — a single premise, so then. Given a proof of A, prove A ∨ B. The buffer inspects the step with a trailing ?; Check ▶ to see what it leaves.

rule or_intro_left(P Q : Prop)
  ⊢ P
  ────────────────────────
  ⊢ P ∨ Q
end;

lemma weaken(A B : Prop, x := A)
  ⊢ A ∨ B;
proof
  by or_intro_left(A, B)?;
wip;

Hint

or_intro_left(A, B) matches ⊢ A ∨ B and leaves the one premise ⊢ A. Drop the ?, continue then ⊢ A;, close by x;, and make the terminator qed.