PADEC - Coq Library
Library Padec.Model.Exec
From Coq Require Import SetoidClass.
From Coq Require Import SetoidList.
From Coq Require Import Bool.
From Coq Require Import SetoidList.
From Coq Require Import Bool.
From Padec Require Import Stream.
From Padec Require Import WellfoundedUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
Open Scope signature_scope.
Set Implicit Arguments.
Section Exec.
Context {Chans: Channels} {Net: Network} {Algo: Algorithm}.
From Padec Require Import WellfoundedUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
Open Scope signature_scope.
Set Implicit Arguments.
Section Exec.
Context {Chans: Channels} {Net: Network} {Algo: Algorithm}.
Execution
An execution is a maximal sequence of steps of the algorithm.Type Exec:
Exec = finite or infinite sequence of configurations (Env)Definition Exec: Type := Stream (A := Env).
Definition finite_exec := (finite (A := Env)).
Definition infinite_exec := (infinite (A := Env)).
is_exec:
a maximal sequence (i.e. infinite unless it reaches a terminal
configuration) such that any two consecutive configurations in
the sequence actually form a Step of the algorithm
Definition is_exec: Exec -> Prop :=
fun e => Always (fun e => match e with
| s_one g => terminal g
| s_cons g e => Step (s_hd e) g end) e.
Lemma is_exec_inv_0: forall g, is_exec (s_one g) -> terminal g.
Lemma is_exec_inv_1:
forall g e, is_exec (s_cons g e) -> Step (s_hd e) g.
Lemma is_exec_inv_1':
forall g e, is_exec (s_cons g e) -> ~ terminal g.
Lemma is_exec_inv_2: forall g e, is_exec (s_cons g e) -> is_exec e.
Global Instance is_exec_compat: Proper fequiv is_exec.
Global Instance is_exec_s_hd_compat: forall e, is_exec e ->
Proper pequiv (s_hd e).
Global Instance is_exec_proper: forall e, is_exec e -> Proper pequiv e.
Lemma proper_Always_hd_proper: forall e,
Proper pequiv e -> Always (fun e => Proper pequiv (s_hd e)) e.
is_exec_alt : aternative is_exec as a conjuction of simpler properties
Notation T := (fun e => match e with s_one g => terminal g
| s_cons _ _ => True end).
Notation S := (fun e => match e with s_one g => True
| s_cons a s => Step (s_hd s) a end).
Lemma is_exec_alt:
forall e, is_exec e <-> Always S e /\ Always T e.
Lemma is_exec_Always:
forall e: Exec, is_exec e -> Always is_exec e.
Lemma finite_exec_E_terminal:
forall e, is_exec e -> finite_exec e ->
Eventually (fun e => terminal (s_hd e)) e.
Lemma finite_exec_E_terminal_converse:
forall e, is_exec e -> Eventually (fun e => terminal (s_hd e)) e ->
finite_exec e.
Lemma RO_is_exec_Always:
forall (VarType: Type) (getVar: State -> VarType)
(SV: Stable_Variable _ getVar),
forall (P: (Node -> VarType) -> Prop) (P_compat: Proper fequiv P) e,
is_exec e -> P (fun n => getVar ((s_hd e) n)) ->
Always (fun e => P (fun n => getVar ((s_hd e) n))) e.
Lemma is_exec_When: forall P e (fe: Finally P e), is_exec e ->
is_exec (When fe).
Lemma is_exec_Assume:
forall {SA: Stable_Assumption} e,
Assume (s_hd e) -> is_exec e ->
Always (fun e => Assume (s_hd e)) e.
Lemma suffix_Assume:
forall {SA: Stable_Assumption} (e: Exec),
is_exec e -> Assume (s_hd e) ->
forall e_suf,
is_suffix e e_suf -> Assume (s_hd e_suf).
Node is enabled at the beginning of execution:
Definition EN_b (n: Node) (e: Exec): bool := enabled_b (s_hd e) n.
Definition EN (n: Node) (e: Exec): Prop := EN_b n e = true.
Definition EN (n: Node) (e: Exec): Prop := EN_b n e = true.
Node is activated at the beginning of execution:
Definition ACT_b (n: Node) (e: Exec): bool :=
match e with
s_one _ => false
| s_cons g e' => has_moved_b (s_hd e') g n
end.
Definition ACT (n: Node) (e: Exec): Prop := ACT_b n e = true.
match e with
s_one _ => false
| s_cons g e' => has_moved_b (s_hd e') g n
end.
Definition ACT (n: Node) (e: Exec): Prop := ACT_b n e = true.
Node is neutralized at the beginning of execution:
Definition NEUT_b (n: Node) (e: Exec): bool :=
match e with
s_one _ => false
| s_cons g e' =>
andb (enabled_b g n)
(andb (negb (has_moved_b (s_hd e') g n))
(negb (enabled_b (s_hd e') n)))
end.
Definition NEUT (n: Node) (e: Exec): Prop := NEUT_b n e = true.
match e with
s_one _ => false
| s_cons g e' =>
andb (enabled_b g n)
(andb (negb (has_moved_b (s_hd e') g n))
(negb (enabled_b (s_hd e') n)))
end.
Definition NEUT (n: Node) (e: Exec): Prop := NEUT_b n e = true.
Node is activated or neutralized at the beginning of execution:
Definition AN (n: Node) (e: Exec): Prop := ACT n e \/ NEUT n e.
Definition AN_b (n: Node) (e: Exec): bool := ACT_b n e || NEUT_b n e.
Lemma AN_alt: forall n e, AN n e <-> AN_b n e = true.
Definition act_neut_b e n := AN_b n e.
Definition AN_b (n: Node) (e: Exec): bool := ACT_b n e || NEUT_b n e.
Lemma AN_alt: forall n e, AN n e <-> AN_b n e = true.
Definition act_neut_b e n := AN_b n e.
Some direct properties (from the model)
Lemma act_en: forall (n: Node) (e: Exec), is_exec e -> ACT n e -> EN n e.
Lemma neut_en: forall (n: Node) (e: Exec), NEUT n e -> EN n e.
Lemma AN_one: forall n g, ~AN n (s_one g).
Lemma AN_en: forall n e, is_exec e -> AN n e -> EN n e.
Lemma en_progress: forall n e g,
EN n (s_cons g e) -> ~EN n e -> AN n (s_cons g e).
Lemma en_terminal: forall (g: Env), terminal g ->
forall (n: Node), ~EN n (s_one g).
Lemma ACT_mov:
forall n g e, ACT n (s_cons g e) ->
~( g n == s_hd e n).
Lemma NEUT_mov:
forall n g e, NEUT n (s_cons g e) -> ~( g =~= s_hd e ).
Lemma AN_mov:
forall n g e, AN n (s_cons g e) -> ~(g =~= s_hd e).
Lemma neut_en: forall (n: Node) (e: Exec), NEUT n e -> EN n e.
Lemma AN_one: forall n g, ~AN n (s_one g).
Lemma AN_en: forall n e, is_exec e -> AN n e -> EN n e.
Lemma en_progress: forall n e g,
EN n (s_cons g e) -> ~EN n e -> AN n (s_cons g e).
Lemma en_terminal: forall (g: Env), terminal g ->
forall (n: Node), ~EN n (s_one g).
Lemma ACT_mov:
forall n g e, ACT n (s_cons g e) ->
~( g n == s_hd e n).
Lemma NEUT_mov:
forall n g e, NEUT n (s_cons g e) -> ~( g =~= s_hd e ).
Lemma AN_mov:
forall n g e, AN n (s_cons g e) -> ~(g =~= s_hd e).
Global Instance EN_b_compat: Proper fequiv EN_b.
Global Instance EN_compat: Proper fequiv EN.
Global Instance ACT_b_compat: Proper fequiv ACT_b.
Global Instance ACT_compat: Proper fequiv ACT.
Global Instance NEUT_b_compat: Proper fequiv NEUT_b.
Global Instance NEUT_compat: Proper fequiv NEUT.
Global Instance AN_b_compat: Proper fequiv AN_b.
Global Instance AN_compat: Proper fequiv AN.
Lemma E_AN_not_constant:
forall e n, Eventually (AN n) e -> forall g, ~ is_constant g e.
Lemma AN_act_neut_b: forall e n, act_neut_b e n = true <-> AN n e.
Lemma EN_enabled_b: forall e n, enabled_b (s_hd e) n = true <-> EN n e.
Global Instance act_neut_b_compat: Proper fequiv act_neut_b.
Lemma act_neut_b_enabled_b: forall e n, is_exec e ->
act_neut_b e n = true ->
enabled_b (s_hd e) n = true.
Lemma ACT_b_EN_b: forall n e, is_exec e ->
ACT_b n e = true ->
EN_b n e = true.
Lemma ACT_EN: forall n e, is_exec e -> ACT n e -> EN n e.
Lemma act_neut_contd:
forall g (e: Exec) n,
enabled_b g n = true ->
act_neut_b (s_cons g e) n = false ->
enabled_b (s_hd e) n = true.
Lemma act_b_true:
forall (g: Env) e p,
Step (s_hd e) g ->
ACT_b p (s_cons g e) = true -> RUN g p == s_hd e p.
Lemma neut_b_true:
forall (g: Env) e p,
Step (s_hd e) g ->
NEUT_b p (s_cons g e) = true -> RUN (s_hd e) p == s_hd e p.
End Enabled_Activated_Neutralized.
Section Synchronous.
CoFixpoint sync_exec (g: Env): Exec :=
if terminal_dec g then s_one g
else s_cons g (sync_exec (RUN g)).
Lemma sync_exec_unfold:
forall g, sync_exec g =
if terminal_dec g then s_one g
else s_cons g (sync_exec (RUN g)).
Lemma sync_exec_hd: forall g, (s_hd (sync_exec g)) = g.
Global Instance sync_exec_compat: Proper fequiv sync_exec.
Definition sync_step (g' g: Env): Prop :=
forall n, enabled_b g n = true -> has_moved_b g' g n = true.
Definition synchronous_exec: Exec -> Prop :=
Always (fun e => match e with
| s_one _ => True
| s_cons g e => sync_step (s_hd e) g end).
Lemma synchronous_exec_sync_exec:
forall g, Proper pequiv g -> synchronous_exec (sync_exec g).
Lemma sync_exec_is_exec:
forall g, Proper pequiv g -> is_exec (sync_exec g).
End Synchronous.
Section Sequential.
Definition at_most_one_enabled (g: Env): Prop :=
forall n n', enabled_b g n = true -> enabled_b g n' = true -> n == n'.
Definition sequential_exec: Exec -> Prop :=
Always (fun e => at_most_one_enabled (s_hd e)).
End Sequential.
End Exec.
Close Scope signature_scope.
Unset Implicit Arguments.
Global Instance EN_compat: Proper fequiv EN.
Global Instance ACT_b_compat: Proper fequiv ACT_b.
Global Instance ACT_compat: Proper fequiv ACT.
Global Instance NEUT_b_compat: Proper fequiv NEUT_b.
Global Instance NEUT_compat: Proper fequiv NEUT.
Global Instance AN_b_compat: Proper fequiv AN_b.
Global Instance AN_compat: Proper fequiv AN.
Lemma E_AN_not_constant:
forall e n, Eventually (AN n) e -> forall g, ~ is_constant g e.
Lemma AN_act_neut_b: forall e n, act_neut_b e n = true <-> AN n e.
Lemma EN_enabled_b: forall e n, enabled_b (s_hd e) n = true <-> EN n e.
Global Instance act_neut_b_compat: Proper fequiv act_neut_b.
Lemma act_neut_b_enabled_b: forall e n, is_exec e ->
act_neut_b e n = true ->
enabled_b (s_hd e) n = true.
Lemma ACT_b_EN_b: forall n e, is_exec e ->
ACT_b n e = true ->
EN_b n e = true.
Lemma ACT_EN: forall n e, is_exec e -> ACT n e -> EN n e.
Lemma act_neut_contd:
forall g (e: Exec) n,
enabled_b g n = true ->
act_neut_b (s_cons g e) n = false ->
enabled_b (s_hd e) n = true.
Lemma act_b_true:
forall (g: Env) e p,
Step (s_hd e) g ->
ACT_b p (s_cons g e) = true -> RUN g p == s_hd e p.
Lemma neut_b_true:
forall (g: Env) e p,
Step (s_hd e) g ->
NEUT_b p (s_cons g e) = true -> RUN (s_hd e) p == s_hd e p.
End Enabled_Activated_Neutralized.
Section Synchronous.
CoFixpoint sync_exec (g: Env): Exec :=
if terminal_dec g then s_one g
else s_cons g (sync_exec (RUN g)).
Lemma sync_exec_unfold:
forall g, sync_exec g =
if terminal_dec g then s_one g
else s_cons g (sync_exec (RUN g)).
Lemma sync_exec_hd: forall g, (s_hd (sync_exec g)) = g.
Global Instance sync_exec_compat: Proper fequiv sync_exec.
Definition sync_step (g' g: Env): Prop :=
forall n, enabled_b g n = true -> has_moved_b g' g n = true.
Definition synchronous_exec: Exec -> Prop :=
Always (fun e => match e with
| s_one _ => True
| s_cons g e => sync_step (s_hd e) g end).
Lemma synchronous_exec_sync_exec:
forall g, Proper pequiv g -> synchronous_exec (sync_exec g).
Lemma sync_exec_is_exec:
forall g, Proper pequiv g -> is_exec (sync_exec g).
End Synchronous.
Section Sequential.
Definition at_most_one_enabled (g: Env): Prop :=
forall n n', enabled_b g n = true -> enabled_b g n' = true -> n == n'.
Definition sequential_exec: Exec -> Prop :=
Always (fun e => at_most_one_enabled (s_hd e)).
End Sequential.
End Exec.
Close Scope signature_scope.
Unset Implicit Arguments.