Restore axiomatic semantics.

theories/ars.v

@@ -64,8 +64,6 @@ Section rtc.
   Proof. exact rtc_transitive. Qed.
   Lemma rtc_once x y : R x y → rtc R x y.
   Proof. eauto. Qed.
-  Instance rtc_once_subrel: subrelation R (rtc R).
-  Proof. exact @rtc_once. Qed.
   Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z.
   Proof. intros. etransitivity; eauto. Qed.
   Lemma rtc_inv x z : rtc R x z → x = z ∨ ∃ y, R x y ∧ rtc R y z.
@@ -156,8 +154,6 @@ Section rtc.
   Proof. intros Hxy Hyz. revert x Hxy. induction Hyz; eauto using tc_r. Qed.
   Lemma tc_rtc x y : tc R x y → rtc R x y.
   Proof. induction 1; eauto. Qed.
-  Instance tc_once_subrel: subrelation (tc R) (rtc R).
-  Proof. exact @tc_rtc. Qed.
 
   Lemma all_loop_red x : all_loop R x → red R x.
   Proof. destruct 1; auto. Qed.
@@ -174,44 +170,21 @@ Section rtc.
   Qed.
 End rtc.
 
-(* Avoid too eager type class resolution *)
-Hint Extern 5 (subrelation _ (rtc _)) =>
-  eapply @rtc_once_subrel : typeclass_instances.
-Hint Extern 5 (subrelation _ (tc _)) =>
-  eapply @tc_once_subrel : typeclass_instances.
-
 Hint Constructors rtc nsteps bsteps tc : ars.
 Hint Resolve rtc_once rtc_r tc_r rtc_transitive tc_rtc_l tc_rtc_r
   tc_rtc bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.
 
 (** * Theorems on sub relations *)
 Section subrel.
-  Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2).
-
-  Lemma red_subrel x : red R1 x → red R2 x.
-  Proof. intros [y ?]. exists y. by apply Hsub. Qed.
-  Lemma nf_subrel x : nf R2 x → nf R1 x.
-  Proof. intros H1 H2. destruct H1. by apply red_subrel. Qed.
-
-  Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
-  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
-  Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
-  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
-  Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
-  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
-  Instance tc_subrel: subrelation (tc R1) (tc R2).
-  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
+  Context {A} (R1 R2 : relation A).
+  Notation subrel := (∀ x y, R1 x y → R2 x y).
+  Lemma red_subrel x : subrel → red R1 x → red R2 x.
+  Proof. intros ? [y ?]; eauto. Qed.
+  Lemma nf_subrel x : subrel → nf R2 x → nf R1 x.
+  Proof. intros ? H1 H2; destruct H1; by apply red_subrel. Qed.
 End subrel.
 
-Hint Extern 5 (subrelation (rtc _) (rtc _)) =>
-  eapply @rtc_subrel : typeclass_instances.
-Hint Extern 5 (subrelation (nsteps _) (nsteps _)) =>
-  eapply @nsteps_subrel : typeclass_instances.
-Hint Extern 5 (subrelation (bsteps _) (bsteps _)) =>
-  eapply @bsteps_subrel : typeclass_instances.
-Hint Extern 5 (subrelation (tc _) (tc _)) =>
-  eapply @tc_subrel : typeclass_instances.
-
+(** * Theorems on well founded relations *)
 Notation wf := well_founded.
 
 Section wf.

theories/collections.v

@@ -138,28 +138,31 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
   | _ ∈ ∅ => apply elem_of_empty in H; destruct H
   | ?x ∈ {[ ?y ]} =>
     apply elem_of_singleton in H; try first [subst y | subst x]
+  | ?x ∉ {[ ?y ]} =>
+    apply not_elem_of_singleton in H
   | _ ∈ _ ∪ _ =>
