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 : ∀ s, length s = 0 → s = nil.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma snoc_app : ∀ 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 : ∀ s, last_spec s.

Lemma last_ind :
  ∀ P (Hnil: P nil) (Hlast: ∀ 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 : ∀ (s: list T), last_spec_eq s.

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

Lemma nth_default : ∀ s n, length s ≤ n → nth x0 s n = x0.

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

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

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

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

Lemma nth_app : ∀ 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 : ∀ 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 : ∀ 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 : ∀ m x n, nth x0 (nlist m x) n = (if ltn n m then x else x0).

Lemma eq_from_nth : ∀ s1 s2
  (EQlength: length s1 = length s2)
  (EQnth: ∀ i, i < length s1 → nth x0 s1 i = nth x0 s2 i),
  s1 = s2.

Lemma length_set_nth :
  ∀ 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 : ∀ n y, set_nth x0 nil n y = ncons n x0 (y :: nil).


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

Lemma onth_none : ∀ s n, length s ≤ n → onth s n = None.

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

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

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

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

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

Lemma onth_snoc : ∀ 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 : ∀ m x s n,
  onth (ncons m x s) n = (if n < m then Some x else onth s (n - m)).

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

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

Lemma length_oset_nth :
  ∀ s n y s´ (EQ: oset_nth s n y = Some s´), length s´ = length s.

Lemma oset_nth_nil : ∀ 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 : ∀ l, count f l = length (filter f l).

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

Lemma count_length : ∀ l, count f l ≤ length l.

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

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

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

Lemma find_length : ∀ l, find f l ≤ length l.

Lemma find_app : ∀ 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 : ∀ x, has f (x :: nil) = f x.

Lemma all_nil : all f nil = true.

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

Lemma nth_find : ∀ s, has f s → f (nth x0 s (find f s)).

Lemma before_find : ∀ s i, i < find f s → f (nth x0 s i) = false.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma all_predI : ∀ 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 : ∀ s, drop 0 s = s.

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

Lemma drop_overlength : ∀ n s, length s ≤ n → drop n s = nil.
Implicit Arguments drop_overlength [n s].

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

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

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

Lemma drop_app : ∀ 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 : ∀ n s1 s2, length s1 = n → drop n (s1 ++ s2) = s2.

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

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

Hint Rewrite take0 : vlib.
Lemma take_overlength : ∀ n s, length s ≤ n → take n s = s.
Implicit Arguments take_overlength [n s].

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

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

Lemma drop_snoc : ∀ s, n0 ≤ length s →
  ∀ x, drop n0 (snoc s x) = snoc (drop n0 s) x.

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

Lemma length_takel : ∀ s (H: n0 ≤ length s), length (take n0 s) = n0.

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

Lemma take_app : ∀ 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 : ∀ n s1 s2, length s1 = n → take n (s1 ++ s2) = s1.

Lemma takel_app : ∀ s1, n0 ≤ length s1 →
  ∀ s2, take n0 (s1 ++ s2) = take n0 s1.

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

Lemma nth_take : ∀ i, i < n0 → ∀ s, nth x0 (take n0 s) i = nth x0 s i.


Lemma drop_nth : ∀ n s, n < length s → drop n s = nth x0 s n :: drop (S n) s.

Lemma take_nth : ∀ n s, n < length s →
  take (S n) s = snoc (take n s) (nth x0 s n).

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

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

Lemma rot_overlength : ∀ n s (H: length s ≤ n), rot n s = s.

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

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

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

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

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

Lemma rot_inj : injective (@rot T n0).

Lemma rot1_cons : ∀ 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 : ∀ s x, rev (snoc s x) = x :: (rev s).

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

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

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

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

Lemma nth_rev : ∀ 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.