Proof techniques crash course

Every proof you’ll ever write is some mix of a small number of standard moves. This chapter is a fast reference: each section names a classic technique, says how it maps onto an Algae rule, and then hands you three exercises to drill it.

Each exercise is a live editor seeded with a hole. Press Check ▶ to see the open goal, click the hole (or press Ctrl-Space) for suggestions, and read the hint if you’re stuck. Everything here uses only core — the rules you met in Inference rules, Reasoning backward, and the tour (The logical toolkit, Quantifiers and ⇔).

Here’s one worked all the way through, so you know what a finished answer looks like — the and-introduction from Reasoning backward:

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

lemma both(A B : Prop, x := A, y := B)
  ⊢ A ∧ B;
proof
  by and_intro(A, B) cases
    case x := A, y := B ⊢ A; by x; qed;
    case x := A, y := B ⊢ B; by y; qed;
  qed;
qed;

Note the shape of each case: it restates the hypotheses it inherits (x := A, y := B) before its ⊢. Every case and every then states its context in full — Algae does no implicit weakening, so an assumption you don’t carry forward is one you discarded. Expect to write your lemma parameters out again in each branch of the exercises below.

Now the techniques.

1. Direct proof

Goal: prove P. Method: apply a rule whose conclusion matches P, then discharge whatever it leaves from your assumptions. A premise-free step (an axiom or an assumption by h) closes a goal outright.

Exercises

1a. From a proof of A, build A ∨ B (the left injection).

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

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

Hint

or_intro_left(A, B) proves A ∨ B from ⊢ A — one premise, so then x := A ⊢ A;, closed by x.

1b. Same, but the right injection: from a proof of B, build A ∨ B.

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

lemma inject_right(A B : Prop, y := B)
  ⊢ A ∨ B;
proof
  by wip(?goal);
wip;

Hint

or_intro_right(A, B) proves A ∨ B from ⊢ B. then y := B ⊢ B; then by y.

1c. Take a conjunction apart: from a proof of A ∧ B, get A.

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

lemma take_left(A B : Prop, h := A ∧ B)
  ⊢ A;
proof
  by wip(?goal);
wip;

Hint

and_left(A, B) concludes ⊢ A from its one premise ⊢ A ∧ B. then h := A ∧ B ⊢ A ∧ B; and close by h.

2. Conditional proof (implication)

Goal: prove P ⇒ Q. Method: assume P, then prove Q. implication_intro does exactly this — it introduces the antecedent as a named hypothesis after its premise P := P ⊢ Q.

Exercises

2a. Prove the identity implication A ⇒ A.

rule implication_intro(P Q : Prop)
  P := P ⊢ Q
  ────────────────────────
  ⊢ P ⇒ Q
end;

lemma id(A : Prop)
  ⊢ A ⇒ A;
proof
  by wip(?goal);
wip;

Hint

by implication_intro(A, A) then P := A ⊢ A; leaves you assuming P : A and proving A — close it by P.

2b. If you already hold a proof of B, then A ⇒ B for any A.

rule implication_intro(P Q : Prop)
  P := P ⊢ Q
  ────────────────────────
  ⊢ P ⇒ Q
end;

lemma const_imp(A B : Prop, q := B)
  ⊢ A ⇒ B;
proof
  by wip(?goal);
wip;

Hint

implication_intro(A, B) then q := B, P := A ⊢ B; — ignore P and close by q.

2c. Prove (A ∧ B) ⇒ A — assume the conjunction, then project.

rule implication_intro(P Q : Prop)
  P := P ⊢ Q
  ────────────────────────
  ⊢ P ⇒ Q
end;

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

lemma proj(A B : Prop)
  ⊢ (A ∧ B) ⇒ A;
proof
  by wip(?goal);
wip;

Hint

implication_intro(A ∧ B, A) then P := A ∧ B ⊢ A; then by and_left(A, B) then P := A ∧ B ⊢ A ∧ B; by P;.

3. Proof by cases

Goal: prove P. Method: split into all possible cases and prove P in each. When the “all possible cases” is a disjunction A ∨ B you have, or_elim is the tool: it gives you two branches, one assuming A and one assuming B, both aiming at the same goal.

Exercises

3a. Disjunction commutes: from A ∨ B, prove B ∨ A.

