Start integrating memory model with sequence point semantics.

theories/assoc.v

@@ -11,13 +11,13 @@ Require Export fin_maps.
 
 (** Because the association list is sorted using [strict lexico] instead of
 [lexico], it automatically guarantees that no duplicates exist. *)
-Definition assoc (K : Type) `{Lexico K} `{!TrichotomyT lexico}
-    `{!StrictOrder lexico} (A : Type) : Type :=
+Definition assoc (K : Type) `{Lexico K, !TrichotomyT lexico,
+    !StrictOrder lexico} (A : Type) : Type :=
   dsig (λ l : list (K * A), StronglySorted lexico (fst <$> l)).
 
 Section assoc.
-Context `{Lexico K} `{!StrictOrder lexico}.
-Context `{∀ x y : K, Decision (x = y)} `{!TrichotomyT lexico}.
+Context `{Lexico K, !StrictOrder lexico,
+  ∀ x y : K, Decision (x = y), !TrichotomyT lexico}.
 
 Infix "⊂" := lexico.
 Notation assoc_before j l :=
@@ -44,6 +44,7 @@ Ltac simplify_assoc := intros;
   | H : StronglySorted _ (_ :: _) |- _ => inversion_clear H
   | _ => progress decompose_elem_of_list
   | _ => progress simplify_equality'
+  | _ => match goal with |- context [?o ≫= _] => by destruct o end
   end;
   repeat first
   [ progress simplify_order
@@ -139,30 +140,45 @@ Proof.
     destruct (f _); simplify_assoc.
 Qed.
 Lemma assoc_fmap_wf {A B} (f : A → B) (l : list (K * A)) :
-  assoc_wf l → assoc_wf (snd_map f <$> l).
+  assoc_wf l → assoc_wf (prod_map id f <$> l).
 Proof.
   intros. by rewrite <-list_fmap_compose,
     (list_fmap_ext _ fst l l) by (done; by intros []).
 Qed.
 Global Program Instance assoc_fmap: FMap (assoc K) := λ A B f m,
   dexist _ (assoc_fmap_wf f _ (proj2_dsig m)).
-
 Lemma assoc_lookup_fmap {A B} (f : A → B) (l : list (K * A)) i :
-  assoc_lookup_raw i (snd_map f <$> l) = fmap f (assoc_lookup_raw i l).
+  assoc_lookup_raw i (prod_map id f <$> l) = fmap f (assoc_lookup_raw i l).
 Proof. induction l as [|[??]]; simplify_assoc. Qed.
 
-Fixpoint assoc_merge_aux {A B} (f : option A → option B)
+Fixpoint assoc_omap_raw {A B} (f : A → option B)
     (l : list (K * A)) : list (K * B) :=
   match l with
   | [] => []
-  | (i,x) :: l => assoc_cons i (f (Some x)) (assoc_merge_aux f l)
+  | (i,x) :: l => assoc_cons i (f x) (assoc_omap_raw f l)
   end.
+Lemma assoc_omap_raw_before {A B} (f : A → option B) l j :
+  assoc_before j l → assoc_before j (assoc_omap_raw f l).
+Proof. induction l as [|[??]]; simplify_assoc. Qed.
+Hint Resolve assoc_omap_raw_before.
+Lemma assoc_omap_wf {A B} (f : A → option B) l :
+  assoc_wf l → assoc_wf (assoc_omap_raw f l).
+Proof. induction l as [|[??]]; simplify_assoc. Qed.
+Hint Resolve assoc_omap_wf.
+Global Instance assoc_omap: OMap (assoc K) := λ A B f m,
+  dexist _ (assoc_omap_wf f _ (proj2_dsig m)).
+Lemma assoc_omap_spec {A B} (f : A → option B) l i :
+  assoc_wf l →
+  assoc_lookup_raw i (assoc_omap_raw f l) = assoc_lookup_raw i l ≫= f.
+Proof. intros. induction l as [|[??]]; simplify_assoc. Qed.
+Hint Rewrite @assoc_omap_spec using (by eauto) : assoc.
+
 Fixpoint assoc_merge_raw {A B C} (f : option A → option B → option C)
     (l : list (K * A)) : list (K * B) → list (K * C) :=
   fix go (k : list (K * B)) :=
   match l, k with
-  | [], _ => assoc_merge_aux (f None) k
-  | _, [] => assoc_merge_aux (flip f None) l
+  | [], _ => assoc_omap_raw (f None ∘ Some) k
+  | _, [] => assoc_omap_raw (flip f None ∘ Some) l
   | (i,x) :: l, (j,y) :: k =>
     match trichotomyT lexico i j with
     | (**i i ⊂ j *) inleft (left _) =>
@@ -173,15 +189,13 @@ Fixpoint assoc_merge_raw {A B C} (f : option A → option B → option C)
       assoc_cons j (f None (Some y)) (go k)
     end
   end.
-
 Section assoc_merge_raw.
-  Context  {A B C} (f : option A → option B → option C).
-
+  Context {A B C} (f : option A → option B → option C).
   Lemma assoc_merge_nil_l k :
-    assoc_merge_raw f [] k = assoc_merge_aux (f None) k.
+    assoc_merge_raw f [] k = assoc_omap_raw (f None ∘ Some) k.
   Proof. by destruct k. Qed.
   Lemma assoc_merge_nil_r l :
-    assoc_merge_raw f l [] = assoc_merge_aux (flip f None) l.
+    assoc_merge_raw f l [] = assoc_omap_raw (flip f None ∘ Some) l.
   Proof. by destruct l as [|[??]]. Qed.
   Lemma assoc_merge_cons i x j y l k :
     assoc_merge_raw f ((i,x) :: l) ((j,y) :: k) =
@@ -195,14 +209,8 @@ Section assoc_merge_raw.
       end.
   Proof. done. Qed.
 End assoc_merge_raw.
-
 Arguments assoc_merge_raw _ _ _ _ _ _ : simpl never.
 Hint Rewrite @assoc_merge_nil_l @assoc_merge_nil_r @assoc_merge_cons : assoc.
-
-Lemma assoc_merge_aux_before {A B} (f : option A → option B) l j :
-  assoc_before j l → assoc_before j (assoc_merge_aux f l).
-Proof. induction l as [|[??]]; simplify_assoc. Qed.
-Hint Resolve assoc_merge_aux_before.
 Lemma assoc_merge_before {A B C} (f : option A → option B → option C) l1 l2 j :
   assoc_before j l1 → assoc_before j l2 →
   assoc_before j (assoc_merge_raw f l1 l2).
@@ -211,26 +219,14 @@ Proof.
     intros l2; induction l2 as [|[??] l2 IH2]; simplify_assoc.
 Qed.
 Hint Resolve assoc_merge_before.
-
 Lemma assoc_merge_wf {A B C} (f : option A → option B → option C) l1 l2 :
   assoc_wf l1 → assoc_wf l2 → assoc_wf (assoc_merge_raw f l1 l2).
 Proof.
-  revert A B C f l1 l2. assert (∀ A B (f : option A → option B) l,
-    assoc_wf l → assoc_wf (assoc_merge_aux f l)).
-  { intros ?? j l. induction l as [|[??]]; simplify_assoc. }
-  intros A B C f l1. induction l1 as [|[i x] l1 IH];
+  revert l2. induction l1 as [|[i x] l1 IH];
     intros l2; induction l2 as [|[j y] l2 IH2]; simplify_assoc.
 Qed.
 Global Instance assoc_merge: Merge (assoc K) := λ A B C f m1 m2,
-  dexist (merge f (`m1) (`m2))
-    (assoc_merge_wf _ _ _ (proj2_dsig m1) (proj2_dsig m2)).
-
-Lemma assoc_merge_aux_spec {A B} (f : option A → option B) l i :
-  f None = None → assoc_wf l →
-  assoc_lookup_raw i (assoc_merge_aux f l) = f (assoc_lookup_raw i l).
-Proof. intros. induction l as [|[??]]; simplify_assoc. Qed.
-Hint Rewrite @assoc_merge_aux_spec using (by eauto) : assoc.
-
+  dexist _ (assoc_merge_wf f _ _ (proj2_dsig m1) (proj2_dsig m2)).
 Lemma assoc_merge_spec {A B C} (f : option A → option B → option C) l1 l2 i :
   f None None = None → assoc_wf l1 → assoc_wf l2 →
   assoc_lookup_raw i (assoc_merge_raw f l1 l2) =
@@ -268,6 +264,7 @@ Proof.
   * intros ??? [??] ?. apply assoc_lookup_fmap.
   * intros ? [??]. apply assoc_to_list_nodup; auto.
   * intros ? [??] ??. apply assoc_to_list_elem_of; auto.
+  * intros ??? [??] ?. apply assoc_omap_spec; auto.
   * intros ????? [??] [??] ?. apply assoc_merge_spec; auto.
 Qed.
 End assoc.
@@ -275,8 +272,8 @@ End assoc.
 (** * Finite sets *)
 (** We construct finite sets using the above implementation of maps. *)
 Notation assoc_set K := (mapset (assoc K)).
-Instance assoc_map_dom `{Lexico K} `{!TrichotomyT (@lexico K _)}
-  `{!StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
+Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
+  !StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
 Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
-    `{!StrictOrder lexico} `{∀ x y : K, Decision (x = y)} :
+    `{!StrictOrder lexico, ∀ x y : K, Decision (x = y)} :
   FinMapDom K (assoc K) (assoc_set K) := mapset_dom_spec.

theories/collections.v

@@ -5,6 +5,9 @@ importantly, it implements some tactics to automatically solve goals involving
 collections. *)
 Require Export base tactics orders.
 
+Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
+  ∀ x, x ∈ X → x ∈ Y.
+
 (** * Basic theorems *)
 Section simple_collection.
   Context `{SimpleCollection A C}.
@@ -16,8 +19,6 @@ Section simple_collection.
   Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y.
   Proof. intros. apply elem_of_union. auto. Qed.
 
-  Global Instance collection_subseteq: SubsetEq C := λ X Y,
-    ∀ x, x ∈ X → x ∈ Y.
   Global Instance: BoundedJoinSemiLattice C.
   Proof. firstorder auto. Qed.
 
@@ -34,29 +35,25 @@ Section simple_collection.
   Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
   Proof.
     split.
-    * intros ??. rewrite elem_of_singleton. intro. by subst.
+    * intros ??. rewrite elem_of_singleton. by intros ->.
     * intros Ex. by apply (Ex x), elem_of_singleton.
   Qed.
   Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton.
-  Proof. repeat intro. by subst. Qed.
+  Proof. by repeat intro; subst. Qed.
   Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5.
-  Proof. intros ???. subst. firstorder. Qed.
+  Proof. intros ???; subst. firstorder. Qed.
 
   Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
   Proof.
     split.
-    * induction Xs; simpl; intros HXs.
-      + by apply elem_of_empty in HXs.
-      + setoid_rewrite elem_of_cons.
-        apply elem_of_union in HXs. naive_solver.
-    * intros [X []]. induction 1; simpl.
-      + by apply elem_of_union_l.
-      + intros. apply elem_of_union_r; auto.
+    * induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
+      setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
+    * intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
+      intros. apply elem_of_union_r; auto.
   Qed.
 
   Lemma non_empty_singleton x : {[ x ]} ≢ ∅.
   Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
-
   Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y.
   Proof. by rewrite elem_of_singleton. Qed.
   Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
@@ -64,7 +61,6 @@ Section simple_collection.
 
   Section leibniz.
     Context `{!LeibnizEquiv C}.
-
     Lemma elem_of_equiv_L X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
     Proof. unfold_leibniz. apply elem_of_equiv. Qed.
     Lemma elem_of_equiv_alt_L X Y :
@@ -78,7 +74,6 @@ Section simple_collection.
 
   Section dec.
     Context `{∀ X Y : C, Decision (X ⊆ Y)}.
-
     Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
     Proof.
       refine (cast_if (decide_rel (⊆) {[ x ]} X));
@@ -203,18 +198,12 @@ Section collection.
   Context `{Collection A C}.
 
   Global Instance: LowerBoundedLattice C.
-  Proof.
-    split.
-    * apply _.
-    * firstorder auto.
-    * solve_elem_of.
-  Qed.
+  Proof. split. apply _. firstorder auto. solve_elem_of. Qed.
 
   Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}.
   Proof. esolve_elem_of. Qed.
   Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
   Proof. esolve_elem_of. Qed.
-
   Lemma empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
   Proof. esolve_elem_of. Qed.
   Lemma difference_diag X : X ∖ X ≡ ∅.
@@ -226,12 +215,10 @@ Section collection.
 
   Section leibniz.
     Context `{!LeibnizEquiv C}.
-
     Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = {[x]}.
     Proof. unfold_leibniz. apply intersection_singletons. Qed.
     Lemma difference_twice_L X Y : (X ∖ Y) ∖ Y = X ∖ Y.
     Proof. unfold_leibniz. apply difference_twice. Qed.
-
     Lemma empty_difference_L X Y : X ⊆ Y → X ∖ Y = ∅.
     Proof. unfold_leibniz. apply empty_difference. Qed.
     Lemma difference_diag_L X : X ∖ X = ∅.
@@ -245,20 +232,14 @@ Section collection.
 
   Section dec.
     Context `{∀ X Y : C, Decision (X ⊆ Y)}.
-
     Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
-    Proof.
-      rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto.
-    Qed.
+    Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed.
     Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
-    Proof.
-      rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto.
-    Qed.
+    Proof. rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto. Qed.
     Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X.
     Proof.
-      split; intros x; rewrite !elem_of_union, elem_of_difference.
-      * destruct (decide (x ∈ X)); intuition.
-      * intuition.
+      split; intros x; rewrite !elem_of_union, elem_of_difference; [|intuition].
+      destruct (decide (x ∈ X)); intuition.
     Qed.
     Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅.
     Proof.
@@ -267,7 +248,6 @@ Section collection.
     Qed.
 
     Context `{!LeibnizEquiv C}.
-
     Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
     Proof. unfold_leibniz. apply union_difference. Qed.
     Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅.
@@ -283,12 +263,10 @@ Section collection_ops.
       Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x.
   Proof.
     split.
-    * revert x. induction Xs; simpl; intros x HXs.
-      + eexists [], x. intuition.
-      + rewrite elem_of_intersection_with in HXs.
-        destruct HXs as (x1 & x2 & Hx1 & Hx2 & ?).
-        destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
-        eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
+    * revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
+      rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?).
+      destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
+      eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
     * intros (xs & y & Hxs & ? & Hx). revert x Hx.
       induction Hxs; intros; simplify_option_equality; [done |].
       rewrite elem_of_intersection_with. naive_solver.
@@ -416,23 +394,17 @@ Section fresh.
 
   Global Instance fresh_list_proper: Proper ((=) ==> (≡) ==> (=)) fresh_list.
   Proof.
-    intros ? n ?. subst. induction n; simpl; intros ?? E; f_equal.
-    * by rewrite E.
-    * apply IHn. by rewrite E.
+    intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|].
+    apply IH. by rewrite E.
   Qed.
