From b3c3d7348c6d77ee8fad7ddc68b35bf443065827 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Feb 2016 18:53:45 +0100
Subject: [PATCH] Let set_solver handle mkSet.

---
 algebra/sts.v         | 19 +++++++------------
 barrier/proof.v       |  6 +++---
 barrier/protocol.v    | 14 +++++---------
 prelude/collections.v |  8 ++++++++
 prelude/sets.v        |  8 +++++---
 5 files changed, 28 insertions(+), 27 deletions(-)

diff --git a/algebra/sts.v b/algebra/sts.v
index 83399315b..9947996ef 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -40,7 +40,7 @@ Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
   closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
 }.
 Definition up (s : state sts) (T : tokens sts) : states sts :=
-  mkSet (rtc (frame_step T) s).
+  {[ s' | rtc (frame_step T) s s' ]}.
 Definition up_set (S : states sts) (T : tokens sts) : states sts :=
   S ≫= λ s, up s T.
 
@@ -70,7 +70,7 @@ Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
 Proof.
   intros s ? <- T T' HT ; apply elem_of_subseteq.
   induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
-  eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
+  eapply elem_of_mkSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
 Qed.
 Global Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
 Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
@@ -128,7 +128,7 @@ Proof.
     specialize (HS s' Hs'); clear Hs' S.
     induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
     inversion_clear Hstep; apply IH; clear IH; auto with sts.
-  - intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
+  - intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; exists s.
     split; [eapply rtc_r|]; eauto.
 Qed.
 Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed (up s T) T.
@@ -359,9 +359,7 @@ Lemma sts_op_auth_frag_up s T :
   sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
-  - intros (?&?&?). destruct_conjs.
-    apply closed_disjoint with (up s T); first done.
-    apply elem_of_up.
+  - intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
   - intros; split_and?.
     + set_solver+.
     + by apply closed_up.
@@ -411,12 +409,9 @@ Lemma up_set_intersection S1 Sf Tf :
   S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.
 Proof.
   intros Hclf. apply (anti_symm (⊆)).
-  + move=>s [HS1 HSf]. split; first by apply HS1.
-    by apply subseteq_up_set.
-  + move=>s [HS1 Hscl]. split; first done.
-    destruct Hscl as [s' [Hsup Hs']].
-    eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
-    set_solver +Hs'.
+  + move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
+  + move=>s [HS1 [s' [/elem_of_mkSet Hsup Hs']]]. split; first done.
+    eapply closed_steps, Hsup; first done. set_solver +Hs'.
 Qed.
 
 (** Inclusion *)
diff --git a/barrier/proof.v b/barrier/proof.v
index a548ed362..444141c54 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -164,7 +164,7 @@ Proof.
       rewrite -sts_ownS_op; eauto using i_states_closed, low_states_closed.
       set_solver.
     + move=> /= t. rewrite !elem_of_mkSet; intros [<-|<-]; set_solver.
-    + rewrite !elem_of_mkSet; set_solver.
+    + rewrite /= /i_states. set_solver.
     + auto using sts.closed_op, i_states_closed, low_states_closed.
 Qed.
 
@@ -293,7 +293,7 @@ Proof.
     apply sep_mono.
     * rewrite -sts_ownS_op; eauto using i_states_closed.
       + apply sts_own_weaken; eauto using sts.closed_op, i_states_closed.
-        rewrite !elem_of_mkSet; set_solver.
+        rewrite /i_states. set_solver.
       + set_solver.
     * rewrite const_equiv // !left_id.
       rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
@@ -319,7 +319,7 @@ Proof.
     apply sep_mono.
     * rewrite -sts_ownS_op; eauto using i_states_closed.
       + apply sts_own_weaken; eauto using sts.closed_op, i_states_closed.
-        rewrite !elem_of_mkSet; set_solver.
+        rewrite /i_states. set_solver.
       + set_solver.
     * rewrite const_equiv // !left_id.
       rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
diff --git a/barrier/protocol.v b/barrier/protocol.v
index 780ec7d72..b6473a49d 100644
--- a/barrier/protocol.v
+++ b/barrier/protocol.v
@@ -36,14 +36,12 @@ Definition low_states : set state := {[ s | state_phase s = Low ]}.
 Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
 Proof.
   split.
-  - move=>[p I]. rewrite /= !elem_of_mkSet /= =>HI.
-    destruct p; set_solver by eauto.
+  - intros [p I]. rewrite /= /i_states /change_tok. destruct p; set_solver.
   - (* If we do the destruct of the states early, and then inversion
        on the proof of a transition, it doesn't work - we do not obtain
        the equalities we need. So we destruct the states late, because this
        means we can use "destruct" instead of "inversion". *)