rule or_elim(P Q R : Prop)
  ⊢ P ∨ Q;
  P := P ⊢ R;
  Q := Q ⊢ R
  ────────────────────────
  ⊢ R
end;

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

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

lemma or_comm(A B : Prop, d := A ∨ B)
  ⊢ B ∨ A;
proof
  by wip(?goal);
wip;

Hint

by or_elim(A, B, B ∨ A) cases gives three goals: re-prove A ∨ B (by d), then a branch P := A (build B ∨ A with or_intro_right) and a branch Q := B (with or_intro_left).

3b. A trivial-looking but instructive one: from A ∨ A, prove A.

rule or_elim(P Q R : Prop)
  ⊢ P ∨ Q;
  P := P ⊢ R;
  Q := Q ⊢ R
  ────────────────────────
  ⊢ R
end;

lemma idem(A : Prop, d := A ∨ A)
  ⊢ A;
proof
  by wip(?goal);
wip;

Hint

or_elim(A, A, A) cases — feed d for the disjunction, and each branch hands you an assumption of A to close with.

3c. The constructive dilemma: from A ∨ B, A ⇒ C and B ⇒ C, conclude C.

rule or_elim(P Q R : Prop)
  ⊢ P ∨ Q;
  P := P ⊢ R;
  Q := Q ⊢ R
  ────────────────────────
  ⊢ R
end;

rule implication_elim(P Q : Prop)
  ⊢ P ⇒ Q;
  ⊢ P
  ────────────────────────
  ⊢ Q
end;

lemma dilemma(A B C : Prop, d := A ∨ B, f := A ⇒ C, g := B ⇒ C)
  ⊢ C;
proof
  by wip(?goal);
wip;

Hint

or_elim(A, B, C) cases. In the P := A branch run implication_elim(A, C) against f and P; symmetrically use g and Q in the Q := B branch.

4. Proof by contradiction

Goal: prove ¬P. Method: assume P, and derive absurdity (False). That’s negation_intro — it assumes P and asks you to reach False. Two more tools travel with it: negation_elim turns a proof of P and ¬P into False, and false_elim turns False into anything at all (the principle of explosion).

Algae’s logic is intuitionistic

Classic “proof by contradiction” sometimes means proving a positive P by assuming ¬P and deriving False. That step needs the law of excluded middle, which core deliberately does not ship — so here contradiction proves negations (¬P), and explosion carries a contradiction to any goal. (This is also why the next section has no exercises.)

Exercises

5a. From A ⇒ False, prove ¬A.

rule negation_intro(P : Prop)
  P := P ⊢ False
  ────────────────────────
  ⊢ ¬P
end;

rule implication_elim(P Q : Prop)
  ⊢ P ⇒ Q;
  ⊢ P
  ────────────────────────
  ⊢ Q
end;

lemma neg_from_imp(A : Prop, f := A ⇒ False)
  ⊢ ¬A;
proof
  by wip(?goal);
wip;

Hint

negation_intro(A) then f := A ⇒ False, P := A ⊢ False; then run implication_elim(A, False) against f and P.

5b. Explosion: from a proof of A and a proof of ¬A, prove any C.

rule false_elim(P : Prop)
  ⊢ False
  ────────────────────────
  ⊢ P
end;

rule negation_elim(P : Prop)
  ⊢ P;
  ⊢ ¬P
  ────────────────────────
  ⊢ False
end;

lemma explode(A C : Prop, x := A, nx := ¬A)
  ⊢ C;
proof
  by wip(?goal);
wip;

Hint

false_elim(C) then x := A, nx := ¬A ⊢ False; reduces the goal to False, which negation_elim(A) produces from x and nx (two cases).

5c. Prove ¬¬A from A.

rule negation_intro(P : Prop)
  P := P ⊢ False
  ────────────────────────
  ⊢ ¬P
end;

rule negation_elim(P : Prop)
  ⊢ P;
  ⊢ ¬P
  ────────────────────────
  ⊢ False
end;

lemma dni(A : Prop, x := A)
  ⊢ ¬(¬A);
proof
  by wip(?goal);
wip;

Hint

negation_intro(¬A) then x := A, P := ¬A ⊢ False; — now you hold P : ¬A and x : A, a contradiction, so negation_elim(A) gives False.

5. Proof by contrapositive

