finally, working parallel substitution

theories/lang/subst_map.v

@@ -38,20 +38,14 @@ Proof.
   induction el; eauto using Forall.
 Qed.
 
-(** Substitution with a list of pairs instead of a pair of lists.
-This lets us do a total operation. *)
-
-Definition is_var {T: Type} (y: string) (x: string * T) :=
-  x.1 = y.
-Global Instance is_var_dec {T: Type} y x : Decision (@is_var T y x).
-Proof. rewrite /is_var /=. apply _. Qed.
-
-Definition subst_map_delete {T: Type} (b: binder) (xs : list (string * T)) :=
-  if b is BNamed s then list_filter (λ x, ¬is_var s x) _ xs else xs.
-
-Fixpoint subst_map (xs : list (string * result)) (e : expr) : expr :=
+(** Parallel Substitution. *)
+Definition binder_delete {T} (b: binder) (xs: gmap string T) :=
+  if b is BNamed x then delete x xs else xs.
+Definition binder_insert {T} (b: binder) (r: T) (xs: gmap string T) :=
+  if b is BNamed x then <[x:=r]> xs else xs.
+Fixpoint subst_map (xs : gmap string result) (e : expr) : expr :=
   match e with
-  | Var y => if snd <$> list_find (is_var y) xs is Some (_, v) then of_result v else Var y
+  | Var y => if xs !! y is Some v then of_result v else Var y
   | Val v => Val v
   | Call e el => Call (subst_map xs e) (map (subst_map xs) el)
   | InitCall e => InitCall (subst_map xs e)
@@ -70,171 +64,98 @@ Fixpoint subst_map (xs : list (string * result)) (e : expr) : expr :=
   | Let x1 e1 e2 =>
       Let x1
         (subst_map xs e1)
-        (subst_map (subst_map_delete x1 xs) e2)
+        (subst_map (binder_delete x1 xs) e2)
   | Case e el => Case (subst_map xs e) (map (subst_map xs) el)
   end.
 
 Lemma subst_map_empty e :
-  subst_map [] e = e.
+  subst_map ∅ e = e.
 Proof.
   induction e using expr_ind; simpl; f_equal; eauto.
   - induction H; first done. simpl. by f_equal.
-  - destruct b; done.
+  - destruct b; first done. simpl. rewrite delete_empty. done.
   - induction H; first done. simpl. by f_equal.
 Qed.
 
-Lemma subst_map_cons x rx xs e :
-  subst_map ((x,rx)::xs) e = subst_map xs (subst x rx e).
+Lemma subst_map_subst map x (r: result) (e: expr) :
+  subst_map map (subst x r e) = subst_map (<[x:=r]>map) e.
 Proof.
-  revert x rx xs; induction e using expr_ind; intros xx rx xs; try (simpl; f_equal; eauto).
-  - destruct (decide (x=xx)) as [<-|ne].
-    + rewrite decide_True //. rewrite bool_decide_true //.
-      destruct rx; done.
-    + rewrite decide_False. { intros ?. apply ne. done. }
-      rewrite bool_decide_false //.
-      simpl. destruct (list_find (is_var x) xs); last done.
-      simpl. destruct p as [? [? ?]]. done.
+  revert x r map; induction e using expr_ind; intros xx r map; simpl;
+  try (f_equal; eauto).
+  - case_bool_decide.
+    + simplify_eq/=. rewrite lookup_insert. destruct r; done.
+    + rewrite lookup_insert_ne //.
   - induction H; first done. simpl. f_equal; done.
   - destruct b; simpl. done.
-    destruct (decide (s=xx)) as [<-|ne].
-    + rewrite decide_False //. { intros HH. apply HH. done. }
-      rewrite bool_decide_false //. intros ?. done.
-    + rewrite decide_True //. { intros ?. apply ne. done. }
-      rewrite bool_decide_true //. intros [= HH]. done.
+    case_bool_decide.
+    + rewrite IHe2. f_equal. rewrite delete_insert_ne //.
+      intros ?. apply H. f_equal. done.
+    + simplify_eq/=. rewrite delete_insert_delete //.
   - induction H; first done. simpl. f_equal; done.
 Qed.
 
