Library skel_sem
Section Process.
Variables TI TO : arity.
Definition process := fam (FL TI) -> fam (FL TO) -> Prop.
Definition Pincl (P1 P2: process) := forall li lo, P1 li lo -> P2 li lo.
Lemma Pincl_refl : Reflexive Pincl.
red; unfold Pincl; auto.
Qed.
Lemma Pincl_trans : Transitive Pincl.
red; unfold Pincl; firstorder.
Qed.
Definition Peq (P1 P2: process) := forall li lo, P1 li lo <-> P2 li lo.
Hint Unfold Peq.
Lemma Peq_refl : Reflexive Peq.
red; unfold Peq; tauto.
Qed.
Lemma Peq_sym: Symmetric Peq.
red; unfold Peq; firstorder.
Qed.
Lemma Peq_trans : Transitive Peq.
red; unfold Peq; intros.
rewrite H; auto.
Qed.
Lemma Peq_incl : forall P Q, Peq P Q -> Pincl P Q.
unfold Pincl, Peq; firstorder.
Save.
Lemma Peq_incl_sym : forall P Q, Peq P Q -> Pincl Q P.
unfold Pincl, Peq; firstorder.
Save.
Lemma Pincl_eq : forall P Q, Pincl P Q -> Pincl Q P -> Peq P Q.
unfold Pincl, Peq; firstorder.
Save.
End Process.
Hint Immediate Peq_incl Peq_incl_sym Pincl_eq Peq_sym.
Hint Resolve Peq_refl Pincl_refl.
Add Parametric Relation {TI TO} : (process TI TO) (@Peq TI TO)
reflexivity proved by (@Peq_refl TI TO)
symmetry proved by (@Peq_sym TI TO)
transitivity proved by (@Peq_trans TI TO)
as Peq_setoid.
Variables TI TO : arity.
Definition process := fam (FL TI) -> fam (FL TO) -> Prop.
Definition Pincl (P1 P2: process) := forall li lo, P1 li lo -> P2 li lo.
Lemma Pincl_refl : Reflexive Pincl.
red; unfold Pincl; auto.
Qed.
Lemma Pincl_trans : Transitive Pincl.
red; unfold Pincl; firstorder.
Qed.
Definition Peq (P1 P2: process) := forall li lo, P1 li lo <-> P2 li lo.
Hint Unfold Peq.
Lemma Peq_refl : Reflexive Peq.
red; unfold Peq; tauto.
Qed.
Lemma Peq_sym: Symmetric Peq.
red; unfold Peq; firstorder.
Qed.
Lemma Peq_trans : Transitive Peq.
red; unfold Peq; intros.
rewrite H; auto.
Qed.
Lemma Peq_incl : forall P Q, Peq P Q -> Pincl P Q.
unfold Pincl, Peq; firstorder.
Save.
Lemma Peq_incl_sym : forall P Q, Peq P Q -> Pincl Q P.
unfold Pincl, Peq; firstorder.
Save.
Lemma Pincl_eq : forall P Q, Pincl P Q -> Pincl Q P -> Peq P Q.
unfold Pincl, Peq; firstorder.
Save.
End Process.
Hint Immediate Peq_incl Peq_incl_sym Pincl_eq Peq_sym.
Hint Resolve Peq_refl Pincl_refl.
Add Parametric Relation {TI TO} : (process TI TO) (@Peq TI TO)
reflexivity proved by (@Peq_refl TI TO)
symmetry proved by (@Peq_sym TI TO)
transitivity proved by (@Peq_trans TI TO)
as Peq_setoid.
Inductive SEQ A B (F:A->B) : process (fsingl A) (fsingl B) :=
SEQ_nil : SEQ F (@nil A) (@nil B)
| SEQ_data :
forall (a : A) (b:B) (li : list A) (lo : list B), b=F a ->
(SEQ F li lo) -> (SEQ F (a::li) (b::lo)).
Hint Constructors SEQ.
Lemma SEQ_map A B (F:A->B) : forall li lo, SEQ F li lo ->
lo = map F li.
induction 1; simpl; auto.
f_equal; trivial.
Save.
Lemma SEQ_eq_incl A B (F G:A->B) : Feq F G -> forall li lo, SEQ F li lo -> SEQ G li lo.
intros Heq; induction 1; auto.
subst b; rewrite (Heq a); auto.
Save.
Add Parametric Morphism A B : (@SEQ A B) with
signature (@Feq A B) ==> (Peq (TI:=fsingl A) (TO:=fsingl B)) as SEQ_eq_morph.
intros F G Heq; split; intros.
apply SEQ_eq_incl with F; auto.
apply SEQ_eq_incl with G; auto.
Save.
Inductive PIPEREL {TI TJ TK} (F:process TI TJ) (G:process TJ TK) li lk : Prop
:= PIPE_trans : forall lj, F li lj -> G lj lk -> PIPEREL F G li lk.
Definition PIPE {TI TJ TK} (F:process TI TJ) (G:process TJ TK) : process TI TK := PIPEREL F G.
Add Parametric Morphism {TI TJ TK} :
(@PIPE TI TJ TK) with signature
(@Pincl TI TJ) ==> (@Pincl TJ TK) ==> (@Pincl TI TK)
as PIPE_monotonic.
intros F1 F2 HF G1 G2 HG.
red; destruct 1.
apply PIPE_trans with lj; auto.
Save.
Hint Resolve PIPE_monotonic.
Add Parametric Morphism {TI TJ TK} : (@PIPE TI TJ TK)
with signature (@Peq TI TJ) ==> (@Peq TJ TK) ==> (@Peq TI TK)
as PIPE_eq_morph.
intros F1 F2 HF G1 G2 HG.
apply Pincl_eq; auto.
Save.
Hint Resolve PIPE_eq_morph.
Binary PAR
Definition PAR {TI TJ TK TL} (F:process TI TJ) (G:process TK TL)
: process (fprod TI TK) (fprod TJ TL)
:= fun lik ljl
=> F (FL_fst lik) (FL_fst ljl) /\ G (FL_snd lik) (FL_snd ljl).
Add Parametric Morphism {TI TJ TK TL}
: (@PAR TI TJ TK TL)
with signature (@Pincl TI TJ) ==> (@Pincl TK TL) ==> (@Pincl (fprod TI TK) (fprod TJ TL))
as PAR_monotonic.
intros F1 F2 HF G1 G2 HG li lo (HP1,HP2); split; auto.
Save.
Hint Resolve PAR_monotonic.
Add Parametric Morphism {TI TJ TK TL}
: (@PAR TI TJ TK TL)
with signature (@Peq TI TJ) ==> (@Peq TK TL) ==> (@Peq (fprod TI TK) (fprod TJ TL))
as PAR_eq_morph.
intros F1 F2 HF G1 G2 HG li lo; unfold Peq.
unfold PAR.
rewrite (HF (FL_fst li) (FL_fst lo)).
rewrite (HG (FL_snd li) (FL_snd lo)); reflexivity.
Save.
Hint Resolve PAR_eq_morph.
Infix "||" := PIPE (left associativity, at level 50) : skel_scope.
Infix "&" := PAR (left associativity, at level 50) : skel_scope.
Open Local Scope skel_scope.
Properties of PIPE
Lemma PIPE_assoc TI TJ TK TL (X:process TI TJ) (Y:process TJ TK) (Z : process TK TL) :
Peq (X || Y || Z) (X || (Y || Z)).
split.
intros (lt1,(lt2,H1,H2), H3).
exists lt2; auto.
exists lt1; auto.
intros (lt1,H,(lt2,H1,H2)).
exists lt2; auto.
exists lt1; auto.
Save.
Lemma PIPE_seq A B C (f:A->B) (g:B->C) : Peq (SEQ f || SEQ g) (SEQ (fun x => g (f x))).
split.
intros (lt,Hf,Hg).
generalize lo Hg; clear lo Hg.
induction Hf; intros.
inversion_clear Hg; auto.
inversion_clear Hg; auto.
intros; apply SEQ_data; subst; auto.
induction 1; simpl; auto.
exists (@nil B); auto.
destruct IHSEQ as (lt,H1,H2).
exists (f a::lt); auto.
Save.
Definition ID TI : process TI TI := fun li lo => li=lo.
Hint Unfold ID.
Lemma PIPE_ID_right {TI TJ} (P:process TI TJ) : Peq (PIPE P (ID TJ)) P.
split.
intros (lt,H1,H2).
destruct H2; auto.
intro; exists lo; auto.
Save.
Lemma PIPE_ID_left {TI TJ} (P:process TI TJ) : Peq (PIPE (ID TI) P) P.
split.
intros (lt,H1,H2).
destruct H1; auto.
intro; exists li; auto.
Save.
Lemma ID_singl : forall A, Peq (SEQ (@id A)) (ID (fsingl A)).
split; unfold ID.
induction 1; simpl; subst; trivial.
intros; subst; trivial.
induction lo; simpl; auto.
Save.
Fixpoint PARDO TI TJ (R:process TI TJ) (n:nat) : process (fdupn TI (S n)) (fdupn TJ (S n)) :=
match n return process (fdupn TI (S n)) (fdupn TJ (S n))
with O => R | (S p) => (PARDO R p) & R end.
Fixpoint PARDO1 A B (R:process (fsingl A) (fsingl B)) (n:nat) : process (fprodn A (S n)) (fprodn B (S n)) :=
match n return process (fprodn A (S n)) (fprodn B (S n))
with O => R | (S p) => R & (PARDO1 R p) end.
Dispatch is introduced as a ternary relation, the flux of indexes can be an input
driving the output channel or can be an output, the choice of the output channel
being non deterministic
A dispatch relation between a value, an index and a family of type (option X)
f2 = f1 i <- x::f1(i)
Fixpoint fadd_disp {X n} (i:nat) (x:X) (f1 f2:fam (FL (fprodn X n))):=
FL_proj i f2 = x:: FL_proj i f1 /\ forall j, i <> j -> FL_proj j f2 = FL_proj j f1.
Inductive DISPREL {n X} : fam (FL (fsingl X)) -> fam (FL (fsingl nat)) -> fam (FL (fprodn X n)) -> Prop :=
DISPREL_nil : DISPREL nil nil Fnil
| DISPREL_add : forall x (lx:list X) i (li:list nat) fl1 fl2,
fadd_disp i x fl1 fl2 -> DISPREL lx li fl1 -> DISPREL (x::lx) (i::li) fl2.
Definition DEMUX n X : process (fcouple X nat) (fprodn X n) :=
fun lxi lf => DISPREL (FL1 lxi) (FL2 lxi) lf.
Implicit Arguments DEMUX [].
Definition DISPATCH n X : process (fsingl X) ((nat:Type)::(fprodn X n)) :=
fun lx lif => DISPREL lx (fhd lif) (ftl lif).
Implicit Arguments DISPATCH [].
Definition MERGE n X : process (fprodn X n) (fcouple X nat) :=
fun lf lxi => DEMUX n X lxi lf.
Implicit Arguments MERGE [].
Definition MUX n X : process ((nat:Type)::(fprodn X n)) (fsingl X) :=
fun lif lx => DISPATCH n X lx lif.
Implicit Arguments MUX [].
Join / Split
Inductive JOINSPLIT {TI:arity} : fam (FL (fsingl (fam TI))) -> fam (FL TI) -> Prop
:= JOINSPLIT_nil : JOINSPLIT nil Fnil
| JOINSPLIT_add : forall p lp lx, JOINSPLIT lp lx -> JOINSPLIT (p::lp) (Fcons p lx).
Hint Constructors JOINSPLIT.
Only true when TI is not nil
Lemma JOINSPLIT_fun1 : forall TI x y (z: fam (FL TI)),
TI<> nil -> JOINSPLIT x z -> JOINSPLIT y z -> x=y.
intros TI x y z HTi H; generalize y; induction H; intros.
inversion H; trivial.
case HTi; apply Fcons_nil with p lx; auto.
inversion H0.
case HTi; apply Fcons_nil with p lx; auto.
destruct (Fcons_inj _ _ _ _ _ H1) as (Hp,Hl).
f_equal; auto.
apply IHJOINSPLIT; auto.
subst lx; auto.
Save.
Lemma JOINSPLIT_fun2 : forall TI x (y z: fam (FL TI)), JOINSPLIT x y -> JOINSPLIT x z -> y=z.
intros TI x y z H; generalize z; induction H; intros.
inversion_clear H; trivial.
inversion_clear H0; f_equal; auto.
Save.
Definition SPLIT (TI:arity) : process (fsingl (fam TI)) TI := @JOINSPLIT TI.
Definition JOIN (TI:arity) : process TI (fsingl (fam TI)) := fun lx lp => JOINSPLIT lp lx.
Hint Unfold JOIN SPLIT.
Lemma JOIN_SPLIT TI : Pincl (JOIN TI || SPLIT TI) (ID TI).
intros li lo (lt,Hj,Hs).
red in Hs; red in Hj.
apply JOINSPLIT_fun2 with lt; auto.
Save.
Lemma SPLIT_JOIN TI : TI<>nil -> Peq (SPLIT TI || JOIN TI) (ID (fsingl (fam TI))).
intro HTI; split.
intros (lt,Hs,Hj).
red in Hs; red in Hj.
apply JOINSPLIT_fun1 with lt; auto.
destruct 1.
simpl in li.
induction li.
exists Fnil; auto.
destruct IHli as (lt,Hs,Hj).
exists (Fcons a lt); auto.
Save.
TI<> nil -> JOINSPLIT x z -> JOINSPLIT y z -> x=y.
intros TI x y z HTi H; generalize y; induction H; intros.
inversion H; trivial.
case HTi; apply Fcons_nil with p lx; auto.
inversion H0.
case HTi; apply Fcons_nil with p lx; auto.
destruct (Fcons_inj _ _ _ _ _ H1) as (Hp,Hl).
f_equal; auto.
apply IHJOINSPLIT; auto.
subst lx; auto.
Save.
Lemma JOINSPLIT_fun2 : forall TI x (y z: fam (FL TI)), JOINSPLIT x y -> JOINSPLIT x z -> y=z.
intros TI x y z H; generalize z; induction H; intros.
inversion_clear H; trivial.
inversion_clear H0; f_equal; auto.
Save.
Definition SPLIT (TI:arity) : process (fsingl (fam TI)) TI := @JOINSPLIT TI.
Definition JOIN (TI:arity) : process TI (fsingl (fam TI)) := fun lx lp => JOINSPLIT lp lx.
Hint Unfold JOIN SPLIT.
Lemma JOIN_SPLIT TI : Pincl (JOIN TI || SPLIT TI) (ID TI).
intros li lo (lt,Hj,Hs).
red in Hs; red in Hj.
apply JOINSPLIT_fun2 with lt; auto.
Save.
Lemma SPLIT_JOIN TI : TI<>nil -> Peq (SPLIT TI || JOIN TI) (ID (fsingl (fam TI))).
intro HTI; split.
intros (lt,Hs,Hj).
red in Hs; red in Hj.
apply JOINSPLIT_fun1 with lt; auto.
destruct 1.
simpl in li.
induction li.
exists Fnil; auto.
destruct IHli as (lt,Hs,Hj).
exists (Fcons a lt); auto.
Save.
Map d : α → β list, c : β → γ, m : γ list → δ
Inductive MAP A B C D (d : A -> list B) (c : B -> C) (m : list C -> D) : process (fsingl A) (fsingl D)
:= MAP_nil : MAP d c m nil nil
| MAP_add : forall (i:A) (li:list A) (o:D)(lo:list D), MAP d c m li lo
-> o=m (List.map c (d i)) -> MAP d c m (i::li) (o::lo).
ToStream and FromStream
Inductive TOSTREAMBUF A B (f: A -> list B) : list B -> process (fsingl A) (fsingl B) :=
TOSTREAMBUF_nil : TOSTREAMBUF f nil nil nil
| TOSTREAMBUF_add : forall (li:list A) b lb (lo:list B),
TOSTREAMBUF f (b::lb) li lo -> TOSTREAMBUF f lb li (b::lo)
| TOSTREAMBUF_input : forall i (li:list A) lb (lo:list B), lb = f i ->
TOSTREAMBUF f nil li lo -> TOSTREAMBUF f lb (i::li) lo.
Definition TOSTREAM A B (f: A -> list B) := TOSTREAMBUF f nil.
Inductive FROMSTREAM A B (f : list B -> option A) : process (fsingl B) (fsingl A) :=
FROMSTREAM_nil : FROMSTREAM f nil nil
| FROMSTREAM_add : forall (l li1 li2:list B) o (lo:list A),
l=li1++li2 -> f li1 = Some o ->
FROMSTREAM f li2 lo -> FROMSTREAM f l (o::lo).
Unordered Farm - an ordered farm behaves like SEQ
Inductive UFARMBUF {TI TJ : arity} n (P : process TI TJ)
: list (fam TJ) -> process TI TJ :=
UFARMBUF_nil : UFARMBUF n P nil Fnil Fnil
| UFARMBUF_push : forall i li b lb lo, List.length lb < n -> P (Fcons i Fnil) (Fcons b Fnil)
-> UFARMBUF n P lb li lo -> UFARMBUF n P (b::lb) (Fcons i li) lo
| UFARMBUF_pull : forall li b lb lb1 lb2 lo, lb = lb1 ++ (b::lb2)
-> UFARMBUF n P (lb1 ++ (b::lb2)) li lo
-> UFARMBUF n P lb li (Fcons b lo).
Definition UFARM {TI TJ : arity} n (P : process TI TJ) := UFARMBUF n P nil.
: list (fam TJ) -> process TI TJ :=
UFARMBUF_nil : UFARMBUF n P nil Fnil Fnil
| UFARMBUF_push : forall i li b lb lo, List.length lb < n -> P (Fcons i Fnil) (Fcons b Fnil)
-> UFARMBUF n P lb li lo -> UFARMBUF n P (b::lb) (Fcons i li) lo
| UFARMBUF_pull : forall li b lb lb1 lb2 lo, lb = lb1 ++ (b::lb2)
-> UFARMBUF n P (lb1 ++ (b::lb2)) li lo
-> UFARMBUF n P lb li (Fcons b lo).
Definition UFARM {TI TJ : arity} n (P : process TI TJ) := UFARMBUF n P nil.