Library seq_ext

Require Import ssreflect seq ssrnat eqtype ssrbool.
Require Lists_ext.
Export seq.

Definition pi (l:seq nat_eqType) := foldr muln 1 l.

Lemma pi_cons : forall t h, pi (h :: t) = h * pi t.

Require Import List.
Require Import seq.

Section seq_list_conversion.

Variable A : Type.

Fixpoint s2l (s:seq A) {struct s} : list A := if s is h :: t then List.cons h (s2l t) else List.nil.

Fixpoint l2s (s:list A) {struct s} : seq A := if s is List.cons h t then h :: l2s t else [::].

Lemma s2l_inj : forall (a b : seq A), s2l a = s2l b -> a = b.

Lemma s2l2s : forall (l:list A), s2l (l2s l) = l.

Lemma l2s2l : forall (l:seq A), l2s (s2l l) = l.

Lemma len_s2l : forall (l:seq A), length (s2l l) = size l.

End seq_list_conversion.

Implicit Arguments s2l [A].
Implicit Arguments l2s [A].
Implicit Arguments s2l2s [A].

Lemma inb_mem : forall {A : eqType} (tl : seq.seq_predType A) (hd : A),
  Lists_ext.inb (fun x y : A => x == y) hd (s2l tl) = (hd \in tl).

Section seq_addendum.

Variable A : eqType.

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

Lemma notin_filter : forall (p : pred A) x s, ~~ p x -> x \notin filter p s.

Lemma filter_mem_cons : forall k (n : A), uniq k -> n \in k ->
  filter (mem (cons n [::])) k = cons n [::].

Fixpoint seq_flat (l : seq (seq_eqType A)) : seq A :=
  if l is h :: t then h ++ seq_flat t else [::].

Lemma seq_flatP : forall (s : seq (seq_eqType A)) y,
  reflect (exists2 s', s' \in s & y \in s') (y \in seq_flat s).

End seq_addendum.

Section disjointness.

Variable A : eqType.
Implicit Type l : seq A.

Fixpoint dis l1 l2 :=
  match l1 with
    | h :: t => if h \in l2 then false else dis t l2
    | nil => true
  end.

Lemma disP : forall l1 l2, reflect (Lists_ext.disj (s2l l1) (s2l l2)) (dis l1 l2).

Lemma disP_l2s : forall (l1 l2: list A), reflect (Lists_ext.disj l1 l2) (dis (l2s l1) (l2s l2)).

Lemma dis_cons : forall l' l (x : A), dis (x :: l) l' = dis l l' && ~~ (x \in l').

Lemma dis_filter : forall l1 l2, dis l1 l2 -> forall f, dis (filter f l1) l2.

