Library NetworkLanguage

This file was written by Colm Bhandal, PhD student, Foundations and Methods group, School of Computer Science and Statistics, Trinity College, Dublin, Ireland.

*************************** Standard Imports

Require Import Coq.Program.Equality.
Require Import ComhCoq.Extras.LibTactics.

Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Export EntityLanguage.
Require Import ComhCoq.EntAuxResults.

Definition Network : Type := list Entity.

Coercion singNet (e : Entity) : Network := [e].

Reserved Notation "e @ i .: n" (at level 50).

e @ i :: n says that e is at position i in the network n. The first position is position 0.

Inductive entInNet (e : Entity) : nat -> Network -> Prop :=
  | einConsLeft : forall (n : Network),
    e @ 0 .: (e :: n)
  | einConsRight : forall (i : nat) (e' : Entity) (n : Network),
    e @ i .: n -> e @ (S i) .: (e' :: n)
  where "e @ i .: n" := (entInNet e i n).

If an entity is in a network according to the definition of entInNet, then it is in the list according to In.

Theorem entInNet_inList : forall (e : Entity) (n : Network) (i : nat),
e @ i .: n -> e _: n.

If e is at i in n and so is e', then e = e'.

Theorem entInNetUnique : forall (e e' : Entity) (i : nat) (n : Network),
  e @ i .: n -> e' @ i .: n -> e = e'.

Ltac entnetuniq U e1 e2 :=
  match goal with
  [H1 : e1 @ ?i .: ?n, H2 : e2 @ ?i .: ?n |- _ ] =>
  let U1 := fresh U in lets U1 : entInNetUnique H1 H2
  end.

Ltac entnetuniq2 U n :=
  match goal with
  [H1 : _ @ _ .: n, H2 : _ @ _ .: n |- _ ] =>
  let U1 := fresh U in lets U1 : entInNetUnique H1 H2
  end.

There either exists an entity at position i or there doesn't.

Theorem decEntInNet : forall (i : nat) (n : Network),
decidable (exists e, e @ i .: n).

Open Scope nat_scope.

We define what it means for a network to be safe.

Definition safe (n : Network) : Prop :=
forall (e1 e2 : Entity) (i j : nat), (i < j) ->
e1 @ i .: n -> e2 @ j .: n -> compatible e1 e2.

An alternative definition of safety. The only difference here is that i <> j rather than i < j.

Definition safeAlt (n : Network) : Prop :=
forall (e1 e2 : Entity) (i j : nat), (i <> j) ->
e1 @ i .: n -> e2 @ j .: n -> compatible e1 e2.

The two definitions of safe are the same.

Theorem safeDefsEquiv : forall n : Network,
safe n <-> safeAlt n.

Defining safety for a single entity in a network as follows: e is safe at i in the network n iff e is at i in n and forall entities e' at j in n for some j not equal i, e and e' are compatible.

Definition safeSing (e : Entity) (i : nat) (n : Network) :=
  e @ i .: n /\
  forall (j : nat) (e' : Entity), j <> i -> e' @ j .: n ->
  e ~~ e'.
Notation "e .! i .: n" := (safeSing e i n) (at level 50, left associativity).

A network n is safe iff every entity in the network is singularly safe.

Theorem safeIffSafeSing : forall (n : Network),
  safe n <->
  forall (e : Entity) (i : nat),
  e @ i .: n -> e .! i .: n.

A discrete action is either the input, output or ignorance of a message, or it is the silent value tau. Notice that output actions are indexed by a natural number- this keeps track of which entity in the network performed the output.

Inductive ActDiscNet : Type :=
  | anOut : Message -> nat -> ActDiscNet
  | anIn : Message -> ActDiscNet
  | anIg : Message -> ActDiscNet

The accept relation is essentially the union of the input and output relations. Its purpose is purely to simplify the expression of the semantics.

| anAcc : Message -> ActDiscNet
| anTau : ActDiscNet.
Notation "b /! i" := (anOut b i) (at level 30).
Notation "b /?" := (anIn b) (at level 30).
Notation "b /:" := (anIg b) (at level 30).
Notation "b /?:" := (anAcc b) (at level 30).

Convert an entity action to a network action

Coercion entToNetAct (a : ActDiscEnt) : ActDiscNet :=
  match a with
  | aeTagOut m => anOut m 0
  | aeTagIn m => anIn m
  | aeTagIg m => anIg m
  | aeTau => anTau
  end.

Reserved Notation "n1 -NA- a -NA> n2" (left associativity, at level 50).
Reserved Notation "n1 -ND- d -ND> n2" (left associativity, at level 50).

The discrete labelled transition relation on networks.

Inductive stepDiscNet : Network -> ActDiscNet -> Network -> Prop :=

The empty network can ignore any value.

| stepDnEmpIg : forall m : Message, [] -NA- m/: -NA> []

For every input, there is a corresponding accept.

  | stepDnAccIn : forall (n n' : Network) (m : Message),
    n -NA- m/? -NA> n' -> n -NA- m/?: -NA> n'

For every ignore, there is a corresponding accept.

  | stepDnAccIg : forall (n n' : Network) (m : Message),
    n -NA- m/: -NA> n' -> n -NA- m/?: -NA> n'
  | stepDnIgnore : forall (n n' : Network) (e e' : Entity) (m : Message),
    e -EA- m#: ->> e' -> n -NA- m/: -NA> n' ->
    (e :: n) -NA- m/: -NA> (e' :: n')
  | stepDnOutHead : forall (n n' : Network) (e e' : Entity) (m : Message),
    e -EA- m#! ->> e' -> n -NA- m/?: -NA> n' ->
    (e :: n) -NA- m/!0 -NA> (e' :: n')
  | stepDnOutInTail : forall (n n' : Network) (e e' : Entity) (m : Message) (i : nat),
    e -EA- m#? ->> e' -> n -NA- m/!i -NA> n' ->
    (e :: n) -NA- m/!(S i) -NA> (e' :: n')
  | stepDnOutIgTail : forall (n n' : Network) (e e' : Entity) (m : Message) (i : nat),
    e -EA- m#: ->> e' -> n -NA- m/!i -NA> n' ->
    (e :: n) -NA- m/!(S i) -NA> (e' :: n')
  | stepDnInHead : forall (n n' : Network) (e e' : Entity) (m : Message),
    e -EA- m#? ->> e' -> n -NA- m/?: -NA> n' ->
    (e :: n) -NA- m/? -NA> (e' :: n')
  | stepDnInTail : forall (n n' : Network) (e e' : Entity) (m : Message),
    e -EA- m#: ->> e' -> n -NA- m/? -NA> n' ->
    (e :: n) -NA- m/? -NA> (e' :: n')
  | stepDnTauHead : forall (n : Network) (e e' : Entity),
    e -EA- aeTau ->> e' -> (e :: n) -NA- anTau -NA> (e' :: n)
  | stepDnTauTail : forall (n n' : Network) (e : Entity),
    n -NA- anTau -NA> n' -> (e :: n) -NA- anTau -NA> (e :: n')
  where "n1 -NA- a -NA> n2" := (stepDiscNet n1 a n2).

Definition discActEnabledNet (n : Network) (a : ActDiscNet) :=
  exists n', n -NA- a -NA> n'.

The time-labelled transition relation on networks.

Inductive stepTimedNet : Network -> Delay -> Network -> Prop :=
  | stepTnEmp : forall (d : Delay), [] -ND- d -ND> []
  | stepTnCons : forall (n n' : Network) (e e' : Entity) (d : Delay),
    e -ED- d ->> e' -> n -ND- d -ND> n' ->
    (e :: n) -ND- d -ND> (e' :: n')
  where "n1 -ND- d -ND> n2" := (stepTimedNet n1 d n2).

An accept action is always the result of an input or an ignore (as opposed to say a lift).

Lemma accInOrIg : forall (n n' : Network) (m : Message),
n -NA- m/?: -NA> n' -> (n -NA- m/? -NA> n') \/ (n -NA- m/: -NA> n').

Definition emptyNet : Network := [].
Notation "[\]" := emptyNet.

Every non-null network is able to accept any message.

Theorem accNet : forall (n : Network) (m : Message),
discActEnabledNet n (m/?:).

The ignore relation preserves networks.

Lemma ignoreEqNet : forall (n n' : Network) (m : Message),
n -NA- m/: -NA> n' -> n = n'.

Membership of the singleton network enforces the obvious equality. Also, the index of the member entity is 0.

Lemma entInNetSing : forall (e e' : Entity) (i : nat),
e @ i .: [e'] -> e = e' /\ i = 0.

If a network ignores a value and there is an entity in the derivative network, then there was an entity in the original network that also ignores the value.

Lemma ignoreLink : forall (n n' : Network) (e : Entity) (i : nat) (m : Message),
n -NA- m/: -NA> n' -> e @ i .: n' ->
e @ i .: n /\ e -EA- m#: ->> e.

If a network accepts a value, then the tail of that network accepts the value.

Lemma acceptTail : forall (e e' : Entity) (n n' : Network) (m : Message),
(e :: n) -NA- m/?: -NA> (e' :: n') -> n -NA- m/?: -NA> n'.

If a network is capable of accepting a message, and there is some entity in the network, then that entity can either input or ignore the message.

Lemma acceptLink : forall (n n' : Network) (e' : Entity) (i : nat) (m : Message),
n -NA- m/?: -NA> n' -> e' @ i .: n' -> exists e,
e @ i .: n /\ (e -EA- m#: ->> e' \/ e -EA- m#? ->> e').

Case: i is 0, entity is at the head of the list

Case: i is not 0, entity is within the smaller list- induct

If an network performs an output with index i, then there are entities e and e' at index i in both the source and derivative networks and e performs the output to become e'.

Lemma outputMatch : forall (n n' : Network) (i : nat) (m : Message),
n -NA- m/!i -NA> n' -> exists e e',
e @ i .: n /\ e' @ i .: n' /\ e -EA- m#! ->> e'.

Case: head.

Case: out tail in head.

Case: out tail, ig head- the very same as before.

If an network performs an output with index i, and there is an entity in the derivative network at index i', with i <> i', then there is a corresponding entity at the index i' in the original network, and the two are linked by either an input or an ignore transition.

Lemma outputMismatch : forall (n n' : Network) (e' : Entity) (i i' : nat) (m : Message),
n -NA- m/!i -NA> n' -> e' @ i' .: n' -> i <> i' -> exists e,
e @ i' .: n /\ (e -EA- m#? ->> e' \/ e -EA- m#: ->> e').

Out head case (haha head-case).

Out tail, in head case.

Out tail, ig head case- almost the same as before.

If a network outputs a message and there is an entity in the derivative network, then there is an entity in the same position in the original network and that entity can either output, input or ignore the same message.

Lemma outputLink : forall (n n' : Network) (e' : Entity) (i i' : nat) (m : Message),
n -NA- m/!i -NA> n' -> e' @ i' .: n' -> exists e,
e @ i' .: n /\ (e -EA- m#! ->> e' \/ e -EA- m#? ->> e' \/ e -EA- m#: ->> e').

If a network performs a silent action, it is due to exactly one of its component entities performing a silent action. The rest of the entities remain the same, unscathed by the muffled action that they cannot see.

Lemma tauLink : forall (n n' : Network),
  n -NA- anTau -NA> n' -> exists i e e',
  e @ i .: n /\ e' @ i .: n' /\ e -EA- aeTau ->> e' /\
  (forall (i' : nat) (e1 : Entity), i <> i' -> e1 @ i' .: n' ->
   e1 @ i' .: n).

Case tau tail

Open Scope R_scope.

If an entity evolves by time delay d, then the change in its position is bounded by d times the assumed maximum speed.

Theorem boundedMovement : forall (e e' : Entity) (d : Delay),
e -ED- d ->> e' -> dist2d e e' <= (d * speedMax).

The discrete transition relation preserves the position of an entity.

Theorem stepDiscPresPos : forall (e e' : Entity) (a : ActDiscEnt),
e -EA- a ->> e' -> posEnt e = posEnt e'.

A discrete action that can be done by an entity can be lifted to the singleton network.

Theorem liftDiscEntNet : forall (e e' : Entity) (a : ActDiscEnt),
  e -EA- a ->> e' -> [e] -NA- a -NA> [e'].
Lemma link_net_ent_disc_fwd :
  forall (n n' : Network) (e : Entity) (i : nat) (a : ActDiscNet),
  n -NA- a -NA> n' ->
  e @ i .: n ->
  exists e', e' @ i .: n' /\ (e = e' \/ (exists a', e -EA- a' ->> e')).
Ltac link_netentdiscfwd_tac0 e' U :=
  match goal with
  | [ H : ?n -NA- ?a -NA> ?n', H0 : ?e @ ?i .: ?n |- _] =>
    let H1 := fresh in lets H1 : link_net_ent_disc_fwd H H0;
    let H2 := fresh in destruct H1 as [e' H2];
    let U1 := fresh U in let H3 := fresh in
    decompAnd2 H2 U1 H3
  end.

Ltac link_netentdiscfwd_tac e' b U :=
  match goal with
  | [ H : ?n -NA- ?a -NA> ?n', H0 : ?e @ ?i .: ?n |- _] =>
    let H1 := fresh in lets H1 : link_net_ent_disc_fwd H H0;
    let H2 := fresh in destruct H1 as [e' H2];
    let U1 := fresh U in let H3 := fresh in
    decompAnd2 H2 U1 H3; let U2 := fresh U in let H4 := fresh in
    elim_intro H3 U2 H4;
    [ | let U3 := fresh U in invertClearAs2 H4 b U3]
  end.

If a network performs a discrete step to another network, then for all entities e' in the derivative network, there is an entity e in the original at the same position as e', and e -a-> e'.

Lemma link_net_ent_disc_bkwd : forall (n n' : Network) (e' : Entity) (i : nat) (a : ActDiscNet),
n -NA- a -NA> n' -> e' @ i .: n' -> exists e, e @ i .: n /\
(e = e' \/ exists a', e -EA- a' ->> e').

Output case.

Input case.

Ignore case- convert to accept and same as last time.

Accept case- same again.

Tau case.

Ltac link_netentdiscbkwd_tac0 e b U :=
  match goal with
  | [ H : ?n -NA- ?a -NA> ?n', H0 : ?e' @ ?i .: ?n' |- _] =>
    let H1 := fresh in lets H1 : link_net_ent_disc_bkwd H H0;
    let H2 := fresh in destruct H1 as [e H2];
    let U1 := fresh U in let H3 := fresh in
    decompAnd2 H2 U1 H3
  end.

Ltac link_netentdiscbkwd_tac e b U :=
  match goal with
  | [ H : ?n -NA- ?a -NA> ?n', H0 : ?e' @ ?i .: ?n' |- _] =>
    let H1 := fresh in lets H1 : link_net_ent_disc_bkwd H H0;
    let H2 := fresh in destruct H1 as [e H2];
    let U1 := fresh U in let H3 := fresh in
    decompAnd2 H2 U1 H3; let U2 := fresh U in let H4 := fresh in
    elim_intro H3 U2 H4;
    [ | let U3 := fresh U in invertClearAs2 H4 b U3]
  end.

Lemma link_net_ent_disc_bkwdW (n n' : Network) (e' : Entity) (i : nat) (a : ActDiscNet) :
  n -NA- a -NA> n' -> e' @ i .: n' -> exists e, e @ i .: n.

If a network performs a timed step to another network, then for all entities e' in the derivative network, there is an entity e in the original at the same position as e', and e can perform the same timed step to e'.

Lemma link_net_ent_del_bkwd : forall (n n' : Network) (e' : Entity) (i : nat) (d : Delay),
  n -ND- d -ND> n' -> e' @ i .: n' -> exists e, e @ i .: n /\ e -ED- d ->> e'.

Ltac link_netentdelbkwd_tac e U :=
  match goal with
  | [ H : ?n -ND- ?d -ND> ?n', H0 : ?e' @ ?i .: ?n' |- _] =>
    let H1 := fresh in lets H1 : link_net_ent_del_bkwd H H0;
    let H2 := fresh in destruct H1 as [e H2];
    let U1 := fresh U in let U2 := fresh U in
    decompAnd2 H2 U1 U2
  end.

A weakened, but easier to use version of the timed linking theorem.

Lemma link_net_ent_delW : forall (n n' : Network) (e e' : Entity) (i : nat) (d : Delay),
n -ND- d -ND> n' -> e' @ i .: n' -> e @ i .: n -> e -ED- d ->> e'.

Lemma link_net_ent_del_fwd : forall (n n' : Network) (e : Entity) (i : nat) (d : Delay),
  n -ND- d -ND> n' -> e @ i .: n -> exists e', e' @ i .: n' /\ e -ED- d ->> e'.

Ltac link_netentdelfwd_tac e' U :=
  match goal with
  | [ H : ?n -ND- ?d -ND> ?n', H0 : ?e @ ?i .: ?n |- _] =>
    let H1 := fresh in lets H1 : link_net_ent_del_fwd H H0;
    let H2 := fresh in destruct H1 as [e' H2];
    let U1 := fresh U in let U2 := fresh U in
    decompAnd2 H2 U1 U2
  end.

Ltac link_netsoftdel_tac U :=
  match goal with
  | [ H : ?n -ND- ?d -ND> ?n', H0 : [|?p, ?l, ?h, ?k|] @ ?i .: ?n,
    H1 : [|?p', ?l', ?h', ?k'|] @ ?i .: ?n' |- _] =>
    let U1 := fresh U in lets U1 : link_net_ent_delW H H0 H1;
    apply link_ent_soft_del in U1
  end.

Ltac link_netmstatedel_tac U :=
  match goal with
  | [ H : ?n -ND- ?d -ND> ?n', H0 : [|?p, ?l, ?h, ?k|] @ ?i .: ?n,
    H1 : [|?p', ?l', ?h', ?k'|] @ ?i .: ?n' |- _] =>
    let U1 := fresh U in lets U1 : link_net_ent_delW H H0 H1;
    apply link_ent_mState_del in U1
  end.

Ltac link_netinterdel_tac U :=
  match goal with
  | [ H : ?n -ND- ?d -ND> ?n', H0 : [|?p, ?l, ?h, ?k|] @ ?i .: ?n,
    H1 : [|?p', ?l', ?h', ?k'|] @ ?i .: ?n' |- _] =>
    let U1 := fresh U in lets U1 : link_net_ent_delW H H0 H1;
    apply link_ent_inter_del in U1
  end.

If a network n delays by d to n', and e1 e2 are separated by x in n, then e1' e2' are separated by at least x - 2*smax*d in n'. Where e1' e2' are the derivatives of e1 and e2 respectively.

Theorem bndDistLwr :
  forall (n n' : Network) (e1 e2 e1' e2' : Entity) (i j : nat) (d : Delay),
  n -ND- d -ND> n' -> e1 @ i .: n -> e1' @ i .: n' -> e2 @ j .: n -> e2' @ j .: n' ->
  dist2d e1 e2 - (2*d*speedMax) <= dist2d e1' e2'.

If a network n delays by d to n', and e1 e2 are separated by x in n, then e1' e2' are separated by at most x + 2*smax*d in n'. Where e1' e2' are the derivatives of e1 and e2 respectively.

Theorem bndDistUpper :
  forall (n n' : Network) (e1 e2 e1' e2' : Entity) (i j : nat) (d : Delay),
  n -ND- d -ND> n' -> e1 @ i .: n -> e1' @ i .: n' -> e2 @ j .: n -> e2' @ j .: n' ->
  dist2d e1' e2' <= dist2d e1 e2 + (2*d*speedMax).

Lemma stepNet_tau_pres_pos (n n' : Network) (e e' : Entity) (i : nat) :
  n -NA- anTau -NA> n' -> e @ i .: n -> e' @ i .: n' -> posEnt e = posEnt e'.

Lemma timeSplit_net n n'' d d' d'' :
  n -ND- d'' -ND> n'' -> d'' = d +d+ d' ->
  exists n', n -ND- d -ND> n' /\ n' -ND- d' -ND> n''.

This page has been generated by coqdoc