Module Lp

From Coq Require Import Datatypes List.
Import List.ListNotations.

From Velus Require Import Common.
From Velus Require Import CommonList.
From Velus Require Import CommonTyping.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LTyping Lustre.LOrdered.

From Velus Require Import Lustre.Denot.Cpo.
Require Import CommonDS SDfuns SD CommonList2.


Propriété de commutativité du préfixe


Module Type LP
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Typ : LTYPING Ids Op OpAux Cks Senv Syn)
       (Import Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import Den : SD Ids Op OpAux Cks Senv Syn Lord).


Utilities
Lemma take_np_of_env :
  forall l env n,
    0 < length l ->
    lift (take n) (np_of_env l env) == np_of_env l (take_env n env).
Proof.

Lemma take_env_of_np :
  forall l (np : nprod (length l)) n,
    env_of_np l (lift (take n) np) == take_env n (env_of_np l np).
Proof.

Lemma take_env_of_np_ext :
  forall l n m (np : nprod m) env,
    m = length l ->
    take_env n (env_of_np_ext l np env) == env_of_np_ext l (lift (take n) np) (take_env n env).
Proof.

On montre que chaque opérateur du langage a cette propriété


Lemma take_bss :
  forall l n (env : DS_prod SI),
    l <> [] ->
    bss l (take_env n env) == take n (bss l env).
Proof.

Lemma take_sbools_of :
  forall m (mp : nprod m) n,
    0 < m ->
    take n (sbools_of mp) == sbools_of (lift (take n) mp).
Proof.

Lemma take_sunop :
  forall A B (op : A -> option B),
  forall n xs,
    take n (sunop op xs) == sunop op (take n xs).
Proof.

Lemma take_sbinop :
  forall A B D (op : A -> B-> option D),
  forall n xs ys,
    take n (sbinop op xs ys) == sbinop op (take n xs) (take n ys).
Proof.

pour fby/fby1, c'est compliqué, on le fait en deux temps

Lemma take_fby1_le1 :
  forall A n oa (xs ys : DS (sampl A)),
    fby1 oa (take n xs) (take n ys) <= take n (fby1 oa xs ys).
Proof.

Lemma take_fby1_le2 :
  forall A n oa (xs ys : DS (sampl A)),
    take n (fby1 oa xs ys) <= fby1 oa (take n xs) (take n ys).
Proof.

Lemma take_fby1 :
  forall A n oa (xs ys : DS (sampl A)),
    take n (fby1 oa xs ys) == fby1 oa (take n xs) (take n ys).
Proof.

Lemma take_fby_le1 :
  forall A n (xs ys : DS (sampl A)),
    fby (take n xs) (take n ys) <= take n (fby xs ys).
Proof.

Lemma take_fby_le2 :
  forall A n (xs ys : DS (sampl A)),
    take n (fby xs ys) <= fby (take n xs) (take n ys).
Proof.

Lemma take_fby :
  forall A n (xs ys : DS (sampl A)),
    take n (fby xs ys) == fby (take n xs) (take n ys).
Proof.

Corollary take_lift_fby :
  forall A n m (xs ys : @nprod (DS (sampl A)) m),
    lift (take n) (lift2 fby xs ys)
    == lift2 fby (lift (take n) xs) (lift (take n) ys).
Proof.

Lemma take_swhenv :
  forall b n xs cs,
    take n (swhenv b xs cs) == swhenv b (take n xs) (take n cs).
Proof.

Corollary take_lift_swhenv :
  forall b n m (np : nprod m) cs,
    lift (take n) (llift (swhenv b) np cs)
    == llift (swhenv b) (lift (take n) np) (take n cs).
Proof.

Lemma take_smergev :
  forall l xs np n,
    take n (smergev l xs np) == smergev l (take n xs) (lift (take n) np).
Proof.

Corollary take_lift_smergev :
  forall l xs m (np : @nprod (nprod m) _) n,
    lift_nprod (take n @_ smergev l xs) np
    == lift_nprod (smergev l (take n xs)) (lift (lift (take n)) np).
Proof.

Lemma take_scasev :
  forall l xs np n,
    take n (scasev l xs np)
    == scasev l (take n xs) (lift (take n) np).
Proof.

Corollary take_lift_scasev :
  forall l xs m (np : @nprod (nprod m) _) n,
    lift_nprod (take n @_ scasev l xs) np
    == lift_nprod (scasev l (take n xs)) (lift (lift (take n)) np).
Proof.

Lemma take_scase_defv :
  forall l xs ds np n,
    take n (scase_defv l xs (nprod_cons ds np))
    == scase_defv l (take n xs) (nprod_cons (take n ds) (lift (take n) np)).
Proof.

Corollary take_lift_scase_defv :
  forall l xs m (np : @nprod (nprod m) _) ds n,
    lift (take n) (lift_nprod (scase_defv l xs) (nprod_cons ds np))
    == lift_nprod (scase_defv l (take n xs)) (nprod_cons (lift (take n) ds) (lift (lift (take n)) np)).
