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

Set Implicit Arguments.

Open Scope bool_scope.
Open Scope list_scope.

Lemma has_psplit (A : Type) (p : pred A) (s : list A) (x : A) :
  has p s ->
  s = take (find p s) s ++ nth x s (find p s) :: drop (S (find p s)) s.

Section EqSeq.

Variables (n0 : nat) (T : eqType) (x0 : T).
Notation Local nth := (nth x0).
Implicit Type s : list T.
Implicit Types x y z : T.

Fixpoint eqlist s1 s2 {struct s2} :=
  match s1, s2 with
  | nil, nil => true
  | x1 :: s1', x2 :: s2' => (x1 == x2) && eqlist s1' s2'
  | _, _ => false
  end.

Lemma eqlistP : Equality.axiom eqlist.

Canonical Structure list_eqMixin := EqMixin eqlistP.
Canonical Structure list_eqType := Eval hnf in EqType _ list_eqMixin.

Lemma eqlistE : eqlist = eq_op.

Lemma eqlist_cons : forall x1 x2 s1 s2,
  (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).

Lemma eqlist_app : forall s1 s2 s3 s4,
  length s1 = length s2 -> (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).

Lemma eqlist_rev2 : forall l1 l2,
  (rev l1 == rev l2) = (l1 == l2).

Lemma eqlist_snoc : forall s1 s2 x1 x2,
  (snoc s1 x1 == snoc s2 x2) = (s1 == s2) && (x1 == x2).

Lemma has_filter : forall a s, has a s = (filter a s != nil).

Lemma length_eq0 : forall l, (length l == 0) = (l == nil).


Fixpoint mem_list (s : list T) :=
  match s with
    | nil => (fun _ => false)
    | y :: s' => (fun x => (x == y) || mem_list s' x)
  end.

Definition eqlist_class := list T.
Identity Coercion list_of_eqlist : eqlist_class >-> list.

Coercion pred_of_eq_list (s : eqlist_class) : pred_class := (fun x => mem_list s x).

Canonical Structure list_predType := @mkPredType T (list T) pred_of_eq_list.
Canonical Structure mem_list_predType := mkPredType mem_list.

Lemma in_cons : forall y s x, (x \in y :: s) = (x == y) || (x \in s).

Hint Rewrite in_cons: vlib.
Lemma in_nil : forall x, (x \in nil) = false.

Lemma mem_list1 : forall x y, (x \in y :: nil) = (x == y).



Lemma mem_app : forall x s1 s2, (x \in s1 ++ s2) = (x \in s1) || (x \in s2).

Lemma mem_snoc : forall s y, snoc s y =i y :: s.

Lemma mem_head : forall x s, x \in x :: s.

Lemma mem_last : forall x s, last x s \in x :: s.

Lemma mem_behead : forall s, {subset behead s <= s}.

Lemma mem_belast : forall s y, {subset belast y s <= y :: s}.

Lemma mem_nth : forall s n, n < length s -> nth s n \in s.

Lemma mem_take : forall s x, x \in take n0 s -> x \in s.

Lemma mem_drop : forall s x, x \in drop n0 s -> x \in s.

Lemma mem_rev : forall s, rev s =i s.

Lemma in_head : forall x l, x \in x :: l.

Lemma in_behead : forall x y l, x \in l -> x \in y :: l.

Lemma in_consE : forall {x y l}, x \in y :: l -> {x = y} + {x \in l}.

Lemma in_split : forall x l, x \in l -> exists l1 l2, l = l1 ++ x :: l2.

Ltac clarify2 :=
  vlib__clarify1;
  repeat match goal with
    | H1: ?x = Some _, H2: ?x = None |- _ => rewrite H2 in H1; discriminate
    | H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; vlib__clarify1
  end; try done.

Lemma inP :
  forall x l , reflect (In x l) (x \in l).

Section Filters.

Variable a : pred T.

Lemma hasP : forall l, reflect (exists2 x, x \in l & a x) (has a l).