-
   Lemma fresh_list_length n X : length (fresh_list n X) = n.
   Proof. revert X. induction n; simpl; auto. Qed.
-
   Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X.
   Proof.
-    revert X. induction n; intros X; simpl.
-    * by rewrite elem_of_nil.
-    * rewrite elem_of_cons. intros [?| Hin]; subst.
-      + apply is_fresh.
-      + apply IHn in Hin. solve_elem_of.
+    revert X. induction n as [|n IH]; intros X; simpl; [by rewrite elem_of_nil|].
+    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
+    apply IH in Hin; solve_elem_of.
   Qed.
-
   Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
   Proof.
     revert X. induction n; simpl; constructor; auto.
@@ -441,20 +413,14 @@ Section fresh.
 End fresh.
 
 Definition option_collection `{Singleton A C} `{Empty C} (x : option A) : C :=
-  match x with
-  | None => ∅
-  | Some a => {[ a ]}
-  end.
+  match x with None => ∅ | Some a => {[ a ]} end.
 
 (** * Properties of implementations of collections that form a monad *)
 Section collection_monad.
   Context `{CollectionMonad M}.
 
   Global Instance collection_guard: MGuard M := λ P dec A x,
-    match dec with
-    | left H => x H
-    | _ => ∅
-    end.
+    match dec with left H => x H | _ => ∅ end.
 
   Global Instance collection_fmap_proper {A B} (f : A → B) :
     Proper ((≡) ==> (≡)) (fmap f).
@@ -496,9 +462,8 @@ Section collection_monad.
   Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
     Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
   Proof.
-    intros Hl. revert k.
-    induction Hl; simpl; intros;
-      decompose_elem_of; simpl; f_equal; auto.
+    intros Hl. revert k. induction Hl; simpl; intros;
+      decompose_elem_of; f_equal'; auto.
   Qed.
 
   Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k :

theories/decidable.v

@@ -70,6 +70,7 @@ Ltac solve_decision := intros; first
 
 (** The following combinators are useful to create Decision proofs in
 combination with the [refine] tactic. *)
+Notation swap_if S := (match S with left H => right H | right H => left H end).
 Notation cast_if S := (if S then left _ else right _).
 Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
 Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
@@ -77,6 +78,8 @@ Notation cast_if_and4 S1 S2 S3 S4 :=
   (if S1 then cast_if_and3 S2 S3 S4 else right _).
 Notation cast_if_and5 S1 S2 S3 S4 S5 :=
   (if S1 then cast_if_and4 S2 S3 S4 S5 else right _).
+Notation cast_if_and6 S1 S2 S3 S4 S5 S6 :=
+  (if S1 then cast_if_and5 S2 S3 S4 S5 S6 else right _).
 Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
 Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3).
 Notation cast_if_not_or S1 S2 := (if S1 then cast_if S2 else left _).
@@ -131,6 +134,8 @@ Proof. by apply dsig_eq. Qed.
 (** Instances of [Decision] for operators of propositional logic. *)
 Instance True_dec: Decision True := left I.
 Instance False_dec: Decision False := right (False_rect False).
+Instance Is_true_dec b : Decision (Is_true b).
+Proof. destruct b; apply _. Defined.
 
 Section prop_dec.
   Context `(P_dec : Decision P) `(Q_dec : Decision Q).
@@ -144,18 +149,17 @@ Section prop_dec.
   Global Instance impl_dec: Decision (P → Q).
   Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
 End prop_dec.
+Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+  Decision (P ↔ Q) := and_dec _ _.
 
 (** Instances of [Decision] for common data types. *)
 Instance bool_eq_dec (x y : bool) : Decision (x = y).
 Proof. solve_decision. Defined.
 Instance unit_eq_dec (x y : unit) : Decision (x = y).
-Proof. refine (left _); by destruct x, y. Defined.
+Proof. solve_decision. Defined.
 Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
   `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
