First Order
Properties of Lists
nat : type.
z : nat.
s : nat -> nat.
list : type.
nil : list.
cons : {n:nat} {l:list} list.
eq_list : {L1:list}{L2:list}type.
refl_list : {L:list} eq_list L L.
append : {L1:list}{L2:list}{L3:list} type.
append_nil : {L:list} append nil L L.
append_cons : {L1:list}{L2:list}{L3:list}{N:nat}{D:append L1 L2 L3}
append (cons N L1) L2 (cons N L3).
rev_app : {L1:list}{L2:list}type.
rev_app_nil : rev_app nil nil.
rev_app_cons : {N:nat} {A:list} {B:list} {BN:list} {D:rev_app A B}
{D2:append B (cons N nil) BN} rev_app (cons N A) BN.
rev_acc : {L1:list}{Acc:list}{L2:list}type.
rev_acc_nil : {L:list} rev_acc nil L L.
rev_acc_cons : {L1:list} {L2:list} {L3:list} {N:nat} {D:rev_acc L1 (cons N L2) L3}
rev_acc (cons N L1) L2 L3.Specification "lists.lf".
%%% append theorems
Theorem app_assoc : forall L1 L2 L3 L23 L4 D1 D2, {D1 : append L2 L3 L23} =>
{D2 : append L1 L23 L4} =>
exists L12 D3 D4, {D3 : append L1 L2 L12} /\ {D4 : append L12 L3 L4}.
induction on 2. intros.
case H2.
% append_cons case.
apply IH to H1 H7.
case H8.
exists (cons N L12).
exists append_cons L5 L2 L12 N D3.
exists append_cons L12 L3 L7 N D4.
split.
search.
search.
% append_nil case.
exists L2.
exists append_nil L2.
exists D1.
split.
search.
search.
Theorem app_identity : forall L1 L2 D, {D : append L1 nil L2} =>
exists R, {R : eq_list L1 L2}.
induction on 1. intros. case H1.
% append_cons case.
apply IH to H6.
case H7.
exists refl_list (cons N L5).
search.
% append_nil case.
exists refl_list nil.
search.
%%% rev_app (reverse defined using append) theorems
% proves that the append of two reverses is the reverse of two appends.
Theorem rev_app_swap : forall A B a b AB ba D1 D2 D3 D4,
{D1 : append A B AB} =>
{D2 : rev_app A a} =>
{D3 : rev_app B b} =>
{D4 : append b a ba} =>
exists D5, {D5 : rev_app AB ba}.
induction on 1. intros. case H1.
% append_cons case.
case H2.
apply app_assoc to H15 H4.
case H16.
apply IH to H9 H14 H3 H17.
exists rev_app_cons N L3 L12 ba D7 D2.
search.
% append_nil case.
case H2.
apply app_identity to H4.
case H6.
exists D3.
search.
Theorem rev_app_rev : forall L1 L2 D1, {D1 : rev_app L1 L2} =>
exists D2, {D2 : rev_app L2 L1}.
induction on 1. intros. case H1.
% rev_app_cons case.
apply IH to H6.
assert exists D3, {D3 : rev_app (cons N nil) (cons N nil)}.
exists rev_app_cons N nil nil (cons N nil) rev_app_nil (append_nil (cons N nil)).
search.
assert exists D4, {D4 : append (cons N nil) A (cons N A)}.
exists append_cons nil A A N (append_nil A).
search.
apply rev_app_swap to H7 H8 H9 H10.
exists D5.
search.
% rev_app_nil case.
exists rev_app_nil.
search.
%%% rev_acc (reverse defined using an accumulator list) theorems
Theorem rev_acc_func : forall L1 L2 L3 L4 D1 D2, {D1 : rev_acc L1 L2 L3} =>
{D2 : rev_acc L1 L2 L4} =>
exists D3, {D3 : eq_list L3 L4}.
induction on 1. intros. case H1.
% rev_acc_cons case.
case H2.
apply IH to H7 H12.
exists D1.
search.
% rev_acc_nil case.
case H2.
exists refl_list L4.
search.
Theorem rev_acc_exists : forall L1 L2, {L1 : list} => {L2 : list} =>
exists L3 D1, {D1 : rev_acc L1 L2 L3}.
induction on 1. intros. case H1.
% rev_acc_cons case.
assert {cons n L2 : list}.
apply IH to H4 H5.
exists L3.
exists rev_acc_cons l L2 L3 n D1.
search.
% rev_acc_nil case.
exists L2.
exists rev_acc_nil L2.
search.
Theorem rev_acc_rev_lem : forall a B AB ba ba2 D1 D2 D3, {D1 : rev_acc a B AB} =>
{D2 : rev_acc AB nil ba} => {D3 : rev_acc B a ba2} =>
exists D4, {D4 : eq_list ba ba2}.
induction on 1. intros. case H1.
% rev_acc_cons case.
assert exists D4, {D4 : rev_acc (cons N B) L1 ba2}.
exists rev_acc_cons B L1 ba2 N D3. search.
apply IH to H8 H2 H9.
case H10.
exists refl_list ba2.
search.
% rev_acc_nil case.
apply rev_acc_func to H2 H3.
exists D1.
search.
Theorem rev_acc_rev : forall L1 L2 D1, {D1 : rev_acc L1 nil L2} =>
exists D2, {D2 : rev_acc L2 nil L1}.
intros.
assert {L2 : list}.
assert {nil : list}.
apply rev_acc_exists to H2 H3.
assert exists D3, {D3 : rev_acc nil L1 L1}. exists rev_acc_nil L1. search.
apply rev_acc_rev_lem to H1 H4 H5.
case H6.
exists D2.
search.