Writing Mathematical Proofs

Combine domain notation, calc!, proof!, and tactics to write mathematical proofs that read well.

17a.1 Which tool to use when

The proofs in chapters 13–17 combined match, Eq::trans, and Eq::congr by hand. When equalities get long, as in mathematical proofs, the tools below let you write the same content in a form close to a proof on paper. Whichever you use, the kernel decides in the end whether a proof is accepted, exactly as before.

17a.2 Chain equalities with calc!

calc!(`$a = $b from $p = $c from $q`) is a syntax macro that starts from the expression a and writes, on each line, the next expression and the proof of that line. Load it with import std::Calc { calc }. As in other syntax macros, expressions and proofs are embedded with $. Nat::add_swap in std/Nat.taut is written in this form too.

import std::Base { Nat }
import std::Calc { calc }
import std::Nat { Nat }

theorem add_swap_ex(a: Nat, b: Nat, c: Nat): Nat::add(Nat::add(a, b), c) = Nat::add(Nat::add(a, c), b) {
  calc!(```
    $Nat::add(Nat::add(a, b), c)
    = $Nat::add(a, Nat::add(b, c)) from $Nat::add_assoc(a, b, c)
    = $Nat::add(a, Nat::add(c, b)) from $Eq::congr(⟦Nat::add(a, □)⟧, Nat::add_comm(b, c))
    = $Nat::add(Nat::add(a, c), b) from $Eq::sym(Nat::add_assoc(a, c, b))
    ```)
}

// Associativity, commutativity, then associativity in reverse swaps the operands

✓ theorem add_swap_ex : ∀ a: Nat. ∀ b: Nat. ∀ c: Nat. Nat::add(Nat::add(a, b), c) = Nat::add(Nat::add(a, c), b)

To the right of from, each line gives a proof of the equation previous = next. The three lines of this example are associativity, commutativity used to replace b + c with c + b, and associativity in the reverse direction. calc! expands them into nested right-associated Eq::trans. The term the kernel receives is the same as one built by writing Eq::trans by hand.

⟦Nat::add(a, □)⟧ on the second line is a congruence context. You may write exactly one □; it marks the only place replaced with a different expression. Here b + c = c + b is lifted into the hole of a + □, giving a + (b + c) = a + (c + b). This is the same as passing the lambda (z: Nat) => Nat::add(a, z) to Eq::congr.

A line that is equal by definition is still written with from Refl, not omitted. This lets the reader check on the spot that the two sides are equal by computation.

calc! also writes chains of ↔.

import std::Calc { calc }

theorem iff_chain(P: Prop, Q: Prop, R: Prop, pq: P ↔ Q, qr: Q ↔ R): P ↔ R {
  calc!(```
    $P
    ↔ $Q from $pq
    ↔ $R from $qr
    ```)
}

// A chain of ↔

✓ theorem iff_chain : ∀ P: Prop. ∀ Q: Prop. ∀ R: Prop. (Iff(P, Q)) -> (Iff(Q, R)) -> Iff(P, R)

You cannot yet mix = and ↔ in one chain, or chain ≤ and <.

17a.3 Build domain notation with syntax macros

Instead of Eq(Nat, Nat::add(n, m), Nat::add(m, n)), we want to write n + m = m + n. The notation of each field of mathematics is built with a syntax macro. The language does not gain notation for a field; a library defines its own notation, and proofs import it.

examples/nat/Lib.taut defines nat!, a notation for propositions about natural numbers (the three code samples below are excerpts of that file). First, write the grammar with syntax!.

syntax!(nat, ```par
%start Stmt
%title "nat"
%%
Stmt: Disj [Arrow Stmt];
Disj: Conj { OrTok Conj };
Conj: Rel { AndTok Rel };
Rel: Sum RelTail;
RelTail: EqTail | LeTail | LtTail | DvdTail;
EqTail: Equals Sum;
LeTail: LeTok Sum;
LtTail: LtTok Sum;
DvdTail: Bar Sum;
Sum: Prod { Plus Prod };
Prod: Atom { Star Atom };
Atom: Num | Paren | Embed;
Paren: LParen Sum RParen;
Embed: TautoExpr;
Num: /[0-9]+/;
Equals: '=';
LeTok: '<=';
LtTok: '<';
Bar: '|';
Arrow: '->';
AndTok: 'and';
OrTok: 'or';
Plus: '+';
Star: '*';
LParen: '(';
RParen: ')';
```) => enum Atom, struct Conj, struct Conj_Rep1, struct Disj, struct Disj_Rep1,
  struct DvdTail, struct EqTail, struct LeTail, struct LtTail, struct Paren,
  struct Prod, struct Prod_Rep1, struct Rel, enum RelTail, struct Stmt,
  struct Stmt_Opt1, struct Sum, struct Sum_Rep1, fn parse

