# lists.thm

%% 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.