Lemma hasPn : forall l, reflect (forall x, x \in l -> negb (a x)) (negb (has a l)).

Lemma allP : forall l, reflect (forall x, x \in l -> a x) (all a l).

Lemma allPn : forall l, reflect (exists2 x, x \in l & negb (a x)) (negb (all a l)).

Lemma mem_filter : forall x l, (x \in filter a l) = a x && (x \in l).

End Filters.

Lemma eq_in_filter : forall (a1 a2 : pred T) s,
  {in s, a1 =1 a2} -> filter a1 s = filter a2 s.

Lemma eq_has_r : forall s1 s2 (EQ: s1 =i s2) f, has f s1 = has f s2.

Lemma eq_all_r : forall s1 s2 (EQ: s1 =i s2) f, all f s1 = all f s2.

Lemma has_sym : forall s1 s2, has (mem s1) s2 = has (mem s2) s1.

Lemma has_pred1 : forall x l, has (fun y => y == x) l = (x \in l).

Definition constant s :=
  match s with
    | nil => true
    | x :: s' => all (fun y => y == x) s'
  end.

Lemma all_pred1P x s :
  reflect (s = nlist (length s) x) (all (fun y => y == x) s).

Lemma all_pred1_constant x s : all (fun y => y == x) s -> constant s.

Implicit Arguments all_pred1_constant [].

Lemma all_pred1_nlist : forall x y n,
  all (fun y => y == x) (nlist n y) = ((n == 0) || (x == y)).

Lemma constant_nlist : forall n x, constant (nlist n x).

Lemma constantP : forall s,
  reflect (exists x, s = nlist (length s) x) (constant s).


Fixpoint uniq s :=
  match s with
    | nil => true
    | x :: s' => (x \notin s') && uniq s'
  end.

Lemma cons_uniq : forall x s, uniq (x :: s) = (x \notin s) && uniq s.

Lemma app_uniq : forall s1 s2,
  uniq (s1 ++ s2) = uniq s1 && negb (has (mem s1) s2) && uniq s2.

Lemma uniq_appC : forall s1 s2, uniq (s1 ++ s2) = uniq (s2 ++ s1).

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

Lemma snoc_uniq : forall s x, uniq (snoc s x) = (x \notin s) && uniq s.

Lemma filter_uniq : forall s a, uniq s -> uniq (filter a s).

Lemma rot_uniq : forall s, uniq (rot n0 s) = uniq s.

Lemma rev_uniq : forall s, uniq (rev s) = uniq s.

Lemma count_uniq_mem :
  forall s x, uniq s -> count (fun y => y == x) s = if (x \in s) then 1 else 0.

Lemma in_split_uniq :
  forall x l,
    x \in l -> uniq l ->
    exists l1 l2, l = l1 ++ x :: l2 /\
      uniq (l1 ++ l2) /\ x \notin (l1 ++ l2).


Fixpoint undup s :=
  match s with
    | nil => nil
    | x :: s' => if x \in s' then undup s' else x :: undup s'
  end.

Lemma length_undup : forall s, length (undup s) <= length s.

Lemma mem_undup : forall s, undup s =i s.

Hint Rewrite mem_undup : vlib.

Lemma undup_uniq : forall s, uniq (undup s).

Lemma undup_id : forall s, uniq s -> undup s = s.

Lemma ltn_length_undup : forall s, (length (undup s) < length s) = negb (uniq s).


Definition index x := find (fun y => y == x).

Lemma index_length : forall x s, index x s <= length s.

Lemma index_mem : forall x s, (index x s < length s) = (x \in s).

Lemma nth_index : forall x s, x \in s -> nth s (index x s) = x.

Lemma index_app : forall x s1 s2,
 index x (s1 ++ s2) = if x \in s1 then index x s1 else length s1 + index x s2.

Lemma index_uniq : forall i s, i < length s -> uniq s -> index (nth s i) s = i.

Lemma index_head : forall x s, index x (x :: s) = 0.

