Require Import Vbase Varith.
Require Coq.omega.Omega.

Set Implicit Arguments.

Open Scope bool_scope.
Open Scope list_scope.

Section Operations.

Variable n0 : nat. Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Type l : (list T).

Definition ohead l :=
  match l with
    | nil => None
    | x :: _ => Some x
  end.

Definition head l :=
  match l with
    | nil => x0
    | x :: _ => x
  end.

Definition behead l :=
  match l with
    | nil => nil
    | _ :: x => x
  end.

Definition ncons n x := iter n (cons x).
Definition nlist n x := ncons n x nil.

Fixpoint snoc l z :=
  match l with
    | nil => z :: nil
    | x :: l => x :: snoc l z
  end.

Fixpoint last x l :=
  match l with
    | nil => x
    | x' :: l' => last x' l'
  end.

Fixpoint olast l :=
  match l with
    | nil => None
    | x' :: l' => Some (last x' l')
  end.

Fixpoint belast x l :=
  match l with
    | nil => nil
    | x' :: l' => x :: belast x' l'
  end.

Fixpoint onth l n {struct n} :=
  match l, n with
    | nil, _ => None
    | x :: l, O => Some x
    | x :: l, S n => onth l n
  end.

Fixpoint oset_nth l n y {struct n} :=
  match l, n with
    | nil, _ => None
    | x :: l, O => Some (y :: l)
    | x :: l, S n => match oset_nth l n y with
                       | None => None
                       | Some l' => Some (x :: l')
                     end
  end.

Fixpoint nth l n {struct n} :=
  match l, n with
    | nil, _ => x0
    | x :: l, O => x
    | x :: l, S n => nth l n
  end.

Fixpoint set_nth l n y {struct n} :=
  match l, n with
    | nil, _ => ncons n x0 (y :: nil)
    | x :: l, O => y :: l
    | x :: l, S n => x :: set_nth l n y
  end.

Fixpoint In x l :=
  match l with
    | nil => False
    | y :: l => y = x \/ In x l
  end.

Fixpoint find f l :=
  match l with
    | nil => 0
    | x :: l' => if (f x : bool) then 0 else S (find f l')
  end.

Fixpoint filter f l :=
  match l with
    | nil => nil
    | x :: l' => if (f x : bool) then x :: filter f l' else filter f l'
  end.

Fixpoint count f l :=
  match l with
    | nil => 0
    | x :: l' => if (f x : bool) then S (count f l') else count f l'
  end.

Fixpoint has f l :=
  match l with
    | nil => false
    | x :: l' => f x || has f l'
  end.

Fixpoint all f l :=
  match l with
    | nil => true
    | x :: l' => f x && all f l'
  end.

Fixpoint sieve (m : list bool) (s : list T) {struct m} : list T :=
  match m, s with
  | b :: m', x :: s' => if b then x :: sieve m' s' else sieve m' s'
  | _, _ => nil
  end.

Fixpoint drop n l {struct l} :=
  match l, n with
  | _ :: l, S n' => drop n' l
  | _, _ => l
  end.

Fixpoint take n l {struct l} :=
  match l, n with
  | x :: l, S n' => x :: take n' l
  | _, _ => nil
  end.

Definition rot n l := drop n l ++ take n l.

Definition rotr n l := rot (length l - n) l.

Fixpoint rev_append l1 l2 :=
  match l1 with
    | nil => l2
    | x :: l1 => rev_append l1 (x :: l2)
  end.

Fixpoint iota (m n : nat) : list nat :=
  match n with
    | O => nil
    | S n => m :: iota (S m) n
  end.

End Operations.


Definition rev T s :=
  match tt with tt =>
    rev_append s (@nil T)
  end.

Section SequencesBasic.

Variable n0 : nat. Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Types s l : (list T).

Lemma length0nil : forall s, length s = 0 -> s = nil.

Lemma length_behead : forall s, length (behead s) = (length s) - 1.

Lemma length_ncons : forall n x s, length (ncons n x s) = n + length s.

Lemma length_nlist : forall n x, length (nlist n x) = n.

Lemma length_app : forall s1 s2, length (s1 ++ s2) = length s1 + length s2.

Lemma app0l : forall s, nil ++ s = s.

Lemma app1l : forall x s, (x :: nil) ++ s = x :: s.

Lemma app_cons : forall x s1 s2, (x :: s1) ++ s2 = x :: s1 ++ s2.

Lemma app_ncons : forall n x s1 s2, ncons n x s1 ++ s2 = ncons n x (s1 ++ s2).

