Lists -- part II

This development is largely ported from the seq library of SSReflect. The names of several operations have been changed to use the standard Coq list definitions (e.g., seq => list, cat => app, size => length) and a few lemmas have been added. The map2 definition and its properties are new.

Require Import Omega.
Require Import Vbase Vlistbase Varith.

Set Implicit Arguments.
Unset Strict Implicit.

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.
Proof.
 intros.
 rewrite <- (app_take_drop (find p s) s) at 1.
 rewrite (drop_nth x); try done.
 by rewrite <- has_find.
Qed.

Equality and eqType for list

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, niltrue
  | x1 :: s1', x2 :: s2'(x1 == x2) && eqlist s1' s2'
  | _, _false
  end.

Lemma eqlistP : Equality.axiom eqlist.
Proof.
red; induction x; destruct y; vauto; simpl.
case eqP; intro X; clarify; try (right; congruence).
destruct (IHx y); vauto; right; congruence.
Qed.

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

Lemma eqlistE : eqlist = eq_op.
Proof. done. Qed.

Lemma eqlist_cons : x1 x2 s1 s2,
  (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).
Proof. done. Qed.

Lemma eqlist_app : s1 s2 s3 s4,
  length s1 = length s2 (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).
Proof.
induction s1; destruct s2; clarsimp.
by rewrite !eqlist_cons, <- andbA, IHs1.
Qed.

Lemma eqlist_rev2 : l1 l2,
  (rev l1 == rev l2) = (l1 == l2).
Proof.
  intros; do 2 case eqP; clarsimp.
  generalize (f_equal (@rev _) e); clarsimp.
Qed.

Lemma eqlist_snoc : s1 s2 x1 x2,
  (snoc s1 x1 == snoc s2 x2) = (s1 == s2) && (x1 == x2).
Proof.
  by intros; rewrite <- eqlist_rev2, !rev_snoc, eqlist_cons, eqlist_rev2, andbC.
Qed.

Lemma has_filter : a s, has a s = (filter a s != nil).
Proof. by intros; rewrite has_count, count_filter; case (filter a s). Qed.

Lemma length_eq0 : l, (length l == 0) = (l == nil).
Proof. intros []; clarsimp. Qed.


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 xmem_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).
Proof. done. Qed.

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

Lemma mem_list1 : x y, (x \in y :: nil) = (x == y).
Proof. clarsimp. Qed.



Lemma mem_app : x s1 s2, (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
Proof. by induction s1; clarsimp; rewrite IHs1, orbA. Qed.

Lemma mem_snoc : s y, snoc s y =i y :: s.
Proof. red; clarsimp; rewrite snocE, mem_app, !in_cons, in_nil, orbC; clarsimp. Qed.

Lemma mem_head : x s, x \in x :: s.
Proof. by intros; rewrite in_cons, eqxx. Qed.

Lemma mem_last : x s, last x s \in x :: s.
Proof. by intros; rewrite lastI, mem_snoc, mem_head. Qed.

Lemma mem_behead : s, {subset behead s s}.
Proof. by destruct s; clarsimp; intro; rewrite in_cons, orbC; intros →. Qed.

Lemma mem_belast : s y, {subset belast y s y :: s}.
Proof. by red; intros; rewrite lastI, mem_snoc, mem_behead. Qed.

Lemma mem_nth : s n, n < length s nth s n \in s.
Proof. induct s [n]. Qed.

Lemma mem_take : s x, x \in take n0 s x \in s.
Proof. by intros; rewrite <-(app_take_drop n0 s), mem_app, H. Qed.

Lemma mem_drop : s x, x \in drop n0 s x \in s.
Proof. by intros; rewrite <-(app_take_drop n0 s), mem_app, H, orbT. Qed.

Lemma mem_rev : s, rev s =i s.
Proof.
by red; induction s; ins; rewrite rev_cons, mem_snoc, !in_cons, IHs.
Qed.

Lemma in_head : x l, x \in x :: l.
Proof. clarsimp. Qed.

Lemma in_behead : x y l, x \in l x \in y :: l.
Proof. clarsimp; clarsimp. Qed.

Lemma in_consE : {x y l}, x \in y :: l {x = y} + {x \in l}.
Proof. intros x y l; rewrite in_cons; case eqP; auto. Qed.

Lemma in_split : x l, x \in l l1 l2, l = l1 ++ x :: l2.
Proof.
  induction l; ins.
  destruct (in_consE H); clarify; [by nil; vauto|].
  specialize (IHl eq_refl); des; (a :: l1); vauto.
Qed.

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).
Proof.
  induction l; simpls; vauto.
  clarsimp; case eqP; ins; vauto.
  case IHl; constructor; auto; intro; desf.
Qed.

Section Filters.

Variable a : pred T.

Lemma hasP : l, reflect (exists2 x, x \in l & a x) (has a l).
Proof.
induction l; simpls; [by right; intro x; case x|].
case_eq (a a0) as A; [by left; a0; clarsimp|].
apply (iffP IHl); intros [x ysx ax]; [|destruct (in_consE ysx)]; x; do 2 clarsimp.
Qed.

Lemma hasPn : l, reflect ( x, x \in l negb (a x)) (negb (has a l)).
Proof.
  induction l; vauto; simpls.
  case_eq (a a0) as A; simpls.
    by right; intros H; exploit (H a0); clarsimp.
  destruct IHl as [X|X]; constructor; clarsimp.
    by destruct (in_consE H); autos.
  intuition (auto using in_behead).
Qed.

Lemma allP : l, reflect ( x, x \in l a x) (all a l).
Proof.
  induction l; vauto; simpls.
  case_eq (a a0) as A; simpls.
  2: by right; intros H; exploit (H a0); clarsimp.
  destruct IHl as [X|X]; constructor; clarsimp.
    by destruct (in_consE H); autos.
  by intuition (auto using in_behead).
Qed.

Lemma allPn : l, reflect (exists2 x, x \in l & negb (a x)) (negb (all a l)).
Proof.
  induction l; simpls; [by right; intro x; case x|].
  case_eq (a a0) as A; simpls; [|by left; a0; clarsimp].
  apply (iffP IHl); intros [x ysx ax]; [|destruct (in_consE ysx)]; x; clarsimp; clarsimp.
Qed.

Lemma mem_filter : x l, (x \in filter a l) = a x && (x \in l).
Proof.
intros; induction l; clarsimp.
case ifP; clarsimp; rewrite IHl; case (eqP x a0); clarsimp.
Qed.

End Filters.

Lemma eq_in_filter : (a1 a2 : pred T) s,
  {in s, a1 =1 a2} filter a1 s = filter a2 s.
Proof.
  induction s; ins; rewrite H, IHs; try done; clarsimp.
  by red; intros; apply H; eapply mem_behead.
Qed.

Lemma eq_has_r : s1 s2 (EQ: s1 =i s2) f, has f s1 = has f s2.
Proof.
  by intros; apply/hasP/hasP; intros [x ? ?]; x; simpls;
   [ rewrite EQ | rewrite <- EQ ].
Qed.