-    move=>s1 s2. rewrite !elem_of_mkSet.
-    intros Hs1 [T1 T2 Hdisj Hstep'].
+    intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
     inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
     destruct Htrans; simpl in *; last done.
     move: Hs1 Hdisj Htok. rewrite elem_of_equiv_empty elem_of_equiv.
@@ -56,10 +54,8 @@ Qed.
 Lemma low_states_closed : sts.closed low_states {[ Send ]}.
 Proof.
   split.
-  - move=>[p I]. rewrite /= /tok !elem_of_mkSet /= =>HI.
-    destruct p; set_solver.
-  - move=>s1 s2. rewrite !elem_of_mkSet.
-    intros Hs1 [T1 T2 Hdisj Hstep'].
+  - intros [p I]. rewrite /low_states. set_solver.
+  - intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
     inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
     destruct Htrans; simpl in *; first by destruct p.
     exfalso; set_solver.
@@ -74,7 +70,7 @@ Lemma wait_step i I :
   sts.steps (State High I, {[ Change i ]}) (State High (I ∖ {[ i ]}), ∅).
 Proof.
   intros. apply rtc_once.
-  constructor; first constructor; simpl; [set_solver by eauto..|].
+  constructor; first constructor; rewrite /= /change_tok; [set_solver by eauto..|].
   (* TODO this proof is rather annoying. *)
   apply elem_of_equiv=>t. rewrite !elem_of_union.
   rewrite !elem_of_mkSet /change_tok /=.
diff --git a/prelude/collections.v b/prelude/collections.v
index 625d16ac3..4e4ecaa37 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -4,6 +4,7 @@
 importantly, it implements some tactics to automatically solve goals involving
 collections. *)
 From prelude Require Export base tactics orders.
+From prelude Require Import sets.
 
 Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
@@ -153,6 +154,9 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
   let rec go H :=
   lazymatch type of H with
   | _ ∈ ∅ => apply elem_of_empty in H; destruct H
+  | _ ∈ ⊤ => clear H
+  | _ ∈ {[ _ | _ ]} => rewrite elem_of_mkSet in H
+  | ¬_ ∈ {[ _ | _ ]} => rewrite not_elem_of_mkSet in H
   | ?x ∈ {[ ?y ]} =>
     apply elem_of_singleton in H; try first [subst y | subst x]
   | ?x ∉ {[ ?y ]} =>
@@ -217,7 +221,9 @@ Ltac set_unfold :=
     | context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L in H
     | context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L in H
     | context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty in H
+    | context [ _ ∈ ⊤ ] => setoid_rewrite elem_of_all in H
     | context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
+    | context [ _ ∈ {[_| _ ]} ] => setoid_rewrite elem_of_mkSet in H; simpl in H
     | context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union in H
     | context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection in H
     | context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference in H
@@ -237,7 +243,9 @@ Ltac set_unfold :=
   | |- context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L
   | |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L
   | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty
+  | |- context [ _ ∈ ⊤ ] => setoid_rewrite elem_of_all
   | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton
+  | |- context [ _ ∈ {[ _ | _ ]} ] => setoid_rewrite elem_of_mkSet; simpl
   | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union
   | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection
   | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference
diff --git a/prelude/sets.v b/prelude/sets.v
index f5304451c..b6f6db4fa 100644
--- a/prelude/sets.v
+++ b/prelude/sets.v
@@ -23,9 +23,11 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
 Instance set_collection : Collection A (set A).
 Proof. split; [split | |]; by repeat intro. Qed.
 
-Lemma elem_of_mkSet {A} (P : A → Prop) x : (x ∈ {[ x | P x ]}) = P x.
+Lemma elem_of_all {A} (x : A) : x ∈ ⊤ ↔ True.
 Proof. done. Qed.
-Lemma not_elem_of_mkSet {A} (P : A → Prop) x : (x ∉ {[ x | P x ]}) = (¬P x).
+Lemma elem_of_mkSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
+Proof. done. Qed.
+Lemma not_elem_of_mkSet {A} (P : A → Prop) x : x ∉ {[ x | P x ]} ↔ ¬P x.
 Proof. done. Qed.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
@@ -38,4 +40,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
 Instance set_collection_monad : CollectionMonad set.
 Proof. by split; try apply _. Qed.
 
-Global Opaque set_union set_intersection set_difference.
+Global Opaque set_elem_of set_union set_intersection set_difference.
-- 
GitLab