prelude.collections: add lemma to prove non-emptiness

barrier/barrier.v

@@ -7,23 +7,34 @@ Definition wait := (rec: "wait" "x" := if: !"x" = '1 then '() else "wait" "x")%L
 
 (** The STS describing the main barrier protocol. *)
 Module barrier_proto.
-  Inductive state := Low (I : gset gname) | High (I : gset gname).
+  Inductive phase := Low | High.
+  Record stateT := State { state_phase : phase; state_I : gset gname }.
   Inductive token := Change (i : gname) | Send.
 
+  Global Instance stateT_inhabited: Inhabited stateT.
+  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).
 
-  Inductive trans : relation state :=
-  | LowChange I1 I2 : trans (Low I1) (Low I2)
-  | HighChange I2 I1 : trans (High I1) (High I2)
-  | LowHigh I : trans (Low I) (High I).
+  Inductive trans : relation stateT :=
+  | ChangeI p I2 I1 : trans (State p I1) (State p I2)
+  | ChangePhase I : trans (State Low I) (State High I).
 
-  Definition tok (s : state) : set token :=
-    match s with
-    | Low I' => change_tokens I'
-    | High I' => change_tokens I' ∪ {[ Send ]}
-    end.
+  Definition tok (s : stateT) : set token :=
+      change_tokens (state_I s)
+    ∪ match state_phase s with Low => ∅ | High => {[ Send ]} end.
 
   Definition sts := sts.STS trans tok.
+
+  Definition i_states (i : gname) : set stateT :=
+    mkSet (λ s, i ∈ state_I s).
+
+  Lemma i_states_closed i :
+    sts.closed sts (i_states i) {[ Change i ]}.
+  Proof.
+    split.
+    - apply non_empty_inhabited.
+    
 End barrier_proto.
 

prelude/collections.v

@@ -280,6 +280,8 @@ Section collection.
     intros X1 X2 HX Y1 Y2 HY; apply elem_of_equiv; intros x.
     by rewrite !elem_of_difference, HX, HY.
   Qed.
+  Lemma non_empty_inhabited x X : x ∈ X → X ≢ ∅.
+  Proof. solve_elem_of. Qed.
   Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
   Proof. solve_elem_of. Qed.
   Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.