Module ResetLs

Require Import List.
Require Import Cpo SDfuns CommonDS.
Open Scope bool_scope.
Import ListNotations.

An attempt to prove the equivalence between the reset construct of Lucid Synchrone and the one of Denot.SDfuns.

Arguments PROJ {I Di}.
Arguments FST {D1 D2}.
Arguments SND {D1 D2}.
Arguments curry {D1 D2 D3}.

Local Hint Rewrite
  curry_Curry Curry_simpl fcont_comp_simpl fcont_comp2_simpl fcont_comp3_simpl
  FST_simpl Fst_simpl SND_simpl Snd_simpl AP_simpl
  : localdb.

Definition DSForall_pres {A} (P : A -> Prop) : DS (sampl A) -> Prop :=
  DSForall (fun s => match s with pres v => P v | _ => True end).

Definition safe_DS {A} : DS (sampl A) -> Prop :=
  DSForall (fun v => match v with err _ => False | _ => True end).

Definition when : forall {A}, DS (sampl bool) -C-> DS (sampl A) -C-> DS (sampl A) :=
  fun _ => ZIP (fun c x => match c, x with
      | abs, abs => abs
      | pres true, pres v => (pres v)
      | pres false, pres v => abs
      | _, _ => err error_Cl
      end).

Lemma when_eq :
  forall A c cs x xs,
    @when A (cons c cs) (cons x xs) ==
      match c, x with
      | abs, abs => cons abs (when cs xs)
      | pres true, pres v => cons (pres v) (when cs xs)
      | pres false, pres v => cons abs (when cs xs)
      | _, _ => cons (err error_Cl) (when cs xs)
      end.

Proof.

Lemma take_when :
forall A n cs xs,
take n (@when A cs xs) == when (take n cs) (take n xs).

Proof.

Lemma rem_when :
forall A cs (xs:DS (sampl A)),
rem (when cs xs) == when (rem cs) (rem xs).

Proof.

Lemma nrem_when :
forall A n cs (xs:DS (sampl A)),
nrem n (when cs xs) == when (nrem n cs) (nrem n xs).

Proof.

Lemma when_true :
  forall A cs (xs:DS (sampl A)),
    safe_DS cs ->
    safe_DS xs ->
    AC cs == AC xs ->
    DSForall_pres (fun b => b = true) cs ->
    when cs xs == xs.

Proof.

Lemma when_false :
  forall A cs (xs:DS (sampl A)),
    safe_DS cs ->
    safe_DS xs ->
    AC cs == AC xs ->
    DSForall_pres (fun b => b = false) cs ->
    when cs xs == map (fun _ => abs) cs.

Proof.

Lemma safe_when :
  forall A cs (xs:DS (sampl A)),
    safe_DS cs ->
    safe_DS xs ->
    AC cs == AC xs ->
    safe_DS (when cs xs).

Proof.

Definition whennot : forall {A}, DS (sampl bool) -C-> DS (sampl A) -C-> DS (sampl A) :=
  fun _ => ZIP (fun c x => match c, x with
      | abs, abs => abs
      | pres false, pres v => (pres v)
      | pres true, pres v => abs
      | _, _ => err error_Cl
      end).

Lemma whennot_eq :
  forall A c cs x xs,
    @whennot A (cons c cs) (cons x xs) ==
      match c, x with
      | abs, abs => cons abs (whennot cs xs)
      | pres false, pres v => cons (pres v) (whennot cs xs)
      | pres true, pres v => cons abs (whennot cs xs)
      | _, _ => cons (err error_Cl) (whennot cs xs)
      end.

Proof.

Lemma whennot_false :
  forall A cs (xs:DS (sampl A)),
    safe_DS cs ->
    safe_DS xs ->
    AC cs == AC xs ->
    DSForall_pres (fun b => b = false) cs ->
    whennot cs xs == xs.

Proof.

Arrow operator initialized by a constant