Lemma eq_all_r : s1 s2 (EQ: s1 =i s2) f, all f s1 = all f s2.
Proof.
  intros; apply/allP/allP; try red; intros; apply H; congruence.
Qed.

Lemma has_sym : s1 s2, has (mem s1) s2 = has (mem s2) s1.
Proof.
intros; case (hasP _ s1); case (hasP _ s2); clarsimp; destruct e, n; eauto.
Qed.

Lemma has_pred1 : x l, has (fun yy == x) l = (x \in l).
Proof. by induction l; clarsimp; rewrite IHl, beq_sym. Qed.

Constant sequences, i.e., the image of nlist.

Definition constant s :=
  match s with
    | niltrue
    | x :: s'all (fun yy == x) s'
  end.

Lemma all_pred1P x s :
  reflect (s = nlist (length s) x) (all (fun yy == x) s).
Proof.
unfold nlist, ncons; induction s; clarsimp; vauto.
case eqP; clarsimp; destruct IHs; constructor; congruence.
Qed.

Lemma all_pred1_constant x s : all (fun yy == x) s constant s.
Proof. induction s; clarsimp; destruct (eqP a x); clarsimp. Qed.

Implicit Arguments all_pred1_constant [].

Lemma all_pred1_nlist : x y n,
  all (fun yy == x) (nlist n y) = ((n == 0) || (x == y)).
Proof.
  destruct n; clarsimp.
  rewrite beq_sym; case eqP; clarsimp.
  induction n; clarsimp.
Qed.

Lemma constant_nlist : n x, constant (nlist n x).
Proof. intros; apply (all_pred1_constant x); rewrite all_pred1_nlist; clarsimp. Qed.

Lemma constantP : s,
  reflect ( x, s = nlist (length s) x) (constant s).
Proof.
intros; apply (iffP (idP _)); [|by intros [x ->]; apply constant_nlist].
destruct s; [by x0|].
intro X; generalize (all_pred1P _ _ X); unfold nlist, ncons; clarsimp.
s; congruence.
Qed.


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

Lemma cons_uniq : x s, uniq (x :: s) = (x \notin s) && uniq s.
Proof. done. Qed.

Lemma app_uniq : s1 s2,
  uniq (s1 ++ s2) = uniq s1 && negb (has (mem s1) s2) && uniq s2.
Proof.
intros; induction s1; clarsimp.
rewrite has_sym; simpl; rewrite has_sym, IHs1, mem_app, !negb_or.
repeat (case in_mem; clarsimp).
Qed.

Lemma uniq_appC : s1 s2, uniq (s1 ++ s2) = uniq (s2 ++ s1).
Proof. intros; rewrite !app_uniq, has_sym; repeat (case uniq; clarsimp). Qed.

Lemma uniq_appCA : s1 s2 s3,
  uniq (s1 ++ s2 ++ s3) = uniq (s2 ++ s1 ++ s3).
Proof.
by intros; rewrite <- !appA, <-!(uniq_appC s3), !(app_uniq s3), uniq_appC, !has_app, orbC.
Qed.

Lemma snoc_uniq : s x, uniq (snoc s x) = (x \notin s) && uniq s.
Proof. by intros; rewrite <-appl1, uniq_appC. Qed.

Lemma filter_uniq : s a, uniq s uniq (filter a s).
Proof.
intros; induction s; clarsimp; rewrite fun_if; simpl.
rewrite mem_filter, !IHs; try done; case ifP; ins; clarify.
Qed.

Lemma rot_uniq : s, uniq (rot n0 s) = uniq s.
Proof. by intros; unfold rot; rewrite uniq_appC, app_take_drop. Qed.

Lemma rev_uniq : s, uniq (rev s) = uniq s.
Proof. by induction s; clarsimp; rewrite snoc_uniq, mem_rev, IHs. Qed.

Lemma count_uniq_mem :
   s x, uniq s count (fun yy == x) s = if (x \in s) then 1 else 0.
Proof.
induction s; clarsimp; []; des; rewrite beq_sym; case eqP; autos.
by rewrite IHs; [case ifP|]; clarsimp.
Qed.

Lemma in_split_uniq :
   x l,
    x \in l uniq l
     l1 l2, l = l1 ++ x :: l2
      uniq (l1 ++ l2) x \notin (l1 ++ l2).
Proof.
 intros; pose proof (in_split H); des; clarify;
 do 3 eexists; eauto; rewrite app_uniq in *; simpls; clarify.
 rewrite mem_app; apply/norP in H1; desc; clarify.
Qed.


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

Lemma length_undup : s, length (undup s) length s.
Proof. induction s; clarsimp; case ifP; autos. Qed.

Lemma mem_undup : s, undup s =i s.
Proof.
intros s x; induction s; clarsimp; rewrite <- IHs.
case ifP; [case eqP|]; clarsimp.
Qed.

Hint Rewrite mem_undup : vlib.

Lemma undup_uniq : s, uniq (undup s).
Proof. by induction s; clarsimp; case ifP; clarsimp. Qed.

Lemma undup_id : s, uniq s undup s = s.
Proof. induct s. Qed.

Lemma ltn_length_undup : s, (length (undup s) < length s) = negb (uniq s).
Proof.
induction s; clarsimp; case ifP; clarsimp; rewrite length_undup; clarsimp.
Qed.


Definition index x := find (fun yy == x).

Lemma index_length : x s, index x s length s.
Proof. intros; unfold index; apply find_length. Qed.

Lemma index_mem : x s, (index x s < length s) = (x \in s).
Proof. by intros; rewrite <- has_pred1, has_find. Qed.

Lemma nth_index : x s, x \in s nth s (index x s) = x.
Proof. by intros; rewrite <- has_pred1 in H; apply (eqP _ _ (nth_find x0 H)). Qed.

Lemma index_app : x s1 s2,
 index x (s1 ++ s2) = if x \in s1 then index x s1 else length s1 + index x s2.
Proof. by unfold index; intros; rewrite find_app, has_pred1. Qed.

Lemma index_uniq : i s, i < length s uniq s index (nth s i) s = i.
Proof.
unfold index; induction[i] s [i]; clarsimp; des.
rewrite IHs; clarsimp; case eqP; clarsimp; rewrite mem_nth in *; clarsimp.
Qed.

Lemma index_head : x s, index x (x :: s) = 0.
Proof. unfold index; clarsimp. Qed.

Lemma index_last : x s,
  uniq (x :: s) index (last x s) (x :: s) = length s.
Proof.
intros x s; rewrite lastI, snoc_uniq, <-appl1, index_app, length_belast.
unfold index; case ifP; clarsimp.
Qed.

Lemma nth_uniq : s i j,
   i < length s j < length s uniq s (nth s i == nth s j) = (i == j).
Proof.
intros; case eqP; case eqP; clarsimp.
elim n; rewrite <- (index_uniq H), <- (index_uniq H0); congruence.
Qed.

Lemma mem_rot : s, rot n0 s =i s.
Proof.
by intros s x; unfold rot; rewrite <- (app_take_drop n0 s) at 3; rewrite !mem_app, orbC.
Qed.

