LP, the Larch Prover -- Induction rules


An induction rule is logically equivalent to an infinite set of formulas, which justify the use of proofs by induction.

Syntax

<induction-rule> ::= sort <sort> generated [ freely ] by <operator>+,
                       | well founded <operator>

Examples

sort Nat generated freely by 0, s
sort Set generated by {}, insert
sort Set generated by {}, {__}, \U
well founded <

Usage

Users can assert or prove induction rules.

Assertions like sort Nat generated by 0, s specify sets of generators for use in proofs by structural induction. The listed operators (e.g, 0 and s) must have the named sort (e.g., Nat) as their range. If none of the domain sorts of an operator is the same as its range sort, the operator is a basis generator (e.g., 0); otherwise, it is an inductive generator (e.g, s). Structural induction rules are logically equivalent to infinite sets of first-order formulas of the form

P(0) /\ \A x (P(x) => P(s(x))) => \A x P(x)
where P is an arbitrary first-order formula.

The use of freely supplements a structural induction rule with a set of formulas asserting that the named operators are one-to-one and have disjoint ranges. For example, sort Nat generated freely by 0, s gives rise to the formulas s(x) = s(y) <=> x = y and 0 ~= s(x).

Assertions like well founded < specify a binary relation for use in proofs by well-founded induction. The listed operator must have a signature of the form S,S->Bool for some sort S. Well-founded induction rules are logically equivalent to infinite sets of first-order formulas of the form

\A x (\A y (y < x => P(y)) => P(x)) => \A x P(x)
where P is an arbitrary first-order formula.

To display the induction rules that LP currently has available for use, type display induction-rules (or disp i-r for short).