HyPre.pred.HyperSim

From HyPre Require Export
  ListExtra
  Tac
  VectorList.

From HyPre Require Export
  MonoidHomomorphism
  Sync.

Import ListNotations.
Import MonoidHomomorphismNotations.
Import VectorListNotations.
Import VecNatNotations.

Section with_k_st.
  Context {k : nat}.
  Context {Input : Type}.
(*  Context `{MM : Monoid}.*)
(*
  Class one_step_hyper_sim
        (i_vec : Vector.t Input k)
        (rel : Vector.t (list State) k -> Prop) (* TODO why is the input not considered here ? *)
        (sem : Input -> list State -> Prop)
        `(Sync : OneStepSynchroniser k) :=
    {
    os_sync_rel : forall a, VecNatO opt_S os_sync (vl_len a) -> rel a;
    os_hsync : forall (a : Vector.t (list State) k),
        rel a
        -> forall (b : Vector.t State k),
          Vector.Forall2 sem i_vec (b :vl: a)
          -> let J := os_sync (vl_len a) in
            rel (repl a (b :vl: a) J);
    }.
*)
  Context {M : Type} {MM : Monoid M} {MML : MonoidLaws MM}.
  Context (hom : M -> Vector.t nat k) {MH : MonoidHomomorphism hom}.

  Class hyper_sim
        (i_vec : Input)
        (rel : M -> Prop) (* TODO why is the input not considered here ? maybe pull the input completely out ? *)
        (hsem : Input -> M -> Prop) sync next (* we could remove the input parameter here,
                                            then hyper_preserve would be an instance of hyper_sim for every input*)
        `(Sync : Synchroniser k sync next) :=
    {
    rel_unit : rel monoid_unit;
    hsync : forall (a : M),
        rel a
        -> reachable (hom a)
        -> hsem i_vec a
        -> forall (b : M),
          hsem i_vec (b +m+ a)
          -> (hom b) = sync (hom a)
          -> rel (b +m+ a);
    }.

  Section with_HS_RS.
    Context `{HS : hyper_sim}.

    Context (constr_M_unit : forall (i : Input), hsem i monoid_unit).
    Context (constr_M_cont : forall (i : Input) (m0 : M), hsem i m0 -> forall (vn : Vector.t nat k),
                  {m1 : M | hsem i (m1 +m+ m0) /\ hom m1 = vn}).
    Context (constr_M_det : forall (i : Input) (a a' : M), hsem i a -> hsem i a' -> hom a = hom a' -> a = a').

    Context (M_plus_eq1 : forall (a1 a2 b1 b2 : M), a2 +m+ a1 = b2 +m+ b1 -> hom a1 = hom b1 -> a1 = b1 /\ a2 = b2).
    Context (M_surj_eq : forall (a : M) v1 v2, hom a = v1 +m+ v2 -> exists a1 a2, hom a1 = v1 /\ hom a2 = v2 /\ a = a1 +m+ a2).
     (* doesn't hold in general on Monoids, contrary example is monhom from nat to bool *)
    Context (M_zero_zero : forall (a : M), hom a = monoid_unit -> a = monoid_unit).

    Lemma constr_M_prefix i a1 a2
      : hsem i (a2 +m+ a1) -> hsem i a1.
    Proof.
      intro H.
      specialize (constr_M_cont i monoid_unit) with (vn:=hom a1) as Q.
      exploit' Q.
      destruct Q as [m1 [Q1 Q2 ] ].
      setoid_rewrite monoid_runit in Q1.
      specialize (constr_M_cont i m1) with (vn:=hom a2) as R.
      exploit' R.
      destruct R as [m2 [R1 R2] ].
      eapply constr_M_det in H;eauto.
      - eapply M_plus_eq1 in H;eauto.
        destruct H.
        subst m1.
        assumption.
      - setoid_rewrite homomorph.
        rewrite Q2,R2.
        reflexivity.
    Qed.

    Lemma reachable_rel
      : forall (a : M) (Hts : hsem i_vec a), VecNatO Nat.add sync (hom a) -> rel a.
    Proof.
      intros a Hts Ha.
      remember (hom a) as n.
      revert dependent a.
      induction Ha;intros.
      - assert (Vector.const 0 k = monoid_unit) by eauto.
        rewrite H in Heqn.
        symmetry in Heqn.
        eapply M_zero_zero in Heqn.
        rewrite Heqn.
        eapply rel_unit.
      - rewrite Heqn in H.
        specialize (M_surj_eq a (sync xt) xt H) as HA.
        destruct HA as [a1 [a2 [Ha1 [Ha2 Q ] ] ] ].
        rewrite <-Ha1, <-Ha2 in H.
        destruct MH.
        setoid_rewrite <-homomorph in H.
        rewrite Q.
        subst xt.
        subst yt.
        assert (hsem i_vec a2) as Hsem.
        {
          eapply constr_M_prefix.
          subst a.
          eauto.
        }
        eapply hsync;eauto.
        subst a.
        assumption.
    Qed.

    Definition hyper_sim_AE_witness (ts : M) H
      := proj1_sig (constr_M_cont i_vec
                                  ts
                                  H
                                  (vn_sub (sync_n_steps (vn_next_postfix (vn_zero k)
                                                                         (hom ts))
                                                        (vn_zero k))
                                          (hom ts))).

    (* This soundness theorem instantiated for hyper_preserve is not enough because it relies on
       a simulated state ts (since simulation is encoded in hsem)
       what I need is another lemma delivering a simulated state.
     *)
    Lemma hyper_sim_AE_explicit
          (ts : M)
          (Hts : hsem i_vec ts)
      : let ts' := hyper_sim_AE_witness ts Hts in rel (ts' +m+ ts) /\ hsem i_vec (ts' +m+ ts).
    Proof.
      intro. subst ts'.
      unfold hyper_sim_AE_witness.
      match goal with |- rel ((_ ?x) +m+ _) /\ _ => remember x as y end.
      specialize (@proj2_sig _ _ y) as Hspec. cbn in Hspec.
      destructH.
      split.
      - eapply reachable_rel;eauto.
        setoid_rewrite homomorph.
        setoid_rewrite Hspec1.
        eapply sync_n_steps_reach_sub_add.
      - assumption.
    Qed.

    Lemma hyper_sim_AE
          (ts : M)
          (Hts : hsem i_vec ts)
      : exists ts', rel (ts' +m+ ts) /\ hsem i_vec (ts' +m+ ts).
    Proof.
      eauto using hyper_sim_AE_explicit.
      Unshelve.
      assumption.
    Qed.

  End with_HS_RS.
End with_k_st.