-Proof.
-  refine (cast_if_and (A_dec (fst x) (fst y)) (B_dec (snd x) (snd y)));
-    abstract (destruct x, y; simpl in *; congruence).
-Defined.
+Proof. solve_decision. Defined.
 Instance sum_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
   `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
 Proof. solve_decision. Defined.
@@ -173,7 +177,11 @@ Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
 Proof. refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. Defined.
 
 (** Some laws for decidable propositions *)
-Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
+Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
+Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
 Proof. destruct (decide P); tauto. Qed.
-Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
+Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
 Proof. destruct (decide Q); tauto. Qed.

theories/fin_collections.v

@@ -34,7 +34,7 @@ Qed.
 Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
 Proof.
   intros. apply equiv_empty. intro. rewrite elements_spec.
-  rewrite (nil_length (elements X)). by rewrite elem_of_nil. done.
+  rewrite (nil_length_inv (elements X)). by rewrite elem_of_nil. done.
 Qed.
 Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
 Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
@@ -54,7 +54,7 @@ Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, collection_size. simpl. rewrite !elements_spec.
   generalize (elements X). intros [|? l]; intro; simplify_equality.
-  rewrite (nil_length l), !elem_of_list_singleton by done. congruence.
+  rewrite (nil_length_inv l), !elem_of_list_singleton by done. congruence.
 Qed.
 
 Lemma collection_choose_Some X x : collection_choose X = Some x → x ∈ X.

theories/fin_map_dom.v

@@ -5,12 +5,11 @@ maps. We provide such an axiomatization, instead of implementing the domain
 function in a generic way, to allow more efficient implementations. *)
 Require Export collections fin_maps.
 
-Class FinMapDom K M D `{!FMap M}
-    `{∀ A, Lookup K A (M A)} `{∀ A, Empty (M A)} `{∀ A, PartialAlter K A (M A)}
-    `{!Merge M} `{∀ A, FinMapToList K A (M A)}
-    `{∀ i j : K, Decision (i = j)}
-    `{∀ A, Dom (M A) D} `{ElemOf K D} `{Empty D} `{Singleton K D}
-    `{Union D}`{Intersection D} `{Difference D} := {
+Class FinMapDom K M D `{FMap M,
+    ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
+    OMap M, Merge M, ∀ A, FinMapToList K A (M A), ∀ i j : K, Decision (i = j),
+    ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
+    Union D, Intersection D, Difference D} := {
   finmap_dom_map :>> FinMap K M;
   finmap_dom_collection :>> Collection K D;
   elem_of_dom {A} (m : M A) i : i ∈ dom D m ↔ is_Some (m !! i)
@@ -19,35 +18,32 @@ Class FinMapDom K M D `{!FMap M}
 Section fin_map_dom.
 Context `{FinMapDom K M D}.
 
+Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m.
+Proof. rewrite elem_of_dom; eauto. Qed.
 Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None.
 Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
-
 Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom D m1 ⊆ dom D m2.
 Proof.
-  unfold subseteq, map_subseteq, collection_subseteq.
-  intros ??. rewrite !elem_of_dom. inversion 1. eauto.
+  rewrite map_subseteq_spec.
+  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
 Qed.
 Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom D m1 ⊂ dom D m2.
 Proof.
-  intros [Hss1 Hss2]. split.
-  { by apply subseteq_dom. }
-  intros Hdom. destruct Hss2. intros i x Hi.
-  specialize (Hdom i). rewrite !elem_of_dom in Hdom.
-  destruct Hdom; eauto. erewrite (Hss1 i) in Hi by eauto. congruence.
+  intros [Hss1 Hss2]; split; [by apply subseteq_dom |].
+  contradict Hss2. rewrite map_subseteq_spec. intros i x Hi.
+  specialize (Hss2 i). rewrite !elem_of_dom in Hss2.
+  destruct Hss2; eauto. by simplify_map_equality.
 Qed.
-
 Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
 Proof.
-  split; intro.
-  * rewrite elem_of_dom, lookup_empty. by inversion 1.
-  * solve_elem_of.
+  split; intro; [|solve_elem_of].
+  rewrite elem_of_dom, lookup_empty. by inversion 1.
 Qed.
 Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
 Proof.
   intros E. apply map_empty. intros. apply not_elem_of_dom.
   rewrite E. solve_elem_of.
 Qed.
-
 Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
 Proof.
   apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
@@ -59,13 +55,11 @@ Proof. rewrite (dom_insert _). solve_elem_of. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
   X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
 Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed.
-
 Lemma dom_singleton {A} (i : K) (x : A) : dom D {[(i, x)]} ≡ {[ i ]}.
 Proof.
   unfold singleton at 1, map_singleton.
   rewrite dom_insert, dom_empty. solve_elem_of.
 Qed.
-
 Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
 Proof.
   apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
@@ -77,32 +71,28 @@ Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
 Lemma delete_insert_dom {A} (m : M A) i x :
   i ∉ dom D m → delete i (<[i:=x]>m) = m.
 Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
-
 Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ m2 ↔ dom D m1 ∩ dom D m2 ≡ ∅.
 Proof.
-  unfold disjoint, map_disjoint, map_intersection_forall.
-  rewrite elem_of_equiv_empty. setoid_rewrite elem_of_intersection.
+  rewrite map_disjoint_spec, elem_of_equiv_empty.
+  setoid_rewrite elem_of_intersection.
   setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
 Qed.
 Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ m2 → dom D m1 ∩ dom D m2 ≡ ∅.
 Proof. apply map_disjoint_dom. Qed.
 Lemma map_disjoint_dom_2 {A} (m1 m2 : M A