Same for unary logrel of F_mu_ref_par.

F_mu_ref_par/fundamental_unary.v

@@ -4,8 +4,9 @@ From iris.algebra Require Export upred_big_op.
 From iris.proofmode Require Import tactics pviewshifts invariants.
 
 Section typed_interp.
-  Context {Σ : gFunctors} `{i : heapIG Σ} {L : namespace}.
-  Implicit Types P Q R : iPropG lang Σ.
+  Context `{heapIG Σ} (L : namespace).
+  Notation D := (valC -n> iPropG lang Σ).
+  Implicit Types Δ : listC D.
 
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
     iApply (@wp_bind _ _ _ [ctx]);
@@ -14,8 +15,7 @@ Section typed_interp.
 
   Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
 
-  Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
-      (HNLdisj : N ⊥ L) (HΔ : ∀ x v, PersistentP (Δ x v)) :
+  Lemma typed_interp N Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) (HNLdisj : N ⊥ L) :
     Γ ⊢ₜ e : τ →
     length Γ = length vs →
     heapI_ctx N ∧ [∧] zip_with (λ τ, interp L τ Δ) Γ vs
@@ -29,7 +29,7 @@ Section typed_interp.
       rewrite /env_subst Hv; value_case.
       iApply (big_and_elem_of with "HΓ").
       apply elem_of_list_lookup_2 with x.
-      rewrite lookup_zip_with; simplify_option_eq; trivial.
+      rewrite lookup_zip_with; by simplify_option_eq.
     - (* unit *) value_case; trivial.
     - (* nat *) value_case; iExists _ ; trivial.
     - (* bool *) value_case; iExists _ ; trivial.
@@ -85,40 +85,31 @@ Section typed_interp.
       smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
       iApply wp_mono; [|iApply "Hv"]; auto.
     - (* TLam *)
-      value_case. iIntros {τi} "! /= %". iApply wp_TLam; iNext.
-      iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
-      iSplit; trivial.
-      rewrite zip_with_context_interp_subst; trivial.
+      value_case.
+      iAlways; iIntros { τi } "%". iApply wp_TLam; iNext. simpl in *.
+      iApply (IHHtyped (τi :: Δ)). by rewrite fmap_length. iFrame "Hheap".
+      rewrite zip_with_fmap_l. by iApply context_interp_ren_S.
     - (* TApp *)
       smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
       iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp L τ' Δ)); iPureIntro; apply _|]; cbn.
       iIntros {w} "?". by rewrite -interp_subst; simpl.
     - (* Fold *)
-      specialize (IHHtyped Δ HΔ vs Hlen).
-      iApply (@wp_bind _ _ _ [FoldCtx]).
-        iApply wp_wand_l.
-        iSplitL; [|iApply IHHtyped; auto].
-      iIntros {v} "#Hv".
-      value_case.
-      rewrite -interp_subst.
-      rewrite fixpoint_unfold; cbn.
+      iApply (@wp_bind _ _ _ [FoldCtx]);
+        iApply wp_wand_l; iSplitL; [|iApply (IHHtyped Δ HΔ vs Hlen); auto].
+      iIntros {v} "#Hv". value_case.
+      rewrite -interp_subst fixpoint_unfold /=.
       iAlways; eauto.
     - (* Unfold *)
       iApply (@wp_bind _ _ _ [UnfoldCtx]);
         iApply wp_wand_l; iSplitL; [|iApply IHHtyped; auto].
-      iIntros {v}.
-      cbn [interp interp_rec cofe_mor_car].
-      rewrite fixpoint_unfold.
-      iIntros "#Hv"; cbn.
-      change (fixpoint _) with (interp L (TRec τ) Δ).
-      iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
+      iIntros {v} "#Hv". rewrite /= fixpoint_unfold.
+      change (fixpoint _) with (interp L (TRec τ) Δ); simpl.
+      iDestruct "Hv" as {w} "#[% Hw]"; subst.
       iApply wp_Fold; cbn; auto using to_of_val.
-      rewrite -interp_subst; auto.
+      iNext; iPvsIntro. by rewrite -interp_subst.
     - (* Fork *)