Proof.

Lemma take_sreset_aux_le1 :
  forall (f : DS_prod SI -C-> DS_prod SI)
    (Hf : forall n envI, f (take_env n envI) == take_env n (f envI)),
  forall n rs X Y,
    take_env n (sreset_aux f rs X Y)
    <= sreset_aux f (take n rs) (take_env n X) (take_env n Y).
Proof.

Lemma take_sreset_aux_le2 :
  forall (f : DS_prod SI -C-> DS_prod SI)
    (Hf : forall n envI, f (take_env n envI) == take_env n (f envI)),
  forall n rs X Y,
    sreset_aux f (take n rs) (take_env n X) (take_env n Y)
    <= take_env n (sreset_aux f rs X Y).
Proof.

Lemma take_sreset_aux :
  forall (f : DS_prod SI -C-> DS_prod SI)
    (Hf : forall n envI, f (take_env n envI) == take_env n (f envI)),
  forall n rs X Y,
    sreset_aux f (take n rs) (take_env n X) (take_env n Y)
    == take_env n (sreset_aux f rs X Y).
Proof.

Corollary take_sreset :
  forall (f : DS_prod SI -C-> DS_prod SI)
    (Hf : forall n envI, f (take_env n envI) == take_env n (f envI)),
  forall n rs X,
    sreset f (take n rs) (take_env n X)
    == take_env n (sreset f rs X).
Proof.

Lemma sreset_aux_false :
  forall f R (X Y : DS_prod SI),
    R == DS_const false ->
    sreset_aux f R X Y == Y.
Proof.


Raisonnement sur les nœuds


Section LP_node.

  Context {PSyn : list decl -> block -> Prop}.
  Context {Prefs : PS.t}.
  Variables
    (G : @global PSyn Prefs)
    (envG : Dprodi FI).

  Hypothesis Hnode :
    forall f n envI,
      envG f (take_env n envI) == take_env n (envG f envI).

  Lemma take_var :
    forall ins x n envI env,
      denot_var ins (take_env n envI) (take_env n env) x
      == take n (denot_var ins envI env x).
  Proof.

  Lemma lift_IH :
    forall ins es envG envI env n,
      Forall (fun e => denot_exp G ins e envG (take_env n envI) (take_env n env)
                    == lift (take n) (denot_exp G ins e envG envI env)) es ->
      denot_exps G ins es envG (take_env n envI) (take_env n env)
      == lift (take n) (denot_exps G ins es envG envI env).
  Proof.

  Lemma lift_IHs :
    forall ins (ess : list (enumtag * _)) m envG envI env n,
      Forall (fun es =>
                Forall (fun e => denot_exp G ins e envG (take_env n envI) (take_env n env)
                    == lift (take n) (denot_exp G ins e envG envI env)) (snd es)) ess ->
      denot_expss G ins ess m envG (take_env n envI) (take_env n env)
      == lift (lift (take n)) (denot_expss G ins ess m envG envI env).
  Proof.

  Lemma lp_exp :
    forall Γ ins e n envI env,
      ins <> [] ->
      wt_exp G Γ e ->
      wl_exp G e ->
      denot_exp G ins e envG (take_env n envI) (take_env n env)
      == lift (take n) (denot_exp G ins e envG envI env).
  Proof.

  Corollary lp_exps :
    forall Γ ins es n envI env,
      ins <> [] ->
      Forall (wt_exp G Γ) es ->
      Forall (wl_exp G) es ->
      denot_exps G ins es envG (take_env n envI) (take_env n env)
      == lift (take n) (denot_exps G ins es envG envI env).
  Proof.

  Lemma lp_block :
    forall Γ ins blk n envI env acc,
      ins <> [] ->
      wt_block G Γ blk ->
      wl_block G blk ->
      denot_block G ins blk envG (take_env n envI) (take_env n env) (take_env n acc)
      == take_env n (denot_block G ins blk envG envI env acc).
  Proof.

  Lemma lp_node :
    forall n nd envI env,
      wt_node G nd ->
      denot_node G nd envG (take_env n envI) (take_env n env)
      == take_env n (denot_node G nd envG envI env).
  Proof.

End LP_node.


Theorem lp_global :
  forall {PSyn Prefs} (G : @global PSyn Prefs),
    wt_global G ->
    forall f n envI,
      denot_global G f (take_env n envI) == take_env n (denot_global G f envI).
Proof.

End LP.

Module LpFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Typ : LTYPING Ids Op OpAux Cks Senv Syn)
       (Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Den : SD Ids Op OpAux Cks Senv Syn Lord)
<: LP Ids Op OpAux Cks Senv Syn Typ Lord Den.
  Include LP Ids Op OpAux Cks Senv Syn Typ Lord Den.
End LpFun.