Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add list lemmas and shorten some other proofs using them #721

Merged
merged 1 commit into from
Feb 20, 2025
Merged

Add list lemmas and shorten some other proofs using them #721

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
84 changes: 45 additions & 39 deletions theories/datatypes/List.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 <> [] =>
Expand Down Expand Up @@ -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 =>
Expand Down Expand Up @@ -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 *)
(* -------------------------------------------------------------------- *)
Expand All @@ -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 *)
Expand All @@ -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):
Expand All @@ -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):
Expand All @@ -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.
Expand All @@ -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).
Expand All @@ -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).
Expand Down
Loading