-      iApply wp_fork.
-      iNext; iSplitL; trivial.
-      iApply wp_wand_l.
-      iSplitL; [|iApply IHHtyped; auto]; auto.
+      iApply wp_fork. iNext; iSplitL; trivial.
+      iApply wp_wand_l. iSplitL; [|iApply IHHtyped; auto]; auto.
     - (* Alloc *)
       smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ".
       iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].

F_mu_ref_par/soundness_unary.v

@@ -2,41 +2,29 @@ From iris_logrel.F_mu_ref_par Require Export fundamental_unary.
 From iris.proofmode Require Import tactics pviewshifts.
 From iris.program_logic Require Import ownership adequacy.
 
-Section Soundness.
-  Let Σ := #[ auth.authGF heapUR ].
+Section soundness.
+  Definition Σ := #[ auth.authGF heapUR ].
 
-  Definition free_type_context: varC -n> valC -n> iPropG lang Σ := λne x y,
-    True%I.
-
-  Lemma wp_soundness e τ :
+  Lemma wp_soundness e τ σ :
     [] ⊢ₜ e : τ →
-    ownP ∅ ⊢ WP e {{v, ∃ H : heapIG Σ,
-      interp (nroot .@ "Fμ,ref,par" .@ 1) τ free_type_context v }}.
+    ownP σ ⊢ WP e {{ v, ∃ H : heapIG Σ, interp (nroot .@ 1) τ [] v}}.
   Proof.
     iIntros {H1} "Hemp".
-    iPvs (heap_alloc (nroot .@ "Fμ,ref,par" .@ 2) with "Hemp")
+    iPvs (heap_alloc (nroot .@ 2) with "Hemp")
       as {H} "[Hheap Hemp]"; first solve_ndisj.
     iApply wp_wand_l. iSplitR.
     { iIntros {v} "HΦ". iExists H. iExact "HΦ". }
     rewrite -(empty_env_subst e).
-    iApply (@typed_interp _ H (nroot .@ "Fμ,ref,par" .@ 1)
-                              (nroot .@ "Fμ,ref,par" .@ 2) _ _ []); eauto.
+    iApply (@typed_interp _ _ (nroot .@ 1) (nroot .@ 2)); eauto.
     solve_ndisj.
   Qed.
 
-  Theorem Soundness e τ :
-    [] ⊢ₜ e : τ →
-    ∀ e' thp h, rtc step ([e], of_heap ∅) (e' :: thp, h) →
-              ¬reducible e' h → is_Some (to_val e').
+  Theorem soundness e τ e' thp σ σ' :
+    [] ⊢ₜ e : τ → rtc step ([e], σ) (e' :: thp, σ') →
+    is_Some (to_val e') ∨ reducible e' σ'.
   Proof.
-    intros H1 e' thp h Hstp Hnr.
-    eapply wp_soundness in H1; eauto.
-    edestruct (@wp_adequacy_reducible lang (globalF Σ) ⊤ (λ v, ∃ H,
-        @interp Σ H (nroot .@ "Fμ,ref,par" .@ 1) τ free_type_context v)%I
-      e e' (e' :: thp) ∅ ∅ h) as [Ha|Ha]; eauto; try tauto.
-    - done.
-    - iIntros "[Hp Hg]". by iApply H1.
-    - by rewrite of_empty_heap in Hstp.
+    intros ??. eapply wp_adequacy_reducible; eauto using ucmra_unit_valid.
+    - iIntros "[??]". by iApply wp_soundness.
     - constructor.
   Qed.
-End Soundness.
+End soundness.

F_mu_ref_par/typing.v

@@ -54,7 +54,7 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
   | App_typed e1 e2 τ1 τ2 :
      Γ ⊢ₜ e1 : TArrow τ1 τ2 → Γ ⊢ₜ e2 : τ1 → Γ ⊢ₜ App e1 e2 : τ2
   | TLam_typed e τ :