Lemma app_nlist : forall n x s, nlist n x ++ s = ncons n x s.

Lemma appl0 : forall s, s ++ nil = s.

Lemma appA : forall s1 s2 s3, (s1 ++ s2) ++ s3 = s1 ++ (s2 ++ s3).

Lemma nconsE : forall n x s, ncons n x s = nlist n x ++ s.

Lemma snoc_cons : forall x s z, snoc (x :: s) z = x :: snoc s z.

Lemma appl1 : forall l x, l ++ (x :: nil) = snoc l x.

Lemma snocE : forall l x, snoc l x = l ++ (x :: nil).

Lemma lastI : forall x s, x :: s = snoc (belast x s) (last x s).

Lemma last_cons : forall x y s, last x (y :: s) = last y s.

Lemma length_snoc : forall s x, length (snoc s x) = S (length s).

Lemma length_belast : forall x s, length (belast x s) = length s.

Lemma last_app : forall x s1 s2, last x (s1 ++ s2) = last (last x s1) s2.

Lemma last_snoc : forall x s z, last x (snoc s z) = z.

Lemma belast_app : forall x s1 s2,
  belast x (s1 ++ s2) = belast x s1 ++ belast (last x s1) s2.

Lemma belast_snoc : forall x s z, belast x (snoc s z) = x :: s.

Lemma app_snoc : forall x s1 s2, snoc s1 x ++ s2 = s1 ++ x :: s2.

Lemma snoc_app : forall x s1 s2,
  snoc (s1 ++ s2) x = s1 ++ snoc s2 x.

Inductive last_spec : list T -> Type :=
  | LastNil : last_spec nil
  | LastRcons s x : last_spec (snoc s x).

Lemma lastP : forall s, last_spec s.

Lemma last_ind :
  forall P (Hnil: P nil) (Hlast: forall s x, P s -> P (snoc s x)) s, P s.

Inductive last_spec_eq (y : list T): Type :=
  | LastEqNil : y = nil -> last_spec_eq y
  | LastEqRcons s x : y = snoc s x -> last_spec_eq y.

Lemma last_eqP : forall (s: list T), last_spec_eq s.

Lemma nth0 : forall l, nth x0 l 0 = head x0 l.

Lemma nth_default : forall s n, length s <= n -> nth x0 s n = x0.

Lemma nth_nil : forall n, nth x0 nil n = x0.

Lemma last_nth : forall x s, last x s = nth x0 (x :: s) (length s).

Lemma nth_last : forall s, nth x0 s (length s - 1) = last x0 s.

Lemma nth_behead : forall s n, nth x0 (behead s) n = nth x0 s (S n).

Lemma nth_app : forall s1 s2 n,
 nth x0 (s1 ++ s2) n = if ltn n (length s1) then nth x0 s1 n else nth x0 s2 (n - length s1).

Lemma nth_snoc : forall s x n,
  nth x0 (snoc s x) n = (if n < length s then nth x0 s n else if n == length s then x else x0).

Lemma nth_ncons : forall m x s n,
  nth x0 (ncons m x s) n = (if ltn n m then x else nth x0 s (n - m)).

Lemma nth_nlist : forall m x n, nth x0 (nlist m x) n = (if ltn n m then x else x0).

Lemma eq_from_nth : forall s1 s2
  (EQlength: length s1 = length s2)
  (EQnth: forall i, i < length s1 -> nth x0 s1 i = nth x0 s2 i),
  s1 = s2.

Lemma length_set_nth :
  forall s n y, length (set_nth x0 s n y) = (if ltn n (length s) then length s else S n).

Lemma set_nth_nil : forall n y, set_nth x0 nil n y = ncons n x0 (y :: nil).


Lemma onth0 : forall l, onth l 0 = ohead l.

Lemma onth_none : forall s n, length s <= n -> onth s n = None.

Lemma onth_nil : forall n, onth nil n = None (A:=T).

Lemma olast_nth : forall s, olast s = onth s (length s - 1).

Lemma onth_last : forall s, onth s (length s - 1) = olast s.

Lemma onth_behead : forall s n, onth (behead s) n = onth s (S n).

Lemma onth_app : forall s1 s2 n,
 onth (s1 ++ s2) n = if n < (length s1) then onth s1 n else onth s2 (n - length s1).

Lemma onth_snoc : forall s x n,
  onth (snoc s x) n = (if n < length s then onth s n else if n == length s then Some x else None).

Lemma onth_ncons : forall m x s n,
  onth (ncons m x s) n = (if n < m then Some x else onth s (n - m)).