Goal: prove P ⇒ Q. Method: prove ¬Q ⇒ ¬P instead. core provides this as the contrapositive rule: it takes your goal P ⇒ Q down to the single premise ¬Q ⇒ ¬P.

This one is classical

Unlike everything else in this chapter, contrapositive is a classical principle — turning ¬Q ⇒ ¬P back into P ⇒ Q rests on the law of excluded middle. core ships it as a primitive rule so the technique is available; the rest of the logic stays intuitionistic.

Exercises

6a. From ¬B ⇒ ¬A, prove A ⇒ B.

rule contrapositive(P Q : Prop)
  ⊢ ¬Q ⇒ ¬P
  ────────────────────────
  ⊢ P ⇒ Q
end;

lemma contra_direct(A B : Prop, nn := ¬B ⇒ ¬A)
  ⊢ A ⇒ B;
proof
  by wip(?goal);
wip;

Hint

by contrapositive(A, B) then nn := ¬B ⇒ ¬A ⊢ ¬B ⇒ ¬A; by nn; — the rule turns the goal straight into the hypothesis you hold.

6b. The mirror: from ¬A ⇒ ¬B, prove B ⇒ A.

rule contrapositive(P Q : Prop)
  ⊢ ¬Q ⇒ ¬P
  ────────────────────────
  ⊢ P ⇒ Q
end;

lemma contra_swap(A B : Prop, nn := ¬A ⇒ ¬B)
  ⊢ B ⇒ A;
proof
  by wip(?goal);
wip;

Hint

by contrapositive(B, A) then nn := ¬A ⇒ ¬B ⊢ ¬A ⇒ ¬B; by nn; — mind the order: the goal is B ⇒ A, so P = B and Q = A.

6c. Prove A ⇒ A the long way round — via its contrapositive.

rule contrapositive(P Q : Prop)
  ⊢ ¬Q ⇒ ¬P
  ────────────────────────
  ⊢ P ⇒ Q
end;

rule implication_intro(P Q : Prop)
  P := P ⊢ Q
  ────────────────────────
  ⊢ P ⇒ Q
end;

lemma contra_id(A : Prop)
  ⊢ A ⇒ A;
proof
  by wip(?goal);
wip;

Hint

contrapositive(A, A) leaves ⊢ ¬A ⇒ ¬A — an identity implication you close with implication_intro(¬A, ¬A) then P := ¬A ⊢ ¬A; by P;.

6. Universal proof

Goal: prove ∀ x. P(x). Method: let x be arbitrary (a fresh eigenvariable), then prove P(x). forall_intro hands you that fresh x in its single premise; because x was arbitrary, proving P(x) proves it for all.

Exercises

7a. Everything equals itself: prove ∀ x. x = x.

rule forall_intro(T : Sort, P : T → Prop)
  x : T ⊢ P(x)
  ────────────────────────
  ⊢ ∀ (x : T) st P(x)
end;

axiom refl(T : Sort, x : T)  ⊢ x = x;

sort T : Sort;

lemma refl_all
  ⊢ ∀ (x : T) st x = x;
proof
  by wip(?goal);
wip;

Hint

forall_intro(T, _ = _) then x : T ⊢ x = x; carries a fresh x in; close by refl(T, x).

7b. Instantiate a universal: from ∀ y. P(y) and a point a, get P(a).

rule forall_elim(T : Sort, P : T → Prop, x : T)
  ⊢ ∀ (y : T) st P(y)
  ────────────────────────
  ⊢ P(x)
end;

sort T : Sort;

lemma at_point(P : T → Prop, a : T, all := ∀ (y : T) st P(y))
  ⊢ P(a);
proof
  by wip(?goal);
wip;

Hint

forall_elim(T, P, a), then restate all in the continuation — then all := ∀ (y : T) st P(y) ⊢ ∀ (y : T) st P(y); — and close by all.

7c. From ∀ x. P(x) and ∀ x. Q(x), prove ∀ x. P(x) ∧ Q(x).

rule forall_intro(T : Sort, P : T → Prop)
  x : T ⊢ P(x)
  ────────────────────────
  ⊢ ∀ (x : T) st P(x)
end;

rule forall_elim(T : Sort, P : T → Prop, x : T)
  ⊢ ∀ (y : T) st P(y)
  ────────────────────────
  ⊢ P(x)
end;

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

sort T : Sort;