-Definition fn_lists_to_subst {T: Type} (xbs : list binder) (xes : list T) :=
-  omap (λ '(x, e), if x is BNamed s then Some (s, e) else None) (zip xbs xes).
-
-Lemma subst_l_map (xbs : list binder) (xes : list value) (e es : expr) :
-  subst_l xbs (Val <$> xes) e = Some es →
-  es = subst_map (fn_lists_to_subst xbs (ValR <$> xes)) e.
+(** Turning list-subst into par-subst while preserving a pointwise property.
+FIXME: There probably is a way to do this with a lemma that talks about
+just one list... *)
+Lemma subst_l_map (xbs : list binder) (xes xet : list result)
+  (ebs ebt es et : expr) (R : result → result → Prop) :
+  subst_l xbs (of_result <$> xes) ebs = Some es →
+  subst_l xbs (of_result <$> xet) ebt = Some et →
+  Forall2 R xes xet →
+  ∃ map : gmap string (result * result),
+  es = subst_map (fst <$> map) ebs ∧ et = subst_map (snd <$> map) ebt ∧
+  map_Forall (λ _ '(s, t), R s t) map.
 Proof.
-  revert xes es e; induction xbs; intros xes es e; destruct xes; try done.
-  - intros [= ->]. simpl.
-    by rewrite subst_map_empty.
-  - simpl.
-    set eo := subst_l _ _ _. destruct eo eqn:EQ; last done.
-    subst eo. intros [=<-].
-    specialize (IHxbs _ _ _ EQ).
-    destruct a.
-    + done.
-    + rewrite subst_map_cons. done.
+  revert xes xet ebs ebt es et; induction xbs;
+  intros xes xet ebs ebt es et Hsubst1 Hsubst2 HR; simplify_eq/=.
+  - exists ∅. rewrite !fmap_empty !subst_map_empty.
+    destruct xes; last done. destruct xet; last done. simplify_eq/=.
+    split; first done. split; first done.
+    apply map_Forall_empty.
+  - destruct xes as [|ees xes]; first done. destruct xet as [|eet xet]; first done.
+    inversion HR. simplify_eq/=. destruct a.
+    + eapply IHxbs; eauto.
+    + edestruct (IHxbs xes xet) as (map & ? & ? & ?); [done..|].
+      exists (<[s:=(ees, eet)]> map). subst es et.
+      rewrite !subst_map_subst !fmap_insert.
+      split; first done. split; first done.
+      apply map_Forall_insert_2; done.
 Qed.
 
-Lemma list_find_delete_None {T: Type} xb b (xs : list (string * T)) :
-  list_find (is_var xb) xs = None →
-  list_find (is_var xb) (subst_map_delete b xs) = None.
+Lemma subst_subst_map x (r: result) map e :
+  subst x r (subst_map (delete x map) e) =
+  subst_map (<[x:=r]>map) e.
 Proof.
-  rewrite /subst_map_delete.
-  induction xs; simpl.
-  - by destruct b.
-  - destruct b; simpl; first done.
-    destruct a as [??]. case_decide; first done.
-    intros Hfind. case_decide; simpl.
-    + rewrite decide_False //. rewrite IHxs //.
-      destruct (list_find (is_var xb) xs); done.
-    + rewrite IHxs //.
-      destruct (list_find (is_var xb) xs); done.
-Qed.
-
-Lemma list_find_delete_ne {T: Type} xb b (xs : list (string * T)) p :
-  (if b is BNamed b then xb ≠ b else True) →
-  snd <$> list_find (is_var xb) xs = Some p →
-  snd <$> list_find (is_var xb) (subst_map_delete b xs) = Some p.
-Proof.
-  destruct b; first done. intros Hne.
-  induction xs; simpl; first done.
-  destruct p as [y ?].
-  case_decide.
-  - rewrite decide_True. { intros ?. apply Hne. etrans; done. }
-    simpl. rewrite decide_True //.
-  - case_decide; simpl; intros Heq.
-    + rewrite decide_False //.
-      destruct (list_find (is_var xb) xs) as [[i' [y' ?]]|]; last done.
-      simpl in Heq. rewrite -IHxs. done.
-      rewrite /subst_map_delete /filter.
-      destruct (list_find _ _); done.
-    + destruct (list_find (is_var xb) xs) as [[i' [y' ?]]|]; last done.
-      simpl in Heq. rewrite -IHxs. done.
-      rewrite /subst_map_delete /filter.
-      destruct (list_find _ _); done.
-Qed.
-
-Lemma subst_subst_map_delete b (r : result) (xs : list (string * result)) e :
-  list_find (is_var b) xs = None →
-  subst b r (subst_map xs e) =
-  subst_map ((b,r)::xs) e.
-Proof.
-  revert xs b r; induction e using expr_ind; intros xs xb xr Hfind;
-  try (simpl; f_equal; by eauto).
-  - destruct (decide (x=xb)) as [<-|ne]; simpl.
-    + rewrite decide_True //. rewrite Hfind /=.
+  revert map r x; induction e using expr_ind; intros map r xx; simpl;
+  try (f_equal; eauto).
+  - destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
       rewrite bool_decide_true //.