Lemma onth_nlist : forall m x n, onth (nlist m x) n = (if n < m then Some x else None).

Lemma eq_from_onth : forall s1 s2
  (EQnth: forall i, onth s1 i = onth s2 i),
  s1 = s2.

Lemma length_oset_nth :
  forall s n y s' (EQ: oset_nth s n y = Some s'), length s' = length s.

Lemma oset_nth_nil : forall n y, oset_nth nil n y = None.

End SequencesBasic.

Hint Rewrite
  length_behead length_ncons length_nlist length_app length_snoc length_belast
  appl0 last_app last_snoc belast_app belast_snoc app_snoc snoc_app : vlib.

Hint Rewrite
  nth_nil nth_behead nth_app nth_snoc nth_ncons nth_nlist
  length_set_nth set_nth_nil : vlib.

Section SeqFind.

Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Types s l : (list T).

Variable f : pred T.

Lemma count_filter : forall l, count f l = length (filter f l).

Lemma has_count : forall l, has f l = ltn 0 (count f l).

Lemma count_length : forall l, count f l <= length l.

Lemma all_count : forall l, all f l = (count f l == length l).

Lemma all_filterP : forall s, reflect (filter f s = s) (all f s).

Lemma has_find : forall l, has f l = ltn (find f l) (length l).

Lemma find_length : forall l, find f l <= length l.

Lemma find_app : forall s1 s2,
  find f (s1 ++ s2) = if has f s1 then find f s1 else length s1 + find f s2.

Lemma has_nil : has f nil = false.

Lemma has_list1 : forall x, has f (x :: nil) = f x.

Lemma all_nil : all f nil = true.

Lemma all_list1 : forall x, all f (x :: nil) = f x.

Lemma nth_find : forall s, has f s -> f (nth x0 s (find f s)).

Lemma before_find : forall s i, i < find f s -> f (nth x0 s i) = false.

Lemma filter_app:
  forall l1 l2, filter f (l1 ++ l2) = filter f l1 ++ filter f l2.

Lemma filter_snoc : forall s x,
  filter f (snoc s x) = if f x then snoc (filter f s) x else filter f s.

Lemma count_app : forall s1 s2, count f (s1 ++ s2) = count f s1 + count f s2.

Lemma has_app : forall s1 s2, has f (s1 ++ s2) = has f s1 || has f s2.

Lemma has_snoc : forall s x, has f (snoc s x) = f x || has f s.

Lemma all_app : forall s1 s2, all f (s1 ++ s2) = all f s1 && all f s2.

Lemma all_snoc : forall s x, all f (snoc s x) = f x && all f s.

Lemma filter_pred0 : forall s, filter pred0 s = nil.

Lemma filter_predT : forall s, filter predT s = s.

Lemma filter_predI : forall a1 a2 s,
  filter (predI a1 a2) s = filter a1 (filter a2 s).

Lemma count_pred0 : forall s, count pred0 s = 0.

Lemma count_predT : forall s, count predT s = length s.

Lemma count_predUI : forall a1 a2 l,
 count (predU a1 a2) l + count (predI a1 a2) l = count a1 l + count a2 l.

Lemma count_predC : forall a l, count a l + count (predC a) l = length l.

Lemma has_pred0 : forall s, has pred0 s = false.

Lemma has_predT : forall s, has predT s = (0 < length s).

Lemma has_predC : forall a l, has (predC a) l = negb (all a l).

Lemma has_predU : forall a1 a2 l, has (predU a1 a2) l = has a1 l || has a2 l.

Lemma all_pred0 : forall l, all pred0 l = (length l == 0).

Lemma all_predT : forall s, all predT s = true.

Lemma all_predC : forall a s, all (predC a) s = negb (has a s).

Lemma all_predI : forall a1 a2 s, all (predI a1 a2) s = all a1 s && all a2 s.

Section EqLemmas.

Variables (a1 a2 : pred T).
Variable (EQ : a1 =1 a2).

Lemma eq_find : find a1 =1 find a2.

Lemma eq_filter : filter a1 =1 filter a2.

Lemma eq_count : count a1 =1 count a2.

Lemma eq_has : has a1 =1 has a2.

Lemma eq_all : all a1 =1 all a2.

End EqLemmas.

End SeqFind.

Hint Rewrite
  count_length find_length filter_app filter_snoc
  count_app has_app has_snoc all_app all_snoc : vlib.

Hint Rewrite has_pred0 : vlib.

Section SequenceSurgery.

Variable n0 : nat. Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Types s l : (list T).

Lemma drop_behead : drop n0 =1 iter n0 (@behead T).

