Library models.IntSpec

Require Import FunctionalExtensionality.
Require Import Classical.
Require Import coqrel.LogicalRelations.
Require Import coqrel.OptionRel.
Require Import structures.Poset.
Require Import structures.Lattice.
Require Import structures.Effects.
Require Import structures.Monad.
Require Import lattices.Downset.
Require Import lattices.Upset.
Require Import lattices.FCD.
Require Import lattices.LatticeProduct.

Preliminaries

The following Proper instance enables rewriting under binders for infinitary operations like sup and inf.

Instance bigop_eq {I A B} (f : (I → A) → B) :
  Proper (pointwise_relation I eq ==> eq) f.
Proof.
  intros x y Hxy.
  apply functional_extensionality in Hxy.
  congruence.
Qed.



Free interpretation


Module ISpec.

  Ltac depsubst :=
    subst;
    lazymatch goal with
      | H : existT _ ?x _ = existT _ ?x _ |- _ ⇒
        apply inj_pair2 in H; depsubst
      | _ ⇒
        idtac
    end.

  Inductive play {E : esig} {V} :=
    | pret (v : V)
    | pmove {X} (m : E X)
    | pcons {X} (m : E X) (n : X) (s : play).

  Arguments play : clear implicits.

  Inductive pref {E : esig} {V} : relation (play E V) :=
    | pret_ref (v : V) :
        pref (pret v) (pret v)
    | pmove_ref {N} (m : E N) :
        pref (pmove m) (pmove m)
    | pmove_cons_ref {N} (m : E N) (n : N) (s : play E V) :
        pref (pmove m) (pcons m n s)
    | pcons_ref {N} (m : E N) (n : N) (s t : play E V) :
        pref s t → pref (pcons m n s) (pcons m n t).

  Instance pref_preo (E : esig) V :
    PreOrder (@pref E V).
  Proof.
    split.
    - intros p.
      induction p; constructor; auto.
    - intros p1 p2 p3 Hp12. revert p3.
      induction Hp12; inversion 1; depsubst; constructor; auto.
  Qed.

  Instance pref_antisym (E : esig) V :
    Antisymmetric (play E V) eq pref.
  Proof.
    intros p1 p2 Hp12 Hp21.
    induction Hp12; inversion Hp21; depsubst; try congruence.
    - apply IHHp12 in H0. congruence.
  Qed.

  Canonical Structure play_poset E V : poset :=
    {|
      ref := @pref E V;
    |}.


Monad


  Definition t E V :=
    FCD.F (play_poset E V).

  Definition ret {E A} (a : A) : t E A :=
    FCD.emb (pret a).

  Fixpoint pbind {E A B} (f : A → t E B) (p : play E A) : t E B :=
    match p with
      | pret a ⇒ f a
      | pmove m ⇒
        FCD.emb (pmove m)
      | pcons m n q ⇒
        FCD.emb (pmove m) ||
        FCD.ext (fun s ⇒ FCD.emb (pcons m n s)) (pbind f q)
    end.

  Global Instance pbind_mor E A B (f : A → t E B):
    PosetMorphism (pbind f).
  Proof.
    constructor. intros x y Hxy.
    induction Hxy; cbn; try rauto.
    - apply join_ub_l.
    - apply join_lub.
      + apply join_ub_l.
      + apply join_r. rauto.
  Qed.

  Definition bind {E A B} (f : A → t E B) : t E A → t E B :=
    FCD.ext (pbind f).

  Instance bind_mor {E A B} (f : A → t E B) :
    CDL.Morphism (bind f).
  Proof.
    unfold bind. typeclasses eauto.
  Qed.

  Instance bind_mor_params :
    Params (@bind) 1.

  Lemma bind_ret_r {E A B} (a : A) (f : A → t E B) :
    bind f (ret a) = f a.
  Proof.
    intros. unfold bind, ret.
    rewrite FCD.ext_ana.
    reflexivity.
  Qed.

  Lemma pbind_ret_l {E A} :
    pbind (@ret E A) = FCD.emb.
  Proof.
    apply functional_extensionality. intros s.
    induction s; cbn; auto.
    rewrite IHs. rewrite @FCD.ext_ana.
    - apply ref_join. rstep. constructor.
    - constructor. repeat rstep. constructor. auto.
  Qed.

  Lemma bind_ret_l {E A} (x : t E A) :
    bind ret x = x.
  Proof.
    unfold bind. rewrite pbind_ret_l.
    apply FCD.ext_emb.
  Qed.

  Lemma bind_bind {E A B C} (g : B → t E C) (f : A → t E B) (x : t E A) :
    bind g (bind f x) = bind (fun a ⇒ bind g (f a)) x.
  Proof.
  Admitted.