lemma forall_and(P Q : T → Prop, hp := ∀ (x : T) st P(x), hq := ∀ (x : T) st Q(x))
  ⊢ ∀ (x : T) st P(x) ∧ Q(x);
proof
  by wip(?goal);
wip;

Hint

forall_intro for a fresh x, then and_intro(P(x), Q(x)); get each half by forall_elim on hp / hq at x.

7. Existential proof (a witness)

Goal: prove ∃ x. P(x). Method: supply a specific witness a and prove P(a). exists_intro takes the witness as an argument and leaves you the single goal P(a).

Exercises

8a. From a proof of P(a), conclude ∃ x. P(x).

rule exists_intro(T : Sort, P : T → Prop, x : T)
  ⊢ P(x)
  ────────────────────────
  ⊢ ∃ (x : T) st P(x)
end;

sort T : Sort;

lemma witnessed(P : T → Prop, a : T, pa := P(a))
  ⊢ ∃ (x : T) st P(x);
proof
  by wip(?goal);
wip;

Hint

exists_intro(T, P, a) then pa := P(a) ⊢ P(a); by pa; — you offered a as the witness, so the leftover goal is P at a.

8b. Something exists that equals a: prove ∃ x. x = a.

rule exists_intro(T : Sort, P : T → Prop, x : T)
  ⊢ P(x)
  ────────────────────────
  ⊢ ∃ (x : T) st P(x)
end;

axiom refl(T : Sort, x : T)  ⊢ x = x;

sort T : Sort;

lemma exists_eq(a : T)
  ⊢ ∃ (x : T) st x = a;
proof
  by wip(?goal);
wip;

Hint

Use a itself as the witness: exists_intro(T, λ (z : T) st z = a, a) then ⊢ a = a; and close by refl(T, a).

8c. Every element is some self-equal thing: prove ∃ z. z = z.

rule exists_intro(T : Sort, P : T → Prop, x : T)
  ⊢ P(x)
  ────────────────────────
  ⊢ ∃ (x : T) st P(x)
end;

axiom refl(T : Sort, x : T)  ⊢ x = x;

sort T : Sort;

lemma exists_self(a : T)
  ⊢ ∃ (z : T) st z = z;
proof
  by wip(?goal);
wip;

Hint

Witness with a: exists_intro(T, λ (z : T) st z = z, a) then ⊢ a = a; then by refl(T, a).

8. Existential elimination (use a witness)

Goal: conclude Q given ∃ x. P(x). Method: introduce a fresh witness a with P(a) in hand, and finish the proof using it — but Q must not mention a, since you don’t get to know which witness you were handed. exists_elim gives you that fresh x and the hypothesis witness := P(x).

Exercises

9a. Unpack and immediately repack: from ∃ x. P(x), prove ∃ x. P(x).

rule exists_intro(T : Sort, P : T → Prop, x : T)
  ⊢ P(x)
  ────────────────────────
  ⊢ ∃ (x : T) st P(x)
end;

rule exists_elim(T : Sort, P : T → Prop, Q : Prop)
  ⊢ ∃ (x : T) st P(x);
  x : T, witness := P(x) ⊢ Q
  ────────────────────────
  ⊢ Q
end;

sort T : Sort;

lemma repack(P : T → Prop, ex := ∃ (x : T) st P(x))
  ⊢ ∃ (x : T) st P(x);
proof
  by wip(?goal);
wip;

Hint

exists_elim(T, P, ∃ (x : T) st P(x)) cases — feed ex for the existential, then in the witness branch (context ex := ∃ (x : T) st P(x), x : T, witness := P(x)) rebuild with exists_intro(T, P, x), carrying that same context into the then and closing by witness.

9b. Flip an existential equation: from ∃ x. x = a, prove ∃ y. a = y.

rule exists_intro(T : Sort, P : T → Prop, x : T)
  ⊢ P(x)
  ────────────────────────
  ⊢ ∃ (x : T) st P(x)
end;

rule exists_elim(T : Sort, P : T → Prop, Q : Prop)
  ⊢ ∃ (x : T) st P(x);
  x : T, witness := P(x) ⊢ Q
  ────────────────────────
  ⊢ Q
end;

rule symmetry(T : Sort, x y : T)
  ⊢ x = y
  ────────────────────────
  ⊢ y = x
