StreamCalculus.sde

Require Import StreamCalculus.streamscommon.
Require Import StreamCalculus.stream_equality_up_to.
Require Import StreamCalculus.stream_equality.
Require Import StreamCalculus.stream_equalities.
Set Implicit Arguments.
Require Import MathClasses.interfaces.abstract_algebra.
Require Import Omega.

Section Causality.
  Variable (T: Type).
  Context `{E: Equiv T}.

  Definition causal_head X (h:(X -> T) -> T):=forall i1 i2,(forall x, i1 x=i2 x) -> h i1=h i2.
  Definition causal2 X (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) :=
        forall a1 a2 i1 i2 n,
        (forall t1 t2, (forall x, StreamEqualUpTo n (t1 x) (t2 x)) -> StreamEqualUpTo n (a1 t1) (a2 t2)) ->
        (forall x, StreamEqualUpTo (S n) (i1 x) (i2 x)) ->
        StreamEqualUpTo n (t i1 a1) (t i2 a2).
End Causality.

Section Corecursion.
  Variable (T: Type).
  Context `{E: Setoid T}.
  Variable (X: Type).

  Fixpoint corec_up_to h (ct: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) nh x:Stream T:=
        fun n => match (nh,n) with
                 | (0, _) => h (fun x' => x x' 0%nat)
                 | (_, 0) => h (fun x' => x x' 0%nat)
                 | (S nh', S n') => ct x (corec_up_to h ct nh') n'
                 end.

  Definition corec h t x n:=corec_up_to h t n x n.

  Lemma corec_head h t x:
    (corec h t x) 0%nat = h (fun x'=>x x' 0%nat).
  Proof.
    now cbn.
  Qed.

  Lemma corec_step_rewrite t h n' x n:
    t x (λ x1, λ n0 : nat,
             match n0 with
             | 0 => h (fun x'=>x1 x' 0%nat)
             | S n'0 => t x1 (corec_up_to h t n) n'0
             end) n'
    ≡ (t x (corec_up_to h t (S n)) n').
  Proof.
    now cbn.
  Qed.
End Corecursion.

Section UniqueSolutionSDE.
  Variable (T: Type).
  Context `{E: Setoid T}.
  Variable X:Type.

  Lemma causality_inheritance h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) n x1 x2:
      causal_head h ->
      causal2 t ->
      (forall x, StreamEqualUpTo (S n) (x1 x) (x2 x)) ->
      StreamEqualUpTo (S n) (corec_up_to h t n x1) (corec_up_to h t n x2).
  Proof.
    revert x1 x2.
    induction n; intros; constructor.
    - constructor. (* trivial up to 0 *)
    - cbn. (* head equal *)
      apply H.
      intros.
      now apply (eqUpTo_inverse_head (n:=0%nat)).
    - unfold derive. (* tail equal up to n *)
      cbn.
      apply H0; trivial.
      intros.
      now apply IHn.
    - cbn. (* heads equal *)
      apply H.
      intros.
      now apply (eqUpTo_inverse_head (n:=S n)). (* TODO Auto *)
  Qed.

  Lemma pre_sfc_tail_step n h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) x:
      causal_head h ->
      causal2 t ->
      StreamEqualUpTo (S n) (corec_up_to h t n x) (corec_up_to h t (S n) x).
  Proof.
    revert x.
    induction n;
    intros x causality_head causality_tail;
    apply eqUpTo_lePointwise;
    destruct n';
    intros; cbn; try easy.
    + cbv in H. omega.
    + rewrite corec_step_rewrite.
      apply (eqUpTo_lePointwise (S n)).
      * apply causality_tail.
        - intros.
          rewrite causality_inheritance; trivial.
          now apply IHn.
        - reflexivity.
      * cbv in H. cbv. omega.
   Qed.

  Lemma corec_up_to_convergates m n h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) x:
      causal_head h ->
      causal2 t ->
      m >=n ->
      corec_up_to h t n x n = corec_up_to h t m x n.
  Proof.
    intros causality_head causality_tail.
    induction 1.
    - reflexivity.
    - rewrite IHle.
      intros.
      apply (eqUpTo_lePointwise (S m)).
      now apply pre_sfc_tail_step.
      cbv. cbv in H. omega.
  Qed.

  Lemma corec_up_to_tail n h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) x:
    causal_head h ->
    causal2 t ->
    derive (corec_up_to h t (S n) x) ≡ t x (corec_up_to h t n).
  Proof.
    now cbn.
  Qed.

  Lemma corec_up_to_eq_upton h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) x n0:
    causal_head h ->
    causal2 t ->
    StreamEqualUpTo (S n0) (corec_up_to h t n0 x) (corec h t x).
  Proof.
    intros ch ct.
    apply eqUpTo_lePointwise.
    intros.
    assert (n' <= n0). { cbv. cbv in H. omega. }
    now rewrite (corec_up_to_convergates x ch ct H0).
  Qed.

  Lemma corec_tail_up_to n h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) x:
    causal_head h ->
    causal2 t ->
    StreamEqualUpTo n (derive (corec h t x)) (t x (corec h t)).
  Proof.
    intros ch ct.
    apply eqUpTo_lePointwise.
    cbn.
    intros.
    apply (eqUpTo_lePointwise (S n')).
    - apply ct.
      + intros.
        rewrite causality_inheritance; trivial.
        now apply corec_up_to_eq_upton.
      + reflexivity.
    - cbv. cbv in H. omega.
  Qed.

  Lemma corec_tail h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) x:
    causal_head h ->
    causal2 t ->
    derive (corec h t x) = t x (corec h t).
  Proof.
    intros ch ct.
    apply streamEqualUpTo_streamEquality.
    intros.
    now apply corec_tail_up_to.
  Qed.

  Lemma corec_causal h (t: (X -> Stream T) -> ((X -> Stream T) -> Stream T) -> Stream T) i1 i2 n:
    (forall x, StreamEqualUpTo n (i1 x) (i2 x)) ->
    causal_head h ->
    causal2 t ->
    StreamEqualUpTo n (corec h t i1) (corec h t i2).
  Proof.
    revert i1 i2.
    induction n; constructor.
    - repeat rewrite corec_tail_up_to; trivial.
      apply H1; trivial.
      intros.
      apply IHn; trivial.
    - cbn.
      apply H0.
      intros. now apply (eqUpTo_inverse_head (n:=n)).
  Qed.
End UniqueSolutionSDE.