HyPre.pred.HyperPreserve

(* CLN C *)
From Coq Require Import
  Program.Equality.

From HyPre Require Export
  ListExtra
  Safety
  Tac
  VectorPair.

From HyPre Require Export
  HyperSim
  HyperSemantics.

Import Veclist Safety.

Import ListNotations.
Import VectorListNotations.

Section with_k_st.
  Context {k : nat}.
  Context {Input SrcSt TgtSt : Type}.

  (* MAYDO : generalise this,
     such that we could use any suitable inductive type as "traces", in particular trees
     maybe this is also the way to support itrees natively
   *)

  (* Is the use of Type-universe sync & tsync making this definition unnecessary strict?
     An alternative could be to have relations between traces (src/tgt, src/src, tgt/tgt)
     and assumptions a la if related we're eventually related again.
     Though to prove them these assumptions you're likely to need an expclicit construction anyway.
   *)
  (* (t_synci : Vector.t (nat -> nat) k) instead of TSi not a good approach bc. Forall_i2 difficult to state & work with *)
  Class hyper_preserve
        (i_vec : Vector.t Input k)
        (src_rel : Vector.t (list SrcSt) k -> Prop)
        (tgt_rel : Vector.t (list TgtSt) k -> Prop)
        (src_sem : Input -> list SrcSt -> Prop)
        (tgt_sem : Input -> list TgtSt -> Prop)
        (t_sync_i : Input -> nat -> nat)
        (t_next_i : Input -> nat -> nat)
        (TSi : forall i, TotalSynchroniser (t_sync_i i) (t_next_i i))
        `(Sync : Synchroniser k) :=
    {
    src_rel_unit : src_rel vl_zero;
    tgt_rel_unit : tgt_rel vl_zero;
    sim := fun (i : Input) a α
           => @t_reachable _ _ (TSi i) (a,α);
    hp_step :
      forall (a : Vector.t (list SrcSt) k),
        src_rel a
        -> reachable (vl_len a)
        -> forall (α : Vector.t (list TgtSt) k),
            tgt_rel α
            -> Vec_Forall3 sim i_vec (vl_len a) (vl_len α) (* there is no vec_foralli2 *)
            -> forall (b : Vector.t (list SrcSt) k),
                Vector.Forall2 src_sem i_vec (b +vl+ a)
                -> forall (β : Vector.t (list TgtSt) k),
                  Vector.Forall2 tgt_sem i_vec (β +vl+ α)
                  -> Vec_Forall3 sim i_vec (vl_len (b +vl+ a)) (vl_len (β +vl+ α))
                  -> vl_len b = sync (vl_len a)
                  -> src_rel (b +vl+ a)
                    /\ tgt_rel (β +vl+ α);
    }.
  (* There ought to be a lemma that guarantees the selection of consistent simulation steps *)

  (*
  Class hyper_preserve
        (i_vec : Vector.t Input k)
        (src_rel : Vector.t (list SrcSt) k -> Prop)
        (tgt_rel : Vector.t (list TgtSt) k -> Prop)
        (*sim : list SrcSt -> list TgtSt -> Prop*)
        (src_sem : Input -> list SrcSt -> Prop)
        (tgt_sem : Input -> list TgtSt -> Prop)
        (* (t_synci : Vector.t (nat -> nat) k) not a good approach bc. Forall_i2 difficult to state & work with *)
        (TSi : Vector.t { tsn : (nat -> nat) * (nat -> nat) | TotalSynchroniser (fst tsn) (snd tsn)} k)
        (* the reason for this vector notation was that I thought it is a weaker requirement,
           since you only need k TotalSyncs, instead of one per possible Input.
           But that does actually not make the requirement weaker, since you can just repeat your k TotalSyncs.
           (except for k=0, but who cares about that case)
           Thus this approach is deprecated.
         *)
        `(Sync : Synchroniser k) :=
    {
    src_rel_unit : src_rel vl_zero;
    tgt_rel_unit : tgt_rel vl_zero;
    (*    sim_unit : sim  ;*)
    sim := fun (TS : { tsn : (nat -> nat) * (nat -> nat) | TotalSynchroniser (fst tsn) (snd tsn)}) a α
           => @t_reachable _ _ (proj2_sig TS) (a,α);
    hp_step :
      forall (a : Vector.t (list SrcSt) k),
        src_rel a
        -> reachable (vl_len a)
        -> forall (α : Vector.t (list TgtSt) k),
            tgt_rel α
            -> Vec_Forall3 sim TSi (vl_len a) (vl_len α) (* there is no vec_foralli2 *)
            -> forall (b : Vector.t (list SrcSt) k),
                Vector.Forall2 src_sem i_vec (b +vl+ a)
                -> forall (β : Vector.t (list TgtSt) k),
                  Vector.Forall2 tgt_sem i_vec (β +vl+ α)
                  -> Vec_Forall3 sim TSi (vl_len (b +vl+ a)) (vl_len (β +vl+ α))
                  -> vl_len b = sync (vl_len a)
                  -> src_rel (b +vl+ a)
                    /\ tgt_rel (β +vl+ α);
    }.
   *)

  Section with_hyper_preserve.
    Context `(HP : hyper_preserve).

    (* i need a generalisation of synchroniser, s.t. I can argue on vectors of pairs
       this IS necessary since src & tgt may have different types

       I can't just say k-hyper-preserve is an instance of 2k-hyper-sim,
       instead: k-hyper-preserve is an instance of k-hyper-sim, where the traces are replaced by pairs of traces.
     *)

    Notation composite_sem
      := (fun (iv : Vector.t Input k) (v : Vector.t (list SrcSt * list TgtSt) k) =>
            let a := Vector.map fst v in
            let α := Vector.map snd v in
            Vector.Forall2 src_sem iv a
            /\ Vector.Forall2 tgt_sem iv α
         (*/\ Vec_Forall3 sim iv a α*)).
    (*
    Notation t_synci' := (Vector.nth (Vector.map t_synci i_vec)).
    Notation t_nexti' := (Vector.nth (Vector.map t_nexti i_vec)).

    Program Instance tot_sync : forall i : Fin.t k, TotalSynchroniser (t_synci' i) (t_nexti' i).
     *)

    Instance tot_sync : forall i : Fin.t k, TotalSynchroniser (t_sync_i (i_vec[[i]])) (t_next_i (i_vec[[i]])).
    Proof.
      intros.
      eapply TSi.
    Qed.

    Lemma vec_map_map2_fst_eq_map2_map_fst {X1 X2 Y1 Y2 Z1 Z2 : Type} (g1 : X1 -> Y1 -> Z1) (g2 : X2 -> Y2 -> Z2)
          (xt : Vector.t (X1 * X2) k) (yt : Vector.t (Y1 * Y2) k)
      : Vector.map fst
                   (Vector.map2
                      (fun (x : X1*X2) (y : Y1*Y2) => let (x1,x2) := x in let (y1,y2) := y in (g1 x1 y1, g2 x2 y2)) xt yt)
        = Vector.map2 g1 (Vector.map fst xt) (Vector.map fst yt).
    Proof.
      rewrite vec_map_map2.
      setoid_rewrite vec_map2_ext with (g:=fun x y => g1 (fst x) (fst y)).
      2: intros;destruct x,y; cbn; reflexivity.
      rewrite vec_map2_fun_app.
      reflexivity.
    Qed.

    Lemma vec_map_map2_snd_eq_map2_map_snd {X1 X2 Y1 Y2 Z1 Z2 : Type} (g1 : X1 -> Y1 -> Z1) (g2 : X2 -> Y2 -> Z2)
          (xt : Vector.t (X1 * X2) k) (yt : Vector.t (Y1 * Y2) k)
      : Vector.map snd
                   (Vector.map2
                      (fun (x : X1*X2) (y : Y1*Y2) => let (x1,x2) := x in let (y1,y2) := y in (g1 x1 y1, g2 x2 y2)) xt yt)
        = Vector.map2 g2 (Vector.map snd xt) (Vector.map snd yt).
    Proof.
      rewrite vec_map_map2.
      setoid_rewrite vec_map2_ext with (g:=fun x y => g2 (snd x) (snd y)).
      2: intros;destruct x,y; cbn; reflexivity.
      rewrite vec_map2_fun_app.
      reflexivity.
    Qed.

    Program Instance hyper_preserve_hyper_sim
      : hyper_sim vpl_len_kk
                  i_vec
                  (fun v => let a := Vector.map fst v in
                         let α := Vector.map snd v in
                         src_rel a /\ tgt_rel α
                  )
                  composite_sem (*
                  (fun iv v => let a := Vector.map fst v in
                            let α := Vector.map snd v in
                            Vector.Forall2 src_sem iv a
                            /\ Vector.Forall2 tgt_sem iv α
                            /\ Vector.Forall2 sim a α
                  )*)
                  merge_sync
                  merge_next
                  us_sync_sync_sync.
    Next Obligation.
      split.
      - rewrite vec_map_const. cbn. eapply src_rel_unit.
      - rewrite vec_map_const. cbn. eapply tgt_rel_unit.
    Qed.
    Next Obligation.
      setoid_rewrite vec_map_map2_fst_eq_map2_map_fst.
      setoid_rewrite vec_map_map2_snd_eq_map2_map_snd.
      eapply hp_step;eauto.
      - rewrite <-vpl_len_kk_fst_vec.
        eapply merge_reach.
        assumption.
      - rewrite <-vpl_len_kk_fst_vec.
        rewrite <-vpl_len_kk_snd_vec.
        eapply vec_forall3_forall.
        intros. unfold sim.
        eapply merge_t_reach in H0.
        cbn in H0.
        eapply H0.
      - setoid_rewrite <-vec_map_map2_fst_eq_map2_map_fst. eassumption.
      - setoid_rewrite <-vec_map_map2_snd_eq_map2_map_snd. eassumption.
      - Import VecNatNotations.
        assert (reachable (vpl_len_kk b +vn+ vpl_len_kk a)) as Hreach.
        {
          econstructor. eauto.
          rewrite H3.
          reflexivity.
        }
        eapply vec_forall3_forall.
        intros. unfold sim.
        eapply merge_t_reach in Hreach.
        cbn in Hreach.
        setoid_rewrite vl_len_vl_app_vn_add.
        setoid_rewrite <-vpl_len_kk_fst_vec.
        setoid_rewrite <-vpl_len_kk_snd_vec.
        setoid_rewrite <-fst_vec_map2.
        setoid_rewrite <-snd_vec_map2.
        eapply Hreach.
      - eapply f_equal with (f:=fst_vec) in H3.
        rewrite vpl_len_kk_fst_vec in H3.
        rewrite merge_sync_fst_vec_eq in H3.
        rewrite vpl_len_kk_fst_vec in H3.
        assumption.
    Qed.

    (* MOVE VectorPair { *)
    (* TODO Prove VectorPair lemmas *)
    (* }*)

    (* MOVE MonoidHomomorphism { *)

    Instance fst_hom {X Y : Type} {XM : Monoid X} {YM : Monoid Y}
      : MonoidHomomorphism (@fst X Y).
    Proof.
      econstructor.
      - intros.
        destruct m1 as [x1 y1]. destruct m2 as [x2 y2].
        cbn.
        reflexivity.
      - cbn.
        reflexivity.
    Qed.

    Instance snd_hom {X Y : Type} {XM : Monoid X} {YM : Monoid Y}
      : MonoidHomomorphism (@snd X Y).
    Proof.
      econstructor.
      - intros.
        destruct m1 as [x1 y1]. destruct m2 as [x2 y2].
        cbn.
        reflexivity.
      - cbn.
        reflexivity.
    Qed.
    (*}*)

    Section with_live.
      Context (Rsrc : rad_semantics src_sem).
      Context (Rtgt : rad_semantics tgt_sem).

      Lemma composite_sem_unit i
        : composite_sem i monoid_unit.
      Proof.
        split.
        1,2: rewrite homomorph_unit.
        1,2: eapply Vec_Forall2_forall2;cbn.
        1,2: setoid_rewrite Vector.const_nth;intros.
        1,2: eapply rooted.
      Qed.
      Import MonoidHomomorphismNotations.

      Lemma composite_sem_cont (i : Vector.t Input k) m0
        : composite_sem i m0 -> forall (vn : Vector.t nat (k + k)),
            {m1 : _ | composite_sem i (m1 +m+ m0) /\ vpl_len_kk m1 = vn}.
      Proof.
        cbn zeta. intros. cbn in H. destructH.
        eapply construct_vec_cont with (v:=fst_vec vn) in H0. 2:eauto.
        eapply construct_vec_cont with (v:=snd_vec vn) in H1. 2:eauto.
        destruct H0 as [fs Hfs].
        destruct H1 as [sn Hsn].
        destructH. destructH.
        exists (t_combine fs sn).
        setoid_rewrite vec_map_map2.
        split;[split|].
        + setoid_rewrite vec_map2_ext;swap 1 2.
          { intros. eapply homomorph. }
          setoid_rewrite vec_map2_fun_app.
          setoid_rewrite t_combine_fst.
          eauto.
        + setoid_rewrite vec_map2_ext;swap 1 2.
          { intros. eapply homomorph. }
          assert (Vector.map2 (fun x y : list SrcSt * list TgtSt => monoid_plus (snd x) (snd y)) (t_combine fs sn) m0
                  = Vector.map2 monoid_plus (Vector.map snd (t_combine fs sn)) (Vector.map snd m0)).
          { eapply vec_map2_fun_app. }
          rewrite H.
          setoid_rewrite t_combine_snd.
          eauto.
        + unfold vpl_len_kk.
          setoid_rewrite vpl_len_t_combine.
          setoid_rewrite vpl_to_kk_t_combine.
          rewrite Hfs1.
          rewrite Hsn1.
          eapply to_kk_self.
      Qed.

      Lemma composite_sem_det (i : Vector.t Input k) a a'
        : composite_sem i a -> composite_sem i a' -> vpl_len_kk a = vpl_len_kk a' -> a = a'.
      Proof.
        intros Ha Ha' Hlen.
        eapply vpl_len_kk_eq_inv in Hlen.
        destruct Hlen as [Hlen Hlen'].
        destruct Ha as [Ha1 Ha2].
        destruct Ha' as [Ha1' Ha2'].
        eapply vsem_leneq_eq in Hlen;eauto.
        eapply vsem_leneq_eq in Hlen';eauto.
        rewrite t_combine_self.
        rewrite t_combine_self at 1.
        rewrite Hlen,Hlen'.
        reflexivity.
      Qed.

      Lemma hyper_preserve_AE
         : forall a α,
          Vector.Forall2 src_sem i_vec a
          -> Vector.Forall2 tgt_sem i_vec α
          -> exists b β,
              Vector.Forall2 src_sem i_vec (b +vl+ a)
              /\ Vector.Forall2 tgt_sem i_vec (β +vl+ α)
              /\ src_rel (b +vl+ a)
              /\ tgt_rel (β +vl+ α).
      Proof.
        intros a α Hsrc_sem Htgt_sem.
        assert (composite_sem i_vec (t_combine a α)) as Q.
        {
          cbn.
          setoid_rewrite t_combine_fst.
          setoid_rewrite t_combine_snd.
          split; assumption.
        }
        eapply hyper_sim_AE in Q.
        3: eapply hyper_preserve_hyper_sim.
        - cbn zeta in Q.
          destructH.
          specialize (t_combine_self ts') as Hts.
          rewrite Hts in Q0, Q2, Q3, Q4.
          rewrite t_combine_monoid_plus in Q0, Q2, Q3, Q4.
          rewrite t_combine_fst in Q0, Q2.
          rewrite t_combine_snd in Q3, Q4.
          eexists. eexists. repeat split;eassumption.
        - eapply vpl_len_kk_hom.
        - eapply composite_sem_unit.
        - eapply composite_sem_cont.
        - eapply composite_sem_det.
        - eapply vpl_len_kk_plus_eq1.
        - eapply vpl_len_kk_surj_eq.
        - eapply vpl_len_kk_zero_zero.
      Qed.

      Lemma hyper_preserve_tgt_AE
            (α : Vector.t _ k)
            (Hα : Vector.Forall2 tgt_sem i_vec α)
        : exists β, Vector.Forall2 tgt_sem i_vec (β +vl+ α) /\ tgt_rel (β +vl+ α).
      Proof.
        eapply hyper_preserve_AE with (a:=vl_zero) in Hα.
        - destructH. exists β. firstorder.
        - eapply Vec_Forall2_forall2. intros.
          setoid_rewrite Vector.const_nth.
          eapply rooted.
      Qed.

      (* TODO show that this lemma also holds
         for the "partial prefix extension" of any vectorlist property.
         or show that such a property is always a hypersafety
       *)

      Lemma hyper_preserve_tgt_safe
            (tgt_safe : Vector.t (list TgtSt) k -> Prop)
            (Hsafety : veclist_safety tgt_safe)
            (Himpl : forall α, Vector.Forall2 tgt_sem i_vec α -> tgt_rel α -> tgt_safe α)
            (α : Vector.t _ k)
            (Hα : Vector.Forall2 tgt_sem i_vec α)
        : tgt_safe α.
      Proof.
        eapply hyper_preserve_tgt_AE in Hα.
        destructH.
        eapply Hsafety;eauto.
        eapply veclist_prefix_app.
      Qed.
    End with_live.
  End with_hyper_preserve.
End with_k_st.