semantics.tower.ex_streams

Require Import base ord data.fintype.
Require Import tower.tarski tower.tower tower.direct_induction tower.cocontinuous_tower.

Section Streams.
Variable A : Type.

Definition SA := nat -> A.

Definition ε (R : Rel SA) : Rel SA :=
  fun f g => f 0 = g 0 /\ R (S >> f) (S >> g).

Global Instance ε_mono :
  monotone ε.
Proof.
  move=> R S le_R_S f g [h t]. split=> //. exact: le_R_S.
Qed.

Definition bisim : Rel SA := gfp ε.

Lemma bisim_def :
  bisim = (fun f g => exists2 R : Rel SA, R f g & (R ≤ ε R)).
Proof.
  fext=> f g. rewrite/bisim gfp_def. rewrite !prod_exE prop_exE /supguard/=.
  apply: pext. case=> R H. rewrite !prod_exE prop_exE in H. case: H; by exists R.
  case=> R rfg rbsim. exists R. rewrite !prod_exE prop_exE. by exists rbsim.
Qed.

Lemma bisim_eq :
  bisim = eq.
Proof.
  rewrite bisim_def. apply: le_eq; hnf=>/=f; hnf=>/=g; hnf=>H.
  - case: H => R rfg rbsim. fext=>n. elim: n f g rfg.
    + move=> f g rfg. by case: (rbsim f g rfg).
    + move=> n ih f g rfg. case: (rbsim f g rfg) => _ H. exact: ih H.
  - exists eq => // f' g' ->. by split.
Qed.

Local Notation rbisim R := (t ε R).

Lemma rbisim_refl R f : rbisim R f f.
Proof.
  apply: (@t_monotone _ ε ⊥) => //. by rewrite t_gfp -/bisim bisim_eq.
Qed.

Lemma rbisim_equivalence R :
  Equivalence (rbisim R).
Proof.
  move: R. apply tower_induction.
  - move=> I F ih. constructor. move=> x i. reflexivity.
    move=> x y rxy i. symmetry. exact: rxy.
    move=> x y z rxy ryz i. transitivity y. exact: rxy. exact: ryz.
  - move=> /= R equ. constructor.
    + move=> x. split=> //. reflexivity.
    + move=> x y [rxy0 rxyS]. split; by symmetry.
    + move=> x y z [rxy0 rxyS] [ryz0 ryzS]. split; etransitivity; by eauto.
Qed.

Inductive ctx_operator (c : SA -> SA) (R : Rel SA) : Rel SA :=
| CtxOperator f g : R f g -> ctx_operator c R (c f) (c g).

Lemma upto_context (c : SA -> SA) :
  (forall R,
      (forall f g, rbisim R f g -> rbisim R (c f) (c g)) ->
      (forall f g, ε (rbisim R) f g -> ε (rbisim R) (c f) (c g))) ->
  (forall R f g, rbisim R f g -> rbisim R (c f) (c g)).
Proof.
  move=> h1. suff/=: forall R, ctx_operator c (rbisim R) ≤ rbisim R.
  move=> /=h2 R f g h3. apply: h2. by constructor. apply: upto_lemma.
  - move=> /= R S le_R_S. hnf=> f. hnf=> g. hnf=> h.
    inversion_clear h. constructor. exact: le_R_S.
  - move=> /= R h2. move=> f. move=> g. move=> h. inversion_clear h.
    apply: h1 => // f' g' h'. apply: h2. by constructor.
Qed.

Definition neq n (f g : SA) :=
  forall m, m < n -> f m = g m.
Definition stream_companion (R : Rel SA) (f g : SA) : Prop :=
  forall n, (R ≤ neq n) -> neq n f g.

Lemma ε_cocontinuous I (F : I -> Rel SA) :
  I -> codirected F -> ∀ i, ε (F i) ≤ ε (inf F).
Proof.
  move=> i0 co. hnf=> f. hnf=> g. rewrite !prod_allE prop_leE prop_allE => H.
  rewrite/ε. split; first by case: (H i0).
  rewrite !prod_allE prop_allE => i. by case: (H i).
Qed.

Lemma stream_companionP R :
  stream_companion R = rbisim R.
Proof.
  rewrite -kleene_t_is_t; last by exact: ε_cocontinuous.
  suff: chain ε = neq by rewrite/kleene_t => ->.
  fext=> n f g. elim: n f g => /=[|n ih] f g.
  - rewrite !prod_topE prop_topE /neq. exact: pext.
  - apply: le_eq.
    + move=> H m lt. case: H => e1. rewrite ih => /(_ _) e2. destruct m => //.
      apply: e2. exact: lt.
    + move=> H. split. exact: H. rewrite ih => m lt. apply: H. exact: lt.
Qed.

End Streams.