1 files changed, 60 insertions, 0 deletions

diff --git a/theories/upstream.v b/theories/upstream.v
new file mode 100644
index 0000000..b74add5
--- /dev/null
+++ b/theories/upstream.v
@@ -0,0 +1,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.