Lemma eqlist_rot : s1 s2, (rot n0 s1 == rot n0 s2) = (s1 == s2).
Proof. by intros; do 2 case eqP; ins; clarify; eapply rot_inj in e. Qed.

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.
Proof.
intros; pose (i := index x s); i (drop (S i) s ++ take i s); subst i.
unfold rot; rewrite <- app_cons.
apply (f_equal (fun s2s2 ++ take (index x s) s)).
unfold index; induction s; clarsimp.
rewrite beq_sym; destruct (eqP x a); autos.
Qed.

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).
Proof.
intros; apply (iffP (idP _)); [|by intros [n Hn <-]; apply mem_nth].
by (index x s); [ rewrite index_mem | apply nth_index ].
Qed.

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).
Proof.
intros; induction s; clarsimp; [by right; intros []|].
case_eq (a a0); clarsimp; [by left; 0|].
apply (iffP IHs); [intros [i] | intros [[|i]]]; [ (S i) | | i]; clarsimp.
Qed.

Lemma all_nthP : (a : pred T) s x0,
  reflect ( i, i < length s a (nth x0 s i)) (all a s).
Proof.
intros; induction s; clarsimp; vauto.
case_eq (a a0); clarsimp.
  by apply (iffP IHs); clarsimp; [destruct i|specialize (H0 (S i))]; autos.
right; intro X; specialize (X 0); autos.
Qed.

End NlistthTheory.

Lemma set_nth_default : T s (y0 x0 : T) n,
  n < length s nth x0 s n = nth y0 s n.
Proof. induct s [n]; auto. Qed.

Lemma headI : T s (x : T),
  snoc s x = head x s :: behead (snoc s x).
Proof. by destruct s. Qed.

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.
Proof.
induction v; intros [|i] [|j]; clarsimp.
induction[j] i [j]; clarsimp.
Qed.

Lemma length_incr_nth : v i,
  length (incr_nth v i) = if i < length v then length v else S i.
Proof.
 induction v; intros [|i]; clarsimp; f_equal.
 - induction i; simpls; congruence.
 - by rewrite <- fun_if, IHv.
Qed.


Section PermSeq.

Variable T : eqType.

Notation cou1 := (fun xcount (fun yy == x)).

Definition same_count1 (s1 s2 : list T) x :=
   count (fun yy == x) s1 == count (fun yy == 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).
Proof.
  intros; apply (iffP allP); try red; intros.
  2: by unfold same_count1; rewrite H; case eqP.
  unfold same_count1 in ×.
    destruct (has (fun yy == x) s1) as [] _eqn: E1.
      rewrite has_pred1 in *; exploit (H x);
      [by clarsimp|by case eqP].
    destruct (has (fun yy == x) s2) as [] _eqn: E2.
      rewrite has_pred1 in *; exploit (H x);
      [by clarsimp|by case eqP].
    rewrite has_filter in ×.
    by rewrite !count_filter, (eqP _ _ (negbFE E1)), (eqP _ _ (negbFE E2)).
Qed.

Lemma perm_eq_refl : s, perm_eq s s.
Proof. by intros; apply/perm_eqP_weak. Qed.
Hint Resolve perm_eq_refl.

Lemma perm_eq_sym : symmetric perm_eq.
Proof. intros s1 s2; apply/perm_eqP_weak/perm_eqP_weak; red; auto using fsym. Qed.

Lemma perm_eq_trans : transitive perm_eq.
Proof.
  red; intros; apply/perm_eqP_weak; intros.
  eapply ftrans, (perm_eqP_weak _ _ H0).
  eapply (perm_eqP_weak _ _ H).
Qed.

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

Lemma perm_eqlP : s1 s2, reflect (perm_eql s1 s2) (perm_eq s1 s2).
Proof.
  intros; apply (iffP (idP _)); [|by intros X; rewrite X].
  split/; [rewrite perm_eq_sym in H|]; eauto using perm_eq_trans.
Qed.

Lemma perm_eqrP : s1 s2, reflect (perm_eqr s1 s2) (perm_eq s1 s2).
Proof.
  intros; apply (iffP (idP _)); [|by intros X; rewrite <- X].
  split/; rewrite !(perm_eq_sym x);
    [rewrite perm_eq_sym in H|]; eauto using perm_eq_trans.
Qed.

Lemma perm_appC : s1 s2, perm_eql (s1 ++ s2) (s2 ++ s1).
Proof.
  ins; apply (elimT (perm_eqlP _ _)); apply/perm_eqP_weak; intro.
  rewrite ?count_app; omega.
Qed.

Lemma perm_app2l : s1 s2 s3,
  perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.
Proof.
  intros; apply/perm_eqP_weak/perm_eqP_weak; intros eq23 a.
    by rewrite !count_app, eq23.
  generalize (eq23 a); rewrite !count_app; intros; omega.
Qed.

Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.
Proof. apply (perm_app2l (cons x nil)). Qed.

Lemma perm_app2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.
Proof. do 2 (rewrite perm_eq_sym, perm_appC); apply perm_app2l. Qed.

Lemma perm_appAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).
Proof.
  apply (elimT (perm_eqlP _ _)); apply/perm_eqP_weak; intro; rewrite !count_app; omega.
Qed.

Lemma perm_appCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).
Proof.
  apply (elimT (perm_eqlP _ _)); apply/perm_eqP_weak; intro; rewrite !count_app; omega.
Qed.

Lemma perm_snoc : x s, perm_eql (snoc s x) (x :: s).
Proof. by simpl; red; intros; rewrite snocE, perm_appC. Qed.

Lemma perm_rot : n s, perm_eql (rot n s) s.
Proof. by simpl; red; intros; unfold rot; rewrite perm_appC, app_take_drop. Qed.

Lemma perm_rotr : n s, perm_eql (rotr n s) s.
Proof. intros; apply perm_rot. Qed.

Lemma perm_eq_mem : s1 s2, perm_eq s1 s2 s1 =i s2.
Proof.
  by intros ? ?; move/perm_eqP_weak; intros eq12 x;
     rewrite <-!has_pred1, !has_count, eq12.
Qed.

Lemma perm_eq_nilD : s, perm_eq nil s s = nil.
Proof.
  destruct s; unfold perm_eq, same_count1; simpls; clarsimp.
Qed.

Lemma perm_eq_consD : x s1 s2,
  perm_eq (x :: s1) s2 sa sb, s2 = sa ++ x :: sb perm_eq s1 (sa ++ sb).
Proof.
  intros; exploit (@in_split _ x s2).
    apply/@allP in H; exploit (H x); [by clarsimp|].
    unfold same_count1; simpl; rewrite eqxx; intro M; clarify.
    by rewrite <- has_pred1, has_count, <- M.
  intros; des; clarify; repeat eexists.
  rewrite perm_eq_sym, perm_appC in H; simpls.
  by rewrite perm_cons, perm_appC, perm_eq_sym in H.
Qed.

Lemma perm_eqD : s1 s2 (EQ: perm_eq s1 s2) f, count f s1 = count f s2.
Proof.
  induction[] s1; ins.
    eapply perm_eq_nilD in EQ; clarify.
  apply perm_eq_consD in EQ; desc; clarify.
  rewrite (IHs1 _ EQ0), !count_app; simpl; desf.
Qed.

