encode in the type of the local simulation that fn arguments are values

theories/lang/lang_base.v

@@ -267,6 +267,23 @@ Lemma is_Some_to_value_result (e: expr):
   is_Some (to_value e) → is_Some (to_result e).
 Proof. destruct e; simpl; intros []; naive_solver. Qed.
 
+Lemma Val_to_value e v : to_value e = Some v → Val v = e.
+Proof. destruct e; try discriminate. intros [= ->]. done. Qed.
+
+Lemma list_Forall_to_value (es: list expr):
+  Forall (λ ei, is_Some (to_value ei)) es ↔ (∃ vs, es = Val <$> vs).
+Proof.
+  induction es; split.
+  - intros _. exists []. done.
+  - intros _. constructor.
+  - intros [[v EQv] [vs EQvs]%IHes]%Forall_cons. exists (v::vs).
+    simpl. f_equal; last done.
+    erewrite Val_to_value; done.
+  - intros [[|v vs] EQ]; first discriminate.
+    move:EQ=> [= -> EQ]. constructor; first by eauto.
+    apply IHes. eexists. done.
+Qed.
+
 (** Global static function table *)
 Inductive function :=
 | FunV (xl : list binder) (e : expr) `{Closed (xl +b+ []) e}.

theories/opt/ex1.v

@@ -28,9 +28,9 @@ Definition ex1_opt : function :=
 
 Lemma ex1_sim_body fs ft : ⊨{fs,ft} ex1 ≥ᶠ ex1_opt.
 Proof.
-  intros rf es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
-  destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
-  destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
+  intros rf es et vls vlt σs σt FREL SUBSTs SUBSTt.
+  destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.
+  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
 
   (* InitCall *)
   exists 10%nat.

theories/opt/ex1_down.v

@@ -25,9 +25,9 @@ Definition ex1_down_opt : function :=
 
 Lemma ex1_down_sim_fun fs ft : ⊨{fs,ft} ex1_down ≥ᶠ ex1_down_opt.
 Proof.
-  intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
-  destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
-  destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
+  intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
+  destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.
+  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
 
   (* InitCall *)
   exists 10%nat.

theories/opt/ex2_down.v

@@ -25,9 +25,9 @@ Definition ex2_down_opt : function :=
 
 Lemma ex2_down_sim_fun fs ft : ⊨{fs,ft} ex2_down ≥ᶠ ex2_down_opt.
 Proof.
-  intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
-  destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
-  destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
+  intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
+  destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.
+  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
 
   (* InitCall *)
   exists 10%nat.

theories/opt/ex3.v

@@ -34,9 +34,9 @@ Definition ex3_opt_2 : function :=
 
 Lemma ex3_sim_fun fs ft : ⊨{fs,ft} ex3 ≥ᶠ ex3_opt_1.
 Proof.
-  intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
-  destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
-  destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
+  intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
+  destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.
+  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
 
   (* InitCall *)
   exists 10%nat.

theories/opt/ex3_down.v

@@ -36,9 +36,9 @@ Definition ex3_down_opt_2 : function :=
 
 Lemma ex3_down_sim_fun fs ft : ⊨{fs,ft} ex3_down ≥ᶠ ex3_down_opt_1.
 Proof.
-  intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
-  destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
-  destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
+  intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
+  destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.
+  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
 
   (* InitCall *)
   exists 10%nat.

theories/sim/local.v

@@ -128,15 +128,13 @@ Qed.
   - The returned result must also be values and related by [vrel]. *)
 Definition sim_local_fun
   (esat: A → state → state → Prop) (fn_src fn_tgt : function) : Prop :=
-  ∀ r es et el_src el_tgt σs σt
-    (VALS: Forall (λ ei, is_Some (to_value ei)) el_src)
-    (VALT: Forall (λ ei, is_Some (to_value ei)) el_tgt)
-    (VALEQ: Forall2 (vrel r) el_src el_tgt)
+  ∀ r es et (vl_src vl_tgt: list value) σs σt
+    (VALEQ: Forall2 (vrel r) (Val <$> vl_src) (Val <$> vl_tgt))
     (EQS: match fn_src with
-          | FunV xl e => subst_l xl el_src e = Some es
+          | FunV xl e => subst_l xl (Val <$> vl_src) e = Some es
           end)
     (EQT: match fn_tgt with
-          | FunV xl e => subst_l xl el_tgt e = Some et
+          | FunV xl e => subst_l xl (Val <$> vl_tgt) e = Some et
           end),
     ∃ idx, sim_local_body r idx
                           (InitCall es) σs (InitCall et) σt

theories/sim/local_adequacy.v

@@ -200,12 +200,14 @@ Proof.
       destruct (FUNS _ _ x3) as ([xls ebs HCss] & Eqfs & Eql & SIMf).
       destruct (subst_l_is_Some xls el_src ebs) as [ess Eqss].
       { by rewrite (Forall2_length _ _ _ VREL) -(subst_l_is_Some_length _ _ _ _ x4). }
-      specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VSRC VTGT VREL Eqss x4) as [idx2 SIMf].
+      apply list_Forall_to_value in VSRC. destruct VSRC as [vl_src ->].
+      apply list_Forall_to_value in VTGT. destruct VTGT as [vl_tgt ->].
+      specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VREL Eqss x4) as [idx2 SIMf].
       esplits.
       * left. eapply tc_rtc_l.
         { apply fill_tstep_rtc. eauto. }
         { econs. rewrite -fill_app. eapply (head_step_fill_tstep).
-          econs; econs; eauto. }
+          econs; econs; eauto. apply list_Forall_to_value. eauto. }
       * right. apply CIH. econs.
         { econs 2; eauto. i. instantiate (1 := mk_frame _ _ _ _). ss.
           destruct (CONT _ _ _ σ_src' σ_tgt' VRET).

theories/sim/program.v

@@ -18,7 +18,7 @@ Proof.
   destruct MAINT as (ebt & HCt & Eqt).
   destruct (FUNS _ _ Eqt) as ([xls ebs HCs] & Eqs & Eql & SIMf).
   apply nil_length_inv in Eql. subst xls.
-  specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM]; [done..|].
+  specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM]; [simpl; done..|].
   unfold behave_prog.
   eapply (adequacy_classical _ _ idx); [apply NSD| |by apply wf_init_state..].
   eapply sim_local_conf_sim; eauto.