From e2211664fd74858e89e19790e8abd2c2fcbe0132 Mon Sep 17 00:00:00 2001 From: Xingyu Xie Date: Fri, 10 Jul 2026 15:28:49 +0200 Subject: [PATCH] new lemmas for List; four new operators: isprefix, prefixes, interval, rfind --- theories/datatypes/List.ec | 316 ++++++++++++++++++++++++++++++++++++- 1 file changed, 311 insertions(+), 5 deletions(-) diff --git a/theories/datatypes/List.ec b/theories/datatypes/List.ec index 074d659fa..a89e80f28 100644 --- a/theories/datatypes/List.ec +++ b/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.