Lemma index_last : forall x s,
  uniq (x :: s) -> index (last x s) (x :: s) = length s.

Lemma nth_uniq : forall s i j,
   i < length s -> j < length s -> uniq s -> (nth s i == nth s j) = (i == j).

Lemma mem_rot : forall s, rot n0 s =i s.

Lemma eqlist_rot : forall s1 s2, (rot n0 s1 == rot n0 s2) = (s1 == s2).

Inductive rot_to_spec (s : list T) (x : T) : Type :=
  RotToSpec i s' (_ : rot i s = x :: s').

Lemma rot_to : forall s x, x \in s -> rot_to_spec s x.

End EqSeq.



Implicit Arguments eqlistP [T x y].
Implicit Arguments all_filterP [T f s].
Implicit Arguments hasP [T a l].
Implicit Arguments hasPn [T a l].
Implicit Arguments allP [T a l].
Implicit Arguments allPn [T a l].
Implicit Arguments index [T].
Implicit Arguments uniq [T].

Hint Rewrite in_cons in_cons mem_app mem_filter mem_rot : vlib.
Hint Resolve in_head in_behead : vlib.
Hint Resolve undup_uniq : vlib.

Section NlistthTheory.

Lemma nthP : forall (T : eqType) (s : list T) x x0,
  reflect (exists2 i, i < length s & nth x0 s i = x) (x \in s).

Variable T : Type.

Lemma has_nthP : forall (a : pred T) s x0,
  reflect (exists2 i, i < length s & a (nth x0 s i)) (has a s).

Lemma all_nthP : forall (a : pred T) s x0,
  reflect (forall i, i < length s -> a (nth x0 s i)) (all a s).

End NlistthTheory.

Lemma set_nth_default : forall T s (y0 x0 : T) n,
  n < length s -> nth x0 s n = nth y0 s n.

Lemma headI : forall T s (x : T),
  snoc s x = head x s :: behead (snoc s x).

Implicit Arguments nthP [T s x].
Implicit Arguments has_nthP [T a s].
Implicit Arguments all_nthP [T a s].



Fixpoint incr_nth (v : list nat) (i : nat) {struct i} : list nat :=
  match v, i with
    | n :: v', 0 => S n :: v'
    | n :: v', S i' => n :: incr_nth v' i'
    | nil, _ => ncons i 0 (1 :: nil)
  end.

Lemma nth_incr_nth : forall v i j,
  nth 0 (incr_nth v i) j = (if i == j then 1 else 0) + nth 0 v j.

Lemma length_incr_nth : forall v i,
  length (incr_nth v i) = if i < length v then length v else S i.


Section PermSeq.

Variable T : eqType.

Notation cou1 := (fun x => count (fun y => y == x)).

Definition same_count1 (s1 s2 : list T) x :=
   count (fun y => y == x) s1 == count (fun y => y == x) s2.

Definition perm_eq (s1 s2 : list T) := all (same_count1 s1 s2) (s1 ++ s2).

Lemma perm_eqP_weak : forall s1 s2,
  reflect (cou1 ^~ s1 =1 cou1 ^~ s2) (perm_eq s1 s2).

Lemma perm_eq_refl : forall s, perm_eq s s.
Hint Resolve perm_eq_refl.

Lemma perm_eq_sym : symmetric perm_eq.

Lemma perm_eq_trans : transitive perm_eq.

Notation perm_eql := (fun s1 s2 => perm_eq s1 =1 perm_eq s2).
Notation perm_eqr := (fun s1 s2 => perm_eq^~ s1 =1 perm_eq^~ s2).

Lemma perm_eqlP : forall s1 s2, reflect (perm_eql s1 s2) (perm_eq s1 s2).

Lemma perm_eqrP : forall s1 s2, reflect (perm_eqr s1 s2) (perm_eq s1 s2).

Lemma perm_appC : forall s1 s2, perm_eql (s1 ++ s2) (s2 ++ s1).

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

Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.

