Require Import Omega.
Require Import Vbase Vlistbase Varith.

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 : ∀ x1 x2 s1 s2,
  (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).

Lemma eqlist_app : ∀ s1 s2 s3 s4,
  length s1 = length s2 → (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).

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

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

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

Lemma length_eq0 : ∀ 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 : ∀ y s x, (x \in y :: s) = (x == y) || (x \in s).

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

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



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

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

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

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

Lemma mem_behead : ∀ s, {subset behead s ≤ s}.

Lemma mem_belast : ∀ s y, {subset belast y s ≤ y :: s}.

Lemma mem_nth : ∀ s n, n < length s → nth s n \in s.

Lemma mem_take : ∀ s x, x \in take n0 s → x \in s.

Lemma mem_drop : ∀ s x, x \in drop n0 s → x \in s.

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

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

Lemma in_behead : ∀ x y l, x \in l → x \in y :: l.

Lemma in_consE : ∀ {x y l}, x \in y :: l → {x = y} + {x \in l}.

Lemma in_split : ∀ x l, x \in l → ∃ 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 :
  ∀ x l , reflect (In x l) (x \in l).

Section Filters.

Variable a : pred T.

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

Lemma hasPn : ∀ l, reflect (∀ x, x \in l → negb (a x)) (negb (has a l)).

Lemma allP : ∀ l, reflect (∀ x, x \in l → a x) (all a l).

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

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

End Filters.
Lemma eq_has_r : ∀ s1 s2 (EQ: s1 =i s2) f, has f s1 = has f s2.

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

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

Lemma has_pred1 : ∀ 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 : ∀ x y n,
  all (fun y ⇒ y == x) (nlist n y) = ((n == 0) || (x == y)).

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

