Merge commit '21652cac'

F_mu_ref_conc/rules_binary.v

@@ -24,24 +24,26 @@ Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
 Section definitionsS.
   Context `{cfgSG Σ, invG Σ}.
 
-  Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
+  Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
     own cfg_name (◯ (∅, {[ l := (q, to_agree v) ]})).
+  Definition heapS_mapsto_aux : { x | x = @heapS_mapsto_def }. by eexists. Qed.
+  Definition heapS_mapsto := proj1_sig heapS_mapsto_aux.
+  Definition heapS_mapsto_eq :
+    @heapS_mapsto = @heapS_mapsto_def := proj2_sig heapS_mapsto_aux.
 
-  Definition tpool_mapsto (j : nat) (e: expr) : iProp Σ :=
+  Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ :=
     own cfg_name (◯ ({[ j := Excl e ]}, ∅)).
+  Definition tpool_mapsto_aux : { x | x = @tpool_mapsto_def }. by eexists. Qed.
+  Definition tpool_mapsto := proj1_sig tpool_mapsto_aux.
+  Definition tpool_mapsto_eq :
+    @tpool_mapsto = @tpool_mapsto_def := proj2_sig tpool_mapsto_aux.
 
   Definition spec_inv (ρ : cfg lang) : iProp Σ :=
     (∃ tp σ, own cfg_name (● (to_tpool tp, to_gen_heap σ)) 
                  ∗ ⌜rtc step ρ (tp,σ)⌝)%I.
   Definition spec_ctx (ρ : cfg lang) : iProp Σ :=
     inv specN (spec_inv ρ).
-
-  Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
-  Proof. apply _. Qed.
-  Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
-  Proof. apply _. Qed.
 End definitionsS.
-Typeclasses Opaque heapS_mapsto tpool_mapsto.
 
 Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦ₛ{ q }  v") : uPred_scope.
@@ -107,7 +109,6 @@ Section conversions.
   Lemma tpool_singleton_included' tp j e :
     {[j := Excl e]} ≼ to_tpool tp → to_tpool tp !! j = Excl' e.
   Proof. rewrite tpool_lookup. by move=> /tpool_singleton_included=> ->. Qed.
-
 End conversions.
 
 Section cfg.
@@ -124,6 +125,11 @@ Section cfg.
   Local Hint Resolve to_tpool_insert'.
   Local Hint Resolve tpool_singleton_included.
 
+  Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
+  Proof. rewrite heapS_mapsto_eq. apply _. Qed.
+  Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
+  Proof. apply _. Qed.
+
   Lemma step_insert K tp j e σ e' σ' efs :
     tp !! j = Some (fill K e) → head_step e σ e' σ' efs →
     step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
@@ -145,7 +151,7 @@ Section cfg.
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
   Proof.
-    iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
+    iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
@@ -161,7 +167,7 @@ Section cfg.
     to_val e = Some v → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Alloc e) ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ v.
   Proof.
-    iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
+    iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 with "Hown Hj")
@@ -173,7 +179,8 @@ Section cfg.
     { eapply auth_update_alloc, prod_local_update_2,
         (alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done.
       by apply lookup_to_gen_heap_None. }
-    iExists l. rewrite /heapS_mapsto. iFrame "Hj Hl". iApply "Hclose". iNext.
+    iExists l. rewrite heapS_mapsto_eq /heapS_mapsto_def.
+    iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K (Loc l)]> tp), (<[l:=v]>σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
@@ -185,7 +192,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
   Proof.
     iIntros (?) "(#Hinv & Hj & Hl)".
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
@@ -205,7 +212,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ v.
   Proof.
     iIntros (??) "(#Hinv & Hj & Hl)".
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
@@ -230,7 +237,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K (#♭ false) ∗ l ↦ₛ{q} v'.
   Proof.
     iIntros (????) "(#Hinv & Hj & Hl)".
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
@@ -251,7 +258,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K (#♭ true) ∗ l ↦ₛ v2.
   Proof.
     iIntros (????) "(#Hinv & Hj & Hl)"; subst.
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
@@ -334,7 +341,7 @@ Section cfg.
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K Unit ∗ j' ⤇ e.
   Proof.
-    iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
+    iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.

F_mu_ref_conc/soundness_binary.v

@@ -31,10 +31,10 @@ Proof.
   { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
   simpl.
   rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
-  { rewrite /tpool_mapsto. asimpl. iFrame. }
+  { rewrite tpool_mapsto_eq /tpool_mapsto_def. asimpl. iFrame. }
   iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
   iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
-  rewrite /tpool_mapsto /=.
+  rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
   iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
   move: Hvalid=> /auth_valid_discrete_2
     [/prod_included [/tpool_singleton_included Hv2 _] _].

F_mu_ref_conc/tactics.v

@@ -31,7 +31,9 @@ Ltac reshape_val e tac :=
 Ltac reshape_expr e tac :=
   let rec go K e :=
   match e with
-  | _ => tac (reverse K) e
+  | _ =>
+     let Krev := eval cbn[reverse rev_append] in (reverse K) in
+     tac Krev e
   | App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
   | App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
   | BinOp ?op ?e1 ?e2 =>
@@ -89,7 +91,7 @@ Proof.
   rewrite right_id. rewrite H1. by rewrite uPred.wand_elim_r.
 Qed.
 
-Lemma tac_tp_bind `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p K' e e' Q :
+Lemma tac_tp_bind `{heapIG Σ, !cfgSG Σ} j e' Δ Δ' i p K' e Q :
   envs_lookup i Δ = Some (p, j ⤇ e)%I →
   e = fill K' e' →
   envs_simple_replace i p (Esnoc Enil i (j ⤇ fill K' e')) Δ = Some Δ' →
@@ -104,37 +106,18 @@ Ltac tp_bind_helper :=
   lazymatch goal with   
   | |- fill ?K ?e = fill _ ?efoc =>
      reshape_expr e ltac:(fun K' e' =>
-        unify e' efoc;
-        let K'' := eval cbn in (K ++ K') in
-        replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
+       unify e' efoc;
+       let K'' := eval cbn[app] in (K ++ K') in
+       replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
   | |- ?e = fill _ ?efoc =>
      reshape_expr e ltac:(fun K' e' =>
-        unify e' efoc;
-        replace e with (fill K' e') by (by rewrite ?fill_app))    
+       unify e' efoc;
+       replace e with (fill K' e') by (by rewrite ?fill_app))
   end; reflexivity.
 
-Ltac tp_bind_helper_constr efoc :=
-  rewrite ?fill_app /=;
-  lazymatch goal with
-  | |- fill ?K ?e = fill _ _ =>
-     reshape_expr e ltac:(fun K' e' =>
-        unify e' efoc;
-        lazymatch eval cbn in (K ++ K') with
-        | ?K'' =>
-           replace (fill K e)
-             with (fill K'' e')
-             by (rewrite ?fill_app; reflexivity)
-        end)
-  | |- ?e = fill _ _ =>
-     reshape_expr e ltac:(fun K' e' =>
-        unify e' efoc;
-        replace e with (fill K' e') by reflexivity)    
-  end; reflexivity.
-
-(* TODO: this is quite slow *)
 Tactic Notation "tp_normalise" constr(j) :=
   iStartProof;
-  (eapply (tac_tp_bind_gen j);
+  eapply (tac_tp_bind_gen j);
     [iAssumptionCore (* prove the lookup *)
     | lazymatch goal with
       | |- fill ?K ?e = _ =>
@@ -143,13 +126,13 @@ Tactic Notation "tp_normalise" constr(j) :=
           idtac "nice"
       end
     |env_cbv; reflexivity
-    |(* new goal *)]).
+    |(* new goal *)].
 
 Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
   iStartProof;
-  eapply (tac_tp_bind j);
+  eapply (tac_tp_bind j efoc);
     [iAssumptionCore (* prove the lookup *)
-    |tp_bind_helper_constr efoc (* do actual work *)
+    |tp_bind_helper (* do actual work *)
     |env_cbv; reflexivity
     |(* new goal *)].
 
@@ -902,7 +885,7 @@ Lemma test1 E1 j K l n ρ :
   nclose specN ⊆ E1 →
   j ⤇ fill K (App (Lam (Store (Loc l) (BinOp Add (Nat 1) (Var 0)))) (Load (Loc l))) -∗
   spec_ctx ρ -∗
-  l ↦ₛ (NatV n) ={E1}=∗ True.                        
+  l ↦ₛ (NatV n) ={E1}=∗ True.
 Proof.
   iIntros (?) "Hj #? Hl".
   tp_load j.
@@ -926,9 +909,10 @@ Proof.
   tp_fork j as i "Hi". Undo.
   tp_fork j as i. Undo.
   tp_fork j. iIntros (i) "Hi".
-  tp_fork i as k "Hk". tp_normalise i. tp_normalise j.
+  tp_fork i as k "Hk". tp_normalise i.
+  tp_normalise j.
   tp_cas_suc k. tp_normalise k.
-  tp_if_true k. 
+  tp_if_true k. tp_normalise k. 
   tp_rec k. asimpl.
   tp_fst k.
   done.