Lemma perm_app2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.

Lemma perm_appAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).

Lemma perm_appCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).

Lemma perm_snoc : forall x s, perm_eql (snoc s x) (x :: s).

Lemma perm_rot : forall n s, perm_eql (rot n s) s.

Lemma perm_rotr : forall n s, perm_eql (rotr n s) s.

Lemma perm_eq_mem : forall s1 s2, perm_eq s1 s2 -> s1 =i s2.

Lemma perm_eq_nilD : forall s, perm_eq nil s -> s = nil.

Lemma perm_eq_consD : forall x s1 s2,
  perm_eq (x :: s1) s2 -> exists sa sb, s2 = sa ++ x :: sb /\ perm_eq s1 (sa ++ sb).

Lemma perm_eqD : forall s1 s2 (EQ: perm_eq s1 s2) f, count f s1 = count f s2.

Lemma perm_eq_length : forall s1 s2, perm_eq s1 s2 -> length s1 = length s2.

Lemma perm_eqP s1 s2 :
  reflect ((@count _) ^~ s1 =1 (@count _) ^~ s2) (perm_eq s1 s2).

Lemma uniq_leq_length : forall s1 s2 : list T,
  uniq s1 -> {subset s1 <= s2} -> length s1 <= length s2.

Lemma leq_length_uniq : forall s1 s2 : list T,
  uniq s1 -> {subset s1 <= s2} -> length s2 <= length s1 -> uniq s2.

Lemma uniq_length_uniq : forall s1 s2 : list T,
  uniq s1 -> s1 =i s2 -> uniq s2 = (length s2 == length s1).

Lemma leq_length_perm : forall s1 s2 : list T,
  uniq s1 -> {subset s1 <= s2} ->
  length s2 <= length s1 ->
  s1 =i s2 /\ length s1 = length s2.

Lemma perm_uniq : forall s1 s2 : list T,
  s1 =i s2 -> length s1 = length s2 -> uniq s1 = uniq s2.

Lemma perm_eq_uniq : forall s1 s2, perm_eq s1 s2 -> uniq s1 = uniq s2.

Lemma uniq_perm_eq : forall s1 s2,
  uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2.

Lemma count_mem_uniq : forall s : list T,
  (forall x, count (fun y => y == x) s = if (x \in s) then 1 else 0) -> uniq s.

End PermSeq.

Section RotrLemmas.

