From e409571ddea3957abbf47f6379c97819b8405c98 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Wed, 22 Apr 2015 21:54:46 +0200
Subject: [PATCH] Restore axiomatic semantics.

theories/ars.v  41 +++++++
theories/collections.v  21 ++++++++++++
theories/fin_map_dom.v  6 ++++++
theories/fin_maps.v  7 +++++++
theories/option.v  4 ++++
5 files changed, 36 insertions(+), 43 deletions()
diff git a/theories/ars.v b/theories/ars.v
index 3b707bf..0b422b9 100644
 a/theories/ars.v
+++ b/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; [lefteright]; eauto; by apply Hsub. Qed.
 Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
 Proof. induction 1; [lefteright]; eauto; by apply Hsub. Qed.
 Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
 Proof. induction 1; [lefteright]; eauto; by apply Hsub. Qed.
 Instance tc_subrel: subrelation (tc R1) (tc R2).
 Proof. induction 1; [lefteright]; 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.
diff git a/theories/collections.v b/theories/collections.v
index 41e7ec5..7169530 100644
 a/theories/collections.v
+++ b/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 [H1H2]; [go H1  go H2]
+ apply elem_of_union in H; destruct H as [HH]; [go Hgo 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
diff git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index fbdd637..a209f4c 100644
 a/theories/fin_map_dom.v
+++ b/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.
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index 31e4ca2..fe28ad9 100644
 a/theories/fin_maps.v
+++ b/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 :
diff git a/theories/option.v b/theories/option.v
index 2878f33..d41b35d 100644
 a/theories/option.v
+++ b/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

GitLab