blob: b74add502e9795f12e3d3913c5cfcbda16330370 (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
From stdpp Require Import prelude ssreflect gmultiset.
From stdpp Require Import options.
Lemma prefix_of_fmap {A B} (f : A → B) (xs xs' : list A) :
xs `prefix_of` xs' →
f <$> xs `prefix_of` f <$> xs'.
Proof. intros [ys ->]. exists (f <$> ys). apply fmap_app. Qed.
Lemma prefix_sublist {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 `sublist_of` l2.
Proof. intros [k ->]. by apply sublist_inserts_r. Qed.
Lemma prefix_submseteq {A} (l1 l2 : list A) : l1 `prefix_of` l2 → l1 ⊆+ l2.
Proof. intros [k ->]. by apply submseteq_inserts_r. Qed.
Lemma take_less_prefix {A} n m (xs : list A) : n ≤ m → take n xs `prefix_of` take m xs.
Proof.
intros Hnm.
replace n with (n `min` m); last lia.
rewrite -take_take.
apply prefix_take.
Qed.
Lemma take_app_prefix {A} n (xs ys : list A) : take n xs `prefix_of` take n (xs ++ ys).
Proof. unfold prefix. exists (take (n - length xs) ys). apply firstn_app. Qed.
Lemma Forall_prefix {A} (xs xs' : list A) Φ : xs `prefix_of` xs' → Forall Φ xs' → Forall Φ xs.
Proof. by intros [? ->] [? _]%Forall_app. Qed.
Lemma drop_cons_inv {A} n x (xs xs' : list A) :
drop n xs = x :: xs' → xs !! n = Some x ∧ drop (S n) xs = xs'.
Proof.
intros Hxs. split.
- by rewrite -[n]Nat.add_0_r -lookup_drop Hxs.
- by rewrite -Nat.add_1_r -drop_drop Hxs.
Qed.
Lemma list_to_set_disj_size `{Countable A} (l : list A) :
size (list_to_set_disj l : gmultiset A) = length l.
Proof.
induction l; first done.
by rewrite /= gmultiset_size_disj_union IHl gmultiset_size_singleton.
Qed.
Lemma gmultiset_subseteq_size_eq `{Countable A, LeibnizEquiv A} (X Y : gmultiset A) :
X ⊆ Y → size Y ≤ size X → X = Y.
Proof.
revert Y. induction X using gmultiset_ind; intros Y HY Hsize.
- rewrite gmultiset_size_empty in Hsize.
apply symmetry, gmultiset_size_empty_inv. lia.
- rewrite gmultiset_size_disj_union gmultiset_size_singleton in Hsize.
assert (X ⊆ Y ∖ {[+ x +]}) as HXY%IHX; [multiset_solver..|].
rewrite gmultiset_size_difference; last multiset_solver.
rewrite gmultiset_size_singleton. lia.
Qed.
Lemma elements_list_to_set_disj_perm `{Countable A} (l : list A) : l ≡ₚ elements (list_to_set_disj l : gmultiset A).
Proof.
induction l; first done.
by rewrite list_to_set_disj_cons gmultiset_elements_disj_union gmultiset_elements_singleton -IHl.
Qed.
|
