Library Systems
Set Implicit Arguments.
Require Export Cpo_streams_type.
Definition of a multiple node :
- index for inputs with associated types
- index for outputs with associated types
- continuous function on corresponding streams
Definition DS_fam (I:Type)(SI:I -> Type) (i:I) := DS (SI i).
Definition DS_prod (I:Type)(SI:I -> Type) := Dprodi (DS_fam SI).
- A node is a continuous function from inpits to outputs
Definition node_fun (I O : Type) (SI : I -> Type) (SO : O -> Type) :cpo
:= DS_prod SI -C-> DS_prod SO.
- node with a single output
Definition snode_fun (I : Type) (SI : I -> Type) (SO : Type) : cpo := DS_prod SI -C-> DS SO.
- Each link is either an input link or is associated to the output of a simple node, each input of that node is associated to a link with the apropriate type
Definition inlSL (LI LO:Type) (SL:(LI+LO)->Type) (i:LI) := SL (inl LO i).
Definition inrSL (LI LO:Type) (SL:(LI+LO)->Type) (o:LO) := SL (inr LI o).
A system associates a continuous functions to a set of typed output links
Definition system (LI LO:Type) (SL:LI+LO->Type)
:= Dprodi (fun (o:LO) => DS_prod SL -C-> DS (inrSL SL o)).
Each system defines a new node with inputs for the inputs of the system
Equations are a continuous functional on links
Definition eqn_of_system : forall (LI LO:Type) (SL:LI+LO->Type),
system SL -> DS_prod (inlSL SL) -> DS_prod SL -m> DS_prod SL.
intros LI LO SL s init.
exists (fun X : DS_prod SL => fun l : LI+LO =>
match l return (DS (SL l)) with
inl i => init i
| inr o => s o X
end).
red;intros X Y Hle; intro l.
case l; auto.
Defined.
Lemma eqn_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init : DS_prod (inlSL SL)) (X:DS_prod SL),
eqn_of_system s init X =
fun l : LI+LO =>
match l return (DS (SL l)) with
inl i => init i
| inr o => s o X
end.
trivial.
Save.
Lemma eqn_of_system_cont : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init : DS_prod (inlSL SL)), continuous (eqn_of_system s init).
intros; apply Dprodi_continuous with (Di:= fun i => DS (SL i)); intro.
red; intros.
rewrite fmon_comp_simpl.
rewrite (Proj_simpl (O:=DS_fam SL)).
rewrite (eqn_of_system_simpl (SL:=SL)).
case i; intros; auto.
apply (le_lub (c:=DS (SL (inl LO l)))) with
(f:=(Proj (DS_fam SL) (inl LO l) @ eqn_of_system s init) @ h)
(n:=O).
rewrite (fcont_continuous (s l)).
apply lub_le_compat; intro n; simpl.
apply DSle_refl.
Save.
Hint Resolve eqn_of_system_cont.
Definition EQN_of_system : forall (LI LO:Type) (SL:LI+LO->Type),
system SL -> DS_prod (inlSL SL) -> DS_prod SL -c> DS_prod SL.
intros LI LO SL s init; exists (eqn_of_system s init); auto.
Defined.
Lemma EQN_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init : DS_prod (inlSL SL)) (X:DS_prod SL),
EQN_of_system s init X = eqn_of_system s init X.
trivial.
Save.
The equations are monotonic with respect to the inputs and the system
Lemma EQN_of_system_mon : forall (LI LO:Type) (SL:LI+LO->Type)
(s1 s2 : system SL) (init1 init2 : DS_prod (inlSL SL)),
s1 <= s2 -> init1 <= init2 -> EQN_of_system s1 init1 <= EQN_of_system s2 init2.
intros; apply fcont_le_intro; intro X.
repeat (rewrite (EQN_of_system_simpl)); repeat (rewrite (eqn_of_system_simpl)).
intro l; case l; auto.
intros; apply (H l0 X).
Save.
Definition Eqn_of_system : forall (LI LO:Type) (SL:LI+LO->Type),
(system SL) -m> DS_prod (inlSL SL) -M-> DS_prod SL -C-> DS_prod SL.
intros; exact (le_compat2_mon (EQN_of_system_mon (SL:=SL))).
Defined.
Lemma Eqn_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init:DS_prod (inlSL SL)), Eqn_of_system SL s init = EQN_of_system s init.
trivial.
Save.
The equations are continuous with respect to the inputs
Lemma Eqn_of_system_cont : forall (LI LO:Type) (SL:LI+LO->Type),
continuous2 (Eqn_of_system SL).
red; intros.
rewrite (Eqn_of_system_simpl (SL:=SL)).
apply (fcont_le_intro (D1:=DS_prod SL) (D2:=DS_prod SL)); intro X.
rewrite EQN_of_system_simpl; rewrite eqn_of_system_simpl; intro l.
case_eq l; intros.
rewrite fcont_lub_simpl.
unfold DS_prod; repeat (rewrite Dprodi_lub_simpl).
apply lub_le_compat; intro n; auto.
unfold system; rewrite Dprodi_lub_simpl.
repeat rewrite fcont_lub_simpl.
unfold DS_prod; rewrite Dprodi_lub_simpl.
apply lub_le_compat.
intro n; simpl; auto.
Save.
Hint Resolve Eqn_of_system_cont.
Lemma Eqn_of_system_cont2 : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL),
continuous (Eqn_of_system SL s).
red; intros; apply continuous2_right; auto.
Save.
Lemma Eqn_of_system_cont1 : forall (LI LO:Type) (SL:LI+LO->Type),
continuous (Eqn_of_system SL).
auto.
Save.
Definition EQN_of_SYSTEM (LI LO:Type) (SL:LI+LO->Type)
: system SL -c> DS_prod (inlSL SL) -C-> DS_prod SL -C-> DS_prod SL
:= continuous2_cont (Eqn_of_system_cont (SL:=SL)).
The solution is defined as the smallest fixpoint of the equations
it is a monotonic function of the inputs
Definition sol_of_system (LI LO:Type) (SL:LI+LO->Type)
: system SL -c> DS_prod (inlSL SL) -C-> DS_prod SL := FIXP (DS_prod SL) @@_ EQN_of_SYSTEM SL.
Lemma sol_of_system_simpl :
forall (LI LO:Type) (SL:LI+LO->Type) (s:system SL) (init:DS_prod (inlSL SL)),
sol_of_system SL s init = FIXP (DS_prod SL) (EQN_of_system s init).
trivial.
Save.
Lemma sol_of_system_eq : forall (LI LO:Type) (SL:LI+LO->Type) (s:system SL) (init:DS_prod (inlSL SL)),
sol_of_system SL s init == eqn_of_system s init (sol_of_system SL s init).
intros; rewrite sol_of_system_simpl.
apply (fixp_eq (D:=DS_prod SL) (f:=eqn_of_system s init)); auto.
Save.
We can choose an arbitrary set of outputs
Definition node_of_system (O:Type)(LI LO:Type) (SL:LI+LO->Type)(indO : O -> LO) :
system SL -C-> node_fun (fun i : LI => SL (inl LO i)) (fun o : O => SL (inr LI (indO o)))
:= DLIFTi (DS_fam SL) (fun o => inr LI (indO o)) @@_ (sol_of_system SL).
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (24 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (13 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
Global Index
D
DS_fam [definition, in Systems]DS_prod [definition, in Systems]
E
EQN_of_SYSTEM [definition, in Systems]eqn_of_system [definition, in Systems]
EQN_of_system [definition, in Systems]
Eqn_of_system [definition, in Systems]
eqn_of_system_cont [lemma, in Systems]
Eqn_of_system_cont [lemma, in Systems]
Eqn_of_system_cont1 [lemma, in Systems]
Eqn_of_system_cont2 [lemma, in Systems]
EQN_of_system_mon [lemma, in Systems]
EQN_of_system_simpl [lemma, in Systems]
Eqn_of_system_simpl [lemma, in Systems]
eqn_of_system_simpl [lemma, in Systems]
I
inlSL [definition, in Systems]inrSL [definition, in Systems]
N
node_fun [definition, in Systems]node_of_system [definition, in Systems]
S
snode_fun [definition, in Systems]sol_of_system [definition, in Systems]
sol_of_system_eq [lemma, in Systems]
sol_of_system_simpl [lemma, in Systems]
system [definition, in Systems]
Systems [library]
Lemma Index
E
eqn_of_system_cont [in Systems]Eqn_of_system_cont [in Systems]
Eqn_of_system_cont1 [in Systems]
Eqn_of_system_cont2 [in Systems]
EQN_of_system_mon [in Systems]
EQN_of_system_simpl [in Systems]
Eqn_of_system_simpl [in Systems]
eqn_of_system_simpl [in Systems]
S
sol_of_system_eq [in Systems]sol_of_system_simpl [in Systems]
Definition Index
D
DS_fam [in Systems]DS_prod [in Systems]
E
EQN_of_SYSTEM [in Systems]eqn_of_system [in Systems]
EQN_of_system [in Systems]
Eqn_of_system [in Systems]
I
inlSL [in Systems]inrSL [in Systems]
N
node_fun [in Systems]node_of_system [in Systems]
S
snode_fun [in Systems]sol_of_system [in Systems]
system [in Systems]
Library Index
S
Systems| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (24 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (10 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (13 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
This page has been generated by coqdoc