-    let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
-    destruct H as [H1|H2]; [go H1 | go H2]
+    apply elem_of_union in H; destruct H as [H|H]; [go H|go H]
+  | _ ∉ _ ∪ _ =>
+    let H1 := fresh H in let H2 := fresh H in apply not_elem_of_union in H;
+    destruct H as [H1 H2]; go H1; go H2
   | _ ∈ _ ∩ _ =>
-    let H1 := fresh in let H2 := fresh in apply elem_of_intersection in H;
+    let H1 := fresh H in let H2 := fresh H in apply elem_of_intersection in H;
     destruct H as [H1 H2]; go H1; go H2
   | _ ∈ _ ∖ _ =>
-    let H1 := fresh in let H2 := fresh in apply elem_of_difference in H;
+    let H1 := fresh H in let H2 := fresh H in apply elem_of_difference in H;
     destruct H as [H1 H2]; go H1; go H2
   | ?x ∈ _ <$> _ =>
-    let H1 := fresh in apply elem_of_fmap in H;
-    destruct H as [? [? H1]]; try (subst x); go H1
+    apply elem_of_fmap in H; destruct H as [? [? H]]; try (subst x); go H
   | _ ∈ _ ≫= _ =>
-    let H1 := fresh in let H2 := fresh in apply elem_of_bind in H;
+    let H1 := fresh H in let H2 := fresh H in apply elem_of_bind in H;
     destruct H as [? [H1 H2]]; go H1; go H2
   | ?x ∈ mret ?y =>
     apply elem_of_ret in H; try first [subst y | subst x]
   | _ ∈ mjoin _ ≫= _ =>
-    let H1 := fresh in let H2 := fresh in apply elem_of_join in H;
+    let H1 := fresh H in let H2 := fresh H in apply elem_of_join in H;
     destruct H as [? [H1 H2]]; go H1; go H2
   | _ ∈ guard _; _ =>
-    let H1 := fresh in let H2 := fresh in apply elem_of_guard in H;
+    let H1 := fresh H in let H2 := fresh H in apply elem_of_guard in H;
     destruct H as [H1 H2]; go H2
   | _ ∈ of_option _ => apply elem_of_of_option in H
   | _ => idtac

theories/fin_map_dom.v

@@ -105,4 +105,10 @@ Proof.
   unfold is_Some. setoid_rewrite lookup_difference_Some.
   destruct (m2 !! i); naive_solver.
 Qed.
+Lemma dom_fmap {A B} (f : A → B) m : dom D (f <$> m) ≡ dom D m.
+Proof.
+  apply elem_of_equiv. intros i.
+  rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
+  destruct (m !! i); naive_solver.
+Qed.
 End fin_map_dom.

theories/fin_maps.v

@@ -450,6 +450,13 @@ Lemma fmap_empty {A B} (f : A → B) : f <$> ∅ = ∅.
 Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
 Lemma omap_empty {A B} (f : A → option B) : omap f ∅ = ∅.
 Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
+Lemma omap_singleton {A B} (f : A → option B) i x y :
+  f x = Some y → omap f {[ i,x ]} = {[ i,y ]}.
+Proof.
+  intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|].
+  * by rewrite lookup_omap, !lookup_singleton.
+  * by rewrite lookup_omap, !lookup_singleton_ne.
+Qed.
 
 (** ** Properties of conversion to lists *)
 Lemma map_to_list_unique {A} (m : M A) i x y :

theories/option.v

@@ -261,6 +261,10 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
     | option ?A =>
       let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
     end
+  | H : context [decide _] |- _ => rewrite decide_True in H by tac
+  | H : context [decide _] |- _ => rewrite decide_False in H by tac
+  | H : context [mguard _ _] |- _ => rewrite option_guard_False in H by tac
+  | H : context [mguard _ _] |- _ => rewrite option_guard_True in H by tac
   | _ => rewrite decide_True by tac
   | _ => rewrite decide_False by tac
   | _ => rewrite option_guard_True by tac