Interaction

The interaction primitive triggers one of the actions from the signature and returns the environment's response.

  Definition int {E ar} (m : E ar) : t E ar :=
    sup k : option ar,
      match k with
        | Some n ⇒ FCD.emb (pcons m n (pret n))
        | None ⇒ FCD.emb (pmove m)
      end.

Morphisms between two effect signatures are substitutions, which give an interaction specification in E for each possible operation in F.

  Definition subst (E F : esig) : cdlattice :=
    pi ar, t E ar ^ F ar.

To apply a substitution f : E → F to an interaction specification in F, we replace each move m by the corresponding interaction as given by f m.

  Fixpoint papply {E F A} (f : subst E F) (s : play F A) : t E A :=
    match s with
      | pret a ⇒ FCD.emb (pret a)
      | pmove m ⇒ bind (fun _ ⇒ bot) (f _ m)
      | pcons m n t ⇒ bind (fun n' ⇒ sup H : n' = n, papply f t) (f _ m)
    end.

  Instance papply_mor {E F A} (f : subst E F) :
    PosetMorphism (@papply E F A f).
  Proof.
    constructor. intros s t Hst.
    induction Hst; cbn in *; try rauto.
    - edestruct (FCD.join_meet_dense (f N m)) as (I & J & c & H). rewrite H.
      rewrite Sup.mor. apply sup_lub. intros i.
      rewrite Sup.mor. apply (sup_at i).
      rewrite Inf.mor. setoid_rewrite Inf.mor.
      apply inf_glb. intros j. apply (inf_at j).
      unfold bind. rewrite !FCD.ext_ana.
      induction (c i j); cbn.
      + apply bot_lb.
      + reflexivity.
      + apply join_lub; [apply join_l | apply join_r]; rauto.
    - edestruct (FCD.join_meet_dense (f N m)) as (I & J & c & H). rewrite H.
      rewrite Sup.mor. apply sup_lub. intros i.
      rewrite Sup.mor. apply (sup_at i).
      rewrite Inf.mor. setoid_rewrite Inf.mor.
      apply inf_glb. intros j. apply (inf_at j).
      unfold bind. rewrite !FCD.ext_ana.
      induction (c i j); cbn.
      + apply sup_lub. intros Hv. apply (sup_at Hv). auto.
      + reflexivity.
      + apply join_lub; [apply join_l | apply join_r]; rauto.
  Qed.

  Definition apply {E F A} (f : subst E F) : t F A → t E A :=
    FCD.ext (papply f).

  Instance apply_mor {E F A} (f : subst E F) :
    CDL.Morphism (@apply E F A f).
  Proof.
    unfold apply.
    typeclasses eauto.
  Qed.

  Instance apply_mor_params :
    Params (@apply) 1.

  Definition compose {E F G} (g : subst F G) (f : subst E F) : subst E G :=
    fun ar m ⇒ apply f (g ar m).