end;

sort T : Sort;

lemma exists_flip(a : T, ex := ∃ (x : T) st x = a)
  ⊢ ∃ (y : T) st a = y;
proof
  by wip(?goal);
wip;

Hint

Open ex with exists_elim; in the witness branch you hold witness := x = a. Offer x as the new witness (exists_intro(T, λ (y : T) st a = y, x), leaving a = x) and flip with symmetry(T, x, a), leaving x = a, closed by witness. Both then s carry the branch context ex := …, x : T, witness := x = a.

9c. Discharge under a universal: from ∃ x. P(x) and ∀ x. P(x) ⇒ R, prove R.

rule exists_elim(T : Sort, P : T → Prop, Q : Prop)
  ⊢ ∃ (x : T) st P(x);
  x : T, witness := P(x) ⊢ Q
  ────────────────────────
  ⊢ Q
end;

rule forall_elim(T : Sort, P : T → Prop, x : T)
  ⊢ ∀ (y : T) st P(y)
  ────────────────────────
  ⊢ P(x)
end;

rule implication_elim(P Q : Prop)
  ⊢ P ⇒ Q;
  ⊢ P
  ────────────────────────
  ⊢ Q
end;

sort T : Sort;

lemma exists_use(P : T → Prop, R : Prop, ex := ∃ (x : T) st P(x),
                 use := ∀ (x : T) st P(x) ⇒ R)
  ⊢ R;
proof
  by wip(?goal);
wip;

Hint

In the witness branch (x : T; witness := P(x)) instantiate use at x with forall_elim to get P(x) ⇒ R, then implication_elim against witness.

9. Equational reasoning (rewriting)

Goal: a goal built from an equation. Method: given a = b, replace a with b (or b with a) somewhere in the goal — that’s forward / backward from Reflexivity and rewriting, and refl closes anything of the form x = x.

Exercises

10a. Close a definitional equation: prove 0 + 0 = 0.

sort Nat : Sort;
op 0 : → Nat;
op s : Nat → Nat;
op + : Nat * Nat → Nat;
axiom add_zero_left(n : Nat)     ⊢ 0 + n = n;
axiom add_succ_left(n m : Nat)   ⊢ s(n) + m = s(n + m);

lemma zero_plus_zero
  ⊢ 0 + 0 = 0;
proof
  by wip(?goal);
wip;

Hint

0 + 0 = 0 is the axiom add_zero_left at 0: by add_zero_left(0);.

10b. Rewrite, then reflect: prove n = 0 + n.

sort Nat : Sort;
op 0 : → Nat;
op s : Nat → Nat;
op + : Nat * Nat → Nat;
axiom add_zero_left(n : Nat)     ⊢ 0 + n = n;
axiom add_succ_left(n m : Nat)   ⊢ s(n) + m = s(n + m);
axiom refl(T : Sort, x : T)  ⊢ x = x;

rule forward(T : Sort, a b : T, eq := a = b, P : T → Prop)
  ⊢ P(b)
  ────────────────────────
  ⊢ P(a)
end;

lemma zero_left_flip(n : Nat)
  ⊢ n = 0 + n;
proof
  by wip(?goal);
wip;

Hint

Turn the 0 + n on the right into n with forward(Nat, 0 + n, n, add_zero_left(n), n = _) then ⊢ n = n; and close by refl(Nat, n).

10c. Flip an equality: from a = b, prove b = a.

sort Nat : Sort;
op 0 : → Nat;
op s : Nat → Nat;
op + : Nat * Nat → Nat;
axiom add_zero_left(n : Nat)     ⊢ 0 + n = n;
axiom add_succ_left(n m : Nat)   ⊢ s(n) + m = s(n + m);
rule symmetry(T : Sort, x y : T)
  ⊢ x = y
  ────────────────────────
  ⊢ y = x
end;

lemma flip_eq(a b : Nat, h := a = b)
  ⊢ b = a;
proof
  by wip(?goal);
wip;

Hint

symmetry(Nat, a, b) concludes b = a from ⊢ a = b: then h := a = b ⊢ a = b; by h;.

That’s the toolbox. Almost every proof in the standard library — and every monster in the Dungeon Proof Crawler — is these moves, combined. When a goal stumps you, ask which shape it has (an implication? a ∀? an equation?) and reach for the matching technique.