From the grammar, typed syntax trees (nat::Sum, nat::Rel, and so on) are generated for each rule. The list after => is the complete list of declarations that get generated; a missing or extra name is an error. Embed: TautoExpr is the rule that lets you embed a Tauto expression in the notation, as in $n or $Succ(k). The symbols of the field (+, *, =, <=, |) are written only in this grammar; they are not built into the language.

Next, write a function that builds a Tauto expression from the syntax tree, and the entry point of the macro.

pub fn nat_rel(r: nat::Rel): SynExpr ! {macro_error, Div} {
  let l := nat_sum(r.sum)
  match r.rel_tail {
    EqTail(t) => {
      let x := nat_sum(t.sum)
      quote { Eq(Nat, $l, $x) }
    }
    LeTail(t) => {
      let x := nat_sum(t.sum)
      quote { Le($l, $x) }
    }
    LtTail(t) => {
      let x := nat_sum(t.sum)
      quote { Lt($l, $x) }
    }
    DvdTail(t) => {
      let x := nat_sum(t.sum)
      quote { Dvd($l, $x) }
    }
  }
}

quote { … } is the syntax that builds an expression, and $l and $x splice in the expressions built so far. = becomes Eq(Nat, …), <= becomes Le, < becomes Lt, and | becomes Dvd (divisibility). and and or expand to And and Or, and -> to a function type (implication). The expansion is limited to calls of existing terms (Eq, Le, …). No new rule is added to the kernel, so more notation does not widen what you trust.

pub macro fn nat(s: nat::Stmt): SynExpr ! {macro_error, Div} {
  let l := nat_disj(s.disj.conj, s.disj.rep)
  match s.opt {
    None => l
    Some(o) => {
      let r := nat(o.stmt)
      ExPi(Cons(SynParam { name: None, ty: l }, Nil), r, None, s.span)
    }
  }
}

Now nat!(`$n + $m = $m + $n`) is read as Eq(Nat, n + m, m + n). The notation string is enclosed in backquotes.

You can check the generated types with tauto syntax show. Run it at the repository root.

tauto syntax show examples/nat nat

enum nat::Atom {
  Num(SynToken)
  Paren(nat::Paren)
  Embed(SynExpr)
}
struct nat::Conj { span: SynSpan, rel: nat::Rel, rep: List(nat::Conj_Rep1) }
…

On the user side, the proposition of a theorem stays a mathematical formula. add_comm, seen in chapter 16, is an example. Add, Mul, Order, Dvd, and More in examples/nat are all written with nat!.

17a.4 Write close to prose with proof!

proof! is a syntax macro that takes a proof written in English sentences, plus a short program that builds the proof term from those sentences, and produces the proof term. The sentences state what a mathematical proof states. The program writes only what the sentences leave out. It does no search; the same input always gives the same term. The kernel checks the produced term as usual, so a wrong program cannot get a false theorem accepted.

std currently has proof! in two forms.

• proof! of std::proof::Lang: labelled sentences are arranged in a tree, and the sentence forms of Forms (By induction on …, We have …) turn each sentence into a proof term.
• proof! of std::proof::Proof: the sentences are followed by %% and then a construction program. examples/nat/proof/Add.taut uses it.

proof! of Lang

A child sentence is indented deeper than its parent. The child sentences of By induction on n. are the cases, one per constructor. Give a label (such as [1]) only to a sentence that is referred to later.

import std::Base { Nat }
import std::proof::Lang { proof }
import std::proof::Forms { proof_by, proof_case, proof_we }

theorem add_zero_left(n: Nat): Nat::add(0, n) = n {
  proof!(```
    By induction on n.
      Case Zero. By Refl.
      Case Succ(k). We have Nat::add(0, Succ(k)) = $Succ(0 + k) = Succ(k) by the induction hypothesis.
  ```)
}

// The induction hypothesis closes the Succ(k) case

✓ theorem add_zero_left : ∀ n: Nat. Nat::add(0, n) = n

