nat : type.
z : nat.
s : {x: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.
Click on a command or tactic to see a detailed view of its use.
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}.