Lemma perm_eq_length : s1 s2, perm_eq s1 s2 length s1 = length s2.
Proof. by intros; rewrite <-!count_predT; apply perm_eqD. Qed.

Lemma perm_eqP s1 s2 :
  reflect ((@count _) ^~ s1 =1 (@count _) ^~ s2) (perm_eq s1 s2).
Proof.
  generalize (@perm_eqD s1 s2).
  case (perm_eqP_weak s1 s2); ins; constructor; intro; auto.
  by destruct n; intro; auto.
Qed.

Lemma uniq_leq_length : s1 s2 : list T,
  uniq s1 {subset s1 s2} length s1 length s2.
Proof.
  induction s1; ins; desc.
  case (@rot_to _ s2 a); try by apply H0.
  intros i ? EQ; rewrite <- (length_rot i s2), EQ; simpls.
  apply IHs1; red; ins.
  eapply (f_equal (fun yx \in y)) in EQ.
  rewrite mem_rot, in_cons, H0 in EQ; try rewrite in_cons; vauto.
  destruct (eqP x a); vauto.
  case eqP; eauto.
Qed.

Lemma leq_length_uniq : s1 s2 : list T,
  uniq s1 {subset s1 s2} length s2 length s1 uniq s2.
Proof.
  induction s1; ins; desc; [by destruct s2|].
  case (@rot_to _ s2 a); try by apply H0.
  intros i ? EQ; rewrite <- (rot_uniq i), EQ; simpls.
  rewrite <- (length_rot i s2), EQ in *; simpls; split/.
    apply/negP; intro.
    assert (X: {subset a :: s1 s'}).
      red; ins; apply (f_equal (fun yx \in y)) in EQ.
      rewrite in_cons in *; destruct (eqP x a); simpls; clarsimp.
      by rewrite <- EQ; apply H0; clarsimp; clarsimp.
    eapply uniq_leq_length in X; simpls; vauto.
    by generalize (len_trans H1 X); rewrite leSn, ltnn.
  eapply IHs1 in H1; red; ins; vauto.
  eapply (f_equal (fun yx \in y)) in EQ.
  rewrite mem_rot, in_cons, H0 in EQ; try rewrite in_cons; repeat clarsimp; vauto.
  destruct (eqP x a); repeat clarsimp; vauto.
Qed.

Lemma uniq_length_uniq : s1 s2 : list T,
  uniq s1 s1 =i s2 uniq s2 = (length s2 == length s1).
Proof.
  ins; rewrite eqn_leAle, andbC, uniq_leq_length; vauto; [|by intro; rewrite H0].
  apply/idP/idP.
    by eapply leq_length_uniq; auto; intro; rewrite H0.
  by ins; eapply uniq_leq_length; auto; intro; rewrite H0.
Qed.

Lemma leq_length_perm : s1 s2 : list T,
  uniq s1 {subset s1 s2}
  length s2 length s1
  s1 =i s2 length s1 = length s2.
Proof.
  ins; assert (U2: uniq s2) by eauto using leq_length_uniq.
  cut (s1 =i s2).
    by split; [|apply/eqP; instantiate; rewrite <- uniq_length_uniq].
  intro x; apply/idP/idP; auto.
  induction [s2 H0 H1 U2] s1; ins; [by destruct s2|]; clarify.
  pose proof (in_split_uniq (H0 _ (mem_head _ _)) U2); desf.
  clarsimp; revert H2; case eqP; ins.
  eapply (IHs1 eq_refl (l1 ++ l2)); auto; clarsimp.
  by intro y; specialize (H0 y); clarsimp; revert H0; case eqP; ins; auto; clarsimp.
Qed.

Lemma perm_uniq : s1 s2 : list T,
  s1 =i s2 length s1 = length s2 uniq s1 = uniq s2.
Proof.
  by ins; apply/idP/idP; intro Us; rewrite (uniq_length_uniq Us), ?H0.
Qed.

Lemma perm_eq_uniq : s1 s2, perm_eq s1 s2 uniq s1 = uniq s2.
Proof.
  by ins; apply perm_uniq; [apply perm_eq_mem | apply perm_eq_length].
Qed.

Lemma uniq_perm_eq : s1 s2,
  uniq s1 uniq s2 s1 =i s2 perm_eq s1 s2.
Proof.
  ins; apply/(@allP); intros x _.
  by unfold same_count1; rewrite !count_uniq_mem, H1.
Qed.

Lemma count_mem_uniq : s : list T,
  ( x, count (fun yy == x) s = if (x \in s) then 1 else 0) uniq s.
Proof.
  ins.
  cut (perm_eq s (undup s) : Prop); [by move/perm_eq_uniq; intros ->|].
  apply/@allP; intros x _; unfold same_count1.
  by rewrite H, count_uniq_mem, mem_undup.
Qed.

End PermSeq.

Section RotrLemmas.

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

Lemma length_rotr : s : list T, length (rotr n0 s) = length s.
Proof. by intros; unfold rotr; rewrite length_rot. Qed.

Lemma mem_rotr : s : list T', rotr n0 s =i s.
Proof. intros; apply mem_rot. Qed.

Lemma rotr_size_app : s1 s2 : list T,
  rotr (length s2) (s1 ++ s2) = s2 ++ s1.
Proof. intros; unfold rotr; clarsimp; rewrite <- addn_subA; clarsimp. Qed.

Lemma rotr1_snoc : x (s : list T), rotr 1 (snoc s x) = x :: s.
Proof. by intros; rewrite <- rot1_cons, rotK. Qed.

Lemma has_rotr : f (s : list T), has f (rotr n0 s) = has f s.
Proof. intros; apply has_rot. Qed.

Lemma rotr_uniq : s : list T', uniq (rotr n0 s) = uniq s.
Proof. intros; apply rot_uniq. Qed.

Lemma rotrK : cancel (rotr n0) (@rot T n0).
Proof.
  intros s; case (ltnP n0 (length s)); intro Hs.
  - rewrite <-(subKn (ltnW Hs)) at 1.
    by rewrite <-(length_rotr) at 1; apply rotK.
  - rewrite <-(rot_overlength Hs) at 2.
    by unfold rotr; rewrite <-subn_eq0 in Hs; rewrite (eqP _ _ Hs), rot0.
Qed.

Lemma rotr_inj : injective (@rotr T n0).
Proof. exact (can_inj rotrK). Qed.

Lemma rev_rot : s : list T, rev (rot n0 s) = rotr n0 (rev s).
Proof.
  unfold rotr; intros; clarsimp.
  rewrite <- (app_take_drop n0 s) at 3; unfold rot at 1.
  by rewrite !rev_app, <- length_drop, <- length_rev, rot_length_app.
Qed.

Lemma rev_rotr : s : list T, rev (rotr n0 s) = rot n0 (rev s).
Proof. intros; rewrite <- (rev_rev s), <- rev_rot; clarsimp. Qed.

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.
Proof. by induction s; destruct n; simpl; try apply IHs. Qed.

Lemma sieve_true : s n, length s n sieve (nlist n true) s = s.
Proof.
  induction s; destruct n; simpl; try done; intros; (try by inv H).
  f_equal; apply IHs; auto with arith.
Qed.

Lemma sieve0 : m, sieve m nil = (@nil T).
Proof. by intros []. Qed.


Lemma sieve_cons : b m x s,
  sieve (b :: m) (x :: s) = (if b then (x :: nil) else nil) ++ sieve m s.
Proof. by intros []. Qed.

Lemma length_sieve : m s,
  length m = length s length (sieve m s) = count id m.
Proof. induct[] m [s]. Qed.

Lemma sieve_app : m1 s1, length m1 = length s1
   m2 s2, sieve (m1 ++ m2) (s1 ++ s2) = sieve m1 s1 ++ sieve m2 s2.
Proof. induct[] m1 [s1]. Qed.

Lemma has_sieve_cons : a b m x s,
  has a (sieve (b :: m) (x :: s)) = b && a x || has a (sieve m s).
Proof. by destruct b. Qed.

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).
Proof.
 intros.
  assert (length (take n0 m) = length (take n0 s)).
  by rewrite !length_take, H.
  rewrite <- (length_sieve H0).
  unfold rot at 1 2; rewrite sieve_app; rewrite ?length_drop; eauto.
  rewrite <- (app_take_drop n0 m) at 4.
  rewrite <- (app_take_drop n0 s) at 4.
  by rewrite sieve_app, rot_length_app.
Qed.

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).
Proof. by case b. Qed.