Variables (n0 : nat) (T : Type) (T' : eqType).

Lemma length_rotr : forall s : list T, length (rotr n0 s) = length s.

Lemma mem_rotr : forall s : list T', rotr n0 s =i s.

Lemma rotr_size_app : forall s1 s2 : list T,
  rotr (length s2) (s1 ++ s2) = s2 ++ s1.

Lemma rotr1_snoc : forall x (s : list T), rotr 1 (snoc s x) = x :: s.

Lemma has_rotr : forall f (s : list T), has f (rotr n0 s) = has f s.

Lemma rotr_uniq : forall s : list T', uniq (rotr n0 s) = uniq s.

Lemma rotrK : cancel (rotr n0) (@rot T n0).

Lemma rotr_inj : injective (@rotr T n0).

Lemma rev_rot : forall s : list T, rev (rot n0 s) = rotr n0 (rev s).

Lemma rev_rotr : forall s : list T, rev (rotr n0 s) = rot n0 (rev s).

End RotrLemmas.

Hint Rewrite length_rotr rotr_size_app rotr1_snoc has_rotr : vlib.


Section Sieve.

Variables (n0 : nat) (T : Type).

Implicit Types l s : list T.

Lemma sieve_false : forall s n, sieve (nlist n false) s = nil.

Lemma sieve_true : forall s n, length s <= n -> sieve (nlist n true) s = s.

Lemma sieve0 : forall m, sieve m nil = (@nil T).


Lemma sieve_cons : forall b m x s,
  sieve (b :: m) (x :: s) = (if b then (x :: nil) else nil) ++ sieve m s.

Lemma length_sieve : forall m s,
  length m = length s -> length (sieve m s) = count id m.

Lemma sieve_app : forall m1 s1, length m1 = length s1 ->
  forall m2 s2, sieve (m1 ++ m2) (s1 ++ s2) = sieve m1 s1 ++ sieve m2 s2.

Lemma has_sieve_cons : forall a b m x s,
  has a (sieve (b :: m) (x :: s)) = b && a x || has a (sieve m s).

Lemma sieve_rot : forall m s, length m = length s ->
 sieve (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (sieve m s).

End Sieve.

Section EqSieve.

Variables (n0 : nat) (T : eqType).

Lemma mem_sieve_cons x b m y (s : list T) :
  (x \in sieve (b :: m) (y :: s)) = b && (x == y) || (x \in sieve m s).

Lemma mem_sieve : forall x m (s : list T), (x \in sieve m s) -> (x \in s).

Lemma sieve_uniq : forall s : list T, uniq s -> forall m, uniq (sieve m s).

Lemma mem_sieve_rot : forall m (s : list T), length m = length s ->
  sieve (rot n0 m) (rot n0 s) =i sieve m s.

End EqSieve.

Section Map.

Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2) (f : T1 -> T2).

Fixpoint map (l : list T1) : list T2 :=
  match l with
    | nil => nil
    | x :: l => f x :: map l
  end.

Lemma map_cons : forall x s, map (x :: s) = f x :: map s.

Lemma map_nlist : forall x, map (nlist n0 x) = nlist n0 (f x).

Lemma map_app : forall s1 s2, map (s1 ++ s2) = map s1 ++ map s2.

Lemma map_snoc : forall s x, map (snoc s x) = snoc (map s) (f x).

Lemma length_map : forall l, length (map l) = length l.

Lemma behead_map : forall l, behead (map l) = map (behead l).

Lemma nth_map : forall n l, n < length l -> nth x2 (map l) n = f (nth x1 l n).

Lemma last_map : forall s x, last (f x) (map s) = f (last x s).

Lemma belast_map : forall s x, belast (f x) (map s) = map (belast x s).

Lemma filter_map a s : filter a (map s) = map (filter (preim f a) s).

Lemma find_map a s : find a (map s) = find (preim f a) s.

Lemma has_map a s : has a (map s) = has (preim f a) s.

Lemma count_map a s : count a (map s) = count (preim f a) s.

Lemma map_take s : map (take n0 s) = take n0 (map s).

Lemma map_drop s : map (drop n0 s) = drop n0 (map s).

Lemma map_rot s : map (rot n0 s) = rot n0 (map s).

Lemma map_rotr s : map (rotr n0 s) = rotr n0 (map s).

Lemma map_rev s : map (rev s) = rev (map s).

Lemma map_sieve m s : map (sieve m s) = sieve m (map s).

Lemma inj_map (Hf : injective f) : injective map.

End Map.

Hint Rewrite map_nlist map_app map_snoc length_map
  behead_map last_map belast_map map_take map_drop
  map_rot map_rev map_sieve map_rotr : vlib.

Section Map2.

Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2).
Variables (T3 : Type) (f : T1 -> T2 -> T3).

Fixpoint map2 (l1 : list T1) (l2 : list T2) {struct l1}: list T3 :=
  match l1, l2 with
    | nil, _ => nil
    | x1 :: l1, nil => nil
    | x1 :: l1, x2 :: l2 => f x1 x2 :: map2 l1 l2
  end.

Lemma map2_0l : forall l, map2 nil l = nil.
Lemma map2_l0 : forall l, map2 l nil = nil.

Lemma map2_cons : forall x1 l1 x2 l2, map2 (x1 :: l1) (x2 :: l2) = f x1 x2 :: map2 l1 l2.

Lemma map2_nlist : forall x y, map2 (nlist n0 x) (nlist n0 y) = nlist n0 (f x y).