Definition arrow {A} (a : A) : DS (sampl A) -C-> DS (sampl A).
  refine (FIXP _ (DSCASE _ _ @_ _)).
  apply ford_fcont_shift; intros [| v | e].
  -
    refine (curry (CONS abs @_ uncurry (AP _ _))).
  -
    apply CTE, (CONS (pres a)).
  -
    apply CTE, (CONS (err e)).
Defined.

Lemma arrow_eq :
  forall A (a : A) x xs,
    arrow a (cons x xs) ==
      match x with
      | abs => cons abs (arrow a xs)
      | pres _ => cons (pres a) xs
      | err e => cons (err e) xs
      end.

Proof.

Lemma arrow_bot : forall A (a:A), arrow a 0 == 0.

Proof.

A special merge operator that produces an abs as soon as an abs is read on the condition stream. Trying to read on both arguments when expecting absences could lead to causality issues in the recursive definition of reset.

Section MERGE.

Definition expecta : forall {A}, DS (sampl A) -C-> DS (sampl A) :=
  fun _ => DSCASE _ _ (fun v => match v with
                | abs => ID _
                | pres _ => MAP (fun _ => err error_Cl)
                | err e => MAP (fun _ => err e)
                    end).

Lemma expecta_eq :
  forall A c cs,
    @expecta A (cons c cs) ==
      match c with
      | abs => cs
      | pres _ => map (fun _ => err error_Cl) cs
      | err _ => map (fun _ => c) cs
      end.

Proof.

Lemma expecta_bot : forall A, @expecta A 0 == 0.

Proof.

