Tactics and Proof Steps

Make explicit which proposition each step transforms into which next proposition.

16.1 Automation should not hide the goals

Longer proofs often require many individual equality rewrites. Tauto's tactics are macros that expand some of this work into proof terms. You must still write the proposition before and after a rewrite.

by rewrite!(e): original_goal {
  ⊢ next_goal from next_proof
}

This is a schematic form, not a complete program. Replace original_goal and next_goal with actual propositions such as a = b. Tauto avoids asking the tactic to infer a rewrite motive: the two written goals should determine it uniquely.

16.2 Inspect an actual rewrite

The repository's examples/nat/Add.taut proves commutativity of addition. It uses nat!, a syntax macro for writing propositions directly as mathematical expressions.

pub theorem add_comm(n: Nat, m: Nat): nat!(`$n + $m = $m + $n`) {
  match m: nat!(`$n + $m = $m + $n`) {
    Zero => Eq::sym(add_zero_l(n))
    Succ(k) => by rewrite!(add_succ_l(k, n)): nat!(`$n + ${Succ(k)} = ${Succ(k)} + $n`) {
      ⊢ nat!(`$n + ${Succ(k)} = ${Succ(k + n)}`) from succ_cong(add_comm(n, k))
    }
  }
}

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

nat! expands to a = b. $n embeds the Tauto variable n; embed a compound expression with braces, as in ${Succ(k)}. This file imports Lib.taut, where nat! is defined, and proves add_zero_l, add_succ_l, and succ_cong earlier in the same file.

To see what rewrite! did, compare the original equality after : with the next equality after ⊢. If either fails to match the actual goal, the kernel rejects the proof.

16.3 nat_norm! normalizes arithmetic

pub theorem add_left_comm(a: Nat, b: Nat, c: Nat): nat!(`$a + ($b + $c) = $b + ($a + $c)`) {
  by nat_norm!(): nat!(`$a + ($b + $c) = $b + ($a + $c)`) {}
}

✓ theorem add_left_comm : ∀ a: Nat. ∀ b: Nat. ∀ c: Nat. a + (b + c) = b + (a + c)

nat_norm! normalizes expressions involving natural-number addition, multiplication, and related operations to prove that both sides coincide. It does not grant arbitrary arithmetic properties without justification.

Check the example from the repository root:

tauto check examples/nat/Add.taut

ok      add_comm
ok      add_assoc
ok      add_left_comm

(The actual output also lists other theorems.)

16.4 Why automation need not be trusted

Even if a macro generates an incorrect proof term, the theorem is not accepted unless the kernel checks that term. A tactic constructs a candidate proof. The kernel decides whether that candidate is valid.

Exercise 16.1: In one sentence, explain why a sound kernel can prevent acceptance of an incorrect theorem even when automation contains bugs.