-    + rewrite decide_False //. { intros ?. apply ne. done. }
-      destruct (list_find (is_var x) xs); simpl.
-      * destruct p as [?[??]]. simpl. by destruct r.
-      * rewrite bool_decide_false //.
-  - simpl. f_equal; first by auto.
-    induction H; first done. simpl. f_equal; by auto.
-  - simpl. case_bool_decide.
-    + f_equal; first by auto. rewrite IHe2.
-      * apply list_find_delete_None. done.
-      * rewrite /subst_map_delete /=.
-        destruct b; try done.
-        rewrite decide_True //. { intros ?. apply H. f_equal. done. }
-    + f_equal; first by auto. subst b. simpl.
-      rewrite decide_False //. intros HH. apply HH. done.
-  - simpl. f_equal; first by auto.
-    induction H; first done. simpl. f_equal; by auto.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (map !! x) as [rr|].
+      * by destruct rr.
+      * simpl. rewrite bool_decide_false //.
+  - induction H; first done. simpl. by f_equal.
+  - destruct b; simpl; first by auto.
+    case_bool_decide.
+    + rewrite delete_insert_ne //. { intros [=EQ]. apply H. f_equal. done. }
+      rewrite delete_commute. apply IHe2.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+  - induction H; first done. simpl. by f_equal.
 Qed.
 
-Definition subst_map_eq (xs1 xs2 : list (string * result)) :=
-  ∀ x, snd <$> list_find (is_var x) xs1 = snd <$> list_find (is_var x) xs2.
-
-Lemma subst_map_delete_proper (xs1 xs2 : list (string * result)) b :
-  subst_map_eq xs1 xs2 →
-  subst_map_eq (subst_map_delete b xs1) (subst_map_delete b xs2).
+Lemma subst'_subst_map b (r: result) map e :
+  subst' b r (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b r map) e.
 Proof.
-  rewrite /subst_map_eq /subst_map_delete=>Heq x.
-  destruct b; first by auto.
-  specialize (Heq x). revert Heq; induction xs1; simpl.
-  - intros Heq. rewrite (list_find_delete_None _ s) //.
-    by destruct (list_find (is_var x) xs2).
-  - 
-    case_decide; simpl.
-    + intros Heq.
-      case_decide; simpl.
-      * rewrite decide_True //. simpl. symmetry.
-        apply (list_find_delete_ne _ (BNamed s)); last done.
-        intros [=->]. done.
-      * apply IHxs1.
-      * 
-    + rewrite decide_False //.
-      rewrite (list_find_delete_None _ s); auto.
-      by destruct (list_find (is_var x) xs2).
-    + rewrite (list_find_delete_None _ s); auto.
-      by destruct (list_find (is_var x) xs2).
-  - 
-
-Lemma subst_map_proper (xs1 xs2 : list (string * result)) e :
-  subst_map_eq xs1 xs2 →
-  subst_map xs1 e = subst_map xs2 e.
-Proof.
-  revert xs1 xs2; induction e using expr_ind; intros xs1 xs2 Heq; simpl;
-  try (f_equal; by eauto).
-  - rewrite Heq. case_match; done.
-  - f_equal; first by auto.
-    induction H; first done. simpl. f_equal; by auto.
-  - f_equal; first by auto.
-    apply IHe2.
+  destruct b; first done.
+  exact: subst_subst_map.
+Qed.
 