Lemma mem_sieve : x m (s : list T), (x \in sieve m s) (x \in s).
Proof.
  induct[x m] s [m]; desf; rewrite ?in_cons in *; clarsimp;
  [revert H; case/|]; intros; clarify; erewrite IHs; eauto; clarsimp.
Qed.

Lemma sieve_uniq : s : list T, uniq s m, uniq (sieve m s).
Proof.
  induction[] s [m]; ins; desf; simpl; eauto.
  apply/andP; split; eauto.
  by apply/negP; intro X; rewrite (mem_sieve X) in ×.
Qed.

Lemma mem_sieve_rot : m (s : list T), length m = length s
  sieve (rot n0 m) (rot n0 s) =i sieve m s.
Proof. by red; ins; rewrite sieve_rot, mem_rot. Qed.

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
    | nilnil
    | x :: lf x :: map l
  end.

Lemma map_cons : x s, map (x :: s) = f x :: map s.
Proof. done. Qed.

Lemma map_nlist : x, map (nlist n0 x) = nlist n0 (f x).
Proof. unfold nlist, ncons; induction n0; ins; eauto using f_equal. Qed.

Lemma map_app : s1 s2, map (s1 ++ s2) = map s1 ++ map s2.
Proof. by intros; induction s1; simpl; [|rewrite IHs1]. Qed.

Lemma map_snoc : s x, map (snoc s x) = snoc (map s) (f x).
Proof. by intros; rewrite !snocE, map_app. Qed.

Lemma length_map : l, length (map l) = length l.
Proof. by induction l; simpl; [|rewrite IHl]. Qed.

Lemma behead_map : l, behead (map l) = map (behead l).
Proof. by intros[]. Qed.

Lemma nth_map : n l, n < length l nth x2 (map l) n = f (nth x1 l n).
Proof.
  induction[n] l; destruct n; simpl; try (by inversion 1).
  auto with arith.
Qed.

Lemma last_map : s x, last (f x) (map s) = f (last x s).
Proof. by induction s; simpl. Qed.

Lemma belast_map : s x, belast (f x) (map s) = map (belast x s).
Proof. by induction s; simpl; [|rewrite IHs]. Qed.

Lemma filter_map a s : filter a (map s) = map (filter (preim f a) s).
Proof. by induction s; simpls; rewrite (fun_if map), IHs. Qed.

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

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

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

Lemma map_take s : map (take n0 s) = take n0 (map s).
Proof. induct[s] n0 [s]. Qed.

Lemma map_drop s : map (drop n0 s) = drop n0 (map s).
Proof. induct[s] n0 [s]. Qed.

Lemma map_rot s : map (rot n0 s) = rot n0 (map s).
Proof. by unfold rot; rewrite map_app, map_take, map_drop. Qed.

Lemma map_rotr s : map (rotr n0 s) = rotr n0 (map s).
Proof. by apply (canRL (@rotK n0 T2)); rewrite <-map_rot, rotrK. Qed.

Lemma map_rev s : map (rev s) = rev (map s).
Proof. by induction s; ins; rewrite !rev_cons, !snocE, map_app, IHs. Qed.

Lemma map_sieve m s : map (sieve m s) = sieve m (map s).
Proof. by induction[s] m [s]; simpls; case a; simpl; rewrite IHm. Qed.

Lemma inj_map (Hf : injective f) : injective map.
Proof. red; induction x0; intros []; clarsimp; f_equal; autos. Qed.

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.

map2 and its properties


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, nilnil
    | x1 :: l1, x2 :: l2f x1 x2 :: map2 l1 l2
  end.

Lemma map2_0l : l, map2 nil l = nil.
Proof. done. Qed.
Lemma map2_l0 : l, map2 l nil = nil.
Proof. by destruct l. Qed.

Lemma map2_cons : x1 l1 x2 l2, map2 (x1 :: l1) (x2 :: l2) = f x1 x2 :: map2 l1 l2.
Proof. done. Qed.

Lemma map2_nlist : x y, map2 (nlist n0 x) (nlist n0 y) = nlist n0 (f x y).
Proof. unfold nlist, ncons; intros; induction n0; simpl; congruence. Qed.

Lemma map2_app : s1 s2 t1 t2 (Leq: length s1 = length t1),
  map2 (s1 ++ s2) (t1 ++ t2) = map2 s1 t1 ++ map2 s2 t2.
Proof. by induction[] s1 [t1]; ins; clarify; rewrite IHs1. Qed.

Lemma length_map2_eq : l1 l2, length l1 = length l2
  length (map2 l1 l2) = (length l1).
Proof. by induction[] l1 [l2]; ins; clarify; rewrite IHl1. Qed.

Lemma map2_take :
   l1 l2, map2 (take n0 l1) (take n0 l2) = take n0 (map2 l1 l2).
Proof.
  by induction n0; destruct l1; destruct l2; simpl; try done; rewrite IHn.
Qed.

Lemma map2_drop :
   l1 l2, map2 (drop n0 l1) (drop n0 l2) = drop n0 (map2 l1 l2).
Proof.
  by induction n0; destruct l1; destruct l2; simpl; rewrite ?map2_l0.
Qed.

Lemma map2_rot l1 l2 (Leq: length l1 = length l2) :
    map2 (rot n0 l1) (rot n0 l2) = rot n0 (map2 l1 l2).
Proof.
  intros; unfold rot; rewrite map2_app, map2_take, map2_drop; try done.
  rewrite ?length_drop; congruence.
Qed.

End Map2.

Lemma map2I :
   {T1} {f: T1 T1 T1} (Cf: x, f x x = x) x,
    map2 f x x = x.
Proof. by induction x; try done; simpl; f_equal. Qed.

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.
Proof. by induction x; destruct y; try done; simpl; f_equal. Qed.

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.
Proof. by induction x; destruct y; destruct z; try done; simpl; f_equal. Qed.