Lemma dis_filter_split : forall (p q : pred A) l l',
  (forall b, (p b -> ~~ q b) /\ (q b -> ~~ p b)) ->
  dis (filter p l) (filter q l').

Lemma dis_sym : forall l l', dis l l' = dis l' l.

Lemma dis_filter_right : forall l1 l2, dis l1 (filter (fun x => ~~ (x \in l1)) l2).

Lemma dis_not_in : forall l l' (x : A), x \in l -> dis l l' -> ~~ (x \in l').

Lemma dis_nil_R : forall l, dis l [::].

Lemma dis_singl : forall x y, x != y = dis [:: x] [:: y].

End disjointness.

Implicit Arguments dis [A].

Section inclusion_seq.

Variable A : eqType.

Fixpoint inc (l1 l2 : seq.seq A) : bool :=
  match l1 with
    | seq.nil => true
    | seq.cons h1 t1 => if h1 \in l2 then inc t1 l2 else false
  end.

Lemma incP : forall (l1 l2 : seq.seq A),
  reflect (incl (s2l l1) (s2l l2)) (inc l1 l2).

Lemma inc_nil_inv : forall (d : seq A), inc d [::] -> d = [::].

Lemma inc_cons_R : forall (h : A) a b, inc a b -> inc a (h :: b).

Lemma inc_refl : forall (k : seq A), inc k k.

Lemma inc_app_L : forall (l k : seq A), inc l (l ++ k).

Lemma inc_app_R : forall (l k : seq A), inc l (k ++ l).

Lemma inc_trans : forall (l1 : seq A) l2 l3, inc l1 l2 -> inc l2 l3 -> inc l1 l3.

Lemma inc_cons_L : forall (x : A) l1 l2, inc (x :: l1) l2 = inc l1 l2 && (x \in l2).

Lemma inc_cons_R_inv : forall l1 (a : A) l2, a \notin l1 -> inc l1 (a :: l2) -> inc l1 l2.

Lemma inc_cons_inv : forall (h : A) t1 t2,
  h \notin t1 -> h \notin t2 -> inc (h :: t1) (h :: t2) -> inc t1 t2.

Lemma inc_filter : forall (l1:seq A) l2, inc l1 l2 -> forall f, inc (filter f l1) (filter f l2).

Lemma inc_filter_L : forall (l1 l2 : seq A),
       inc l1 l2 -> forall f : pred A, inc (filter f l1) l2.

Lemma inc_seq_filter_imp : forall (k : seq A) (p p': pred A),
  (forall x, x \in k -> p x -> p' x ) -> inc (filter p k) (filter p' k).

End inclusion_seq.

Implicit Arguments inc [A].

Section OCamlFind.

Variable A : eqType.
Variable a : pred A.

Fixpoint ocamlfind s := if s is x :: s' then if a x then Some x else ocamlfind s' else None.

Lemma ocamlfind_cons : forall hd tl, a hd -> ocamlfind (hd :: tl) = Some hd.

Lemma ocamlfind_cons' : forall hd tl, ~ a hd -> ocamlfind (hd :: tl) = ocamlfind tl.

Lemma ocamlfind_cons'' : forall hd tl r, ocamlfind (hd :: tl) = Some r -> a hd \/ ocamlfind tl = Some r.

Lemma ocamlfind_Some_mem : forall k r, ocamlfind k = Some r -> a r /\ r \in k.

End OCamlFind.

Implicit Arguments ocamlfind [A].

Fixpoint ran (a n : nat) : seq nat_eqType :=
  if n is (S n') then a :: ran (S a) n' else [::].

Lemma size_ran : forall n m, size (ran m n) = n.

Section converters.

Variables A B : Type.

Lemma map_s2l : forall l (f : A -> B), List.map f (s2l l) = s2l (map f l).
Lemma l2s_map : forall l (f : A -> B), l2s (List.map f l) = map f (l2s l).

Lemma s2l_cat : forall (l1 l2 : seq A), s2l (l1 ++ l2) = (s2l l1 ++ s2l l2)%list.
Lemma l2s_cat : forall (l1 l2 : list A), l2s (l1 ++ l2)%list = l2s l1 ++ l2s l2.

Lemma drop_skipn : forall (l : seq A) n, drop n l = l2s (skipn n (s2l l)).

Lemma s2l_take : forall n (l : seq A), s2l (take n l) = firstn n (s2l l).

Implicit Type k : list (A * B).

Lemma unzip1_l2s : forall k, unzip1 (l2s k) = l2s (List.map (fun x => fst x) k).
Lemma unzip2_l2s : forall k, unzip2 (l2s k) = l2s (List.map (fun x => snd x) k).

Lemma l2s_seq : forall b a, l2s (List.seq a b) = ran a b.

Lemma s2l_ran : forall n a, s2l (ran a n) = List.seq a n.

End converters.

Lemma inc_map_fst : forall (A B : eqType) (l1 l2 : seq (prod_eqType A B)),
  inc l1 l2 -> inc (map (fun x => fst x) l1) (map (fun x => fst x) l2).

Section delete.

Variable A : eqType.
Variable P : pred A.
Definition del (l : seq.seq A) : seq.seq A := filter (predC P) l.

Lemma s2l_del_remove_pred : forall l, s2l (del l) = Lists_ext.remove_pred (s2l l) P.

End delete.

Implicit Arguments del [A].
Implicit Arguments s2l_del_remove_pred [A].

Lemma l2s_filter : forall {A : Type} (P : pred A) (l : seq A),
  List.filter P (s2l l) = s2l (filter P l).

Lemma filter_ran_ran : forall l1 l2, dis l1 l2 ->
  filter (fun x : ssrnat.nat_eqType => ~~ (x \in l2)) (l1 ++ l2) = l1.