LP, the Larch Prover -- Proofs by multilevel induction


The command prove F by induction on x depth n using IR directs LP to prove a formula F by n-level structural induction; by default, n is 1. For example, proving a formula F(x) by depth 2 induction using the induction rule sort Nat generated by 0, s, involves proving two basis subgoals, F(0) and F(s(0)), and one induction subgoal, F(s(s(xc))), given F(xc) and F(s(xc)) as induction hypotheses.

In general, LP constructs the basis and induction steps using the set G of generators for the sort S of x specified by the induction rule IR, as follows.

Definition 1. A (G,F,C)-ground term, where C is a set of constants of sort S, is a quantifier-free term of sort S in which all operators are either in C or are inductive generators in G, no variable has sort S, no variable occurs more than once, and no variable also occurs in F.

Definition 2. A (G,F)-ground term is a (G,F,B)-ground term, where B is the set of basis generators in G.

Definition 3. The depth of a quantifier-free term is 0 if the term consists of a variable; otherwise it is one more than the maximum depth of its arguments.

Definition 4. A (G,F,{c1,...,cm})-ground term is canonical if it contains exactly one occurrence of each of c1, ..., ck for some k <= m.

The basis step involves proving all formulas of the form F(x gets t) where t is an (G,F,B)-ground term of depth at most n.

The induction step introduces a set C = {c1,...,cm} of new constants of sort S, where m is the maximum number of arguments of sort S in a generator in G raised to the power n. The induction step involves proving all formulas of the form F(x gets t), where t is a canonical (G,F,C)-ground term of depth n+1. The induction hypotheses available in the induction step consist of all formulas of the form F(x gets t), where t is a (G,F,C)-ground term of depth at most n.

When n is 1, the induction hypotheses consist of all formulas of the form F(x gets c), where c is in C; and the induction step involves proving all formulas of the form F(x gets t), where t is a canonical (G,F,C)-ground term of depth 2.

Examples:

Gener-  Level   Basis           Induction                 Induction
ators           Subgoals        Hypotheses                Subgoals

0, s      1     f(0)            f(c)                      f(s(c))

0, s      2     f(0)            f(c)                      f(s(s(c)))
                f(s(0))         f(s(c))

0, 1, +   1     f(0)            f(c1)                     f(c1+c2)
                f(1)            f(c2)

0, 1, +   2     f(0)            f(c1), f(c2)              f(c1+(c2+c3)
                f(1)            f(c3), f(c4)              f((c1+c2)+c3)
                f(0+0)          f(c1+c1), f(c1+c2), ...   f((c1+c2)+(c3+c4))
                f(0+1)          f(c2+c1), f(c2+c2), ...       
                f(1+0)          f(c3+c1), f(c3+c2), ...
                f(1+1)          f(c4+c1), f(c4+c2), ...
                                
                                
nil       1     f(nil)          f(c)                      f(cons(x, c))
cons

nil       2     f(nil)          f(c)                      f(cons(x,cons(y,c))
cons            f(cons(x,nil))  f(cons(x,c))