From aa2fc8c2e30a8cccea486df166c8efce9eae122f Mon Sep 17 00:00:00 2001 From: k32 <10274441+k32@users.noreply.github.com> Date: Thu, 11 Apr 2024 00:15:42 +0200 Subject: [PATCH] More work on transition systems --- theories/Foundations.v | 271 +++++++++++++++++++++++++++++++---------- 1 file changed, 207 insertions(+), 64 deletions(-) diff --git a/theories/Foundations.v b/theories/Foundations.v index c68e5ed..d13f9a5 100644 --- a/theories/Foundations.v +++ b/theories/Foundations.v @@ -1,5 +1,5 @@ (* SLOT, proofs about distributed systems design - Copyright (C) 2019-2023 k32 + Copyright (C) 2019-2024 k32 This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by @@ -22,10 +22,14 @@ From Coq Require Import Program List Ensembles + Relation_Definitions RelationClasses. Import ListNotations. +From Hammer Require Import + Tactics. + Declare Scope slot_scope. Open Scope slot_scope. (* end hide *) @@ -42,110 +46,249 @@ Section transition_system. }. End transition_system. -Notation "'~[' A ']~>' B" := (fut_cont A B) (at level 20). -Notation "'~>x' A" := (fut_result A)(at level 20). +Global Arguments TransitionSystem (_ _ _) : clear implicits. + +Notation "A '~[' L ']~>' S" := (A (fut_cont L S)) (at level 20) : slot_scope. +Notation "A '~|' R" := (A (fut_result R)) (at level 20) : slot_scope. Section trans_prod. - Context {S1 S2 Label R1 R2 : Type} - `(T1 : TransitionSystem S1 Label R1) `(T2 : TransitionSystem S2 Label R2). - Inductive TransProd := - trans_prod : S1 -> S2 -> TransProd. + (* Product of transition systems: *) + Context {Label S1 S2 R1 R2 : Type} + `{T1 : TransitionSystem S1 Label R1} `{T2 : TransitionSystem S2 Label R2}. + + Let State : Type := S1 * S2. Inductive TransProdResult := - | tpr_l : R1 -> S2 -> TransProdResult - | tpr_r : R2 -> S1 -> TransProdResult. + | tpr_l : forall (result_left : R1) (state_right : S2), TransProdResult + | tpr_r : forall (state_left : S1) (result_right : R2), TransProdResult. - Inductive TransProdFuture : TransProd -> @Future TransProd Label TransProdResult -> Prop := + Inductive TransProdFuture : State -> @Future State Label TransProdResult -> Prop := | tpf_cc : forall (label : Label) (s1 s1' : S1) (s2 s2' : S2), - future s1 (~[label]~> s1')-> - future s2 (~[label]~> s2') -> - TransProdFuture (trans_prod s1 s2) (~[label]~> (trans_prod s1' s2')) + future s1 ~[label]~> s1' -> + future s2 ~[label]~> s2' -> + TransProdFuture (s1, s2) ~[label]~> (s1', s2') | tpf_rc : forall s1 s2 r, - future s1 (~>x r) -> - TransProdFuture (trans_prod s1 s2) (~>x (tpr_l r s2)) + future s1 ~| r -> + TransProdFuture (s1, s2) ~| (tpr_l r s2) | tpf_cr : forall s1 s2 r, - future s2 (~>x r) -> - TransProdFuture (trans_prod s1 s2) (~>x (tpr_r r s1)). + future s2 ~| r -> + TransProdFuture (s1, s2) ~| (tpr_r s1 r). - Global Instance transMult : @TransitionSystem TransProd Label TransProdResult := + Instance transProd : @TransitionSystem State Label TransProdResult := { future := TransProdFuture }. End trans_prod. +Global Arguments transProd {_ _ _ _ _} (_ _). + +Infix "<*>" := (transProd) (at level 98) : slot_scope. + Section trans_sum. + (* Sum of transition systems: *) Context {S1 L1 R1 S2 L2 R2} `{T1 : TransitionSystem S1 L1 R1} `{T2 : TransitionSystem S2 L2 R2}. - Inductive TransSum := - trans_sum : S1 -> S2 -> TransSum. + Let State : Type := S1 * S2. Let Label : Type := L1 + L2. Let Result : Type := R1 * R2. - Inductive TransSumFuture : TransSum -> @Future TransSum Label Result -> Prop := + Inductive TransSumFuture : State -> @Future State Label Result -> Prop := | tsf_rr : forall s1 s2 r1 r2, - future s1 (~>x r1) -> - future s2 (~>x r2) -> - TransSumFuture (trans_sum s1 s2) (~>x (r1, r2)) + future s1 ~| r1 -> + future s2 ~| r2 -> + TransSumFuture (s1, s2) ~| (r1, r2) | tsf_l : forall s1 s1' s2 label, - future s1 (~[label]~> s1') -> - TransSumFuture (trans_sum s1 s2) (~[inl label]~> trans_sum s1' s2) + future s1 ~[label]~> s1' -> + TransSumFuture (s1, s2) ~[inl label]~> (s1', s2) | tsf_r : forall s1 s2 s2' label, - future s2 (~[label]~> s2') -> - TransSumFuture (trans_sum s1 s2) (~[inr label]~> trans_sum s1 s2'). + future s2 ~[label]~> s2' -> + TransSumFuture (s1, s2) ~[inr label]~> (s1, s2'). - Global Instance transSum : @TransitionSystem TransSum Label Result := + Instance transSum : @TransitionSystem State Label Result := { future := TransSumFuture }. End trans_sum. -Section reachability. +Global Arguments transSum {_ _ _ _ _ _} (_ _). + +Infix "<+>" := (transSum) (at level 99) : slot_scope. + +Section state_reachability. Context `{HT : TransitionSystem}. Inductive ReachableBy : State -> list Label -> State -> Prop := | tsrb_nil : forall s, ReachableBy s [] s - | tsrb_cons : forall s s' s'' t l, - future s (~[l]~> s') -> - ReachableBy s' t s'' -> - ReachableBy s (l :: t) s''. -End reachability. + | tsrb_cons : forall s s' s'' label trace, + future s ~[label]~> s' -> + ReachableBy s' trace s'' -> + ReachableBy s (label :: trace) s''. + + Definition HoareTriple (precondition : State -> Prop) + (trace : list Label) + (postcondition : State -> Prop) := + forall s s', + ReachableBy s trace s' -> precondition s -> + postcondition s'. +End state_reachability. + +Notation "'{{' a '}}' t '{{' b '}}'" := (HoareTriple a t b) (at level 40) : slot_scope. +Notation "'{{}}' t '{{' b '}}'" := (HoareTriple (const True) t b) (at level 39) : slot_scope. -Section trace_ensemble. +Inductive TraceInvariant `{TransitionSystem} (prop : State -> Prop) : list Label -> Prop := +| inv_nil : + TraceInvariant prop [] +| inv_cons : forall label trace, + {{prop}} [label] {{prop}} -> + TraceInvariant prop trace -> + TraceInvariant prop (label :: trace). + +Section result_reachability. Context `{HT : TransitionSystem}. - (* - Inductive TraceEnsemble : State -> list Label -> Result -> Prop := - trace_ensemble : forall s s' t r, - future s' (~>x r) -> - ReachableBy s t s' -> - TraceEnsemble s t r. *) - - Inductive CompleteEnsemble : State -> list Label -> Result -> Prop := - | te_nil : forall s r, - future s (~>x r) -> - CompleteEnsemble s [] r - | te_cons : forall s s' l t r, - future s (~[l]~> s') -> - CompleteEnsemble s' t r -> - CompleteEnsemble s (l :: t) r. -End trace_ensemble. + Inductive RReachableBy : State -> list Label -> Result -> Prop := + | tsrrb_nil : forall s result, + future s ~| result -> + RReachableBy s [] result + | tsrrbt_cons : forall s s' label trace result, + future s ~[label]~> s' -> + RReachableBy s' trace result -> + RReachableBy s (label :: trace) result. + + Definition RHoareTriple (precondition : State -> Prop) + (trace : list Label) + (postcondition : Result -> Prop) := + forall s result, + RReachableBy s trace result -> precondition s -> + postcondition result. +End result_reachability. + +Notation "'{{' a '}}' t '{<' b '>}'" := (RHoareTriple a t b) (at level 40) : slot_scope. +Notation "'{{}}' t '{<' b '>}'" := (RHoareTriple (const True) t b) (at level 39) : slot_scope. -Section commutativity. +(* begin hide *) +Global Arguments In {_}. +Global Arguments Complement {_}. +Global Arguments Disjoint {_}. +(* end hide *) + +Section trace_ensembles. Context `{HT : TransitionSystem}. - Definition labels_commute (l1 l2 : Label) : Prop := - forall (s s' : State), - ReachableBy s [l1; l2] s' <-> ReachableBy s [l2; l1] s'. + Definition TraceEnsemble := Ensemble (list Label). + + (** Hoare logic of trace ensembles consists of a single rule: *) + Definition EHoareTriple (precondition : State -> Prop) + (ensemble : TraceEnsemble) + (postcondition : State -> Prop) := + forall t, In ensemble t -> + {{ precondition }} t {{ postcondition }}. + + Definition EnsembleInvariant (prop : State -> Prop) (ens : TraceEnsemble) : Prop := + forall (t : list Label), ens t -> TraceInvariant prop t. + + (** Hoare logic of trace ensembles consists of a single rule: *) + Definition ERHoareTriple (precondition : State -> Prop) + (ensemble : TraceEnsemble) + (postcondition : Result -> Prop) := + forall t, In ensemble t -> + {{ precondition }} t {< postcondition >}. +End trace_ensembles. + +Notation "'-{{' a '}}' e '{{' b '}}'" := (EHoareTriple a e b)(at level 40) : slot_scope. +Notation "'-{{}}' e '{{' b '}}'" := (EHoareTriple (const True) e b)(at level 40) : slot_scope. +Notation "'-{{}}' e '{{}}'" := (forall t, e t -> exists s s', ReachableBy s t s')(at level 38) : slot_scope. + +Notation "'-{{' a '}}' e '{<' b '>}'" := (ERHoareTriple a e b)(at level 40) : slot_scope. +Notation "'-{{}}' e '{<' b '>}'" := (ERHoareTriple (const True) e b)(at level 40) : slot_scope. - Global Instance events_commuteSymm : Symmetric labels_commute. - Proof. - intros a b Hab s s''. - unfold labels_commute in *. specialize (Hab s s''). - now symmetry in Hab. - Qed. +Section commutativity. + Section defn. + Context `{HT : TransitionSystem}. + + Definition labels_commute (l1 l2 : Label) : Prop := + forall (s s' : State), + ReachableBy s [l1; l2] s' <-> ReachableBy s [l2; l1] s'. + + Global Instance events_commuteSymm : Symmetric labels_commute. + Proof. + intros a b Hab s s''. + unfold labels_commute in *. specialize (Hab s s''). + now symmetry in Hab. + Qed. + End defn. + + Section summ. + Context {S1 L1 R1 S2 L2 R2 : Type} + `{T1 : TransitionSystem S1 L1 R1} `{T2 : TransitionSystem S2 L2 R2}. + + Lemma transition_system_sum_comm (l1 : L1) (l2 : L2) : + @labels_commute _ _ _ (T1 <+> T2) (inl l1) (inr l2). + Proof. + unfold labels_commute. intros s s'. + split; sauto. + Qed. + End summ. + + Section product. + Context {Label S1 R1 S2 R2 : Type} + `{T1 : TransitionSystem S1 Label R1} `{T2 : TransitionSystem S2 Label R2}. + + Lemma transition_system_prod_comm (l1 : Label) (l2 : Label) : + @labels_commute _ _ _ T1 l1 l2 -> + @labels_commute _ _ _ T2 l1 l2 -> + @labels_commute _ _ _ (T1 <*> T2) l1 l2. + Proof. + unfold labels_commute. intros Hl Hr [s_l s_r] [s_l'' s_r'']. + split; intros H. + - specialize (Hl s_l s_l''). specialize (Hr s_r s_r''). + inversion_clear H; inversion_clear H1; inversion_clear H2; subst. + simpl in *. + constructor 2 with (s' := s'). + simpl. + + inversion_clear H0. + inversion_clear H. + simpl in *. + Abort. + End product. End commutativity. -Class CanonicalOrder {L : Type} := - { canonical_order : L -> L -> bool }. + +Section canonical_order. + Class CanonicalOrder (Label : Type) := + { + canon_rel : relation Label; + canon_decidable a b : {canon_rel a b} + {~canon_rel a b}; + canon_trans : Transitive canon_rel; + canon_irrefl : Irreflexive canon_rel; + }. + + Section comm. + Context `{TransitionSystem} `{CanonicalOrder Label}. + + Definition can_follow (a b : Label) := + (~labels_commute a b) \/ (canon_rel a b). + + Definition can_follow_hd (label : Label) (trace : list Label) : Prop := + match trace with + | [] => True + | head :: _ => can_follow label head + end. + + Inductive CanonicalTrace : list Label -> Prop := + | canontr_nil : CanonicalTrace [] + | canontr_cons : forall label trace, + can_follow_hd label trace -> + CanonicalTrace trace -> + CanonicalTrace (label :: trace). + + Theorem canon_trace_replacement : + (forall t, + + + + End comm. +End canonical_order. (** ** State space