We have a = b = c by R. is a chain of equalities. Each step is joined with Eq::trans, and a step with no reason written is treated as equal by computation (Refl). The reason of the last step, the induction hypothesis, is the induction hypothesis of the Succ(k) case. A part that starts with $ is an embedded Tauto expression. Inside the parentheses of a call, as in $Succ(0 + k), you can also write operators.

The caller imports the sentence forms. Here they are proof_by (By …), proof_case (Case …), and proof_we (We have …).

Other sentence forms include the following.

If h is contradictory, write This contradicts h.

import std::Base { Nat }
import std::proof::Lang { proof }
import std::proof::Forms { proof_this }

theorem no_succ_le_zero(n: Nat, h: Nat::le(Succ(n), Zero) = true): False {
  proof!(```
    This contradicts h.
  ```)
}

// From a contradictory h anything follows

✓ theorem no_succ_le_zero : ∀ n: Nat. ¬(Nat::le(Succ(n), Zero) = true)

You can also name a chain of equalities and use it in a later sentence. A named chain is passed in the program (after %%).

import std::proof::Lang { proof }
import std::proof::Forms { proof_by, proof_we }

theorem named<A>(
  op: (A, A) -> A,
  unit: A,
  a: A,
  b: A,
  h1: op(a, b) = a,
  h2: a = unit
): unit = op(a, b) {
  proof!(```
    [1] We have h: op(a, b) = a by h1 = unit by h2. By Eq::sym.
    %%
    [1] h
  ```)
}

// Name the chain h and pass it in the program

✓ theorem named : ∀ A: Type. ∀ op: (A) -> (A) -> A. ∀ unit: A. ∀ a: A. ∀ b: A. (op(a, b) = a) -> (a = unit) -> unit = op(a, b)

h1 is the reason for op(a, b) = a and h2 the reason for a = unit. The chain op(a, b) = a = unit is named h, and passing h to the last By Eq::sym. closes the goal unit = op(a, b).

proof! of Proof

The other form separates one text and one program with %%. Look at a proof in examples/nat/proof/Add.taut.

pub theorem succ_inj<a: Nat, b: Nat>(h: Succ(a) = Succ(b)): a = b {
  proof!(```
    [main] We have $a = $pred(Succ(a)) = $pred(Succ(b)) = $b.

    %%
    main:calc(conv,congr($pred,$h),conv)
    ```)
}

✓ theorem succ_inj : ∀ a: Nat. ∀ b: Nat. (Succ(a) = Succ(b)) -> a = b

We have $a = … = $b. in the text is the same chain of equalities as the calc of 17a.2. main:calc(conv,congr($pred,$h),conv) in the program lists, in order, the reason for each pair of adjacent expressions.

• conv: equal by computation alone. pred(Succ(a)) reduces to a.
• congr($pred,$h): lift h: Succ(a) = Succ(b) through pred.
• app: use an embedded piece of evidence (such as $succ_cong(ih)).

The label main is the label of the text. The program assigns an instruction to each label of the text. The next proof by induction is an example in which the proof has several labels.

pub theorem add_zero_l(n: Nat): nat!(`0 + $n = $n`) {
  proof!(```
    [main] We prove $nat!(`0 + $n = $n`) by induction on $n.
    [zero] Case Zero is immediate.
    [succ] Case Succ($k).
      Assume $k: $Nat, $ih: $nat!(`0 + $k = $k`).
      We have $(0 + Succ(k)) = $Succ(0 + k) = $Succ(k).

    %%
    main:ind(zero:refl,succ:calc(conv,congr($Succ,$ih)))
    ```)
}

✓ theorem add_zero_l : ∀ n: Nat. 0 + n = n

main:ind(zero:refl,succ:calc(…)) says that the sentence main is an induction whose zero case is refl and whose succ case is calc. Assume $k: $Nat, $ih: … writes out, with types, the variable of the case and the name of the induction hypothesis. Since the types are written in the text, the reader learns what the hypothesis is without reading the program.

The instructions of the program are as follows.

The proof of add_comm combines sym, rewrite, and calc.

pub theorem add_comm(n: Nat, m: Nat): nat!(`$n + $m = $m + $n`) {
  proof!(```
    [main] We prove $nat!(`$n + $m = $m + $n`) by induction on $m.
    [zero] Case Zero.
      We prove $(n + Zero = Zero + n).
      By symmetry of [left].
    [left] We prove $(0 + n = n).
      By $add_zero_l(n).
    [succ] Case Succ($k).
      Assume $k: $Nat, $ih: $(n + k = k + n).
      We prove $nat!(`$n + $Succ(k) = $Succ(k) + $n`).
      Using $add_succ_l(k, n): $nat!(`$Succ(k) + $n = $Succ(k + n)`), rewrite the goal to
      $nat!(`$n + $Succ(k) = $Succ(k + n)`).
    [cong] We have $(n + Succ(k)) = $Succ(n + k) = $Succ(k + n).

    %%
    main:ind(zero:sym(left:app),succ:rewrite(cong:calc(conv,app($succ_cong(ih)))))
    ```)
}

