diff --git a/barrier/protocol.v b/barrier/protocol.v index ab28a2ed69c6672cfc43958de9e73c295712669e..53b315536f1382a066285f0cfb8b5cbca672ebef 100644 --- a/barrier/protocol.v +++ b/barrier/protocol.v @@ -17,12 +17,9 @@ Inductive prim_step : relation state := | ChangeI p I2 I1 : prim_step (State p I1) (State p I2) | ChangePhase I : prim_step (State Low I) (State High I). -Definition change_tok (I : gset gname) : set token := - {[ t | match t with Change i => i ∉ I | Send => False end ]}. -Definition send_tok (p : phase) : set token := - match p with Low => ∅ | High => {[ Send ]} end. Definition tok (s : state) : set token := - change_tok (state_I s) ∪ send_tok (state_phase s). + {[ t | ∃ i, t = Change i ∧ i ∉ state_I s ]} ∪ + (if state_phase s is High then {[ Send ]} else ∅). Global Arguments tok !_ /. Canonical Structure sts := sts.STS prim_step tok. @@ -35,30 +32,22 @@ Definition low_states : set state := {[ s | state_phase s = Low ]}. Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}. Proof. - split. - - 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". *) - 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. - move=> ? /(_ (Change i)) Hdisj /(_ (Change i)); move: Hdisj. - rewrite elem_of_intersection elem_of_union !elem_of_mkSet. - intros; apply dec_stable. - destruct p; set_solver. + split; first (intros [[] I]; 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". *) + intros s1 s2 Hs1 [T1 T2 Hdisj Hstep']. + inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok]. + destruct Htrans as [[] ??|]; done || set_solver. Qed. Lemma low_states_closed : sts.closed low_states {[ Send ]}. Proof. - split. - - 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; apply dec_stable; set_solver. + split; first (intros [??]; set_solver). + intros s1 s2 Hs1 [T1 T2 Hdisj Hstep']. + inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok]. + destruct Htrans as [[] ??|]; done || set_solver. Qed. (* Proof that we can take the steps we need. *) @@ -70,12 +59,8 @@ Lemma wait_step i I : sts.steps (State High I, {[ Change i ]}) (State High (I ∖ {[ i ]}), ∅). Proof. intros. apply rtc_once. - 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 /=. - destruct t as [j|]; last set_solver. - rewrite elem_of_difference elem_of_singleton. + constructor; first constructor; [set_solver..|]. + apply elem_of_equiv=>-[j|]; last set_solver. destruct (decide (i = j)); set_solver. Qed. @@ -85,17 +70,14 @@ Lemma split_step p i i1 i2 I : (State p I, {[ Change i ]}) (State p ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))), {[ Change i1; Change i2 ]}). Proof. - intros. apply rtc_once. - constructor; first constructor; simpl. + intros. apply rtc_once. constructor; first constructor. + - destruct p; set_solver. - destruct p; set_solver. - (* This gets annoying... and I think I can see a pattern with all these proofs. Automatable? *) - - apply elem_of_equiv=>t. destruct t; last set_solver. - rewrite !elem_of_mkSet !not_elem_of_union !not_elem_of_singleton - not_elem_of_difference elem_of_singleton !(inj_iff Change). - destruct p; naive_solver. - - apply elem_of_equiv=>t. destruct t as [j|]; last set_solver. - rewrite !elem_of_mkSet !not_elem_of_union !not_elem_of_singleton - not_elem_of_difference elem_of_singleton !(inj_iff Change). - destruct (decide (i1 = j)) as [->|]; first tauto. - destruct (decide (i2 = j)) as [->|]; intuition. + - apply elem_of_equiv=> /= -[j|]; last set_solver. + set_unfold; rewrite !(inj_iff Change). + assert (Change j ∈ match p with Low => ∅ | High => {[Send]} end ↔ False) + as -> by (destruct p; set_solver). + destruct (decide (i1 = j)) as [->|]; first naive_solver. + destruct (decide (i2 = j)) as [->|]; first naive_solver. + destruct (decide (i = j)) as [->|]; naive_solver. Qed.