Add some useful advantage properties

theories/Crypt/package/fmap_extra.v

@@ -153,6 +153,17 @@ Qed.
 Lemma fsubmapxx {T : ordType} {S} (m : {fmap T → S}) : fsubmap m m.
 Proof. rewrite /fsubmap unionmI //. Qed.
 
+Lemma fsubmap_implies_fcompat :
+  forall {T : ordType} {S} {E E' : _},
+    fsubmap E' E →
+    fcompat (T := T) (S := S) E' E.
+Proof.
+  intros.
+  eapply fsubmap_fcompat.
+  1: apply H.
+  apply fsubmapxx.
+Qed.
+
 Lemma fsubmap_eq {T : ordType} {S} (m m' : {fmap T → S}) :
   fsubmap m m' → fsubmap m' m → m = m'.
 Proof.
@@ -513,3 +524,105 @@ Qed.
 
 Hint Extern 4 (is_true (_ \notin _)) =>
   eapply notin_has_separate; [ eassumption | ] : fmap_solve_db.
+
+Lemma fmap_as_list :
+  forall {T : ordType} {S} (p2 : {fmap T -> S}),
+  exists l, mkfmap l = p2.
+Proof.
+  destruct p2.
+  exists fmval.
+  - apply eq_fmap.
+    apply mkfmapE.
+Qed.
+
+Lemma fmapK_list :
+  forall {T : ordType} {S} (p2 : {fmap T -> S}),
+  mkfmap (FMap.fmval p2) = p2.
+Proof.
+  destruct p2.
+  apply eq_fmap.
+  apply mkfmapE.
+Qed.
+
+Lemma in_cat :
+  forall (X : eqType) l1 l2, forall (x : X), (x \in (l1 ++ l2)) = ((x \in l1) || (x \in l2)).
+Proof.
+  intros.
+  generalize dependent l1.
+  induction l2 ; intros.
+  + setoid_rewrite List.app_nil_r.
+    now rewrite Bool.orb_false_r.
+  + replace (l1 ++ _) with ((l1 ++ [:: a]) ++ l2).
+    2:{
+      rewrite <- List.app_assoc.
+      reflexivity.
+    }
+    rewrite IHl2.
+    rewrite in_cons.
+    induction l1.
+    * simpl.
+      rewrite in_cons.
+      rewrite in_nil.
+      now rewrite Bool.orb_false_r.
+    * simpl.
+      rewrite !in_cons.
+      rewrite <- !orbA.
+      now rewrite IHl1.
+Qed.
+
+Lemma fdisjoint_weak : (forall {T : ordType}, forall (A B C : {fset T}), A :#: B -> A :#: (B :\: C)).
+Proof.
+  intros.
+  apply /fsetDidPl.
+  rewrite fsetDDr.
+  move /fsetDidPl: H ->.
+  apply eq_fset.
+  intros i.
+  rewrite in_fset.
+  simpl.
+  rewrite in_cat.
+  rewrite in_fsetI.
+  destruct (i \in A) eqn:i_in ; now rewrite i_in.
+Qed.
+
+Lemma fsubmap_split :
+  forall {T : ordType} {S}, forall (A B : {fmap T -> S}), fsubmap A B -> exists C, unionm A C = B /\ fseparate A C.
+Proof.
+  clear ; intros.
+  exists (filterm (fun x y => x \notin domm A) B).
+
+  assert (unionm A (filterm (λ (x : T) (_ : S), x \notin domm A) B) = B).
+  {
+    apply eq_fmap.
+    intros ?.
+    rewrite unionmE.
+    destruct (A x) eqn:Ahas.
+    + simpl.
+      symmetry.
+      apply (fsubmap_fhas _ _ (x, s) H Ahas).
+    + simpl.
+      rewrite filtermE.
+      unfold obind, oapp.
+      move /dommPn: Ahas ->.
+      now destruct (B x).
+  }
+  split.
+  - apply H0.
+  - simpl.
+    rewrite <- (fmapK_list B) in H, H0 |- *.
+    destruct B ; simpl in *.
+    simpl.
+    constructor.
+    clear i H H0.
+    induction fmval.
+    + rewrite filterm0.
+      rewrite domm0.
+      apply fdisjoints0.
+    + simpl.
+      rewrite filterm_set.
+
+      destruct (a.1 \notin domm A) eqn:a_not_in_A.
+      2: rewrite domm_rem ; apply fdisjoint_weak.
+      1: rewrite domm_set ; rewrite fdisjointUr ; rewrite fdisjoints1 ; rewrite a_not_in_A ; simpl.
+      1,2: apply IHfmval.
+Qed.