[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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; |
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] | [ ? ] |