%% Various results about lists
%% (append, reverse, perm)
Specification "lists".
% Append is total
Theorem app_total : forall A B,
{list A} -> {list B} -> exists C, {append A B C}.
induction on 1. intros. case H1.
search.
apply IH to H3 H2. search.
% Append is deterministic
Theorem app_det : forall A B C C',
{append A B C} -> {append A B C'} -> C = C'.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
% Append is associative
Theorem app_assoc : forall A B C AB ABC,
{append A B AB} -> {append AB C ABC} ->
exists BC, {append B C BC} /\ {append A BC ABC}.
induction on 1. intros. case H1.
search.
case H2. apply IH to H3 H4. search.
Theorem rev_lemma : forall A A' B X,
{rev A A'} -> {append A (cons X nl) B} -> {rev B (cons X A')}.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H5. search.
% Reverse is its own inverse
Theorem rev_rev : forall A B,
{rev A B} -> {rev B A}.
induction on 1. intros. case H1.
search.
apply IH to H2. apply rev_lemma to H4 H3. search.
Theorem perm_lemma : forall A B B' X,
{perm B' A} -> {select B X B'} -> {perm B (cons X A)}.
induction on 2. intros. case H2.
search.
case H1. apply IH to H5 H3. search.
% Permutations are invertible
Theorem perm_perm : forall A B,
{perm A B} -> {perm B A}.
induction on 1. intros. case H1.
search.
apply IH to H3. apply perm_lemma to H4 H2. search.
%% We can define append at the meta-level and show a connection
Define app : lst -> lst -> lst -> prop by
app nl C C ;
app (cons X A) B (cons X C) := app A B C.
Theorem meta_implies_obj : forall A B C,
app A B C -> {append A B C}.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem obj_implies_meta : forall A B C,
{append A B C} -> app A B C.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