Lemma map2K :
   {T1 T2} {f: T1 T1 T2} {v} (Cf: x, f x x = v) x,
    map2 f x x = nlist (length x) v.
Proof. by unfold nlist, ncons; induction x; try done; simpl; f_equal. Qed.

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.
Proof.
  unfold nlist, ncons; induction n; destruct x; simpl;
  intros; clarify; f_equal; auto.
Qed.

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.
Proof.
  unfold nlist, ncons; induction n; destruct x; simpl;
  intros; clarify; f_equal; auto.
Qed.

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.
Proof.
  unfold nlist, ncons; induction n; destruct x; simpl;
  intros; clarify; f_equal; auto.
Qed.

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.
Proof.
induction s; clarsimp.
destruct (eqP x a); clarsimp.
rewrite IHs; clarsimp.
Qed.

Lemma mapP : (s : list T1) y,
  reflect (exists2 x, x \in s & y = f x) (y \in map f s).
Proof.
induction s; clarsimp; [by right; intros []|].
case (eqP); clarsimp.
  by left; a; clarsimp.
apply (iffP (IHs y)); intros []; clarsimp; x; clarsimp;
destruct (eqP x a); clarsimp.
Qed.

Lemma map_uniq : s, uniq (map f s) uniq s.
Proof.
induction s; clarsimp; des.
split/; [apply/; intro; rewrite map_f in *|]; intuition.
Qed.

Lemma map_inj_in_uniq : s : list T1,
  {in s &, injective f} uniq (map f s) = uniq s.
Proof.
  split/; eauto using map_uniq.
  induction s; ins; desf.
  apply/andP; split.
    apply/negP; intro X. generalize (mapP _ _ X).
    by intros [? ? M]; eapply H in M; repeat clarsimp.
  apply IHs; eauto; red; intros; apply H; repeat clarsimp.
Qed.

Hypothesis Hf : injective f.

Lemma mem_map : s x, (f x \in map f s) = (x \in s).
Proof.
  induct s; rewrite IHs; repeat case eqP; ins; clarify; exfalso; eauto.
Qed.

Lemma index_map : s x, index (f x) (map f s) = index x s.
Proof. unfold index; induction s; clarsimp; desf; clarify; eauto; exfalso; eauto. Qed.

Lemma map_inj_uniq : s, uniq (map f s) = uniq s.
Proof. by induction s; clarsimp; rewrite mem_map, IHs. Qed.

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.
Proof. by induction s; clarsimp; rewrite IHs. Qed.

Section MapComp.

Variable T1 T2 T3 : Type.

Lemma map_id : s : list T1, map id s = s.
Proof. by induction s; simpls; rewrite IHs. Qed.

Lemma eq_map : f1 f2 : T1 T2, f1 =1 f2 map f1 =1 map f2.
Proof. red; induction x; clarsimp; f_equal; clarsimp. Qed.

Lemma map_comp : (f1 : T2 T3) (f2 : T1 T2) s,
  map (f1 \o f2) s = map f1 (map f2 s).
Proof. induction s; clarsimp; f_equal; clarsimp. Qed.

Lemma mapK : (f1 : T1 T2) (f2 : T2 T1),
  cancel f1 f2 cancel (map f1) (map f2).
Proof. red; induction x; clarsimp; f_equal; clarsimp. Qed.

End MapComp.

Lemma eq_in_map : (T1 : eqType) T2 (f1 f2 : T1 T2) (s : list T1),
  {in s, f1 =1 f2} map f1 s = map f2 s.
Proof.
  by induction s; ins; f_equal; try apply IHs; try red; intros; apply H; clarsimp; clarsimp.
Qed.

Lemma map_id_in : (T : eqType) f (s : list T),
  {in s, f =1 id} map f s = s.
Proof. intros; apply eq_in_map in H; rewrite H; apply map_id. Qed.


Section Pmap.

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

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

Lemma map_pK : pcancel g f cancel (map g) pmap.
Proof. by red; induction x; ins; rewrite H, IHx. Qed.

Lemma length_pmap s :
  length (pmap s) = count (fun xmatch f x with Nonefalse | Some _true end) s.
Proof. induction s; ins; desf; simpls; auto. Qed.

Lemma pmapS_filter s :
  map some (pmap s)
  = map f (filter (fun xmatch f x with Nonefalse | Some _true end) s).
Proof. induction s; ins; desf; simpls; congruence. Qed.

Lemma pmap_filter (fK : ocancel f g) s :
  map g (pmap s) = filter (fun xmatch f x with Nonefalse | Some _true end) s.
Proof. induction s; ins; specialize (fK a); desf; simpls; congruence. Qed.

End Pmap.


Index sequence


Lemma length_iota : m n, length (iota m n) = n.
Proof. by induction[m] n; intros; simpl; try done; rewrite IHn. Qed.

Lemma iota_add : m n1 n2,
  iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
Proof. by induction[m] n1; clarsimp; rewrite IHn1. Qed.

Lemma iota_addl : m1 m2 n,
  iota (m1 + m2) n = map (plus m1) (iota m2 n).
Proof.
induction[m2] n; clarsimp; rewrite <- IHn; clarsimp.
Qed.

Lemma nth_iota : n0 m n i, i < n nth n0 (iota m n) i = m + i.
Proof. by induction[m] n; destruct i; clarsimp; apply IHn. Qed.

Lemma mem_iota : m n i, (i \in iota m n) = (m i) && (i < m + n).
Proof.
induction[m] n; clarsimp; [by case cmpP|].
rewrite IHn; case (cmpP i m); clarsimp.
by rewrite ltnE, ltnW.
Qed.

Lemma iota_uniq : m n, uniq (iota m n).
Proof. induction[m] n; clarsimp; rewrite mem_iota; clarsimp. Qed.

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.
Proof. by intros; unfold mklist; rewrite length_map, length_iota. Qed.

Lemma eq_mklist : f g, f =1 g mklist f =1 mklist g.
Proof. by red; intros; apply eq_map. Qed.

Lemma nth_mklist : f n i, i < n nth x0 (mklist f n) i = f i.
Proof.
by intros; unfold mklist; rewrite (nth_map 0), nth_iota; rewrite ?length_iota.
Qed.

Lemma mklist_nth : s, mklist (nth x0 s) (length s) = s.
Proof.
  intros; apply (@eq_from_nth _ x0); rewrite length_mklist; try done.
  by intros; apply nth_mklist.
Qed.

End MakeSeq.

Lemma mklist_uniq : (T : eqType) (f : nat T) n,
  injective f uniq (mklist f n).
Proof. by unfold mklist; ins; rewrite map_inj_uniq, iota_uniq. Qed.

Section FoldRight.

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

Fixpoint foldr (l : list T) (z0: R) : R :=
  match l with
    | nilz0
    | x :: lf 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).
Proof. by intros; induction s1; simpls; rewrite IHs1. Qed.

Lemma foldr_map :
   s : list T1, foldr f (map h s) z0 = foldr (fun x zf (h x) z) s z0.
Proof. by induction s; simpls; rewrite IHs. Qed.

