Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/sts.v

@@ -48,9 +48,15 @@ Inductive frame_step (T : set token) (s1 s2 : state) : Prop :=
 Hint Resolve Frame_step.
 Record closed (S : set state) (T : set token) : Prop := Closed {
   closed_ne : S ≢ ∅;
-  closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅;
+  closed_disjoint s : s ∈ S → tok s ∩ T ⊆ ∅;
   closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
 }.
+Lemma closed_disjoint' S T s :
+  closed S T → s ∈ S → tok s ∩ T ≡ ∅.
+Proof.
+  move=>Hcl Hin. move:(closed_disjoint _ _ Hcl _ Hin).
+  solve_elem_of+.
+Qed.
 Lemma closed_steps S T s1 s2 :
   closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
 Proof. induction 3; eauto using closed_step. Qed.
@@ -144,13 +150,13 @@ Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
 Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T.
 Proof. by rewrite /up_set collection_bind_singleton. Qed.
 Lemma closed_up_set S T :
-  (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → S ≢ ∅ → closed (up_set S T) T.
+  (∀ s, s ∈ S → tok s ∩ T ⊆ ∅) → S ≢ ∅ → closed (up_set S T) T.
 Proof.
   intros HS Hne; unfold up_set; split.
   * assert (∀ s, s ∈ up s T) by eauto using elem_of_up. solve_elem_of.
   * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
     specialize (HS s' Hs'); clear Hs' Hne S.
-    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; auto.
+    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.
     split; [eapply rtc_r|]; eauto.

barrier/barrier.v

@@ -15,7 +15,7 @@ Module barrier_proto.
   Proof. split. exact (State Low ∅). Qed.
 
   Definition change_tokens (I : gset gname) : set token :=
-    mkSet (λ t, match t with Change i => i ∈ I | Send => False end).
+    mkSet (λ t, match t with Change i => i ∉ I | Send => False end).
 
   Inductive trans : relation stateT :=
   | ChangeI p I2 I1 : trans (State p I1) (State p I2)
@@ -34,7 +34,27 @@ Module barrier_proto.
     sts.closed sts (i_states i) {[ Change i ]}.
   Proof.
     split.
-    - apply non_empty_inhabited.
+    - apply (non_empty_inhabited (State Low {[ i ]})). rewrite !mkSet_elem_of /=.
+      apply lookup_singleton.
+    - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
+      move=>s' /elem_of_intersection. rewrite !mkSet_elem_of /=.
+      move=>[[Htok|Htok] ? ]; subst s'; first done.
+      destruct p; done.
+    - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
+      (* We probably want some helper lemmas for this... *)
+      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
+      inversion_clear Hstep' as [? ? ? ? Htrans Htok1 Htok2 Htok].
+      destruct Htrans; last done; move:Hs1 Hdisj Htok1 Htok2 Htok.
+      rewrite /= /tok /=.
+      intros. apply dec_stable. 
+      assert (Change i ∉ change_tokens I1) as HI1
+        by (rewrite mkSet_not_elem_of; solve_elem_of +Hs1).
+      assert (Change i ∉ change_tokens I2) as HI2.
+      { destruct p.
+        - solve_elem_of +Htok Hdisj HI1.
+        - solve_elem_of +Htok Hdisj HI1 / discriminate. }
+      done.
+  Qed.
     
 End barrier_proto.
 

prelude/sets.v

@@ -18,9 +18,9 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
 Instance set_collection : Collection A (set A).
 Proof. by split; [split | |]; repeat intro. Qed.
 
-Lemma mkSet_elem_of {A} (f : A → Prop) x : f x → x ∈ mkSet f.
+Lemma mkSet_elem_of {A} (f : A → Prop) x : (x ∈ mkSet f) = f x.
 Proof. done. Qed.
-Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ¬f x → x ∉ mkSet f.
+Lemma mkSet_not_elem_of {A} (f : A → Prop) x : (x ∉ mkSet f) = (¬f x).
 Proof. done. Qed.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.

program_logic/sts.v

@@ -97,7 +97,7 @@ Section sts.
     - intros Hdisj. split_ands; first by solve_elem_of+.
       + done.
       + constructor; [done | solve_elem_of-].
-    - intros _. by eapply closed_disjoint.
+    - intros _. by eapply closed_disjoint'.
     - intros _. constructor. solve_elem_of+.
   Qed.