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.