End FoldRightComp.

Definition sumn l := foldr plus l 0.

Lemma sumn_nil : sumn nil = 0.
Proof. done. Qed.

Lemma sumn_cons : n l, sumn (n :: l) = n + sumn l.
Proof. done. Qed.

Hint Rewrite sumn_nil sumn_cons : vlib.

Lemma sumn_nlist : x n : nat, sumn (nlist n x) = x × n.
Proof.
intros; rewrite mulnC; unfold nlist, ncons, sumn.
by induction n; clarsimp; rewrite IHn.
Qed.

Lemma sumn_app : s1 s2, sumn (s1 ++ s2) = sumn s1 + sumn s2.
Proof. by unfold sumn; induction s1; clarsimp; rewrite IHs1, addnA. Qed.

Lemma natnlist0P : s : list nat,
  reflect (s = nlist (length s) 0) (sumn s == 0).
Proof.
unfold sumn, nlist, ncons.
induction s; clarsimp; [by constructor; clarsimp|].
rewrite <- eqnE in *; destruct IHs; clarsimp.
case eqnP; constructor; congruence.
constructor; congruence.
Qed.

Section FoldLeft.

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

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

Lemma foldl_rev : z s, foldl z (rev s) = foldr (fun x zf z x) s z.
Proof.
  intros; revert z; pattern s; apply (last_ind); intros; simpl; try done.
  by rewrite rev_snoc, <- appl1, foldr_app, <- H.
Qed.

Lemma foldl_app : z s1 s2, foldl z (s1 ++ s2) = foldl (foldl z s1) s2.
Proof.
  intros; rewrite <- (rev_rev (s1 ++ s2)), foldl_rev, rev_app.
  by rewrite foldr_app, <- !foldl_rev, !rev_rev.
Qed.

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
    | nilnil
    | y :: s'f x y :: pairmap y s'
  end.

Lemma length_pairmap : x s, length (pairmap x s) = length s.
Proof. induct[x] s. Qed.

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).
Proof. induct s [n]. Qed.

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

Lemma length_scanl : x s, length (scanl x s) = length s.
Proof. induct[x] s. Qed.

Lemma nth_scanl : s n, n < length s
   x, nth x1 (scanl x s) n = foldl g x (take (S n) s).
Proof. induct s [n]. Qed.

Lemma scanlK :
  ( x, cancel (g x) (f x)) x, cancel (scanl x) (pairmap x).
Proof. induct[x] x0; rewrite H; hacksimp. Qed.

Lemma pairmapK :
  ( x, cancel (f x) (g x)) x, cancel (pairmap x) (scanl x).
Proof. induct[x] x0; rewrite H; hacksimp. Qed.

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.
Proof. by induction s as [|[x1 x2] s IH]; simpl; [|rewrite IH]. Qed.

Lemma unzip1_zip : s1 s2,
  length s1 length s2 unzip1 (zip s1 s2) = s1.
Proof. induct s1 [s2]. Qed.

Lemma unzip2_zip : s1 s2,
  length s2 length s1 unzip2 (zip s1 s2) = s2.
Proof. induct s1 [s2]. Qed.

Lemma length1_zip : s1 s2,
  length s1 length s2 length (zip s1 s2) = length s1.
Proof. induct s1 [s2]. Qed.

Lemma length2_zip : s1 s2,
  length s2 length s1 length (zip s1 s2) = length s2.
Proof. induct s1 [s2]. Qed.

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
    | nilnil
    | n :: sh'take n s :: reshape sh' (drop n s)
  end.

Lemma flatten_cons : l ll, flatten (l :: ll) = l ++ flatten ll.
Proof. done. Qed.

Lemma flatten_app : l l', flatten (l ++ l') = flatten l ++ flatten l'.
Proof. by induction l; ins; rewrite !flatten_cons, IHl, appA. Qed.

Hint Rewrite flatten_cons flatten_app : vlib.

Lemma length_flatten : ss, length (flatten ss) = sumn (shape ss).
Proof. induct ss. Qed.

Lemma flattenK : ss, reshape (shape ss) (flatten ss) = ss.
Proof.
by unfold flatten; induction ss; simpls; rewrite take_length_app, drop_length_app, IHss.
Qed.

Lemma reshapeKr : sh s, length s sumn sh flatten (reshape sh s) = s.
Proof.
induction sh; clarsimp; [by destruct s|rewrite IHsh, app_take_drop; clarsimp].
Qed.

Lemma reshapeKl : sh s, length s sumn sh shape (reshape sh s) = sh.
Proof.
  induction sh; clarsimp.
  case (ltnP); clarsimp.
  rewrite IHsh; clarsimp.
  rewrite <- (len_add2l a), subnKC; autos.
  assert (X := len_sub2 H H0); clarsimp.
  rewrite X in *; clarsimp.
  destruct (cmpP a (length s)); hacksimp.
Qed.

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.
Proof.
  induction l; clarsimp.
  case_eq (f a); clarsimp.
    by eapply (HasSpec (l1:=nil)); simpls.
  destruct IHl; clarsimp.
  eapply (HasSpec (l1 := a :: l1)); clarsimp.
Qed.

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.
Proof.
  induction l; clarsimp.
  destruct (eqP x a); clarsimp.
    by eapply (InSpec (l1 := nil)); simpls.
  destruct IHl; try eapply (InSpec (l1 := a :: l1)); clarsimp.
  case eqP; clarsimp.
Qed.

Lemma uniqE (T: eqType) (l : list T) :
  uniq l ( n l1 l2 l3, l = l1 ++ n :: l2 ++ n :: l3 False).
Proof.
  induction l; split; clarsimp.
  - by destruct l1.
  - destruct l1; simpls; clarify; [|eby eapply IHl].
    by clarsimp; simpls; rewrite eqnn in *; clarsimp.
  - apply/andP; split.
    × by apply/negP; intro X; case (inD X); clarsimp; eapply (H a nil).
    × by apply IHl; clarsimp; eapply (H _ (a :: l1)).
Qed.

Properties of In

Lemma In_eq : A (a:A) (l:list A), In a (a :: l).
Proof. vauto. Qed.

Lemma In_cons : A (a b:A) (l:list A), In b l In b (a :: l).
Proof. vauto. Qed.

Lemma In_nil : A (a:A), ¬ In a nil.
Proof. by red. Qed.

Lemma In_split : A x (l:list A), In x l l1 l2, l = l1++x::l2.
Proof.
  induction l; simpl; intros; des; vauto.
  - nil; vauto.
  - destruct IHl; des; try done; eexists (_ :: _); vauto.
Qed.

Lemma In_dec :
   A (D: x y:A, {x = y} + {x y}) (a: A) l, {In a l} + {¬ In a l}.
Proof.
  induction l; vauto; simpl; destruct (D a a0); intuition.
Qed.

Lemma In_appI1 : A (x:A) l (IN: In x l) l', In x (l++l').
Proof. induction l; ins; desf; eauto. Qed.

Lemma In_appI2 : A (x:A) l' (IN: In x l') l, In x (l++l').
Proof. induction l; ins; desf; eauto. Qed.

Lemma In_appD : A (x:A) l l' (IN: In x (l++l')), In x l In x l'.
Proof. induction l; intuition. Qed.