✓ theorem add_comm : ∀ n: Nat. ∀ m: Nat. n + m = m + n

The text of rewrite writes both the equation used and the goal after rewriting. As with rewrite! in chapter 16, the reader can see where and how the rewriting happens. Note that the propositions of this example are written with the nat! of 17a.3. Domain notation and proof! are combined in this way.

17a.5 A tactic that closes arithmetic equations in one step

nat_norm! proves an equation by comparing normal forms, as ring does in other provers. It treats +, *, Succ, numeric literals, and every other term as variables, and shows that both sides have the same normal form by applying the theorem Nat::norm_eq.

import std::Tactic { nat_norm }

theorem square_sum(a: Nat, b: Nat): (a + b) * (a + b) = a * a + 2 * a * b + b * b {
  by nat_norm!(): (a + b) * (a + b) = a * a + 2 * a * b + b * b {}
}

// Both sides have one normal form, so no arm is written

✓ theorem square_sum : ∀ a: Nat. ∀ b: Nat. (a + b) * (a + b) = a * a + 2 * a * b + b * b

The tactic is not what you trust. If its reading is wrong, the kernel does not accept Refl and the proof fails. A tactic that leaves no goal takes no arms (nothing inside {}). For inequalities l <= r = true and l < r = true there is nat_le!.

An equation that needs a hypothesis is not closed by nat_norm!. Use the hypothesis in one step of calc! or rewrite!, and leave the remaining arithmetic to nat_norm!.

17a.6 Work in progress, and reading it back

A proof is not written in one go. If you put a goal hole ?name, the check treats that declaration as incomplete, does not accept it, and tells you the goal and context of the hole.

import std::Base { Nat }

theorem add_zero_right(n: Nat): Nat::add(n, 0) = n {
  ?todo
}

// A declaration with a hole is not accepted; it stays incomplete

… theorem add_zero_right : ∀ n: Nat. Nat::add(n, 0) = n

?todo  (4:3)
  n : Nat
⊢ Nat::add(n, 0) = n

tauto goals src/todo.taut

?todo in add_zero_right (src/todo.taut:5:3)
  n : Nat
⊢ Nat::add(n, 0) = n

When you are unsure what to write next, tauto suggest FILE --hole todo lists lemmas that fit the goal. With --verify, it actually checks the candidates.

For a finished proof, tauto proof reads it back as natural prose. Let us have it read the calc! proof of 17a.2.

tauto proof src/calc.taut add_swap_ex --format natural

add_swap_ex
Assume a: Nat, b: Nat, c: Nat.
We prove Nat::add(Nat::add(a, b), c) = Nat::add(Nat::add(a, c), b).

Nat::add(Nat::add(a, b), c) = Nat::add(a, Nat::add(b, c))    (Nat::add_assoc(a, b, c))
 = Nat::add(a, Nat::add(c, b))    (Nat::add_comm(b, c) and congruence)
 = Nat::add(Nat::add(a, c), b)    (Nat::add_assoc(a, c, b) in reverse)

Because the prose is made from the proof term, it shows what the accepted term actually does, not what the author intended. When a human checks a proof written by an AI, this output is what to read. tauto assumptions FILE NAME lists whether the theorem relies on axioms or external functions.

17a.7 Which to choose

• For an equality proof that transforms an expression line by line, start with calc!.
• If you write many theorems in the same field, build that field's notation with a syntax macro.
• For a proof that contains induction or case analysis and that people should read, use proof!.
• For an identity of only additions and multiplications, use nat_norm!.
• When unsure, put a hole ?name and look at the goal with tauto goals.

Exercise 17a.1: Rewrite add_swap_ex of 17a.2 by joining Nat::add_assoc and Nat::add_comm directly with Eq::trans. What becomes easier to read with calc!?

Exercise 17a.2: Write Nat::add(a, b) = Nat::add(b, a) by induction on b with the proof! of Lang in 17a.4. Put ?todo where it does not work out, and use tauto goals to find out what is needed.