-     map (λ t, t.[ren (+1)]) Γ ⊢ₜ e : τ → Γ ⊢ₜ TLam e : TForall τ
+     subst (ren (+1)) <$> Γ ⊢ₜ e : τ → Γ ⊢ₜ TLam e : TForall τ
   | TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ → Γ ⊢ₜ TApp e : τ.[τ'/]
   | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜ Fold e : TRec τ
   | TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ Unfold e : τ.[TRec τ/]
@@ -67,72 +67,26 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
      Γ ⊢ₜ CAS e1 e2 e3 : TBool
 where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
 
-Local Hint Extern 1 =>
-  match goal with
-  | H : context [length (map _ _)] |- _ => rewrite map_length in H
-  end : typed_subst_invariant.
-
 Lemma typed_subst_invariant Γ e τ s1 s2 :
   Γ ⊢ₜ e : τ → (∀ x, x < length Γ → s1 x = s2 x) → e.[s1] = e.[s2].
 Proof.
   intros Htyped; revert s1 s2.
-  assert (∀ {A} `{Ids A} `{Rename A}
-            (s1 s2 : nat → A) x, (x ≠ 0 → s1 (pred x) = s2 (pred x)) →
-                               up s1 x = up s2 x).
+  assert (∀ x Γ, x < length (subst (ren (+1)) <$> Γ) → x < length Γ).
+  { intros ??. by rewrite fmap_length. } 
+  assert (∀ {A} `{Ids A} `{Rename A} (s1 s2 : nat → A) x,
+    (x ≠ 0 → s1 (pred x) = s2 (pred x)) → up s1 x = up s2 x).
   { intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
-  (induction Htyped => s1 s2 Hs; f_equal/=);
-    eauto using lookup_lt_Some with omega typed_subst_invariant.
+  induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
 Qed.
 
-Definition env_subst (vs : list val) (x : var) : expr :=
-  from_option id (Var x) (of_val <$> vs !! x).
-
-Lemma context_gen_weakening ξ Γ' Γ e τ :
-  Γ' ++ Γ ⊢ₜ e : τ →
-  Γ' ++ ξ ++ Γ ⊢ₜ e.[iter (length Γ') up (ren (+ (length ξ)))] : τ.
-Proof.
-  intros H1.
-  remember (Γ' ++ Γ) as Ξ. revert Γ' Γ ξ HeqΞ.
-  induction H1 => Γ1 Γ2 ξ HeqΞ; subst; asimpl in *; eauto using typed.
-  - rewrite iter_up; destruct lt_dec as [Hl | Hl].
-    + constructor. rewrite lookup_app_l; trivial. by rewrite lookup_app_l in H.
-    + asimpl. constructor. rewrite lookup_app_r; auto with omega.
-      rewrite lookup_app_r; auto with omega.
-      rewrite lookup_app_r in H; auto with omega.
-      match goal with
-        |- _ !! ?A = _ => by replace A with (x - length Γ1) by omega
-      end.
-  - econstructor; eauto.
-    + eapply (IHtyped2 (_ :: Γ1) Γ2 ξ Logic.eq_refl).
-    + eapply (IHtyped3 (_ :: Γ1) Γ2 ξ Logic.eq_refl).
-  - constructor.
-    eapply (IHtyped (_ :: _ :: Γ1) Γ2 ξ Logic.eq_refl).
-  - constructor.
-    specialize (IHtyped
-                  (map (λ t : type, t.[ren (+1)]) Γ1)
-                  (map (λ t : type, t.[ren (+1)]) Γ2)
-                  (map (λ t : type, t.[ren (+1)]) ξ)).
-    asimpl in *. rewrite ?map_length in IHtyped.
-    repeat rewrite map_app. apply IHtyped.
-    by repeat rewrite map_app.
-Qed.
-
-Lemma context_weakening ξ Γ e τ :
-  Γ ⊢ₜ e : τ → ξ ++ Γ ⊢ₜ e.[(ren (+ (length ξ)))] : τ.
-Proof. eapply (context_gen_weakening _ []). Qed.
-
-Lemma closed_context_weakening ξ Γ e τ :
-  (∀ f, e.[f] = e) → Γ ⊢ₜ e : τ → ξ ++ Γ ⊢ₜ e : τ.
-Proof. intros H1 H2. erewrite <- H1. by eapply context_weakening. Qed.
-
 Lemma n_closed_invariant n (e : expr) s1 s2 :
   (∀ f, e.[iter n up f] = e) → (∀ x, x < n → s1 x = s2 x) → e.[s1] = e.[s2].
 Proof.
   intros Hnc. specialize (Hnc (ren (+1))).
   revert n Hnc s1 s2.
-  (induction e => m Hmc s1 s2 H1); asimpl in *; try f_equal;
+  induction e => m Hmc s1 s2 H1; asimpl in *; try f_equal;
     try (match goal with H : _ |- _ => eapply H end; eauto;
-         try inversion Hmc; try match goal with H : _ |- _ => (by rewrite H) end;
+         try inversion Hmc; try match goal with H : _ |- _ => by rewrite H end;
          fail).
   - apply H1. rewrite iter_up in Hmc. destruct lt_dec; try omega.
     asimpl in *. cbv in x. replace (m + (x - m)) with x in Hmc by omega.
@@ -158,6 +112,9 @@ Proof.
       asimpl; rewrite H1; auto with omega.
 Qed.
 
+Definition env_subst (vs : list val) (x : var) : expr :=
+  from_option id (Var x) (of_val <$> vs !! x).
+
 Lemma typed_n_closed Γ τ e :
   Γ ⊢ₜ e : τ → (∀ f, e.[iter (length Γ) up f] = e).
 Proof.
@@ -207,24 +164,39 @@ Proof.
   by rewrite Hv.
 Qed.
 
-Local Opaque eq_nat_dec.
+Lemma empty_env_subst e : e.[env_subst []] = e.
+Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
 
-Lemma iter_up_subst_type (m : nat) (τ : type) (x : var) :
-  iter m up (τ .: ids) x =
-    if lt_dec x m then ids x else
-    if eq_nat_dec x m then τ.[ren (+m)] else ids (x - 1).
+(** Weakening *)
+Lemma context_gen_weakening ξ Γ' Γ e τ :
+  Γ' ++ Γ ⊢ₜ e : τ →
+  Γ' ++ ξ ++ Γ ⊢ₜ e.[iter (length Γ') up (ren (+ (length ξ)))] : τ.
 Proof.