Lemma drop0 : forall s, drop 0 s = s.

Hint Rewrite drop0 : vlib.
Lemma drop1 : forall l, drop 1 l = behead l.

Lemma drop_overlength : forall n s, length s <= n -> drop n s = nil.
Implicit Arguments drop_overlength [n s].

Lemma drop_length : forall s, drop (length s) s = nil.

Lemma drop_cons : forall x s,
  drop n0 (x :: s) = (match n0 with O => x :: s | S n => drop n s end).

Lemma length_drop : forall s, length (drop n0 s) = length s - n0.

Lemma drop_app : forall s1 s2,
 drop n0 (s1 ++ s2) =
   if ltn n0 (length s1) then drop n0 s1 ++ s2 else drop (n0 - length s1) s2.

Lemma drop_length_app : forall n s1 s2, length s1 = n -> drop n (s1 ++ s2) = s2.

Lemma nconsK : forall n x, cancel (ncons n x) (drop n).

Lemma take0 : forall s, take 0 s = nil.

Hint Rewrite take0 : vlib.
Lemma take_overlength : forall n s, length s <= n -> take n s = s.
Implicit Arguments take_overlength [n s].

Lemma take_length : forall s, take (length s) s = s.

Lemma take_cons : forall x s,
  take n0 (x :: s) = (match n0 with O => nil | S n => x :: take n s end).

Lemma drop_snoc : forall s, n0 <= length s ->
  forall x, drop n0 (snoc s x) = snoc (drop n0 s) x.

Lemma app_take_drop : forall s, take n0 s ++ drop n0 s = s.

Lemma length_takel : forall s (H: n0 <= length s), length (take n0 s) = n0.

Lemma length_take : forall s,
  length (take n0 s) = if ltn n0 (length s) then n0 else length s.

Lemma take_app : forall s1 s2,
 take n0 (s1 ++ s2) =
   if ltn n0 (length s1) then take n0 s1 else s1 ++ take (n0 - length s1) s2.

Lemma take_length_app : forall n s1 s2, length s1 = n -> take n (s1 ++ s2) = s1.

Lemma takel_app : forall s1, n0 <= length s1 ->
  forall s2, take n0 (s1 ++ s2) = take n0 s1.

Lemma nth_drop : forall s i, nth x0 (drop n0 s) i = nth x0 s (n0 + i).

Lemma nth_take : forall i, i < n0 -> forall s, nth x0 (take n0 s) i = nth x0 s i.


Lemma drop_nth : forall n s, n < length s -> drop n s = nth x0 s n :: drop (S n) s.

Lemma take_nth : forall n s, n < length s ->
  take (S n) s = snoc (take n s) (nth x0 s n).

Lemma rot0 : forall s, rot 0 s = s.

Lemma length_rot : forall s, length (rot n0 s) = length s.

Lemma rot_overlength : forall n s (H: length s <= n), rot n s = s.

Lemma rot_length : forall s, rot (length s) s = s.

Lemma has_rot : forall l f, has f (rot n0 l) = has f l.

Lemma all_rot : forall l f, all f (rot n0 l) = all f l.

Lemma rot_length_app : forall s1 s2, rot (length s1) (s1 ++ s2) = s2 ++ s1.

Lemma rotK : forall l, rotr n0 (rot n0 l) = l.

Lemma rot_inj : injective (@rot T n0).

Lemma rot1_cons : forall x s, rot 1 (x :: s) = snoc s x.

End SequenceSurgery.

Hint Rewrite drop0 drop_length length_drop : vlib.
Hint Rewrite take0 take_length length_take : vlib.
Hint Rewrite nth_drop : vlib.
Hint Rewrite rot0 length_rot rot_length has_rot all_rot rot_length_app rotK rot1_cons : vlib.

Section Rev.

Variable T : Type.
Implicit Type s : list T.

Lemma rev_nil : rev nil = (@nil T).

Lemma rev_snoc : forall s x, rev (snoc s x) = x :: (rev s).

Lemma rev_cons : forall x s, rev (x :: s) = snoc (rev s) x.

Lemma length_rev : forall s, length (rev s) = length s.

Lemma rev_app : forall s1 s2, rev (s1 ++ s2) = rev s2 ++ rev s1.

Lemma rev_rev : forall s, rev (rev s) = s.

Lemma nth_rev : forall x0 n s,
  n < length s -> nth x0 (rev s) n = nth x0 s (length s - S n).

End Rev.

Hint Rewrite rev_snoc rev_cons length_rev rev_app rev_rev : vlib.