From 8930527adada3fcd0472f80d4f390526cb9b141d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 7 Mar 2016 16:37:24 +0100 Subject: [PATCH] establish some properties of STSs without tokens --- algebra/sts.v | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) diff --git a/algebra/sts.v b/algebra/sts.v index 0c04c525..512e2f42 100644 --- a/algebra/sts.v +++ b/algebra/sts.v @@ -450,3 +450,78 @@ Proof. Qed. End stsRA. + +(** STSs without tokens: Some stuff is simpler *) +Module sts_notok. +Structure stsT := STS { + state : Type; + prim_step : relation state; +}. +Arguments STS {_} _. +Arguments prim_step {_} _ _. +Notation states sts := (set (state sts)). + +Canonical sts_notok (sts : stsT) : sts.stsT := + sts.STS (token:=Empty_set) (@prim_step sts) (λ _, ∅). + +Section sts. +Context {sts : stsT}. +Implicit Types s : state sts. +Implicit Types S : states sts. + +Notation prim_steps := (rtc prim_step). + +Lemma sts_step s1 s2 : + prim_step s1 s2 → sts.step (s1, ∅) (s2, ∅). +Proof. + intros. split; set_solver. +Qed. + +Lemma sts_steps s1 s2 : + prim_steps s1 s2 → sts.steps (s1, ∅) (s2, ∅). +Proof. + induction 1; eauto using sts_step, rtc_refl, rtc_l. +Qed. + +Lemma frame_prim_step T s1 s2 : + sts.frame_step T s1 s2 → prim_step s1 s2. +Proof. + inversion 1 as [??? Hstep]. inversion_clear Hstep. done. +Qed. + +Lemma prim_frame_step T s1 s2 : + prim_step s1 s2 → sts.frame_step T s1 s2. +Proof. + intros Hstep. apply sts.Frame_step with ∅ ∅; first set_solver. + by apply sts_step. +Qed. + +Lemma mk_closed S : + (∀ s1 s2, s1 ∈ S → prim_step s1 s2 → s2 ∈ S) → sts.closed S ∅. +Proof. + intros ?. constructor; first by set_solver. + intros ????. eauto using frame_prim_step. +Qed. + +End sts. +Notation steps := (rtc prim_step). +End sts_notok. + +Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT. +Notation sts_notokT := sts_notok.stsT. +Notation STS_NoTok := sts_notok.STS. + +Section sts_notokRA. +Import sts_notok. +Context {sts : sts_notokT}. +Implicit Types s : state sts. +Implicit Types S : states sts. + +Lemma sts_notok_update_auth s1 s2 : + rtc prim_step s1 s2 → sts_auth s1 ∅ ~~> sts_auth s2 ∅. +Proof. + intros. by apply sts_update_auth, sts_steps. +Qed. + +End sts_notokRA. + -- GitLab