Definition merge {A} : DS (sampl bool) -C-> DS (sampl A) -C-> DS (sampl A) -C-> DS (sampl A).
  refine (FIXP _ _).
  apply curry, curry, curry.
  refine ((DSCASE _ _ @2_ _) (SND @_ FST @_ FST)).
  apply ford_fcont_shift; intro c.
  apply curry.
  match goal with
  | |- _ (_ (Dprod ?pl ?pr) _) =>
      pose (f := FST @_ FST @_ FST @_ (@FST pl pr))
      ; pose (X := SND @_ FST @_ (@FST pl pr))
      ; pose (Y := SND @_ (@FST pl pr))
      ; pose (C' := @SND pl pr)
  end.
  destruct c as [|[]| e].
  -
    refine (CONS abs @_ _).
    refine ((f @4_ ID _) C' (expecta @_ X) (expecta @_ Y)).
  -
    refine ((APP _ @2_ X) _).
    refine ((f @4_ ID _) C' (REM _ @_ X) (expecta @_ Y)).
  -
    refine ((APP _ @2_ Y) _).
    refine ((f @4_ ID _) C' (expecta @_ X) (REM _ @_ Y)).
  -
    refine ((MAP (fun _ => err e) @_ CONS (err e) @_ C')).
Defined.

Lemma merge_eq :
  forall A c cs xs ys,
    @merge A (cons c cs) xs ys ==
      match c with
      | abs => cons abs (merge cs (expecta xs) (expecta ys))
      | pres true => app xs (merge cs (rem xs) (expecta ys))
      | pres false => app ys (merge cs (expecta xs) (rem ys))
      | err e => map (fun _ => err e) (cons c cs)
      end.

Proof.

Global Opaque merge.

Lemma expecta_inf :
  forall A (xs:DS (sampl A)),
    infinite xs ->
    infinite (expecta xs).

Proof.

Lemma merge_false:
  forall A cs (xs:DS (sampl A)),
    safe_DS cs ->
    safe_DS xs ->
    infinite cs ->
    infinite xs ->
    DSForall_pres (fun b => b = false) cs ->
    AC cs == AC xs ->
    merge cs (map (fun _ : sampl bool => abs) cs) xs == xs.

Proof.

Lemma merge_false_merge:
  forall A cs cs2 (xs ys:DS (sampl A)),
    safe_DS cs ->
    safe_DS cs2 ->
    infinite cs ->
    infinite xs ->
    DSForall_pres (fun b => b = false) cs ->
    AC cs == AC cs2 ->
    merge cs (map (fun _ : sampl bool => abs) cs) (merge cs2 xs ys) == merge cs2 xs ys.

Proof.

End MERGE.

Definition and characterisations of true_until

Section TRUE_UNTIL.

Definition true_until : DS (sampl bool) -C-> DS (sampl bool).
  refine (FIXP _ _).
  apply curry.
  refine (arrow true @_ _).
  refine ((sbinop (fun b1 b2 => Some (negb b1 && b2)) @2_ SND) _).
  refine ((fby @2_ sconst true @_ AC @_ SND) _).
  refine ((AP _ _ @2_ FST) SND).
Defined.

Lemma true_until_eq :
  forall r, true_until r ==
         arrow true
           (sbinop (fun b1 b2 => Some (negb b1 && b2)) r
              (fby (sconst true (AC r)) (true_until r))).

Proof.

Lemma true_until_abs :
forall r, true_until (cons abs r) == cons abs (true_until r).

Proof.

Lemma true_until_pres1 :
  forall b r,
    safe_DS r ->
    exists U,
      true_until (cons (pres b) r) == cons (pres true) U
      /\ U == (sbinop (fun b1 b2 => Some (negb b1 && b2)) r
                (fby1 (Some true) (sconst true (AC r)) U)).

Proof.

Lemma cs_spec1 :
  forall cs rs,
    infinite rs ->
    safe_DS rs ->
    cs == sbinop (fun b1 b2 : bool => Some (negb b1 && b2)) rs
            (fby1 (Some false) (sconst true (AC rs)) cs) ->
    cs == map (fun v : sampl bool => match v with
                               | abs => abs
                               | pres _ => pres false
                               | err e => err e
                               end) rs.

Proof.

Lemma cs_spec :
  forall n cs rs,
    infinite rs ->
    safe_DS rs ->
    cs == sbinop (fun b1 b2 : bool => Some (negb b1 && b2)) rs
            (fby1 (Some true) (sconst true (AC rs)) cs) ->
    exists m, (m <= n)%nat
         /\ take m cs == map (fun v => match v with
                                   | pres _ => pres true
                                   | abs => abs
                                   | err e => err e end) (take m rs)
         /\ take (n - m) (nrem m cs) ==
             map (fun v => match v with
                        | pres _ => pres false
                        | abs => abs
                        | err e => err e end) (take (n - m) (nrem m rs)).

Proof.

combining previous lemmas, we get the characterisations of true_until

Lemma take_true_until_spec :
  forall n rs,
    infinite rs ->
    safe_DS rs ->
    exists m,
      (m <= n)%nat
      /\ take m (true_until rs) ==
          map (fun v => match v with
                     | pres _ => pres true
                     | abs => abs
                     | err e => err e end) (take m rs)
      /\ take (n - m) (nrem m (true_until rs)) ==
          map (fun v => match v with
                     | pres _ => pres false
                     | abs => abs
                     | err e => err e end) (take (n - m) (nrem m rs)).

Proof.

Other properties of true_until

Lemma true_until_is_cons :
forall rs, is_cons (true_until rs) -> is_cons rs.

Proof.

Lemma AC_true_until :
  forall rs,
    safe_DS rs ->
    AC rs == AC (true_until rs).

Proof.

Corollary true_until_inf :
  forall rs,
    safe_DS rs ->
    infinite rs ->
    infinite (true_until rs).

Proof.

Lemma safe_true_until :
  forall rs,
    safe_DS rs ->
    safe_DS (true_until rs).

Proof.

End TRUE_UNTIL.

Section RESET.

Definition of the recursive reset operator, using true_until

Context {A : Type}.
Variable (f : DS (sampl A) -C-> DS (sampl A)).

Definition reset : DS (sampl bool) -C-> DS (sampl A) -C-> DS (sampl A).
  refine (FIXP _ _).
  apply curry, curry.
  match goal with
  | |- _ (_ (Dprod ?pl ?pr) _) =>
      pose (freset := FST @_ @FST pl pr)
      ; pose (r := SND @_ @FST pl pr)
      ; pose (x := @SND pl pr)
      ; pose (c := true_until @_ r)
  end.
  refine ((merge @3_ c) _ _).
  -
    refine (f @_ (when @2_ c) x).
  -
    refine ((AP _ _ @3_ freset)
              ((whennot @2_ c) r)
              ((whennot @2_ c) x)).
Defined.

Lemma reset_eq :
  forall r x,
    reset r x ==
      let c := true_until r in
      merge c (f (when c x))
              (reset (whennot c r) (whennot c x)).

Proof.

End RESET.

simplified version of the denotational sreset (no environnements)

Section SRESET.

Parameter sreset' : forall {A}, (DS A -C-> DS A) -C-> DS bool -C-> DS A -C-> DS A -C-> DS A.
Conjecture sreset'_eq : forall A f r R X Y,
    @sreset' A f (cons r R) X Y ==
      if r
      then sreset' f (cons false R) X (f X)
      else app Y (sreset' f R (rem X) (rem Y)).

Definition sreset {A} : (DS A -C-> DS A) -C-> DS bool -C-> DS A -C-> DS A.
  apply curry, curry.
  match goal with
  | |- _ (_ (Dprod ?pl ?pr) _) =>
      pose (f := FST @_ (@FST pl pr));
      pose (R := SND @_ (@FST pl pr));
      pose (X := @SND pl pr);
      idtac
  end.
  exact ((sreset' @4_ f) R X ((AP _ _ @2_ f) X)).
Defined.

Lemma sreset_eq : forall A f R X,
    @sreset A f R X == sreset' f R X (f X).

Proof.

End SRESET.

Module RESET_OK.

Parameter (A : Type).
Parameter (f : DS (sampl A) -C-> DS (sampl A)).

Conjecture AbsF : forall xs, f (cons abs xs) == cons abs (f xs).

Corollary AbsConstF : f (DS_const abs) == DS_const abs.

Proof.

Conjecture LpF : forall xs n, f (take n xs) == take n (f xs).

Conjecture SafeF : forall xs, safe_DS xs -> safe_DS (f xs).

we only consider functions of clock α → α

Conjecture AcF : forall xs, AC xs == AC (f xs).

Corollary InfF : forall xs, infinite xs -> infinite (f xs).

Proof.

Corollary AlignF :
  forall n xs,
    safe_DS xs ->
    first (nrem n xs) == cons abs 0 ->
    first (nrem n (f xs)) == cons abs 0.

Proof.

Corollary AlignF_take :
  forall xs n m,
    safe_DS xs ->
    take m (nrem n xs) == take m (DS_const abs) ->
    take m (nrem n (f xs)) == take m (DS_const abs).

Proof.

Lemma f_cons_elim :
  forall x xs,
  exists y ys',
    f (cons (pres x) xs) == cons (pres y) ys'.

Proof.

Lemma reset_abs :
forall r x,
reset f (cons abs r) (cons abs x) == cons abs (reset f r x).

Proof.

Key lemma to prove the equivalence of resets

Lemma f_when :
  forall rs xs,
    infinite rs ->
    infinite xs ->
    safe_DS rs ->
    safe_DS xs ->
    AC xs == AC rs ->
    f (when (true_until rs) xs) == when (true_until rs) (f xs).

Proof.

Definition bool_of : sampl bool -> bool :=
  fun v => match v with pres true => true | _ => false end.

Lemma sreset_match_aux :
  forall rs xs cs ys,
    infinite rs ->
    infinite xs ->
    infinite ys ->
    safe_DS rs ->
    safe_DS xs ->
    safe_DS ys ->
    AC xs == AC rs ->
    AC xs == AC ys ->
    cs == sbinop (fun b1 b2 : bool => Some (negb b1 && b2)) rs
            (fby1 (Some true) (sconst true (AC rs)) cs) ->
    merge cs (when cs ys) (reset f (whennot cs rs) (whennot cs xs))
    == sreset' f (map bool_of rs) xs ys.

Proof.

Theorem reset_match :
  forall rs xs,
    infinite rs ->
    infinite xs ->
    safe_DS rs ->
    safe_DS xs ->
    AC xs == AC rs ->
    let rsb := map bool_of rs in
    reset f rs xs == sreset f rsb xs.

Proof.

End RESET_OK.