Lemma In_app : A (x:A) l l', In x (l++l') In x l In x l'.
Proof. intuition; auto using In_appI1, In_appI2. Qed.

Lemma In_rev : A (x: A) l, In x (rev l) In x l.
Proof.
  intros; unfold rev; symmetry; rewrite <- appl0 at 1; generalize (@nil A).
  induction l; simpl; intros; try rewrite <- IHl, !In_app; simpl; tauto.
Qed.

Lemma In_revI : A (x: A) l (IN: In x l), In x (rev l).
Proof. by intros; apply In_rev. Qed.

Lemma In_revD : A (x: A) l (IN: In x (rev l)), In x l.
Proof. by intros; apply In_rev. Qed.

Lemma In_mapI : A B (f: A B) x l (IN: In x l), In (f x) (map f l).
Proof.
  induction l; simpl; intros; intuition vauto.
Qed.

Lemma In_mapD :
   A B (f: AB) y l, In y (map f l) x, f x = y In x l.
Proof.
  induction l; simpl in *; intuition; des; eauto.
Qed.

Lemma In_map :
   A B (f: AB) y l, In y (map f l) x, f x = y In x l.
Proof.
  split; intros; des; clarify; auto using In_mapI, In_mapD.
Qed.

Lemma In_filter :
   A (x:A) f l, In x (filter f l) In x l f x.
Proof. induction l; ins; desf; simpls; intuition; clarify. Qed.

Lemma In_filterI :
   A x l (IN: In x l) (f: Abool) (F: f x), In x (filter f l).
Proof. by intros; apply In_filter. Qed.

Lemma In_filterD :
   A (x:A) f l (D: In x (filter f l)), In x l f x.
Proof. by intros; apply In_filter. Qed.

Hint Resolve In_eq In_cons In_appI1 In_appI2 In_mapI In_revI In_filterI : vlib.

Lemma uniqP : (T : eqType) (l: list T), reflect (List.NoDup l) (uniq l).
Proof.
  induction l; simpl; vauto.
  case (inP a l); ins; vauto; [|case IHl; vauto];
    by constructor; inversion 1; clarify.
Qed.

Lemma In_dec_strong :
   {A : Type} (P Q : A Prop)
    (dP: i:A, {P i} + {Q i})
    (l : list A),
      {e | In e l P e} + {( e, In e l Q e)}.
Proof.
  intros; induction l as [|h t [(e & IH & inP)|IH]]; vauto.
    by left; e; simpl; tauto.
  destruct (dP h) as [hdP | nhdP].
  - by left; h; simpl; tauto.
  - by right; intros e [H|H]; clarify; apply (IH e).
Qed.

Lemma In_dec_strong_prop :
   {A : Type} (P : A Prop)
    (dP: i:A, P i ¬ P i)
    (l : list A),
      ( e, In e l P e) ( e, ¬ (In e l P e)).
Proof.
  intros; induction l as [|h t [(e & IH & inP)|IH]].
  - by right; intros e [H _].
  - by left; e; simpl; tauto.
  - destruct (dP h) as [hdP | nhdP].
    + by left; h; simpl; tauto.
    + by right; intros e [[] Pe]; clarify; elim (IH e).
Qed.

Lemma In_dec_strong_neg :
   {A : Type} (P : A Prop)
    (dP: i:A, {P i} + {¬ P i})
    (l : list A),
      {e | In e l ¬ P e} + {( e, In e l P e)}.
Proof.
  intros; induction l as [|h t [(e & IH & inP)|IH]]; vauto.
    by left; e; simpl; tauto.
  destruct (dP h) as [hdP | nhdP].
  - by right; intros e [H|H]; clarify; apply IH.
  - by left; h; simpl; tauto.
Qed.

Setoid rewriting for equality up to permutation


Require Import Setoid.

Add Parametric Relation (T: eqType) : (list T) (@perm_eq T)
  reflexivity proved by (@perm_eq_refl T)
  symmetry proved by (pre_from_symmetric (@perm_eq_sym T))
  transitivity proved by (@perm_eq_trans T)
  as perm_rel.

Lemma perm_eq_map (T U : eqType) (f : T U) :
   xs ys (PE : perm_eq xs ys), perm_eq (map f xs) (map f ys).
Proof.
  induction xs; intros; [apply perm_eq_nilD in PE; subst; apply perm_eq_refl |].
  apply perm_eq_consD in PE; des; subst; rewrite map_app; simpl.
  rewrite perm_eq_sym, perm_appC; simpl;
  rewrite perm_cons, perm_appC, perm_eq_sym, <- map_app; auto.
Qed.

Lemma perm_eq_flatten (T : eqType) :
   (xs ys: list (list T)) (PE : perm_eq xs ys), perm_eq (flatten xs) (flatten ys).
Proof.
  induction xs; intros; [apply perm_eq_nilD in PE; subst; apply perm_eq_refl |].
  apply perm_eq_consD in PE; des; subst; rewrite flatten_app, !flatten_cons.
  rewrite perm_eq_sym, perm_appCA, perm_app2l, <- flatten_app, perm_eq_sym; auto.
Qed.

Lemma perm_eq_map2 (T U : eqType) (f g : T U) :
   xs ys (PE : perm_eq xs ys) (EQ: x (IN: In x xs), f x = g x),
    perm_eq (map f xs) (map g ys).
Proof.
  induction xs; intros; [apply perm_eq_nilD in PE; subst; apply perm_eq_refl |].
  apply perm_eq_consD in PE; des; subst; rewrite map_app; simpl.
  rewrite perm_eq_sym, perm_appC; ins.
  rewrite EQ; vauto.
  rewrite perm_cons, perm_appC, perm_eq_sym, <- map_app; eauto.
Qed.

Add Parametric Morphism A : (@perm_eq A)
  with signature (@perm_eq A) ==> (@perm_eq A) ==> (@eq bool) as perm_morph.
Proof.
  ins; apply/perm_eqP in H; apply/perm_eqP in H0; apply/perm_eqP/perm_eqP; congruence.
Qed.

Add Parametric Morphism A a : (cons a)
  with signature (@perm_eq A) ==> (@perm_eq _) as cons_morph.
Proof. by ins; rewrite perm_cons. Qed.

Add Parametric Morphism A : (@app A)
  with signature (@perm_eq A) ==> (@perm_eq _) ==> (@perm_eq _) as app_morph.
Proof. by etransitivity; [rewrite perm_app2l|rewrite perm_app2r]. Qed.

Add Parametric Morphism A B f : (@map A B f)
  with signature (@perm_eq A) ==> (@perm_eq B) as map_morph.
Proof. apply perm_eq_map. Qed.

Add Parametric Morphism A : (@flatten A)
  with signature (@perm_eq _) ==> (@perm_eq A) as flatten_morph.
Proof. apply perm_eq_flatten. Qed.

Add Parametric Morphism T : (@uniq T)
  with signature (@perm_eq T) ==> (@eq bool) as uniq_morph.
Proof. apply perm_eq_uniq. Qed.


This page has been generated by coqdoc Imprint | Data protection