Lemma map2_app : forall s1 s2 t1 t2 (Leq: length s1 = length t1),
  map2 (s1 ++ s2) (t1 ++ t2) = map2 s1 t1 ++ map2 s2 t2.

Lemma length_map2_eq : forall l1 l2, length l1 = length l2 ->
  length (map2 l1 l2) = (length l1).

Lemma map2_take :
  forall l1 l2, map2 (take n0 l1) (take n0 l2) = take n0 (map2 l1 l2).

Lemma map2_drop :
  forall l1 l2, map2 (drop n0 l1) (drop n0 l2) = drop n0 (map2 l1 l2).

Lemma map2_rot l1 l2 (Leq: length l1 = length l2) :
    map2 (rot n0 l1) (rot n0 l2) = rot n0 (map2 l1 l2).

End Map2.

Lemma map2I :
  forall {T1} {f: T1 -> T1 -> T1} (Cf: forall x, f x x = x) x,
    map2 f x x = x.

Lemma map2C :
  forall {T1 T2} {f: T1 -> T1 -> T2} (Cf: forall x y, f x y = f y x) x y,
    map2 f x y = map2 f y x.

Lemma map2A :
  forall {T1} {f: T1 -> T1 -> T1} (Cf: forall x y z, f x (f y z) = f (f x y) z) x y z,
    map2 f x (map2 f y z) = map2 f (map2 f x y) z.

Lemma map2K :
  forall {T1 T2} {f: T1 -> T1 -> T2} {v} (Cf: forall x, f x x = v) x,
    map2 f x x = nlist (length x) v.

Lemma map2Kl :
  forall {T1 T2 T3} {f: T1 -> T2 -> T3} {v1 v2} (Cf: forall x, f v1 x = v2)
    n x (Leq: length x = n),
    map2 f (nlist n v1) x = nlist n v2.

Lemma map2Il :
  forall {T1 T2} {f: T1 -> T2 -> T2} {v1} (Cf: forall x, f v1 x = x)
    n x (Leq: length x = n),
    map2 f (nlist n v1) x = x.

Lemma map2Sl :
  forall {T1 T2} {f: T1 -> T1 -> T2} {v g} (Cf: forall x, f v x = g x)
    n x (Leq: length x = n),
    map2 f (nlist n v) x = map g x.

Section EqMap.

Variables (n0 : nat) (T1 : eqType) (x1 : T1).
Variables (T2 : eqType) (x2 : T2) (f : T1 -> T2).

Lemma map_f : forall (s : list T1) x, x \in s -> f x \in map f s.

Lemma mapP : forall (s : list T1) y,
  reflect (exists2 x, x \in s & y = f x) (y \in map f s).

Lemma map_uniq : forall s, uniq (map f s) -> uniq s.

Lemma map_inj_in_uniq : forall s : list T1,
  {in s &, injective f} -> uniq (map f s) = uniq s.

Hypothesis Hf : injective f.

Lemma mem_map : forall s x, (f x \in map f s) = (x \in s).

Lemma index_map : forall s x, index (f x) (map f s) = index x s.

Lemma map_inj_uniq : forall s, uniq (map f s) = uniq s.

End EqMap.

Implicit Arguments mapP [T1 T2 f s y].

Lemma filter_sieve : forall T a (s : list T), filter a s = sieve (map a s) s.

Section MapComp.

Variable T1 T2 T3 : Type.

Lemma map_id : forall s : list T1, map id s = s.

Lemma eq_map : forall f1 f2 : T1 -> T2, f1 =1 f2 -> map f1 =1 map f2.

Lemma map_comp : forall (f1 : T2 -> T3) (f2 : T1 -> T2) s,
  map (f1 \o f2) s = map f1 (map f2 s).

Lemma mapK : forall (f1 : T1 -> T2) (f2 : T2 -> T1),
  cancel f1 f2 -> cancel (map f1) (map f2).

End MapComp.

Lemma eq_in_map : forall (T1 : eqType) T2 (f1 f2 : T1 -> T2) (s : list T1),
  {in s, f1 =1 f2} -> map f1 s = map f2 s.

