From 5fc1f1fc46e936823f4a1910884ebc4c848ec21b Mon Sep 17 00:00:00 2001 From: Matthias Meijers Date: Wed, 19 Feb 2025 18:47:06 +0100 Subject: [PATCH] Add list lemmas and shorten other proofs with some of them.# --- theories/datatypes/List.ec | 84 ++++++++++++++++++++------------------ 1 file changed, 45 insertions(+), 39 deletions(-) diff --git a/theories/datatypes/List.ec b/theories/datatypes/List.ec index 63af4dfc4f..d7159c869a 100644 --- a/theories/datatypes/List.ec +++ b/theories/datatypes/List.ec @@ -85,6 +85,10 @@ proof. by []. qed. lemma behead_cons (x : 'a) xs: behead (x :: xs) = xs. proof. by []. qed. +lemma size_behead (s : 'a list) : + size (behead s) = if s = [] then 0 else size s - 1. +proof. by elim: s. qed. + (* -------------------------------------------------------------------- *) lemma head_behead (xs : 'a list) z0: xs <> [] => @@ -850,6 +854,10 @@ lemma drop_drop (s : 'a list) (i j : int) : 0 <= i => 0 <= j => drop i (drop j s) = drop (i + j) s. proof. by elim: s i j => //= /#. qed. +lemma behead_drop (s : 'a list) (n : int) : + 0 <= n => behead (drop n s) = drop (n + 1) s. +proof. by elim: s n => // /#. qed. + op take n (xs : 'a list) = with xs = [] => [] with xs = y :: ys => @@ -1624,6 +1632,10 @@ proof. (* FIXME: subseq *) by move: y_notin_s; apply/contra => /mem_rem. qed. +lemma uniq_drop (s : 'a list) (n : int) : + uniq s => uniq (drop n s). +proof. by elim: s n => // /#. qed. + (* -------------------------------------------------------------------- *) (* Removing duplicates *) (* -------------------------------------------------------------------- *) @@ -1647,6 +1659,10 @@ lemma count_uniq_mem s (x : 'a): uniq s => count (pred1 x) s = b2i (mem s x). proof. elim: s; smt(). qed. +lemma count_mem_uniq (s : 'a list) : + (forall x, count (pred1 x) s = b2i (mem s x)) => uniq s. +proof. elim s => //; smt(mem_count). qed. + lemma uniq_leq_size (s1 s2 : 'a list): uniq s1 => (mem s1 <= mem s2) => size s1 <= size s2. proof. (* FIXME: test case: for views *) @@ -1658,20 +1674,34 @@ proof. (* FIXME: test case: for views *) by rewrite -(mem_rot i) def_s2; case. qed. +lemma uniq_le_perm_eq (s1 s2 : 'a list) : + uniq s1 => mem s1 <= mem s2 => size s2 <= size s1 => perm_eq s1 s2. +proof. + elim: s1 s2 => [| x l ih s2 /= [ninl uql] lemem le1sz]; 1: smt(size_ge0). + move: (ih (rem x s2) uql _ _); 1,2: smt(mem_rem_neq size_rem). + rewrite -(perm_cons x) => pxc; rewrite (perm_eq_trans _ _ _ pxc). + by rewrite perm_eq_sym perm_to_rem /#. +qed. + +lemma uniq_eq_perm_eq (s1 s2 : 'a list) : + uniq s1 => mem s1 = mem s2 => size s2 = size s1 => perm_eq s1 s2. +proof. by move=> /(uniq_le_perm_eq s1 s2) + eqmem eqsz; rewrite eqmem eqsz. qed. + +lemma perm_eq_uniq_impl (s1 s2 : 'a list) : + perm_eq s1 s2 => uniq s1 => uniq s2. +proof. + move=> ^ /perm_eqP_pred1 + /perm_eq_mem + /count_uniq_mem => eqcnt eqin cntin. + by apply count_mem_uniq => x; rewrite -(eqcnt x) -(eqin x) (cntin x). +qed. + +lemma perm_eq_uniq (s1 s2 : 'a list) : + perm_eq s1 s2 => uniq s1 <=> uniq s2. +proof. by move=> ^ /perm_eq_sym /perm_eq_uniq_impl + /perm_eq_uniq_impl. qed. + lemma leq_size_uniq (s1 s2 : 'a list): uniq s1 => (mem s1 <= mem s2) => size s2 <= size s1 => uniq s2. proof. - rewrite /Core.(<=); elim: s1 s2 => [[] | x s1 IHs s2] //; first smt(size_ge0). - move=> Us1x; have [not_s1x Us1] := Us1x; rewrite -(allP (mem s2)). - case=> s2x; rewrite allP => ss12 le_s21. - have := rot_to s2 x _ => //; case=> {s2x} i s3 def_s2. - move: le_s21; rewrite -(rot_uniq i) -(size_rot i) def_s2 /= lez_add2l => le_s31. - have ss13: forall y, mem s1 y => mem s3 y. - move=> y s1y; have := ss12 y _ => //. - by rewrite -(mem_rot i) def_s2 in_cons; case=> // eq_yx. - rewrite IHs //=; move: le_s31; apply contraL; rewrite -ltzNge => s3x. - rewrite -lez_add1r; have := uniq_leq_size (x::s1) s3 _ => //= -> //. - by apply (allP (mem s3)); rewrite /= s3x /= allP. + by move=> uqs1 lemem lesz; rewrite -(perm_eq_uniq s1) 1:uniq_le_perm_eq. qed. lemma uniq_size_uniq (s1 s2 : 'a list): @@ -1685,15 +1715,11 @@ proof. qed. lemma leq_size_perm (s1 s2 : 'a list): - uniq s1 => (mem s1 <= mem s2) => size s2 <= size s1 + uniq s1 => (mem s1 <= mem s2) => size s2 <= size s1 => (forall x, mem s1 x <=> mem s2 x) /\ (size s1 = size s2). proof. - move=> Us1 ss12 le_s21; have Us2 := leq_size_uniq s1 s2 _ _ _ => //. - rewrite -andaE; split=> [|h]; last by rewrite eq_sym -uniq_size_uniq. - move=> x; split; [by apply ss12 | move=> s2x; move: le_s21]. - apply absurd => not_s1x; rewrite -ltzNge -lez_add1r. - have := uniq_leq_size (x :: s1) => /= -> //=. - by rewrite /Core.(<=) -(allP (mem s2)) /= s2x /= allP. + move=> Us1 ss12 le_s21; have pmeq := uniq_le_perm_eq s1 s2 _ _ _ => //. + by split => [x|]; [apply perm_eq_mem | apply perm_eq_size]. qed. lemma perm_uniq (s1 s2 : 'a list): @@ -1705,13 +1731,6 @@ proof. by rewrite (uniq_size_uniq s2) // => y; rewrite Es12. qed. -lemma perm_eq_uniq (s1 s2 : 'a list): - perm_eq s1 s2 => uniq s1 <=> uniq s2. -proof. - move=> eq_s12; apply perm_uniq; - [by apply perm_eq_mem | by apply perm_eq_size]. -qed. - lemma uniq_perm_eq (s1 s2 : 'a list): uniq s1 => uniq s2 => (forall x, mem s1 x <=> mem s2 x) => perm_eq s1 s2. proof. @@ -1725,11 +1744,7 @@ lemma uniq_perm_eq_size ['a] (s1 s2 : 'a list) : => size s1 = size s2 => (mem s1 <= mem s2) => perm_eq s1 s2. -proof. -move=> uq_s1 uq_s2 eq_sz s1_in_s2; apply: uniq_perm_eq => //. -have := leq_size_perm s1 s2 uq_s1 s1_in_s2 _. -- by rewrite eq_sz. - by case=> + _; apply. -qed. +proof. by move => uqs1 _ eqsz lemem; rewrite uniq_le_perm_eq 3:eqsz. qed. lemma perm_eq_undup (s1 s2 : 'a list): perm_eq s1 s2 => perm_eq (undup s1) (undup s2). @@ -1738,15 +1753,6 @@ move=> peq_s1s2; rewrite uniq_perm_eq 1,2:undup_uniq => x. by rewrite 2!mem_undup &(perm_eq_mem). qed. -lemma count_mem_uniq (s : 'a list): - (forall x, count (pred1 x) s = b2i (mem s x)) => uniq s. -proof. - move=> count1_s; have Uus := undup_uniq s. - apply (perm_eq_uniq (undup s)); last by apply undup_uniq. - rewrite /perm_eq allP => x _ /=; rewrite count1_s. - by rewrite (count_uniq_mem (undup s) x) ?undup_uniq // mem_undup. -qed. - lemma filter_swap ['a] (xs ys : 'a list) : uniq xs => uniq ys => perm_eq (filter (mem xs) ys) (filter (mem ys) xs).