Here is some advice about what to do next in a proof. Options 1, 5, and 6 make use of the table below.
Prove the goal by decomposing it into sub-goals. In the table below, look at the entry in the row for the current goal formula and the Prove column. The entry suggests the proof statement to use next. (This is the advice that Deduce outputs when you write ?.) When the goal is an all formula on a union type, you need to choose between arbitrary or induction. If the all variable in your goal appears in the formula as the first argument of a recursive function, then induction is a good choice. Otherwise choose arbitrary.
If the goal formula involves a function that is defined using a switch, then it is a good idea to use the switch proof statement.
If a recursive function's first parameter type is a view, reason about the view's target constructors. The view declaration itself requires a theorem of the form into(out(v)) = v.
Work backwards from the goal using a suffices statement. After the by keyword, write the reason, often expand and/or replace, which transform the goal formula.
Work forwards from a given with a have statement. Look at the entry in the row for the given formula and the Use column. The table entry suggests what to write for the reason after the by keyword of your have statement. (This is the advice that Deduce outputs when you write help L where L is the label for the given.)
conclude the proof of the goal formula. For the reason after the by keyword, one can use a given according to the Use column in the table below, or one can prove the goal formula according to the Prove column.
| Formula | Prove | Use |
|---|---|---|
true |
. |
No uses |
false |
Contradiction | implicitly proves anything |
P and Q |
, Comma |
(1) implicitly proves P, (2) implicitly proves Q |
P or Q |
(1) implicit from P, (2) implicit from Q |
cases |
if P then Q |
assume |
apply-to |
not P |
assume |
contradict, apply-to |
all x:T. P |
arbitrary, induction |
brackets |
some x:T. P |
choose |
obtain |
x = y |
symmetric, transitive, equations, expand, replace |
symmetric, transitive, replace, replace-in |
a ≤ b, a < b |
expand / replace to reduce to a base lemma (e.g. uint_less_equal_add); apply-to with a transitivity lemma (e.g. uint_less_equal_trans[a,b,c]) to chain |
apply-to with a transitivity lemma to chain with another inequality; replace with a cancellation lemma (e.g. uint_add_both_sides_of_less_equal[k]) to strip an additive prefix |
pred(args) |
one of pred's rule-name proofs (auto-generated by predicate / relation) |
rule induction, rule inversion |
Inside an equations block, expand and replace apply to the left-hand side of each step by default. To unfold or rewrite a part of the right-hand side, wrap that part in hash marks (#...#):
equations
length(node(x,xs)) = 1 + length(xs) by expand length.
... = # length(node(y,xs)) # by expand length.If you see could not find a place to expand definition of f in: ... and the displayed term is your RHS, you almost certainly need #...# around the call you want to unfold. See Equations for the long form.
+ that look trivial+ on UInt (and Int, Nat) is declared associative, which lets Deduce normalize chains like (a + b) + c and a + (b + c) to the same flat form — so by . closes any goal that differs only by re-parenthesization. But + is not registered as commutative (this would cause an auto rule to loop — see the discussion of auto), so any swap of summands still needs an explicit replace step. If your by . fails on what looks like a trivial arithmetic identity, look for an out-of-order pair.
For example, a + (1 + b) = 1 + (a + b) does not close with by . — associativity flattens both sides to a + 1 + b and 1 + a + b, which differ by swapping the first two summands. Close it with:
replace uint_add_commute[a, 1].The commute lemmas to reach for, by type: uint_add_commute (UInt), int_add_commute (Int), add_commute (Nat). The same trap applies to *: it is associative but not registered commutative, so look for uint_mult_commute / int_mult_commute / mult_commute when a multiplicative equation refuses to close.
≤, <)Inequality goals come up constantly in stdlib and algorithm proofs (e.g. count_if(xs', p) ≤ length(xs'), 1 + a ≤ 1 + b). The tactics for = rarely close them directly — reach for one of these moves instead, picking the type-specific lemma by prefix (uint_* / int_* / * for Nat):
a ≤ b and b ≤ c, apply uint_less_equal_trans[a, b, c] to p1, p2 produces a ≤ c. The bracket arguments are usually optional but help when overloading or unification is ambiguous. Same shape for < via uint_less_trans, and analogous for Int (int_less_equal_trans, int_less_trans) and Nat (less_equal_trans, less_trans).uint_add_both_sides_of_less_equal[k] is a bi-implication k + a ≤ k + b ⇔ a ≤ b, so replace uint_add_both_sides_of_less_equal[k] rewrites the goal k + a ≤ k + b into a ≤ b (or vice versa via replace ... rewriting). The strict version is uint_add_both_sides_of_less. Int has int_add_both_sides_of_less_equal / int_add_both_sides_of_less; Nat has add_both_sides_of_less_equal / add_both_sides_of_less.uint_less_equal_add: x ≤ x + y and uint_less_equal_add_left: y ≤ x + y close goals where one side is a summand of the other. Nat has less_equal_add / less_equal_add_left in the same shape.< to ≤ or back. uint_less_implies_less_equal and uint_not_less_implies_less_equal move between < and ≤; uint_not_less_equal_iff_greater (and its int_/Nat siblings) handle negated inequalities.Strict-then-weak chains use the mixed transitivity variants — for example int_less_trans_less_equal_right: if x < y and y ≤ z then x < z.
The Deduce surface syntax does not have separate ≥ / > operators; write b ≤ a for a ≥ b and b < a for a > b. The library follows the same convention, so search for the less_equal / less lemma whose pattern matches your goal after that flip.
For a full inventory of inequality lemmas, browse lib/UIntLess.pf, lib/IntLess.pf, and lib/NatLess.pf; the _add / _mult cancellation lemmas live in the corresponding *Add.pf / *Mult.pf files.