Lemma map_id_in : forall (T : eqType) f (s : list T),
  {in s, f =1 id} -> map f s = s.


Section Pmap.

Variables (aT rT : Type) (f : aT -> option rT) (g : rT -> aT).

Fixpoint pmap s :=
  match s with
    | nil => nil
    | x :: s' => oapp ((@cons _)^~ (pmap s')) (pmap s') (f x)
  end.

Lemma map_pK : pcancel g f -> cancel (map g) pmap.

Lemma length_pmap s :
  length (pmap s) = count (fun x => match f x with None => false | Some _ => true end) s.

Lemma pmapS_filter s :
  map some (pmap s)
  = map f (filter (fun x => match f x with None => false | Some _ => true end) s).

Lemma pmap_filter (fK : ocancel f g) s :
  map g (pmap s) = filter (fun x => match f x with None => false | Some _ => true end) s.

End Pmap.

Lemma length_iota : forall m n, length (iota m n) = n.

Lemma iota_add : forall m n1 n2,
  iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.

Lemma iota_addl : forall m1 m2 n,
  iota (m1 + m2) n = map (plus m1) (iota m2 n).

Lemma nth_iota : forall n0 m n i, i < n -> nth n0 (iota m n) i = m + i.

Lemma mem_iota : forall m n i, (i \in iota m n) = (m <= i) && (i < m + n).

Lemma iota_uniq : forall m n, uniq (iota m n).

Hint Resolve iota_uniq : vlib.
Hint Rewrite length_iota mem_iota iota_uniq : vlib.


Section MakeSeq.

Variables (T : Type) (x0 : T).

Definition mklist f n : list T := map f (iota 0 n).

Lemma length_mklist : forall f n, length (mklist f n) = n.

Lemma eq_mklist : forall f g, f =1 g -> mklist f =1 mklist g.

Lemma nth_mklist : forall f n i, i < n -> nth x0 (mklist f n) i = f i.

Lemma mklist_nth : forall s, mklist (nth x0 s) (length s) = s.

End MakeSeq.

Lemma mklist_uniq : forall (T : eqType) (f : nat -> T) n,
  injective f -> uniq (mklist f n).

Section FoldRight.

Variables (T R : Type) (f : T -> R -> R).

Fixpoint foldr (l : list T) (z0: R) : R :=
  match l with
    | nil => z0
    | x :: l => f x (foldr l z0)
  end.

End FoldRight.

Section FoldRightComp.

Variables (T1 T2 : Type) (h : T1 -> T2).
Variables (R : Type) (f : T2 -> R -> R) (z0 : R).

Lemma foldr_app :
  forall s1 s2, foldr f (s1 ++ s2) z0 = foldr f s1 (foldr f s2 z0).

Lemma foldr_map :
  forall s : list T1, foldr f (map h s) z0 = foldr (fun x z => f (h x) z) s z0.

End FoldRightComp.

Definition sumn l := foldr plus l 0.

Lemma sumn_nil : sumn nil = 0.

Lemma sumn_cons : forall n l, sumn (n :: l) = n + sumn l.

Hint Rewrite sumn_nil sumn_cons : vlib.

Lemma sumn_nlist : forall x n : nat, sumn (nlist n x) = x * n.

Lemma sumn_app : forall s1 s2, sumn (s1 ++ s2) = sumn s1 + sumn s2.

Lemma natnlist0P : forall s : list nat,
  reflect (s = nlist (length s) 0) (sumn s == 0).

Section FoldLeft.

Variables (T R : Type) (f : R -> T -> R).

Fixpoint foldl z (l : list T) :=
  match l with
    | nil => z
    | x :: l => (foldl (f z x) l)
  end.

Lemma foldl_rev : forall z s, foldl z (rev s) = foldr (fun x z => f z x) s z.

Lemma foldl_app : forall z s1 s2, foldl z (s1 ++ s2) = foldl (foldl z s1) s2.

End FoldLeft.

Section Scan.

Variables (T1 : Type) (x1 : T1) (T2 : Type) (x2 : T2).
Variables (f : T1 -> T1 -> T2) (g : T1 -> T2 -> T1).

Fixpoint pairmap x (s : list T1) {struct s} :=
  match s with
    | nil => nil
    | y :: s' => f x y :: pairmap y s'
  end.

Lemma length_pairmap : forall x s, length (pairmap x s) = length s.

Lemma nth_pairmap : forall s n, n < length s ->
  forall x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n).

