From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Coq Require Import Setoid Morphisms.
From Velus Require Import Common.
From Velus Require Import Operators FunctionalEnvironment.
From Velus Require Import Clocks.
From Velus Require Import CoindStreams IndexedStreams.
From Velus Require Import CoindIndexed.
From Velus Require Import Fresh.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LOrdered Lustre.LClocking Lustre.LSemantics Lustre.LClockedSemantics.
From Velus Require Import Lustre.NormFby.NormFby.
From Velus Require Import Lustre.NormFby.NFClocking.
From Velus Require Import Lustre.SubClock.SCCorrectness.
Module Type NFCORRECTNESS
(
Import Ids :
IDS)
(
Import Op :
OPERATORS)
(
Import OpAux :
OPERATORS_AUX Ids Op)
(
Import Cks :
CLOCKS Ids Op OpAux)
(
Import CStr :
COINDSTREAMS Ids Op OpAux Cks)
(
Import Senv :
STATICENV Ids Op OpAux Cks)
(
Import Syn :
LSYNTAX Ids Op OpAux Cks Senv)
(
Import Cl :
LCLOCKING Ids Op OpAux Cks Senv Syn)
(
Import Ord :
LORDERED Ids Op OpAux Cks Senv Syn)
(
Import Sem :
LSEMANTICS Ids Op OpAux Cks Senv Syn Ord CStr)
(
Import LCS :
LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Cl Ord CStr Sem)
(
Import NF :
NORMFBY Ids Op OpAux Cks Senv Syn).
Import Fresh Tactics NF.
Module Import Clocking :=
NFClockingFun Ids Op OpAux Cks Senv Syn Cl NF.
Module Import SCC :=
SCCorrectnessFun Ids Op OpAux Cks CStr Senv Syn Cl Ord Sem LCS SC.
Import SC.
Section normfby_node_sem.
Variable G1 : @
global normlast last_prefs.
Variable G2 : @
global normalized fby_prefs.
Hypothesis Hiface :
global_iface_incl G1 G2.
Hypothesis HGref :
global_sem_refines G1 G2.
Hypothesis HwcG1 :
wc_global G1.
Manipulation of initialization streams
We want to specify the semantics of the init equations created during the normalization
with idents stored in the env
Definition false_val :=
Venum 0.
Definition true_val :=
Venum 1.
Lemma sfby_const :
forall bs v,
sfby v (
const_val bs v) ≡ (
const_val bs v).
Proof.
cofix CoFix.
intros [
b bs]
v.
rewrite const_val_Cons.
destruct b;
rewrite sfby_Cons;
constructor;
simpl;
auto.
Qed.
Lemma case_false :
forall bs xs ys,
aligned xs bs ->
aligned ys bs ->
case (
const_val bs false_val) [(1,
ys); (0,
xs)]
None xs.
Proof.
cofix CoFix.
intros [
b bs]
xs ys Hsync1 Hsync2.
rewrite const_val_Cons.
unfold false_val.
inv Hsync1;
inv Hsync2;
econstructor;
simpl;
eauto.
+
repeat constructor;
simpl;
congruence.
Qed.
Lemma sfby_fby1 :
forall bs v y ys,
aligned ys bs ->
fby1 y (
const_val bs v)
ys (
sfby y ys).
Proof with
eauto.
cofix sfby_fby1.
intros [
b bs]
v y ys Hsync.
specialize (
sfby_fby1 bs).
inv Hsync;
rewrite const_val_Cons;
rewrite unfold_Stream;
simpl.
-
constructor...
-
constructor...
Qed.
Lemma sfby_fby1' :
forall y y0s ys zs,
fby1 y y0s ys zs ->
zs ≡ (
sfby y ys).
Proof.
cofix CoFix.
intros y y0s ys zs Hfby1.
inv Hfby1; constructor; simpl; eauto.
Qed.
Lemma sfby_fby :
forall b v y,
aligned y b ->
fby (
const_val b v)
y (
sfby v y).
Proof with
eauto.
cofix sfby_fby.
intros [
b bs]
v y Hsync.
rewrite const_val_Cons.
rewrite unfold_Stream;
simpl.
destruct b;
simpl;
inv Hsync.
-
econstructor.
eapply sfby_fby1...
-
econstructor;
simpl...
Qed.
Definition init_stream bs :=
sfby true_val (
enum bs 0).
Global Instance init_stream_Proper:
Proper (@
EqSt bool ==> @
EqSt svalue)
init_stream.
Proof.
intros bs bs'
Heq1.
unfold init_stream.
rewrite Heq1.
reflexivity.
Qed.
Lemma fby_case :
forall bs v y0s ys zs,
(
aligned y0s bs \/
aligned ys bs \/
aligned zs bs) ->
fby y0s ys zs ->
case (
sfby true_val (
const_val bs false_val)) [(1,
y0s);(0,
sfby v ys)]
None zs.
Proof with
eauto.
cofix CoFix.
intros [
b bs]
v y0s ys zs Hsync Hfby1.
apply fby_aligned in Hsync as [
Hsync1 [
Hsync2 Hsync3]]; [|
auto].
destruct b;
inv Hsync1;
inv Hsync2;
inv Hsync3.
-
repeat rewrite const_val_Cons.
inv Hfby1.
repeat rewrite sfby_Cons.
econstructor;
simpl.
+
rewrite sfby_const.
assert (
vs1 ≡
sfby v1 vs0)
as Heq by (
eapply sfby_fby1';
eauto).
rewrite Heq.
apply case_false...
rewrite <-
Heq;
auto.
+
repeat constructor;
simpl;
auto;
congruence.
+
constructor.
+
repeat constructor.
-
rewrite const_val_Cons.
repeat rewrite sfby_Cons.
inv Hfby1.
constructor;
auto.
eapply CoFix;
eauto.
simpl;
auto.
Qed.
Corollary fby_init_stream_case :
forall bs v y0s ys zs,
(
aligned y0s bs \/
aligned ys bs \/
aligned zs bs) ->
fby y0s ys zs ->
case (
init_stream bs) [(1,
y0s); (0,
sfby v ys)]
None zs.
intros *
Hsync Hfby1.
eapply fby_case in Hfby1;
eauto.
unfold init_stream.
rewrite const_val_enum;
eauto.
Qed.