helphome pageduck scriptspecificationfirst proof pagepage 1 1 2 3 xpage 2

Inductive Properties of Lists, Part 2
Associativity of Append


We want to prove
( L0  L1  L2  : List  ) append(append(L0 , L1) , L2) = append(L0 , append(L1 , L2)) .
We use induction on L0 to prove this goal. For this, we use the induction scheme based on the signature { nil, cons } for List. Induction requires that we do the following:
  1. Base case: prove the assertion for L0 = nil .
    • Quantifier elimination introduces the new constant(s) l1, l2 : List  .
    • We show append(append(nil , l1) , l2) = append(nil , append(l1 , l2)) by reduction.
  2. Induction case: assume the assertion for L0 = L0 , and then prove it for L0 = cons(N0 , L0) .

And thus the main goal is proved.

Explanation

This is a standard proof of the familiar result that append is associative, using induction on the first variable, over the two constructors nil and cons. However, it should be noted that once the associativity equation is proved, instead of being added to the specification as a new equation that is available for reduction, the operation append is given the the attribute assoc. This is because the Duck score gives the command
goal: assoc-of append
instead of the command
goal: (forall L1 L2 L3 : List) append(append(L1, L2), L3) = append(L1, append(L2, L3)) .
Note that the syntax of the request to use induction here differs from that in the case of proving an equation by induction, because we do not have explicit names for the variables.


BOBJ proof scoreLeft    Up    Down    Right   
 

       This page was generated by Kumo on Tue Feb 13 19:34:15 PST 2001.