-Lemma subst'_subst_map_delete b (r : result) (xs : list (string * result)) e :
-  subst' b r (subst_map (subst_map_delete b xs) e) =
-  subst_map (if b is BNamed s then (s,r)::xs else xs) e.
+Lemma binder_insert_map {T U: Type} b (r: T) (f : T → U) map :
+  binder_insert b (f r) (f <$> map) =
+  f <$> binder_insert b r map.
 Proof.
   destruct b; first done. simpl.
-  rewrite subst_subst_map_delete.
-  - admit.
-  - 
+  rewrite fmap_insert. done.
+Qed.

theories/opt/ex1.v

@@ -53,7 +53,6 @@ Proof.
   sim_apply sim_simple_let_val=>/=.
   sim_apply (sim_simple_call 10 [] [] ε); [done|done|solve_res|].
   intros rf frs frt FREL.
-  apply sim_simple_val.
 
 Admitted.
 

theories/sim/refl.v

@@ -51,12 +51,12 @@ Definition sem_post (r: resUR) (n: nat) rs css' rt cst': Prop :=
 
 (** We define a "semantic well-formedness", in some context. *)
 Definition sem_wf (r: resUR) es et :=
-  ∀ xs : list (string * (result * result)),
-    Forall (λ '(_, (rs, rt)), rrel r rs rt) xs →
+  ∀ xs : gmap string (result * result),
+    map_Forall (λ _ '(rs, rt), rrel r rs rt) xs →
     r ⊨ˢ{sem_steps,fs,ft}
-      (subst_map (prod_map id fst <$> xs) es, css)
+      (subst_map (fst <$> xs) es, css)
     ≥
-      (subst_map (prod_map id snd <$> xs) et, cst)
+      (subst_map (snd <$> xs) et, cst)
     : sem_post.
 
 Lemma value_wf_soundness r v :
@@ -69,32 +69,25 @@ Proof.
     + apply IHv. done.
 Qed.
 
-Lemma list_find_var {A B : Type} x (f : A → B) (xs : list (string * A)):
-  list_find (is_var x) (prod_map id f <$> xs) =
-  prod_map id (prod_map id f) <$> list_find (is_var x) xs.
-Proof.
-  rewrite list_find_fmap. f_equal. apply list_find_proper. auto.
-Qed.
-
 Lemma expr_wf_soundness r e :
   expr_wf e → sem_wf r e e.
 Proof.
-  intros Hwf. induction e using expr_ind; simpl in Hwf.
+  revert r. induction e using expr_ind; simpl; intros r Hwf.
   - (* Value *)
     move=>_ _ /=.
     apply sim_simple_val.
-    split; first admit.
+    split; first done.
     split; first done. split; first done.
     apply value_wf_soundness. done.
   - (* Variable *)
     move=>{Hwf} xs Hxswf /=.
-    rewrite !list_find_var. destruct (list_find (is_var x) xs) eqn:Hfind; simpl.
-    + destruct p as [i [x' [rs rt]]]. simpl.
-      destruct (list_find_Some _ _ _ _ Hfind).
+    rewrite !lookup_fmap. specialize (Hxswf x).
+    destruct (xs !! x); simplify_eq/=.
+    + destruct p as [rs rt].
       intros σs σt ??. eapply sim_body_result=>_.
-      split; first admit.
+      split; first done.
       split; first done. split; first done.
-      eapply (Forall_lookup_1 _ _ _ _ Hxswf H).
+      eapply (Hxswf (rs, rt)). done.
     + simpl.
       (* FIXME: need lemma for when both sides are stuck on an unbound var. *)
       admit.
@@ -122,7 +115,11 @@ Proof.
     intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
     intros σs σt ??. eapply sim_body_let.
     { destruct rs; eauto. } { destruct rt; eauto. }
-    
+    rewrite !subst'_subst_map.
+    change rs with (fst (rs, rt)). change rt with (snd (rs, rt)) at 2.
+    rewrite !binder_insert_map.
+    eapply sim_simplify', IHe2; [done..|by apply Hwf|].
+    admit. (* resources dont match?? *)
   - (* Case *) admit.
 Admitted.
 
@@ -145,29 +142,9 @@ Proof.
       admit. (* end_call_sat *)
     - done.
   }
-  rewrite (subst_l_map _ _ _ _ Hsubst1).
-  rewrite (subst_l_map _ _ _ _ Hsubst2).
-  set subst := fn_lists_to_subst (fun_args f) (zip (ValR <$> vs) (ValR <$> vt)).
-  (* FIXME: we do 3 very similar inductions here. Not sure how to generalize though. *)
-  replace (fn_lists_to_subst (fun_args f) (ValR <$> vs)) with (prod_map id fst <$> subst); last first.
-  { rewrite /subst /fn_lists_to_subst. rewrite list_fmap_omap.
-    apply omap_ext'. revert Hrel. clear. revert vs vt.
-    induction (fun_args f); intros vs vt Hrel; simpl; first constructor.
-    inversion Hrel; simplify_eq/=; first constructor.
-    constructor. by destruct a. exact: IHl. }
-  replace (fn_lists_to_subst (fun_args f) (ValR <$> vt)) with (prod_map id snd <$> subst); last first.
-  { rewrite /subst /fn_lists_to_subst. rewrite list_fmap_omap.
-    apply omap_ext'. revert Hrel. clear. revert vs vt.
-    induction (fun_args f); intros vs vt Hrel; simpl; first constructor.
-    inversion Hrel; simplify_eq/=; first constructor.
-    constructor. by destruct a. exact: IHl. }
+  destruct (subst_l_map _ _ _ _ _ _ _ _ Hsubst1 Hsubst2 Hrel) as (map & -> & -> & Hmap).
   eapply sim_simplify, expr_wf_soundness; [done..|].
-  subst subst. revert Hrel. clear. revert vs vt.
-  induction (fun_args f); intros vs vt Hrel; simpl; first constructor.
-  inversion Hrel; simplify_eq/=; first constructor.
-  destruct a; first exact: IHl. constructor.
-  { admit. (* resource stuff. *) }
-  exact: IHl.
+  admit. (* resource stuff. *)
 Admitted.
 
 Lemma sim_mod_funs_refl prog :

theories/sim/simple.v

@@ -41,6 +41,18 @@ Proof.
   intros HΦ HH. eapply sim_local_body_post_mono; last exact: HH.
   apply HΦ.
 Qed.
+Lemma sim_simplify'
+  (Φnew: resUR → nat → result → call_id_stack → result → call_id_stack → Prop)
+  (Φ: resUR → nat → result → state → result → state → Prop)
+  r n fs ft es σs et σt css cst :
+  (∀ r n vs σs vt σt, Φnew r n vs σs.(scs) vt σt.(scs) → Φ r n vs σs vt σt) →
+  σs.(scs) = css →
+  σt.(scs) = cst →
+  r ⊨ˢ{ n , fs , ft } (es, css) ≥ (et, cst) : Φnew →
+  r ⊨{ n , fs , ft } (es, σs) ≥ (et, σt) : Φ.
+Proof.
+  intros HΦ <-<-. eapply sim_simplify. done.
+Qed.
 
 Lemma sim_simple_post_mono Φ1 Φ2 r n fs ft es css et cst :
   Φ1 <6= Φ2 →