New lemmas for List

theories/datatypes/List.ec

@@ -548,6 +548,11 @@ elim: xs => //= x xs ih; rewrite addrACA -ih.
 by move=> @/predI @/predC; case: (q x).
 qed.
 
+(* Inclusion-exclusion principle for count *)
+lemma count_predU ['a] (P Q : 'a -> bool) (s : 'a list) :
+  count (predU P Q) s = count P s + count Q s - count (predI P Q) s.
+proof. by elim: s => //= /#. qed.
+
 lemma count_pred0 (s : 'a list): count pred0 s = 0.
 proof. by rewrite -size_filter filter_pred0. qed.
 
@@ -722,6 +727,15 @@ rewrite {1 2}(_ : i = (i + -1)+1) 1:-addzA //.
 by rewrite ltz_add2r ltzS => /ih.
 qed.
 
+lemma find_le ['a] (p : 'a -> bool) (s : 'a list) (n : int) :
+  0 <= n < size s => p (nth witness s n) => find p s <= n.
+proof.
+move=> [ge0_n _] pn; apply/lezNgt/negP => lt_n.
+have npn: ! p (nth witness s n).
++ by rewrite &(before_find) ge0_n /= lt_n.
+by move: npn; rewrite pn.
+qed.
+
 lemma filter_pred1 x (s : 'a list) :
   filter (pred1 x) s = nseq (count (pred1 x) s) x.
 proof.
@@ -858,7 +872,12 @@ proof. by rewrite /= lezNgt; case: (0 < n). qed.
 
 lemma size_drop n (s : 'a list):
   0 <= n => size (drop n s) = max 0 (size s - n).
-proof. by elim: s n => //= /#. qed.
+proof.
+elim: s n=> //= n; first by smt(lez_maxl).
+move=> l ih n0 ?; case (n0 = 0).
++ by move=> -> /=; smt(size_ge0).
++ by smt().
+qed.
 
 lemma drop_cat n (s1 s2 : 'a list):
   drop n (s1 ++ s2) =
@@ -1130,10 +1149,9 @@ proof. by rewrite /rot /= take0 drop0 -cats1. qed.
 lemma rot_to (s : 'a list) x:
   mem s x => exists i s', rot i s = x :: s'.
 proof.
-  move=> s_x; pose i := index x s.
-  exists i; exists (drop (i + 1) s ++ take i s).
-  rewrite -cat_cons /i /rot => {i}; congr=> //=.
-  elim: s s_x => //= y s IHs; case: (x = y); smt().
+  rewrite (nthP witness).
+  elim => i [#] ???; exists i (drop (i + 1) s ++ take i s).
+  by rewrite /rot (drop_nth witness) 1:/# cat_cons.
 qed.
 
 (* -------------------------------------------------------------------- *)
@@ -1450,6 +1468,21 @@ qed.
 lemma trim_neg (xs : 'a list) (n : int): n < 0 => trim xs n = xs.
 proof. by move=> lt0_n; rewrite /trim take_le0 2:drop_le0 /#. qed.
 
+lemma trim_id ['a] (l : 'a list) (i : int) :
+  ! (0 <= i < size l) => trim l i = l.
+proof.
+move=> hrng; case: (i < 0) => hi; first by rewrite trim_neg.
+by rewrite /trim take_oversize 1:/# drop_oversize 1:/# cats0.
+qed.
+
+lemma mem_trim ['a] (l : 'a list) (i : int) (v : 'a) :
+  v \in trim l i => v \in l.
+proof.
+rewrite /trim mem_cat => -[h|h].
+- exact (mem_take i).
+- exact (mem_drop (i+1)).
+qed.
+
 lemma size_trim (xs : 'a list) (n : int): 0 <= n < size xs =>
   size (trim xs n) = size xs - 1.
 proof.
@@ -1646,6 +1679,21 @@ proof. by rewrite -cats1 uniq_catC /=. qed.
 lemma filter_uniq (s : 'a list) p: uniq s => uniq (filter p s).
 proof. by elim: s => //=; smt(mem_filter). qed.
 
+(* filtering preserves relative order: if a precedes b in `filter P l`   *)
+(* then a precedes b in l.                                               *)
+lemma index_filter_mono ['a] (P : 'a -> bool) (l : 'a list) (a b : 'a) :
+  uniq l => a \in filter P l => b \in filter P l =>
+  index a (filter P l) < index b (filter P l) =>
+  index a l < index b l.
+proof.
+elim: l => [|x l ih] //= [hxl hul].
+case: (P x) => Px /=.
++ rewrite !index_cons; case: (a = x) => hax; case: (b = x) => hbx //=;
+    by smt(mem_filter index_ge0 index_mem).
++ rewrite (index_cons a x) (index_cons b x);
+    smt(mem_filter index_ge0 index_mem).
+qed.
+
 lemma rot_uniq n (s : 'a list): uniq (rot n s) = uniq s.
 proof. by rewrite /rot uniq_catC cat_take_drop. qed.
 
@@ -1689,6 +1737,21 @@ apply ih => i j rng_i rng_j neqj_i.
 by move: (neq_nth (i + 1) (j + 1) _ _ _) => /#.
 qed.
 
+lemma nth_uniqP ['a] (s : 'a list) :
+  uniq s <=>
+  (forall (i j : int),
+       0 <= i < size s => 0 <= j < size s
+    => i <> j => nth witness s i <> nth witness s j).
+proof.
+split; last by apply nth_uniq.
+move=> uniq_s i j rng_i rng_j neq_ij.
+apply: contraL neq_ij => eq_nth.
+by rewrite -(index_uniq witness i s) // -(index_uniq witness j s) // eq_nth.
+qed.
+
+lemma uniq_take ['a] (s : 'a list) (n : int) : uniq s => uniq (take n s).
+proof. by rewrite -{1}[s](cat_take_drop n) cat_uniq. qed.
+
 lemma rem_uniq x s: uniq<:'a> s => uniq (rem x s).
 proof.                          (* FIXME: subseq *)
   elim: s=> [|y s ih] //= [y_notin_s uq_s].
@@ -2468,6 +2531,10 @@ theory Range.
     0 <= i < p - k => nth w (range k p) i = k + i.
   proof. by apply/nth_iota. qed.
 
+  lemma last_range (x0 : int) (n m : int) :
+    n < m => last x0 (range n m) = m - 1.
+  proof. by move=> ?; rewrite -(nth_last x0) nth_range size_range /#. qed.
+
   lemma le2_mem_range (m n i: int):
     (m <= i <= n) <=> (mem (range m (n+1)) i).
   proof. by rewrite mem_range ltzS. qed.
@@ -2570,6 +2637,10 @@ proof.
   by move=> _; rewrite addz1_neq0 // index_ge0.
 qed.
 
+lemma assoc_seq1 ['a 'b] (x1 x2 : 'a) (y : 'b) :
+   assoc [(x1, y)] x2 = (x1 = x2) ? Some y : None.
+proof. by rewrite assoc_cons assoc_nil [x2 = x1] eq_sym. qed.
+
 lemma assoc_head x y s: assoc<:'a, 'b> ((x, y) :: s) x = Some y.
 proof. by rewrite assoc_cons. qed.
 
@@ -3315,6 +3386,9 @@ qed.
 lemma subseq_cons (s : 'a list) x : subseq s (x :: s).
 proof. by apply/(@cat_subseq [] s [x] s)=> //; apply/subseq_refl. qed.
 
+lemma subseq_behead ['a] (s : 'a list) : subseq (behead s) s.
+proof. by case: s => //= x s; apply: subseq_cons. qed.
+
 lemma subseq_consI ['a] (x : 'a) (s1 s2 : 'a list) :
   subseq (x :: s1) s2 => subseq s1 s2.
 proof.
@@ -3352,6 +3426,238 @@ rewrite !(ifF (_ <= 0)) ~-1:/#; apply: ih => //.
 by move: h; case: (x2 = x1) => //= ? /subseq_consI.
 qed.
 
+lemma subseq_range (l1 l2 r1 r2 : int) :
+   l1 <= l2 <= r2 <= r1 => subseq (range l2 r2) (range l1 r1).
+proof.
+move=> ?.
+rewrite [range l1 r1] (range_cat l2) 1,2:/#.
+rewrite [range l2 r1] (range_cat r2) 1,2:/#.
+by rewrite &(subseq_catL) &(subseq_catR) subseq_refl.
+qed.
+
+(* -------------------------------------------------------------------- *)
+(*                              prefixes                                *)
+(* -------------------------------------------------------------------- *)
+op isprefix ['a] (s1 s2 : 'a list) : bool =
+  s1 = take (size s1) s2.
+
+op prefixes ['a] (s : 'a list) =
+  map (fun i => take i s) (range 0 (size s + 1)).
+
+lemma isprefix_size ['a] (s1 s2 : 'a list) :
+  isprefix s1 s2 => size s1 <= size s2.
+proof. by move=> @/isprefix ->; rewrite size_take //#. qed.
+
+lemma isprefixP ['a] (s1 s2 : 'a list) :
+  isprefix s1 s2 <=> (exists t, s1 ++ t = s2).
+proof.
+split=> @/isprefix.
+- by move=> ->; exists (drop (size s1) s2); rewrite cat_take_drop.
+- by case=> t <-; rewrite take_cat_le /= take_size.
+qed.
+
+lemma isprefix_catR ['a] (q2 q1 p : 'a list) :
+  isprefix (q1 ++ q2) p => isprefix q1 p.
+proof.
+rewrite /isprefix => />?.
++ have ?: take (size q1) (q1 ++ q2) = q1.
+  + by rewrite take_cat /= take0 cats0.
+  have ->/#: take (size q1) p = take (size q1) (take (size (q1 ++ q2)) p).
+  + by rewrite size_cat take_take #smt:(size_ge0).
+qed.
+
+lemma isprefix_elem ['a] (s1 s2 : 'a list) :
+    isprefix s1 s2 <=> (size s1 <= size s2
+                        /\ forall i, 0 <= i < size s1 =>
+                             nth witness s1 i = nth witness s2 i).
+proof.
+rewrite /isprefix; split.
++ by smt(size_take nth_take).
++ move=> [#]??; apply (eq_from_nth witness).
+  + by smt(size_take size_ge0).
+  + by smt(nth_take).
+qed.
+
+lemma isprefix1 ['a] (s1 : 'a list) (x : 'a) :
+    isprefix s1 (s1 ++ [x]).
+proof. by rewrite /isprefix take_cat /= cats0 //. qed.
+
+lemma prefixes_size ['a] (s : 'a list) :
+    size (prefixes s) = size s + 1.
+proof.
+by rewrite /prefixes size_map size_range lez_maxr #smt:(size_ge0).
+qed.
+
+lemma prefixes_isprefix ['a] (s1 s2 : 'a list) :
+    s1 \in (prefixes s2) <=> isprefix s1 s2.
+proof.
+rewrite /prefixes /isprefix (nthP witness) => />; split.
++ move=> i.
+  rewrite size_map size_range lez_maxr 1:#smt:(size_ge0) //= => ??.
+  rewrite (nth_map witness witness) 1:#smt:(size_range size_ge0).
+  by rewrite nth_range //= size_take // #smt:(take_take).
++ move=> H.
+  exists (size s1).
+  rewrite size_map size_range lez_maxr 1:#smt:(size_ge0).
+  have ?: size s1 <= size s2 by rewrite H size_take #smt:(size_ge0).
+  rewrite (nth_map witness witness).
+  + by rewrite size_range lez_maxr #smt:(size_ge0).
+  by rewrite nth_range //= #smt:(size_ge0).
+qed.
+
+lemma isprefix_take ['a] (s : 'a list) (n : int) :
+  isprefix (take n s) s.
+proof.
+case (n <= 0) => @/isprefix ?.
++ by rewrite take_le0 //= take0.
+case (n < size s) => ?.
++ by rewrite size_take /#.
+by rewrite !take_oversize /#.
+qed.
+
+(* -------------------------------------------------------------------- *)
+(*                               rfind                                  *)
+(*    rfind p l = index of the last element of l satisfying p           *)
+(*    (or -1 if there is none).                                         *)
+(* -------------------------------------------------------------------- *)
+op rfind ['a] (p : 'a -> bool) (l : 'a list) : int =
+  size l - find p (rev l) - 1.
+
+lemma rfind_cat ['a] (p : 'a -> bool) (l1 l2 : 'a list) :
+  rfind p (l1 ++ l2) = if has p l2 then size l1 + rfind p l2 else rfind p l1.
+proof. by rewrite /rfind rev_cat -has_rev size_cat find_cat size_rev /#. qed.
+
+lemma rfind_catl ['a] (p : 'a -> bool) (l1 l2 : 'a list) :
+  !has p l2 => rfind p (l1 ++ l2) = rfind p l1.
+proof. by rewrite rfind_cat => ->. qed.
+
+lemma rfind_in_eq ['a] (p1 p2 : 'a -> bool) (l : 'a list) :
+     (forall x, x \in l => (p1 x <=> p2 x))
+  => rfind p1 l = rfind p2 l.
+proof.
+move=> ? @/rfind.
+suff: find p1 (rev l) = find p2 (rev l) by smt().
+apply find_eq_in => x.
+by rewrite mem_rev /#.
+qed.
+
+lemma rfind_rng ['a] (p : 'a -> bool) (s : 'a list) :
+  -1 <= rfind p s < size s.
+proof.
+rewrite /rfind; split.
++ suff: find p (rev s) <= size s by smt().
+  by rewrite -(size_rev s) find_size.
++ by smt(find_ge0).
+qed.
+
+lemma rfind_ge ['a] (p : 'a -> bool) (s : 'a list) (i : int) :
+     0 <= i < size s
+  => p (nth witness s i)
+  => i <= rfind p s.
+proof.
+move=> Hirng @/rfind.
+rewrite -{1}revK (nth_rev witness) size_rev 1:/# => ?.
+suff: find p (rev s) <= size s - i - 1 by smt().
+by rewrite &(find_le) 1:size_rev /#.
+qed.
+
+lemma rfind_last ['a] (p : 'a -> bool) (l : 'a list) :
+  l <> [] => (p (last witness l) <=> rfind p l = size l - 1).
+proof.
+case: l => // x s _.
+rewrite last_cons (lastI x s) -cats1 rfind_cat size_cat /=.
+suff: p (last x s) => rfind p [last x s] = 0 by smt(rfind_rng).
+move=> Hp; apply/eqz_leq; split.
++ by smt(rfind_rng).
++ by rewrite &(rfind_ge).
+qed.
+
+lemma rfindP ['a] (p : 'a -> bool) (s : 'a list) :
+  0 <= rfind p s => p (nth witness s (rfind p s)).
+proof.
+move=> @/rfind Hge0.
+have Hhas : has p (rev s).
++ by rewrite has_find size_rev /#.
+rewrite -{1}revK nth_rev size_rev.
++ by smt(find_ge0).
+by smt(nth_find).
+qed.
+
+(* -------------------------------------------------------------------- *)
+(*                              interval                                *)
+(*    interval s l r = the slice s[l..r) (l included, r excluded)       *)
+(* -------------------------------------------------------------------- *)
+op interval ['a] (s : 'a list) (l r : int) = drop l (take r s).
+
+lemma interval_catR ['a] (s1 s2 : 'a list) (l r : int) :
+  r <= size s1 => interval (s1 ++ s2) l r = interval s1 l r.
+proof. by move=> *; rewrite /interval take_cat_le ifT. qed.
+
+lemma interval_size ['a] (s : 'a list) (l r : int) :
+  0 <= l <= r <= size s => size (interval s l r) = r - l.
+proof. by move => ?; rewrite /interval size_drop 1:/# size_take /#. qed.
+
+lemma interval_nth ['a] (s : 'a list) (m l r : int) (x : 'a) :
+     0 <= l
+  => 0 <= m < r - l
+  => nth x (interval s l r) m = nth x s (m + l).
+proof. by move => ??; rewrite /interval nth_drop // 1:/# nth_take /#. qed.
+
+lemma interval_split ['a] (s : 'a list) (m l r : int) :
+     0 <= l <= m <= r <= size s
+  => interval s l r = interval s l m ++ interval s m r.
+proof.
+move=> ?; apply (eq_from_nth witness).
++ by rewrite size_cat !interval_size /#.
++ move=> i; rewrite interval_size 1:/#.
+  case: (i < m - l) => ??.
+  + rewrite interval_nth 1,2:/# nth_cat interval_size #smt:(interval_nth).
+  + rewrite nth_cat interval_size #smt:(interval_nth).
+qed.
+
+lemma intervalS ['a] (s : 'a list) (n m : int) :
+     0 <= n < m <= size s
+  => m = n + 1 => interval s n m = [nth witness s n].
+proof.
+move=> ??; rewrite /interval drop_take 1,2:/# (_ : _ - _ = 1) 1:/#.
+by rewrite (drop_take1_nth witness) /#.
+qed.
+
+lemma interval_empty ['a] (s : 'a list) (l r : int) :
+  r <= l => interval s l r = [].
+proof.
+move=> ?; rewrite /interval.
+case (l <= 0) => ?.
++ by rewrite drop_le0 // &(take_le0) /#.
++ rewrite drop_oversize //.
+  case (r <= 0) => ?.
+  + by rewrite take_le0 // /#.
+  + by rewrite size_take /#.
+qed.
+
+lemma interval_oversize ['a] (s : 'a list) (l r : int) :
+    size s <= r => interval s l r = drop l s.
+proof. by move=> *; rewrite /interval take_oversize. qed.
+
+lemma interval_subseq ['a] (s : 'a list) (l1 l2 r1 r2 : int) :
+     0 <= l1 <= l2 <= r1 <= r2
+  => subseq (interval s l2 r1) (interval s l1 r2).
+proof.
+move=> rng @/interval.
+apply (subseq_trans (drop l1 (take r1 s))).
+- have ->: drop l2 (take r1 s) = drop (l2 - l1) (drop l1 (take r1 s)).
+  + by rewrite drop_drop 1,2:/# (_ : l2 - l1 + l1 = l2) 1:/#.
+  by apply subseq_drop; exact subseq_refl.
+- apply subseq_drop_congr.
+  have ->: take r1 s = take r1 (take r2 s).
+  + by rewrite take_take ifT 1:/#.
+  by apply subseq_take; exact subseq_refl.
+qed.
+
+lemma interval_take ['a] (s : 'a list) (l r : int) :
+    l <= 0 => interval s l r = take r s.
+proof. by move => ? @/interval; rewrite drop_le0 //. qed.
+
 lemma rem_subseq x (s : 'a list) : subseq (rem x s) s.
 proof.
 elim: s => //= y s ih; rewrite eq_sym.