[ < ] [ > ] [ << ] [ Up ] [ >> ] [Top] [Contents] [Index] [ ? ]

# 8. Structural Induction

Similar to reasoning about natural numbers is reasoning about lists. We introduce structural induction and an equality over lists. This equality is denoted by the same symbol `=' as the one for natural numbers. The context makes it clear which of the two relations is meant.

The use of list-induction is analogous to nat-induction. This example should make it clear:
 ```proof symList : !l:t list. !k:t list. (l = k) => (k = l) = begin [ l:t list; [ k: t list; [ nil = nil; nil = nil ]; (nil = nil) => (nil = nil); [ y: t, ys: t list, nil = ys => ys = nil; [ nil = y :: ys; y :: ys = nil ]; nil = y :: ys => y :: ys = nil; nil = k => k = nil ]; !k:t list. nil = k => k = nil; [ x: t, xs: t list, !k:t list. xs = k => k = xs; [ k: t list. [ nil = x::xs; x::xs = nil ]; nil = x::xs => x::xs = nil; l = x::xs => x::xs = l ]; !k:t list. l = x::xs => x::xs = l ]; !k:t list. l = k => k = l ]; !l:t list. !k:t list. l = k => k = l end; ```

 [ < ] [ > ] [ << ] [ Up ] [ >> ] [Top] [Contents] [Index] [ ? ]

## 8.1 Proof terms

UNDER CONSTRUCTION!

We prove properties of these three functions:
 ```val app : t list -> t list -> t list = fn l => rec l of f nil => fn l' => l' | f (x :: xs) => fn l' => x :: f xs l' end; val rev : t list -> t list -> t list = fn l => rec l of f nil => fn k => k | f (x::xs) => fn k => f xs (x :: k) end; val reverse : t list -> t list = fn l => rev l nil; ```
Here are the proofs:
 ```term appnil : !l:t list. app l nil = l = fn l => rec l of f nil => eqN | f (x :: xs) => eqC (f xs) end; term refll : !l:t list. (l = l); % Homework ! term apprev : !l:t list. !k:t list. !m:t list. app (rev l k) m = rev l (app k m) = fn l => rec l of f nil => fn k => fn m => refll (app k m) | f (x::xs) => fn k => fn m => f xs (x :: k) m end; term revapp : !l:t list. !k:t list. !m:t list. rev (app l k) m = rev k (rev l m) = fn l => rec l of f nil => fn k => fn m => refll (rev k m) | f (x :: xs) => fn k => fn m => f xs k (x :: m) end; ```

 [ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

This document was generated by Andreas Abel on October, 24 2002 using texi2html