Lemma constantP : ∀ s,
  reflect (∃ 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 : ∀ x s, uniq (x :: s) = (x \notin s) && uniq s.

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

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

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

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

Lemma filter_uniq : ∀ s a, uniq s → uniq (filter a s).

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

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

Lemma count_uniq_mem :
  ∀ s x, uniq s → count (fun y ⇒ y == x) s = if (x \in s) then 1 else 0.

Lemma in_split_uniq :
  ∀ x l,
    x \in l → uniq l →
    ∃ 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 : ∀ s, length (undup s) ≤ length s.

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

Hint Rewrite mem_undup : vlib.

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

Lemma undup_id : ∀ s, uniq s → undup s = s.

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


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

Lemma index_length : ∀ x s, index x s ≤ length s.

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

Lemma nth_index : ∀ x s, x \in s → nth s (index x s) = x.

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

Lemma index_uniq : ∀ i s, i < length s → uniq s → index (nth s i) s = i.

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

Lemma index_last : ∀ x s,
  uniq (x :: s) → index (last x s) (x :: s) = length s.

Lemma nth_uniq : ∀ s i j,
   i < length s → j < length s → uniq s → (nth s i == nth s j) = (i == j).

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

Lemma eqlist_rot : ∀ 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 : ∀ 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 : ∀ (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 : ∀ (a : pred T) s x0,
  reflect (exists2 i, i < length s & a (nth x0 s i)) (has a s).

Lemma all_nthP : ∀ (a : pred T) s x0,
  reflect (∀ i, i < length s → a (nth x0 s i)) (all a s).

End NlistthTheory.

Lemma set_nth_default : ∀ T s (y0 x0 : T) n,
  n < length s → nth x0 s n = nth y0 s n.

Lemma headI : ∀ 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 : ∀ 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 : ∀ 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 : ∀ s1 s2,
  reflect (cou1 ^~ s1 =1 cou1 ^~ s2) (perm_eq s1 s2).

Lemma perm_eq_refl : ∀ 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 : ∀ s1 s2, reflect (perm_eql s1 s2) (perm_eq s1 s2).

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

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

Lemma perm_app2l : ∀ 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 : ∀ x s, perm_eql (snoc s x) (x :: s).

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

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

Lemma perm_eq_mem : ∀ s1 s2, perm_eq s1 s2 → s1 =i s2.

Lemma perm_eq_nilD : ∀ s, perm_eq nil s → s = nil.

Lemma perm_eq_consD : ∀ x s1 s2,
  perm_eq (x :: s1) s2 → ∃ sa sb, s2 = sa ++ x :: sb ∧ perm_eq s1 (sa ++ sb).

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

Lemma perm_eq_length : ∀ 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 : ∀ s1 s2 : list T,
  uniq s1 → {subset s1 ≤ s2} → length s1 ≤ length s2.

Lemma leq_length_uniq : ∀ s1 s2 : list T,
  uniq s1 → {subset s1 ≤ s2} → length s2 ≤ length s1 → uniq s2.

Lemma uniq_length_uniq : ∀ s1 s2 : list T,
  uniq s1 → s1 =i s2 → uniq s2 = (length s2 == length s1).

Lemma leq_length_perm : ∀ s1 s2 : list T,
  uniq s1 → {subset s1 ≤ s2} →
  length s2 ≤ length s1 →
  s1 =i s2 ∧ length s1 = length s2.

Lemma perm_uniq : ∀ s1 s2 : list T,
  s1 =i s2 → length s1 = length s2 → uniq s1 = uniq s2.

Lemma perm_eq_uniq : ∀ s1 s2, perm_eq s1 s2 → uniq s1 = uniq s2.

Lemma uniq_perm_eq : ∀ s1 s2,
  uniq s1 → uniq s2 → s1 =i s2 → perm_eq s1 s2.

Lemma count_mem_uniq : ∀ s : list T,
  (∀ 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 : ∀ s : list T, length (rotr n0 s) = length s.

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

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

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

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

Lemma rotr_uniq : ∀ 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 : ∀ s : list T, rev (rot n0 s) = rotr n0 (rev s).

Lemma rev_rotr : ∀ 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 : ∀ s n, sieve (nlist n false) s = nil.

Lemma sieve_true : ∀ s n, length s ≤ n → sieve (nlist n true) s = s.

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


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

Lemma length_sieve : ∀ m s,
  length m = length s → length (sieve m s) = count id m.

Lemma sieve_app : ∀ m1 s1, length m1 = length s1 →
  ∀ m2 s2, sieve (m1 ++ m2) (s1 ++ s2) = sieve m1 s1 ++ sieve m2 s2.

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

Lemma sieve_rot : ∀ 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 : ∀ x m (s : list T), (x \in sieve m s) → (x \in s).

Lemma sieve_uniq : ∀ s : list T, uniq s → ∀ m, uniq (sieve m s).

Lemma mem_sieve_rot : ∀ 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 : ∀ x s, map (x :: s) = f x :: map s.

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

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

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

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

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

Lemma nth_map : ∀ n l, n < length l → nth x2 (map l) n = f (nth x1 l n).

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

Lemma belast_map : ∀ 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 : ∀ l, map2 nil l = nil.
Lemma map2_l0 : ∀ l, map2 l nil = nil.

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

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

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

Lemma length_map2_eq : ∀ l1 l2, length l1 = length l2 →
  length (map2 l1 l2) = (length l1).

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

Lemma map2_drop :
  ∀ 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 :
  ∀ {T1} {f: T1 → T1 → T1} (Cf: ∀ x, f x x = x) x,
    map2 f x x = x.

Lemma map2C :
  ∀ {T1 T2} {f: T1 → T1 → T2} (Cf: ∀ x y, f x y = f y x) x y,
    map2 f x y = map2 f y x.

Lemma map2A :
  ∀ {T1} {f: T1 → T1 → T1} (Cf: ∀ 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 :
  ∀ {T1 T2} {f: T1 → T1 → T2} {v} (Cf: ∀ x, f x x = v) x,
    map2 f x x = nlist (length x) v.

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

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

Lemma map2Sl :
  ∀ {T1 T2} {f: T1 → T1 → T2} {v g} (Cf: ∀ 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 : ∀ (s : list T1) x, x \in s → f x \in map f s.

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

Lemma map_uniq : ∀ s, uniq (map f s) → uniq s.


Hypothesis Hf : injective f.

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

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

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

End EqMap.

Implicit Arguments mapP [T1 T2 f s y].

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

Section MapComp.

Variable T1 T2 T3 : Type.

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

Lemma eq_map : ∀ f1 f2 : T1 → T2, f1 =1 f2 → map f1 =1 map f2.

Lemma map_comp : ∀ (f1 : T2 → T3) (f2 : T1 → T2) s,
  map (f1 \o f2) s = map f1 (map f2 s).

Lemma mapK : ∀ (f1 : T1 → T2) (f2 : T2 → T1),
  cancel f1 f2 → cancel (map f1) (map f2).

End MapComp.


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 : ∀ m n, length (iota m n) = n.

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

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

Lemma nth_iota : ∀ n0 m n i, i < n → nth n0 (iota m n) i = m + i.

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

Lemma iota_uniq : ∀ 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 : ∀ f n, length (mklist f n) = n.

Lemma eq_mklist : ∀ f g, f =1 g → mklist f =1 mklist g.

Lemma nth_mklist : ∀ f n i, i < n → nth x0 (mklist f n) i = f i.

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

End MakeSeq.

Lemma mklist_uniq : ∀ (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 :
  ∀ s1 s2, foldr f (s1 ++ s2) z0 = foldr f s1 (foldr f s2 z0).

Lemma foldr_map :
  ∀ 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 : ∀ n l, sumn (n :: l) = n + sumn l.

Hint Rewrite sumn_nil sumn_cons : vlib.

Lemma sumn_nlist : ∀ x n : nat, sumn (nlist n x) = x × n.

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

Lemma natnlist0P : ∀ 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 : ∀ z s, foldl z (rev s) = foldr (fun x z ⇒ f z x) s z.

Lemma foldl_app : ∀ 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 : ∀ x s, length (pairmap x s) = length s.

Lemma nth_pairmap : ∀ s n, n < length s →
  ∀ 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 : ∀ x s, length (scanl x s) = length s.

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

Lemma scanlK :
  (∀ x, cancel (g x) (f x)) → ∀ x, cancel (scanl x) (pairmap x).

Lemma pairmapK :
  (∀ x, cancel (f x) (g x)) → ∀ 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 : ∀ s, zip (unzip1 s) (unzip2 s) = s.

Lemma unzip1_zip : ∀ s1 s2,
  length s1 ≤ length s2 → unzip1 (zip s1 s2) = s1.

Lemma unzip2_zip : ∀ s1 s2,
  length s2 ≤ length s1 → unzip2 (zip s1 s2) = s2.

Lemma length1_zip : ∀ s1 s2,
  length s1 ≤ length s2 → length (zip s1 s2) = length s1.

Lemma length2_zip : ∀ 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 : ∀ l ll, flatten (l :: ll) = l ++ flatten ll.

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

Hint Rewrite flatten_cons flatten_app : vlib.

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

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

Lemma reshapeKr : ∀ sh s, length s ≤ sumn sh → flatten (reshape sh s) = s.

Lemma reshapeKl : ∀ 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 ↔ (∀ n l1 l2 l3, l = l1 ++ n :: l2 ++ n :: l3 → False).