Properties of apply.

  Lemma apply_ret {E F A} (f : subst E F) (a : A) :
    apply f (ret a) = ret a.
  Proof.
    unfold apply, ret. rewrite FCD.ext_ana. cbn. auto.
  Qed.

  Lemma apply_bind {E F A B} (f : subst E F) (g : A → t F B) (x : t F A) :
    apply f (bind g x) = bind (fun a ⇒ apply f (g a)) (apply f x).
  Admitted.

  Lemma apply_int_r {E F ar} (m : F ar) (f : subst E F) :
    apply f (int m) = f ar m.
  Proof.
    unfold apply, int.
    rewrite Sup.mor.
    edestruct (FCD.join_meet_dense (f ar m)) as (I & J & c & H).
    apply antisymmetry.
    - eapply sup_lub. intros i.
      destruct i; rewrite FCD.ext_ana; cbn.
      + rewrite H.
        setoid_rewrite Sup.mor. apply sup_lub. intros i. apply (sup_at i).
        setoid_rewrite Inf.mor. apply inf_glb. intros j. apply (inf_at j).
        unfold bind. rewrite FCD.ext_ana.
        induction (c i j); cbn.
        × apply sup_lub. intro. subst. reflexivity.
        × reflexivity.
        × apply join_lub.
          -- rstep. constructor.
          -- rewrite IHp. rewrite @FCD.ext_ana. reflexivity.
             constructor. repeat rstep. constructor. auto.
      + rewrite H.
        setoid_rewrite Sup.mor. apply sup_lub. intros i. apply (sup_at i).
        setoid_rewrite Inf.mor. apply inf_glb. intros j. apply (inf_at j).
        unfold bind. rewrite FCD.ext_ana.
        induction (c i j); cbn.
        × apply bot_lb.
        × reflexivity.
        × apply join_lub.
          -- rstep. constructor.
          -- rewrite IHp. rewrite @FCD.ext_ana. reflexivity.
             constructor. repeat rstep. constructor. auto.
  Admitted.

  Lemma apply_int_l {E A} (x : t E A) :
    apply (@int E) x = x.
  Proof.
    unfold apply, int. symmetry.
    change x with ((fun x ⇒ x) x) at 1.
    apply FCD.ext_unique.
    - admit.     - intros s.
      induction s; cbn.
      + reflexivity.
      + rewrite Sup.mor. unfold bind.
        apply antisymmetry.
        × apply (sup_at None).
          rewrite FCD.ext_ana. cbn.
          reflexivity.
        × apply sup_lub. intros i.
          destruct i; rewrite FCD.ext_ana; cbn.
          -- apply join_lub.
             ++ reflexivity.
             ++ Transparent bot. unfold bot. rewrite Sup.mor.
                apply sup_lub. intros [ ].
          -- reflexivity.
      +
  Admitted.

  Lemma apply_assoc {E F G A} (f : subst E F) (g : subst F G) (x : t G A) :
    apply f (apply g x) = apply (compose g f) x.
  Proof.
    unfold apply, compose.
    rewrite @FCD.ext_ext by typeclasses eauto.
    f_equal. apply functional_extensionality. intros s.
    induction s; cbn.
    - rewrite FCD.ext_ana. reflexivity.
    - unfold bind, apply. rewrite !@FCD.ext_ext by typeclasses eauto.
      f_equal. apply functional_extensionality. intros s.
      induction s; cbn.
      + rewrite FCD.ext_ana. cbn. admit.
      + rewrite FCD.ext_ana. cbn.
        unfold bind. rewrite @FCD.ext_ext by typeclasses eauto.
        f_equal. apply functional_extensionality. intros s.
        induction s; cbn.
        × admit.         × rewrite FCD.ext_ana. cbn. reflexivity.
        × admit.       + admit.
    - admit.
  Admitted.

Properties of compose

  Lemma compose_int_l {E F} (f : subst E F) :
    compose (@int F) f = f.
  Proof.
    unfold compose.
    apply functional_extensionality_dep; intros ar.
    apply functional_extensionality_dep; intros m.
    apply apply_int_r.
  Qed.

  Lemma compose_int_r {E F} (f : subst E F) :
    compose f (@int E) = f.
  Proof.
    unfold compose.
    apply functional_extensionality_dep; intros ar.
    apply functional_extensionality_dep; intros m.
    apply apply_int_l.
  Qed.

  Lemma compose_assoc {E F G H} (f : subst E F) (g : subst F G) (h : subst G H) :
    compose (compose h g) f = compose h (compose g f).
  Proof.
    unfold compose.
    apply functional_extensionality_dep; intros ar.
    apply functional_extensionality_dep; intros m.
    apply apply_assoc.
  Qed.

End ISpec.

Notation ispec := ISpec.t.