Lvc.Equiv.SimF

Require Import List paco2.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL AllInRel.
Require Export Sim SimTactics IL BlockType.

Set Implicit Arguments.
Unset Printing Records.

A Framework for Simulation Proofs by Induction: Functional Version

Proof Relation


Class ProofRelationF (A:Type) := {
    
    ParamRelF : A list var list var Prop;
    
    ArgRelF : onv val onv val A list val list val Prop;
    
    IndexRelF : A nat nat Prop;
    Image : A nat;
    IndexRelDrop : AL' AL n n', IndexRelF (AL' ++ AL) n n'
                                  n length AL'
                                   IndexRelF AL (n - length AL') (n' - Image AL')
}.

Definition frel := rel3 simtype (fun _ : simtypeF.state)
                       (fun (_ : simtype) (_ : F.state) ⇒ F.state).

Parameter Relation and Separation


Definition paramrel A (PR:ProofRelationF A) AL L L' :=
   (f f':lab) E Z s i E' Z' s' i' a,
    IndexRelF AL f f'
     get AL f a
     get L f (F.blockI E Z s i)
     get L' f' (F.blockI E' Z' s' i')
     ParamRelF a Z Z'.

Definition indexwise_paramrel A (PR:ProofRelationF A) (F F':params × stmt) AL' AL :=
   n n' Z s Z' s' a,
    IndexRelF (AL' ++ AL) n n'
     get F n (Z,s)
     get F' n' (Z',s')
     get AL' n a
     ParamRelF a Z Z'.

Definition separates A (PR:ProofRelationF A) AL' AL (F F':params × stmt) :=
  length AL' = length F
   Image AL' = length F'
   ( n n', IndexRelF (AL' ++ AL) n n' n < length F n' < length F')
   ( n n', IndexRelF (AL' ++ AL) n n' n length F n' length F').

Lemma complete_paramrel A (PR:ProofRelationF A) E E' F F' AL' AL L L'
  : indexwise_paramrel PR F F' AL' AL
     paramrel PR AL L L'
     separates PR AL' AL F F'
     paramrel PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L').
Proof.
  intros IPR PAR [Len1 [Img [Ilt Ige]]].
  hnf; intros ? ? ? ? ? ? ? ? ? ? ? RN GetAL GetFL GetL'.
  eapply get_app_cases in GetFL; destruct GetFL as [GetFL'| [GetFL GE]].
  - exploit Ilt; eauto. eapply get_range in GetFL'.
    rewrite mapi_length in GetFL'; eauto.
    eapply get_app_lt_1 in GetL'; [| rewrite mapi_length; eauto ].
    inv_get. destruct x0 as [Z s], x as [Z' s']. simpl in ×. clear EQ0 EQ.
    eauto.
  - rewrite mapi_length in *; eauto.
    exploit Ige; eauto.
    eapply get_app_right_ge in GetAL; [ | rewrite Len1; eauto ].
    eapply get_app_right_ge in GetL'; [ | rewrite mapi_length; eauto ].
    eapply IndexRelDrop in RN; [| rewrite Len1; rewrite mapi_length in *; eauto].
    exploit (PAR (LabI (f - AL')) (LabI (f' - Image AL'))); eauto.
    rewrite Len1; eauto. rewrite Img; rewrite mapi_length in *; eauto.
Qed.

Definition indexes_exists {A} (PR:ProofRelationF A) AL (L L' : F.labenv) :=
   n n' a b, IndexRelF AL n n' get AL n a get L n b b', get L' n' b'.

Lemma complete_indexes_exists A (PR:ProofRelationF A) E E' F F' AL' AL L L'
  : indexes_exists PR AL L L'
     separates PR AL' AL F F'
     indexes_exists PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L').
Proof.
  intros IE [Len1 [Img [Ilt Ige]]].
  hnf; intros ? ? ? ? RN GetAL GetF.
  assert (Len3: E, AL' = mapi (F.mkBlock E) F) by eauto with len.
  eapply get_app_cases in GetF. destruct GetF as [GetF| [GetFL GE]].
  + inv_get. exploit Ilt; eauto using get_range.
    edestruct get_in_range; eauto.
    eexists; eapply get_app, get_mapi; eauto.
  + eapply get_app_right_ge in GetAL; [ | erewrite Len3; eauto ].
    exploit Ige; eauto. rewrite mapi_length in *; eauto.
    eapply IndexRelDrop in RN; [| erewrite Len3; eauto].
    edestruct IE; eauto. erewrite Len3. eauto.
    rewrite Img in H0. eexists.
    eapply get_app_right; eauto. rewrite mapi_length in ×. omega.
Qed.

Application Relation


Definition app_r t (r:frel) A (PR:ProofRelationF A) AL L L' :=
   (f f':lab) a E Z s i E' Z' s' i',
    IndexRelF AL f f'
     get AL f a
     get L f (F.blockI E Z s i)
     get L' f' (F.blockI E' Z' s' i')
     V V' Yv Y'v Y Y',
        ArgRelF E E' a Yv Y'v
         omap (op_eval V) Y = Some Yv
         omap (op_eval V') Y' = Some Y'v
         Z = Yv
         Z' = Y'v
         r t (L, V, stmtApp f Y)
            (L', V', stmtApp f' Y').

Lemma app_r_mon t (r r':frel) A (PR:ProofRelationF A) AL L L'
  : app_r t r PR AL L L'
     ( t x y, r t x y r' t x y)
     app_r t r' PR AL L L'.
Proof.
  intros Lr LE; hnf; intros; eauto.
Qed.

Label Environment Relation


Definition labenv_sim t (r:frel)
           {A} (PR:ProofRelationF A) (AL:list A) L L' :=
  length AL = length L
  smaller L'
  smaller L
  paramrel PR AL L L'
  indexes_exists PR AL L L'
  app_r t r PR AL L L'.

Lemma labenv_sim_nil t r A PR
  : @labenv_sim t r A PR nil nil nil.
Proof.
  do 5 (try split); hnf; intros; isabsurd.
Qed.

Hint Immediate labenv_sim_nil.

Lemma labenv_sim_mon t (r r':frel) A (PR:ProofRelationF A) AL L L'
  : labenv_sim t r PR AL L L'
     ( t x y, r t x y r' t x y)
     labenv_sim t r' PR AL L L'.
Proof.
  intros [LEN [STL [STL' [PAR [IE SIM]]]]] LE; hnf; do 5 (try split); eauto.
  eapply app_r_mon; eauto.
Qed.

Definition indexwise_r t (r:frel) A (PR:ProofRelationF A) AL' E E' F F' AL L L' :=
   n n' Z s Z' s' a,
    IndexRelF (AL' ++ AL) n n'
     get F n (Z,s)
     get F' n' (Z',s')
     get AL' n a
     VL VL',
        ArgRelF E E' a VL VL'
         r t (mapi (F.mkBlock E) F ++ L, E[Z <-- List.map Some VL], s)
            (mapi (F.mkBlock E') F' ++ L', E'[Z' <-- List.map Some VL'], s').

Lemma indexwise_r_mon t (r r':frel) A (PR:ProofRelationF A) AL' E E' F F' AL L L'
  : indexwise_r t r PR AL' E E' F F' AL L L'
     ( t x y, r t x y r' t x y)
     indexwise_r t r' PR AL' E E' F F' AL L L'.
Proof.
  intros Idx LE; hnf; intros; eauto.
Qed.

Hint Unfold separates.

Lemma labenv_sim_extension' t r A (PR:ProofRelationF A) (AL AL':list A) E E' F F' L L'
  : indexwise_r t (sim r \3/ r) PR AL' E E' F F' AL L L'
     indexwise_paramrel PR F F' AL' AL
     separates PR AL' AL F F'
     labenv_sim t (sim r) PR AL L L'
     labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L').
Proof.
  intros SIM IPR [Len2 [Img [Ilt Ige]]] [Len1 [STL [STL' [PAR [IE LSIM]]]]].
  hnf; do 5 (try split);
    eauto 20 using smaller_F_mkBlocks, complete_paramrel, complete_indexes_exists with len.
  intros f f' ? ? ? ? ? ? ? ? ? RN GetAL GetFL GetL'.
  assert (Len3: E, AL' = mapi (F.mkBlock E) F) by eauto with len.
  eapply get_app_cases in GetFL. destruct GetFL as [GetFL'| [GetFL GE]].
  - exploit Ilt; eauto. eapply get_range in GetFL'.
    rewrite mapi_length in GetFL'; eauto.
    eapply get_app_lt_1 in GetL'; [| rewrite mapi_length; eauto ].
    inv_get. destruct x0 as [Z s], x as [Z' s']. simpl in ×. clear EQ0 EQ.
    pone_step; simpl; eauto using get_app, get_mapi; simpl; eauto with len.
    orewrite (f-f=0). orewrite (f'-f'=0). simpl.
    exploit SIM; eauto.
  - intros. exploit Ige; eauto. rewrite mapi_length in GE; eauto.
    eapply get_app_right_ge in GetAL; [ | rewrite (Len3 E); eauto ].
    eapply get_app_right_ge in GetL'; [ | rewrite mapi_length; eauto ].
    rewrite mapi_length in ×.
    eapply IndexRelDrop in RN; eauto; [| rewrite (Len3 E); eauto].
    exploit (LSIM (LabI (f - AL')) (LabI (f' - Image AL'))) as SIMR; eauto.
    rewrite Len2; eauto. rewrite Img; eauto.
    eapply (@sim_Y_left F.state _ F.state _).
    eapply (@sim_Y_right F.state _ F.state _).
    rewrite Img in SIMR. rewrite Len2 in SIMR.
    eapply paco3_mon; [| eauto].
    eapply SIMR; eauto.
    econstructor; simpl; eauto with len. simpl. eauto with len.
    eapply F.StepGoto_mapi; simpl in *; eauto with len.
    rewrite mapi_length. exploit STL; eauto; simpl in *; omega.
    econstructor; simpl; eauto. simpl. eauto with len.
    eapply F.StepGoto_mapi; simpl in *; eauto with len.
    rewrite mapi_length. exploit STL'; eauto; simpl in *; omega.
    erewrite <- Len3, Len2; eauto.
Qed.

Key Lemmata

Fix Compatibility


Lemma fix_compatible_separate t A (PR:ProofRelationF A) AL' AL E E' F F' L L'
  : ( r,
        labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L')
         indexwise_r t (sim r) PR AL' E E' F F' AL L L')
     indexwise_paramrel PR F F' AL' AL
     separates PR AL' AL F F'
     r, labenv_sim t (sim r) PR AL L L'
            indexwise_r t (sim r) PR AL' E E' F F' AL L L'.
Proof.
  intros ISIM LP SEP r SIML. pcofix CIH.
  eapply ISIM.
  eapply labenv_sim_extension'; eauto.
  eauto using indexwise_r_mon; eauto.
  eapply labenv_sim_mon; eauto.
Qed.

Extension Lemma


Lemma labenv_sim_extension t A (PR:ProofRelationF A) (AL AL':list A) E E' F F' L L'
  : ( r,
        labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L')
         indexwise_r t (sim r) PR AL' E E' F F' AL L L')
     indexwise_paramrel PR F F' AL' AL
     separates PR AL' AL F F'
     r, labenv_sim t (sim r) PR AL L L'
            labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L').
Proof.
  intros ISIM IP SEP r SIML.
  eapply labenv_sim_extension'; eauto.
  eapply indexwise_r_mon.
  eapply fix_compatible_separate; eauto. eauto.
Qed.

Fun Compatibility


Lemma sim_fun t A (PR:ProofRelationF A) (AL AL':list A) E E' F F' L L' s s'
  : ( r, labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L')
           (sim r \3/ r) t (mapi (F.mkBlock E) F ++ L, E, s) (mapi (F.mkBlock E') F' ++ L', E', s'))
     ( r,
          labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L')
           indexwise_r t (sim r) PR AL' E E' F F' AL L L')
     indexwise_paramrel PR F F' AL' AL
     separates PR AL' AL F F'
     r, labenv_sim t (sim r) PR AL L L'
            sim r t (L, E, stmtFun F s) (L', E', stmtFun F' s').

Proof.
  intros SIM_s ISIM IP SEP r SIML.
  pone_step.
  eapply SIM_s.
  eapply labenv_sim_extension; eauto.
Qed.

Specialized Version if function bindings are not changed


Class PointwiseProofRelationF (A:Type) := {
    
    ParamRelFP : A list var list var Prop;
    
    ArgRelFP : onv val onv val A list val list val Prop;
    
}.

Lemma pointwise_PR_as_PR A
  : PointwiseProofRelationF A ProofRelationF A.
Proof.
  intros. destruct X as [B C].
  eapply (Build_ProofRelationF B C (fun L n n'eq n n') (@length _)).
  - intros; dcr; subst; eauto.
Defined.

Arguments pointwise_PR_as_PR : simpl never.

Hint Resolve pointwise_PR_as_PR : typeclass_instances.
Coercion pointwise_PR_as_PR : PointwiseProofRelationF >-> ProofRelationF.

Lemma IndexRelFP_eq A PR L n n'
  : @IndexRelF A (pointwise_PR_as_PR PR) L n n' n = n'.
Proof.
  destruct PR; simpl. reflexivity.
Qed.

Lemma IndexRelFP_refl A PR L n
  : @IndexRelF A (pointwise_PR_as_PR PR) L n n.
Proof.
  destruct PR; simpl. reflexivity.
Qed.

Hint Resolve IndexRelFP_refl.

Lemma labenv_sim_extension_ptw t A (PR:PointwiseProofRelationF A) (AL AL':list A) E E' F F' L L'
  : ( r ,
        labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L')
         indexwise_r t (sim r) PR AL' E E' F F' AL L L')
     indexwise_paramrel PR F F' AL' AL
     length AL' = length F
     length F = length F'
     r, labenv_sim t (sim r) PR AL L L'
         labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L').
Proof.
  intros ISIM IP Len1 Len2 r SIML.
  assert (separates PR AL' AL F F'). {
    destruct SIML; dcr.
    hnf; destruct PR; simpl; repeat split; intros; omega.
  }
  eapply labenv_sim_extension'; eauto.
  eapply indexwise_r_mon.
  eapply fix_compatible_separate; eauto. eauto.
Qed.

Lemma sim_fun_ptw t A (PR:PointwiseProofRelationF A) (AL AL':list A) F F' L L' E E' s s'
  : ( r, labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L')
           (sim r \3/ r) t (mapi (F.mkBlock E) F ++ L, E, s) (mapi (F.mkBlock E') F' ++ L', E', s'))
     ( r,
          labenv_sim t (sim r) PR (AL' ++ AL) (mapi (F.mkBlock E) F ++ L) (mapi (F.mkBlock E') F' ++ L')
           indexwise_r t (sim r) PR AL' E E' F F' AL L L')
     indexwise_paramrel PR F F' AL' AL
     length AL' = length F
     length F = length F'
     r, labenv_sim t (sim r) PR AL L L'
            sim r t (L, E, stmtFun F s) (L', E', stmtFun F' s').
Proof.
  intros SIM_s ISIM IP Len1 Len2 r SIML.
  pone_step.
  eapply SIM_s.
  eapply labenv_sim_extension_ptw; eauto.
Qed.

Lemma labenv_sim_app i A (PR:ProofRelationF A) AL L L' r V V' Y Y' (f f':lab) a
  : labenv_sim i (sim r) PR AL L L'
     get AL f a
     IndexRelF AL f f'
     ( E Z s n E' Z' s' n',
         get L f (F.blockI E Z s n)
          get L' f' (F.blockI E' Z' s' n')
          ParamRelF a Z Z'
          ( Yv, omap (op_eval V) Y = Yv Z = Yv
                  Y'v, omap (op_eval V') Y' = Y'v
                          Z' = Y'v ArgRelF E E' a Yv Y'v)
            (if isBisim i then
                (omap (op_eval V) Y = None omap (op_eval V') Y' = None)
                 (Z Y Z' Y')
              else True))
     sim r i (L, V, stmtApp f Y) (L', V', stmtApp f' Y').
Proof.
  intros LSIM GetAL RN ALL.
  edestruct LSIM as [Len1 [STL [STL' [PAR [IE SIM]]]]]; eauto; dcr.
  inv_get. edestruct IE; eauto.
  destruct x as [E Z s n], x0 as [E' Z' s' n'].
  exploit PAR; eauto.
  edestruct ALL as [A1 A2]; eauto; dcr.
  case_eq (omap (op_eval V) Y); intros.
  - decide (Z = Y).
    + edestruct A1; dcr; eauto with len.
    + destruct i; simpl in *; dcr.
      × exploit H4; eauto.
        pno_step.
      × perr.
  - destruct i; simpl in *; dcr.
    + exploit H3; eauto. pno_step.
    + perr.
Qed.

A small study on IL fixed-points in general


Definition bodies_r t (r:frel) A (PR:ProofRelationF A) AL (L1 L2 L L':F.labenv) :=
   f f' E Z s i E' Z' s' i' a,
    IndexRelF AL f f'
     get L f (F.blockI E Z s i)
     get L' f' (F.blockI E' Z' s' i')
     get AL f a
     VL VL',
        ArgRelF E E' a VL VL'
         r t (drop (f - i) L1, E[Z <-- List.map Some VL], s)
            (drop (f' - i') L2, E'[Z' <-- List.map Some VL'], s').

Lemma bodies_r_mon t (r r':frel) A (PR:ProofRelationF A) AL L1 L2 L L'
  : bodies_r t r PR AL L1 L2 L L'
     ( t x y, r t x y r' t x y)
     bodies_r t r' PR AL L1 L2 L L'.
Proof.
  intros Idx LE; hnf; intros; eauto.
Qed.

Lemma bodies_r_app_r t A (PR:ProofRelationF A) AL L L' r
  : bodies_r t r PR AL L L' L L'
     app_r t (sim r) PR AL L L'.
Proof.
  intros SIM.
  hnf; intros.
  pone_step; simpl; eauto with len.
Qed.

Lemma fix_compatible_bodies t A (PR:ProofRelationF A) AL L L'
  : ( (r:frel) L1 L2, app_r t (sim r) PR AL L1 L2
           bodies_r t (sim r) PR AL L1 L2 L L')
     r, bodies_r t (sim r) PR AL L L' L L'.
Proof.
  intros ISIM r.
  pcofix CIH;
  change (bodies_r t (sim r) PR AL L L' L L');
  change (bodies_r t r PR AL L L' L L') in CIH.
  eapply ISIM.
  eapply bodies_r_app_r; eauto.
Qed.