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;
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;
Go to the first, previous, next, last section, table of contents.