-  revert x τ.
-  induction m; intros x τ; cbn.
-  - destruct x; cbn.
-    + destruct eq_nat_dec; auto with omega.
-      asimpl; trivial.
-    + destruct eq_nat_dec; auto with omega.
-  - destruct x; asimpl; trivial.
-    rewrite IHm.
-    repeat destruct lt_dec; repeat destruct eq_nat_dec;
-      asimpl; auto with omega.
+  intros H1.
+  remember (Γ' ++ Γ) as Ξ. revert Γ' Γ ξ HeqΞ.
+  induction H1 => Γ1 Γ2 ξ HeqΞ; subst; asimpl in *; eauto using typed.
+  - rewrite iter_up; destruct lt_dec as [Hl | Hl].
+    + constructor. rewrite lookup_app_l; trivial. by rewrite lookup_app_l in H.
+    + asimpl. constructor. rewrite lookup_app_r; auto with omega.
+      rewrite lookup_app_r; auto with omega.
+      rewrite lookup_app_r in H; auto with omega.
+      match goal with
+        |- _ !! ?A = _ => by replace A with (x - length Γ1) by omega
+      end.
+  - econstructor; eauto. by apply (IHtyped2 (_::_)). by apply (IHtyped3 (_::_)).
+  - constructor. by apply (IHtyped (_ :: _ :: _)).
+  - constructor.
+    specialize (IHtyped
+      (subst (ren (+1)) <$> Γ1) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
+    asimpl in *. rewrite ?map_length in IHtyped.
+    repeat rewrite fmap_app. apply IHtyped.
+    by repeat rewrite fmap_app.
 Qed.
 
-Lemma empty_env_subst e : e.[env_subst []] = e.
-Proof. change (env_subst []) with (@ids expr _); by asimpl. Qed.
+Lemma context_weakening ξ Γ e τ :
+  Γ ⊢ₜ e : τ → ξ ++ Γ ⊢ₜ e.[(ren (+ (length ξ)))] : τ.
+Proof. eapply (context_gen_weakening _ []). Qed.
+
+Lemma closed_context_weakening ξ Γ e τ :
+  (∀ f, e.[f] = e) → Γ ⊢ₜ e : τ → ξ ++ Γ ⊢ₜ e : τ.
+Proof. intros H1 H2. erewrite <- H1. by eapply context_weakening. Qed.