Fixpoint scanl x (s : list T2) {struct s} :=
  match s with
    | nil => nil
    | y :: s' => let x' := g x y in x' :: scanl x' s'
  end.

Lemma length_scanl : forall x s, length (scanl x s) = length s.

Lemma nth_scanl : forall s n, n < length s ->
  forall x, nth x1 (scanl x s) n = foldl g x (take (S n) s).

Lemma scanlK :
  (forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x).

Lemma pairmapK :
  (forall x, cancel (f x) (g x)) -> forall x, cancel (pairmap x) (scanl x).

End Scan.


Section Zip.

Variables T1 T2 : Type.

Fixpoint zip (s1 : list T1) (s2 : list T2) {struct s2} :=
  match s1, s2 with
  | x1 :: s1', x2 :: s2' => (x1,x2) :: zip s1' s2'
  | _, _ => nil
  end.

Definition unzip1 := map (@fst T1 T2).
Definition unzip2 := map (@snd T1 T2).

Lemma zip_unzip : forall s, zip (unzip1 s) (unzip2 s) = s.

Lemma unzip1_zip : forall s1 s2,
  length s1 <= length s2 -> unzip1 (zip s1 s2) = s1.

Lemma unzip2_zip : forall s1 s2,
  length s2 <= length s1 -> unzip2 (zip s1 s2) = s2.

Lemma length1_zip : forall s1 s2,
  length s1 <= length s2 -> length (zip s1 s2) = length s1.

Lemma length2_zip : forall s1 s2,
  length s2 <= length s1 -> length (zip s1 s2) = length s2.

End Zip.


Section Flatten.

Variable T : Type.

Definition flatten l := foldr (@app _) l (@nil T).
Definition shape := map (@length T).
Fixpoint reshape (sh : list nat) (s : list T) {struct sh} :=
  match sh with
    | nil => nil
    | n :: sh' => take n s :: reshape sh' (drop n s)
  end.

Lemma flatten_cons : forall l ll, flatten (l :: ll) = l ++ flatten ll.

Lemma flatten_app : forall l l', flatten (l ++ l') = flatten l ++ flatten l'.

Hint Rewrite flatten_cons flatten_app : vlib.

Lemma length_flatten : forall ss, length (flatten ss) = sumn (shape ss).

Lemma flattenK : forall ss, reshape (shape ss) (flatten ss) = ss.

Lemma reshapeKr : forall sh s, length s <= sumn sh -> flatten (reshape sh s) = s.

Lemma reshapeKl : forall sh s, length s >= sumn sh -> shape (reshape sh s) = sh.

End Flatten.


Inductive has_spec T (f : T -> bool) (l : list T) : Prop :=
  HasSpec (l1 l2: list T) (n : T) (EQ: l = l1 ++ n :: l2) (HOLDS : f n) (PREV: has f l1 = false).

Lemma hasD T (f : T -> bool) l (H: has f l): has_spec f l.

Inductive in_spec {T : eqType} (x : T) (l : list T) : Prop :=
  InSpec (l1 l2: list T) (EQ: l = l1 ++ x :: l2) (PREV: x \notin l1).

Lemma inD {T: eqType} {x: T} {l} (H: x \in l): in_spec x l.

Lemma uniqE (T: eqType) (l : list T) :
  uniq l <-> (forall n l1 l2 l3, l = l1 ++ n :: l2 ++ n :: l3 -> False).