LP, the Larch Prover -- Proofs by structural induction

A proof of a formula F by structural induction on a variable x of sort S is based on an induction rule that specifies a set G of generators for S, that is, a set of operators with range S. LP generates subgoals for the basis and induction steps in a proof by structural induction, as follows.

The basis subgoals involve proving the formulas that result from substituting the basis generators in G for x in F. Basis generators are those with no arguments of sort S; fresh variables are used for variables of other sorts, as in {e}.
LP introduces additional hypotheses for the induction subgoals by substituting one or more new constants for x in F. Each induction subgoal involves proving a formula that results from substituting a nonbasis generator of G (applied to these constants) for x in F (e.g., s(xc) or xc \U xc1).

Examples

assert sort Nat generated by 0, s
prove 0 + x = x by induction
  Basis subgoal:        0 + 0 = 0
  New constant:         xc
  Induction hypothesis: 0 + xc = xc
  Induction subgoal:    0 + s(xc) = s(xc)

assert sort Set generated by {}, {__}, \U
prove x \subseteq x by induction
  Basis subgoals:       {} \subseteq {},    {e} \subseteq {e}
  New constants:        xc,                 xc1
  Induction hypotheses: xc \subseteq xc,    xc1 \subseteq xc1
  Induction subgoal:    (xc \U xc1) \subseteq (xc \U xc1)

LP, the Larch Prover -- Proofs by structural induction

Examples

See also