Commit 88c9a1e0 by Robbert Krebbers

### Make logical relations look like logical relations.

parent b98e54c9
 ... ... @@ -16,20 +16,14 @@ Section typed_interp. Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial. Lemma typed_interp Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) : Γ ⊢ₜ e : τ → length Γ = length vs → [∧] zip_with (λ τ, interp τ Δ) Γ vs ⊢ WP e.[env_subst vs] {{ interp τ Δ }}. Theorem fundamental Δ Γ vs e τ (HΔ : env_PersistentP Δ) : Γ ⊢ₜ e : τ → ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Proof. intros Htyped. revert Δ HΔ vs. induction Htyped; iIntros {Δ HΔ vs Hlen} "#HΓ"; cbn. intros Htyped. revert Δ vs HΔ. induction Htyped; iIntros {Δ vs HΔ} "#HΓ"; cbn. - (* var *) destruct (lookup_lt_is_Some_2 vs x) as [v Hv]. { by rewrite -Hlen; apply lookup_lt_Some with τ. } 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; by simplify_option_eq. iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done. rewrite /env_subst. simplify_option_eq. by value_case. - (* unit *) value_case. - (* pair *) smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHHtyped1. ... ... @@ -51,47 +45,43 @@ Section typed_interp. value_case; eauto. - (* case *) smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn. iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; subst. + iApply wp_case_inl; auto 1 using to_of_val; asimpl. specialize (IHHtyped2 Δ HΔ (w::vs)). erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto). iNext; iApply IHHtyped2; cbn; auto. + iApply wp_case_inr; auto 1 using to_of_val; asimpl. specialize (IHHtyped3 Δ HΔ (w::vs)). erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto). iNext; iApply IHHtyped3; cbn; auto. iDestruct (interp_env_length with "HΓ") as %?. iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; simplify_eq/=. + iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto. + iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto. - (* lam *) value_case; iAlways; iIntros {w} "#Hw". iApply wp_lam; auto 1 using to_of_val. asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto. iNext; iApply (IHHtyped Δ HΔ (w :: vs)); cbn; auto. iDestruct (interp_env_length with "HΓ") as %?. iApply wp_lam; auto 1 using to_of_val. iNext. asimpl. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped Δ (w :: vs)). iApply interp_env_cons; auto. - (* app *) smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2. iApply wp_mono; [|iApply "Hv"]; auto. - (* TLam *) value_case. iAlways; iIntros { τi } "%". iApply wp_TLam; iNext. simpl in *. iApply (IHHtyped (τi :: Δ)). by rewrite fmap_length. rewrite zip_with_fmap_l. by iApply context_interp_ren_S. iAlways; iIntros { τi } "%". iApply wp_TLam; iNext. iApply IHHtyped. by iApply interp_env_ren. - (* TApp *) smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn. iApply wp_wand_r; iSplitL; [iApply ("Hv" \$! (interp τ' Δ)); iPureIntro; apply _|]. iApply wp_wand_r; iSplitL; [iApply ("Hv" \$! (⟦ τ' ⟧ Δ)); iPureIntro; apply _|]. iIntros {w} "?". by rewrite interp_subst. - (* Fold *) rewrite map_length in IHHtyped. iApply (@wp_bind _ _ _ [FoldCtx]). iApply wp_wand_l. iSplitL; [|iApply (IHHtyped (interp (TRec τ) Δ :: Δ)); trivial]. + iIntros {v} "#Hv". value_case. change (fixpoint _) with (interp (TRec τ) Δ) at 1; trivial. rewrite fixpoint_unfold /=. iAlways; eauto 10. + rewrite zip_with_fmap_l. by iApply context_interp_ren_S. iApply (@wp_bind _ _ _ [FoldCtx]); iApply wp_wand_l; iSplitL; [|iApply (IHHtyped Δ vs); 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; trivial]. iIntros {v} "#Hv". rewrite /= fixpoint_unfold. change (fixpoint _) with (interp (TRec τ) Δ); simpl. change (fixpoint _) with (⟦ TRec τ ⟧ Δ); simpl. iDestruct "Hv" as {w} "#[% Hw]"; subst. iApply wp_Fold; cbn; auto using to_of_val. by rewrite -interp_subst. ... ...
 From iris.proofmode Require Import tactics. From iris.program_logic Require Export weakestpre. From iris_logrel.F_mu Require Export lang typing. Import uPred. ... ... @@ -65,29 +66,39 @@ Section logrel. | TForall τ' => interp_forall (interp τ') | TRec τ' => interp_rec (interp τ') end%I. Notation "⟦ τ ⟧" := (interp τ). Class ctx_PersistentP Δ := Definition interp_env (Γ : list type) (Δ : listC D) (vs : list val) : iProp lang Σ := (length Γ = length vs ∧ [∧] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I. Notation "⟦ Γ ⟧*" := (interp_env Γ). Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp lang Σ := WP e {{ ⟦ τ ⟧ Δ }}%I. Class env_PersistentP Δ := ctx_persistentP : Forall (λ τi, ∀ v, PersistentP (τi v)) Δ. Global Instance ctx_persistent_nil : ctx_PersistentP []. Global Instance ctx_persistent_nil : env_PersistentP []. Proof. by constructor. Qed. Global Instance ctx_persistent_cons τi Δ : (∀ v, PersistentP (τi v)) → ctx_PersistentP Δ → ctx_PersistentP (τi :: Δ). (∀ v, PersistentP (τi v)) → env_PersistentP Δ → env_PersistentP (τi :: Δ). Proof. by constructor. Qed. Global Instance ctx_persistent_lookup Δ x v : ctx_PersistentP Δ → PersistentP (ctx_lookup x Δ v). env_PersistentP Δ → PersistentP (ctx_lookup x Δ v). Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed. Global Instance interp_var_persistent τ Δ v : ctx_PersistentP Δ → PersistentP (interp τ Δ v). Global Instance interp_persistent τ Δ v : env_PersistentP Δ → PersistentP (⟦ τ ⟧ Δ v). Proof. revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _. rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=. by apply always_intro'. Qed. Global Instance interp_env_persistent Γ Δ vs : env_PersistentP Δ → PersistentP (⟦ Γ ⟧* Δ vs) := _. Lemma interp_weaken Δ1 Π Δ2 τ : interp τ.[iter (length Δ1) up (ren (+ length Π))] (Δ1 ++ Π ++ Δ2) ≡ interp τ (Δ1 ++ Δ2). ⟦ τ.[iter (length Δ1) up (ren (+ length Π))] ⟧ (Δ1 ++ Π ++ Δ2) ≡ ⟦ τ ⟧ (Δ1 ++ Δ2). Proof. revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. ... ... @@ -103,8 +114,8 @@ Section logrel. Qed. Lemma interp_subst_up Δ1 Δ2 τ τ' : interp τ (Δ1 ++ interp τ' Δ2 :: Δ2) ≡ interp τ.[iter (length Δ1) up (τ' .: ids)] (Δ1 ++ Δ2). ⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2) ≡ ⟦ τ.[iter (length Δ1) up (τ' .: ids)] ⟧ (Δ1 ++ Δ2). Proof. revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl. - done. ... ... @@ -124,15 +135,41 @@ Section logrel. - intros w; simpl; properness; auto. apply (IHτ (_ :: _)). Qed. Lemma interp_subst Δ2 τ τ' : interp τ (interp τ' Δ2 :: Δ2) ≡ interp τ.[τ'/] Δ2. Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2. Proof. apply (interp_subst_up []). Qed. Lemma context_interp_ren_S Δ (Γ : list type) (vs : list val) τi : ([∧] zip_with (λ τ, interp τ Δ) Γ vs) ⊣⊢ ([∧] zip_with (λ τ, interp τ.[ren (+1)] (τi :: Δ)) Γ vs). Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ length Γ = length vs. Proof. by iIntros "[% ?]". Qed. Lemma interp_env_Some_l Δ Γ vs x τ : Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, vs !! x = Some v ∧ ⟦ τ ⟧ Δ v. Proof. revert Δ vs τi; induction Γ=> Δ [|v vs] τi; simpl; auto. apply and_proper; auto. symmetry. apply (interp_weaken [] [τi] Δ). iIntros {?} "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen. destruct (lookup_lt_is_Some_2 vs x) as [v Hv]. { by rewrite -Hlen; apply lookup_lt_Some with τ. } iExists v; iSplit. done. iApply (big_and_elem_of with "HΓ"). apply elem_of_list_lookup_2 with x. rewrite lookup_zip_with; by simplify_option_eq. Qed. Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ []. Proof. iIntros ""; iSplit; auto. Qed. Lemma interp_env_cons Δ Γ vs τ v : ⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∧ ⟦ Γ ⟧* Δ vs. Proof. rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc. by apply and_proper; [apply pure_proper; omega|]. Qed. Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi : ⟦ subst (ren (+1)) <\$> Γ ⟧* (τi :: Δ) vs ⊣⊢ ⟦ Γ ⟧* Δ vs. Proof. apply and_proper; [apply pure_proper; by rewrite fmap_length|]. revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto. apply and_proper; auto. apply (interp_weaken [] [τi] Δ). Qed. End logrel. Notation "⟦ τ ⟧" := (interp τ). Notation "⟦ τ ⟧ₑ" := (interp_expr τ). Notation "⟦ Γ ⟧*" := (interp_env Γ).
 ... ... @@ -9,7 +9,7 @@ Section soundness. [] ⊢ₜ e : τ → True ⊢ WP e {{ @interp (globalF Σ) τ [] }}. Proof. iIntros {H} "". rewrite -(empty_env_subst e). by iApply (@typed_interp _ _ _ []). iApply (@fundamental _ _ _ []); eauto. by iApply interp_env_nil. Qed. Theorem soundness e τ e' thp : ... ...
 ... ... @@ -32,7 +32,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 τ : subst (ren (+1)) <\$> Γ ⊢ₜ e : τ → Γ ⊢ₜ TLam e : TForall τ | TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ → Γ ⊢ₜ TApp e : τ.[τ'/] | TFold e τ : subst (ren (+1)) <\$> Γ ⊢ₜ e : τ → Γ ⊢ₜ Fold e : TRec τ | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜ Fold e : TRec τ | TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ Unfold e : τ.[TRec τ/] where "Γ ⊢ₜ e : τ" := (typed Γ e τ). ... ...
 ... ... @@ -15,21 +15,15 @@ Section typed_interp. Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]. Lemma typed_interp Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) : Theorem fundamental Δ Γ vs e τ (HΔ : env_PersistentP Δ) : Γ ⊢ₜ e : τ → length Γ = length vs → heap_ctx ∧ [∧] zip_with (λ τ, interp τ Δ) Γ vs ⊢ WP e.[env_subst vs] {{ interp τ Δ }}. heap_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Proof. intros Htyped; revert Δ HΔ vs. induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ] /=". intros Htyped; revert Δ vs HΔ. induction Htyped; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=". - (* var *) destruct (lookup_lt_is_Some_2 vs x) as [v Hv]. { by rewrite -Hlen; apply lookup_lt_Some with τ. } rewrite /env_subst Hv; value_case. iApply (big_and_elem_of with "HΓ"). apply elem_of_list_lookup_2 with x. by rewrite lookup_zip_with; simplify_option_eq. iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done. rewrite /env_subst. simplify_option_eq. by value_case. - (* unit *) by value_case. - (* pair *) smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1. ... ... @@ -51,41 +45,38 @@ Section typed_interp. value_case; eauto. - (* case *) smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn. iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; subst. + iApply wp_case_inl; auto 1 using to_of_val; asimpl. specialize (IHHtyped2 Δ HΔ (w::vs)). erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto). iNext; iApply IHHtyped2; cbn; auto. + iApply wp_case_inr; auto 1 using to_of_val; asimpl. specialize (IHHtyped3 Δ HΔ (w::vs)). erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto). iNext; iApply IHHtyped3; cbn; auto. iDestruct (interp_env_length with "HΓ") as %?. iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; simplify_eq/=. + iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped2 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. + iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped3 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. - (* lam *) value_case; iAlways; iIntros {w} "#Hw". iApply wp_lam; auto 1 using to_of_val. asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto. iNext; iApply (IHHtyped Δ HΔ (w :: vs)); cbn; auto. iDestruct (interp_env_length with "HΓ") as %?. iApply wp_lam; auto 1 using to_of_val. iNext. asimpl. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped Δ (w :: vs)). iFrame "Hheap". iApply interp_env_cons; auto. - (* app *) smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2. iApply wp_mono; [|iApply "Hv"]; auto. - (* TLam *) 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. iAlways; iIntros { τi } "%". iApply wp_TLam; iNext. iApply IHHtyped. iFrame "Hheap". by iApply interp_env_ren. - (* TApp *) smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn. iApply wp_wand_r; iSplitL; [iApply ("Hv" \$! (interp τ' Δ)); iPureIntro; apply _|]. iIntros {w} "?". by rewrite interp_subst. - (* Fold *) rewrite map_length in IHHtyped. iApply (@wp_bind _ _ _ [FoldCtx]). iApply wp_wand_l. iSplitL; [|iApply (IHHtyped (interp (TRec τ) Δ :: Δ)); trivial]. + iIntros {v} "#Hv". value_case. rewrite fixpoint_unfold /=. iAlways; eauto 10. + iFrame "Hheap". rewrite zip_with_fmap_l. by iApply context_interp_ren_S. iApply (@wp_bind _ _ _ [FoldCtx]); iApply wp_wand_l; iSplitL; [|iApply (IHHtyped Δ vs); 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]. ... ...
 From iris.prelude Require Import strings. From iris.proofmode Require Import tactics. From iris.program_logic Require Export weakestpre. From iris_logrel.F_mu_ref Require Export rules typing. Import uPred. ... ... @@ -78,29 +78,39 @@ Section logrel. | TRec τ' => interp_rec (interp τ') | Tref τ' => interp_ref (interp τ') end. Notation "⟦ τ ⟧" := (interp τ). Class ctx_PersistentP Δ := Definition interp_env (Γ : list type) (Δ : listC D) (vs : list val) : iPropG lang Σ := (length Γ = length vs ∧ [∧] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I. Notation "⟦ Γ ⟧*" := (interp_env Γ). Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iPropG lang Σ := WP e {{ ⟦ τ ⟧ Δ }}%I. Class env_PersistentP Δ := ctx_persistentP : Forall (λ τi, ∀ v, PersistentP (τi v)) Δ. Global Instance ctx_persistent_nil : ctx_PersistentP []. Global Instance ctx_persistent_nil : env_PersistentP []. Proof. by constructor. Qed. Global Instance ctx_persistent_cons τi Δ : (∀ v, PersistentP (τi v)) → ctx_PersistentP Δ → ctx_PersistentP (τi :: Δ). (∀ v, PersistentP (τi v)) → env_PersistentP Δ → env_PersistentP (τi :: Δ). Proof. by constructor. Qed. Global Instance ctx_persistent_lookup Δ x v : ctx_PersistentP Δ → PersistentP (ctx_lookup x Δ v). env_PersistentP Δ → PersistentP (ctx_lookup x Δ v). Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed. Global Instance interp_var_persistent τ Δ v : ctx_PersistentP Δ → PersistentP (interp τ Δ v). Global Instance interp_persistent τ Δ v : env_PersistentP Δ → PersistentP (⟦ τ ⟧ Δ v). Proof. revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _. rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=. by apply always_intro'. Qed. Global Instance interp_env_persistent Γ Δ vs : env_PersistentP Δ → PersistentP (⟦ Γ ⟧* Δ vs) := _. Lemma interp_weaken Δ1 Π Δ2 τ : interp τ.[iter (length Δ1) up (ren (+ length Π))] (Δ1 ++ Π ++ Δ2) ≡ interp τ (Δ1 ++ Δ2). ⟦ τ.[iter (length Δ1) up (ren (+ length Π))] ⟧ (Δ1 ++ Π ++ Δ2) ≡ ⟦ τ ⟧ (Δ1 ++ Δ2). Proof. revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. ... ... @@ -117,8 +127,8 @@ Section logrel. Qed. Lemma interp_subst_up Δ1 Δ2 τ τ' : interp τ (Δ1 ++ interp τ' Δ2 :: Δ2) ≡ interp τ.[iter (length Δ1) up (τ' .: ids)] (Δ1 ++ Δ2). ⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2) ≡ ⟦ τ.[iter (length Δ1) up (τ' .: ids)] ⟧ (Δ1 ++ Δ2). Proof. revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl. - done. ... ... @@ -139,15 +149,42 @@ Section logrel. - intros w; simpl; properness; auto. by apply IHτ. Qed. Lemma interp_subst Δ2 τ τ' : interp τ (interp τ' Δ2 :: Δ2) ≡ interp τ.[τ'/] Δ2. Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2. Proof. apply (interp_subst_up []). Qed. Lemma context_interp_ren_S Δ (Γ : list type) (vs : list val) τi : ([∧] zip_with (λ τ, interp τ Δ) Γ vs) ⊣⊢ ([∧] zip_with (λ τ, interp τ.[ren (+1)] (τi :: Δ)) Γ vs). Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ length Γ = length vs. Proof. by iIntros "[% ?]". Qed. Lemma interp_env_Some_l Δ Γ vs x τ : Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, vs !! x = Some v ∧ ⟦ τ ⟧ Δ v. Proof. revert Δ vs τi; induction Γ=> Δ [|v vs] τi; simpl; auto. apply and_proper; auto. symmetry. apply (interp_weaken [] [τi] Δ). iIntros {?} "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen. destruct (lookup_lt_is_Some_2 vs x) as [v Hv]. { by rewrite -Hlen; apply lookup_lt_Some with τ. } iExists v; iSplit. done. iApply (big_and_elem_of with "HΓ"). apply elem_of_list_lookup_2 with x. rewrite lookup_zip_with; by simplify_option_eq. Qed. Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ []. Proof. iIntros ""; iSplit; auto. Qed. Lemma interp_env_cons Δ Γ vs τ v : ⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∧ ⟦ Γ ⟧* Δ vs. Proof. rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc. by apply and_proper; [apply pure_proper; omega|]. Qed. Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi : ⟦ subst (ren (+1)) <\$> Γ ⟧* (τi :: Δ) vs ⊣⊢ ⟦ Γ ⟧* Δ vs. Proof. apply and_proper; [apply pure_proper; by rewrite fmap_length|]. revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto. apply and_proper; auto. apply (interp_weaken [] [τi] Δ). Qed. End logrel. Typeclasses Opaque interp_env. Notation "⟦ τ ⟧" := (interp τ). Notation "⟦ τ ⟧ₑ" := (interp_expr τ). Notation "⟦ Γ ⟧*" := (interp_env Γ).
 ... ... @@ -13,7 +13,8 @@ Section soundness. iPvs (heap_alloc 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; eauto. rewrite -(empty_env_subst e). iApply fundamental; repeat iSplit; eauto. by iApply interp_env_nil. Qed. Theorem soundness e τ e' thp σ σ' : ... ...
 ... ... @@ -35,7 +35,7 @@ Inductive typed (Γ : list type) : expr → type → Prop := | TLam_typed e τ : subst (ren (+1)) <\$> Γ ⊢ₜ e : τ → Γ ⊢ₜ TLam e : TForall τ | TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ → Γ ⊢ₜ TApp e : τ.[τ'/] | TFold e τ : subst (ren (+1)) <\$> Γ ⊢ₜ e : τ → Γ ⊢ₜ Fold e : TRec τ | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜ Fold e : TRec τ | TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ Unfold e : τ.[TRec τ/] | TAlloc e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ | TLoad e τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ Load e : τ ... ...
 ... ... @@ -201,8 +201,8 @@ Section bin_log_related_under_typed_ctx. (∀ f, e.[base.iter (length Γ) up f] = e) → (∀ f, e'.[base.iter (length Γ) up f] = e') → typed_ctx K Γ τ Γ' τ' → (∀ Δ (HΔ : ctx_PersistentP Δ), Δ ∥ Γ ⊨ e ≤log≤ e' : τ) → ∀ Δ (HΔ : ctx_PersistentP Δ), (∀ Δ (HΔ : env_PersistentP Δ), Δ ∥ Γ ⊨ e ≤log≤ e' : τ) → ∀ Δ (HΔ : env_PersistentP Δ), Δ ∥ Γ' ⊨ fill_ctx K e ≤log≤ fill_ctx K e' : τ'. Proof. revert Γ τ Γ' τ' e e'. ... ... @@ -211,31 +211,31 @@ Section bin_log_related_under_typed_ctx. - inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. intros H3 Δ HΔ. specialize (IHK _ _ _ _ e e' H1 H2 Hx2 H3). inversion Hx1; subst; simpl. + eapply typed_binary_interp_Lam; eauto; + eapply bin_log_related_Lam; eauto; match goal with H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H) end. + eapply typed_binary_interp_App; eauto using typed_binary_interp. + eapply typed_binary_interp_App; eauto using typed_binary_interp. + eapply typed_binary_interp_Pair; eauto using typed_binary_interp. + eapply typed_binary_interp_Pair; eauto using typed_binary_interp. + eapply typed_binary_interp_Fst; eauto. + eapply typed_binary_interp_Snd; eauto. + eapply typed_binary_interp_InjL; eauto. + eapply typed_binary_interp_InjR; eauto. + eapply bin_log_related_App; eauto using binary_fundamental. + eapply bin_log_related_App; eauto using binary_fundamental. + eapply bin_log_related_Pair; eauto using binary_fundamental. + eapply bin_log_related_Pair; eauto using binary_fundamental. + eapply bin_log_related_Fst; eauto. + eapply bin_log_related_Snd; eauto. + eapply bin_log_related_InjL; eauto. + eapply bin_log_related_InjR; eauto. + match goal with H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst end. eapply typed_binary_interp_Case; eauto using typed_binary_interp; eapply bin_log_related_Case; eauto using binary_fundamental; match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. + match goal with H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst end. eapply typed_binary_interp_Case; eauto using typed_binary_interp; eapply bin_log_related_Case; eauto using binary_fundamental; try match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end; ... ... @@ -245,36 +245,33 @@ Section bin_log_related_under_typed_ctx. + match goal with H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst end. eapply typed_binary_interp_Case; eauto using typed_binary_interp; eapply bin_log_related_Case; eauto using binary_fundamental; try match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end; match goal with H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H) end. + eapply typed_binary_interp_If; eauto using typed_ctx_typed, typed_binary_interp. + eapply typed_binary_interp_If; eauto using typed_ctx_typed, typed_binary_interp. + eapply typed_binary_interp_If; eauto using typed_ctx_typed, typed_binary_interp. + eapply typed_binary_interp_nat_bin_op; eauto using typed_ctx_typed, typed_binary_interp. + eapply typed_binary_interp_nat_bin_op; eauto using typed_ctx_typed, typed_binary_interp. + eapply typed_binary_interp_Fold; eauto. + eapply typed_binary_interp_Unfold; eauto. + eapply typed_binary_interp_TLam; eauto with typeclass_instances. + eapply typed_binary_interp_TApp; eauto. + eapply typed_binary_interp_Fork; eauto. + eapply typed_binary_interp_Alloc; eauto. + eapply typed_binary_interp_Load; eauto. + eapply typed_binary_interp_Store; eauto using typed_binary_interp. + eapply typed_binary_interp_Store; eauto using typed_binary_interp. + eapply typed_binary_interp_CAS; eauto using typed_binary_interp. + eapply typed_binary_interp_CAS; eauto using typed_binary_interp. + eapply typed_binary_interp_CAS; eauto using typed_binary_interp. + eapply bin_log_related_If; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_If; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_If; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_nat_bin_op; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_nat_bin_op; eauto using typed_ctx_typed, binary_fundamental. + eapply bin_log_related_Fold; eauto. + eapply bin_log_related_Unfold; eauto. + eapply bin_log_related_TLam; eauto with typeclass_instances. + eapply bin_log_related_TApp; eauto. + eapply bin_log_related_Fork; eauto. + eapply bin_log_related_Alloc; eauto. + eapply bin_log_related_Load; eauto. + eapply bin_log_related_Store; eauto using binary_fundamental. + eapply bin_log_related_Store; eauto using binary_fundamental. + eapply bin_log_related_CAS; eauto using binary_fundamental. + eapply bin_log_related_CAS; eauto using binary_fundamental. + eapply bin_log_related_CAS; eauto using binary_fundamental. Unshelve. all: trivial. Qed. End bin_log_related_under_typed_ctx.
 ... ... @@ -253,13 +253,12 @@ Section CG_Counter. Definition counterN : namespace := nroot .@ "counter". Lemma FG_CG_counter_refinement Δ {HΔ : ctx_PersistentP Δ} : Lemma FG_CG_counter_refinement Δ {HΔ : env_PersistentP Δ} : Δ ∥ [] ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat). Proof. (* executing the preambles *) intros [|v vs] ρ j K [=]. cbn -[FG_counter CG_counter]. iIntros "(#Hheap & #Hspec & _ & Hj)". iIntros { [|??] ρ} "#(Hheap & Hspec & HΓ)"; iIntros {j K} "Hj"; last first. { iDestruct (interp_env_length with "HΓ") as %[=]. } iClear "HΓ". cbn -[FG_counter CG_counter]. rewrite ?empty_env_subst /CG_counter /FG_counter. iPvs (steps_newlock _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]") as {l} "[Hj Hl]"; eauto. ... ...
 ... ... @@ -12,15 +12,16 @@ Section Stack_refinement. Notation D := (prodC valC valC -n> iPropG lang Σ). Implicit Types Δ : listC D. Lemma FG_CG_counter_refinement Δ {HΔ : ctx_PersistentP Δ} : Lemma FG_CG_counter_refinement Δ {HΔ : env_PersistentP Δ} : Δ ∥ [] ⊨ FG_stack ≤log≤ CG_stack : TForall (TProd (TProd (TArrow (TVar 0) TUnit) (TArrow TUnit (TSum TUnit (TVar 0)))) (TArrow (TArrow (TVar 0) TUnit) TUnit)). Proof. (* executing the preambles *) iIntros { [|??] ρ j K [=] } "[#Hheap [#Hspec [_ Hj]]]". cbn -[FG_stack CG_stack]. iIntros { [|??] ρ} "#(Hheap & Hspec & HΓ)"; iIntros {j K} "Hj"; last first. { iDestruct (interp_env_length with "HΓ") as %[=]. } iClear "HΓ". cbn -[FG_stack CG_stack]. rewrite ?empty_env_subst /CG_stack /FG_stack. iApply wp_value; eauto. iExists (TLamV _); iFrame "Hj". ... ... @@ -29,8 +30,7 @@ Section Stack_refinement. iApply wp_TLam; iNext. iPvs (steps_newlock _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]") as {l} "[Hj Hl]"; eauto. rewrite fill_app; simpl. iFrame "Hspec Hj"; trivial. { rewrite fill_app; simpl. iFrame "Hspec Hj"; trivial. } rewrite fill_app; simpl. iPvs (step_lam _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto. simpl. ... ...
This diff is collapsed.
 ... ... @@ -15,36 +15,30 @@ Section typed_interp. Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]. Lemma typed_interp Δ Γ vs e τ (HΔ : ctx_PersistentP Δ) : Theorem fundamental Δ Γ vs e τ (HΔ : env_PersistentP Δ) : Γ ⊢ₜ e : τ → length Γ = length vs → heapI_ctx ∧ [∧] zip_with (λ τ, interp τ Δ) Γ vs ⊢ WP e.[env_subst vs] {{ interp τ Δ }}. heapI_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Proof. intros Htyped; revert Δ HΔ vs. induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ] /=". intros Htyped; revert Δ vs HΔ. induction Htyped; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=". - (* var *) destruct (lookup_lt_is_Some_2 vs x) as [v Hv]. { by rewrite -Hlen; apply lookup_lt_Some with τ. } 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; by simplify_option_eq. iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done. rewrite /env_subst. simplify_option_eq. by value_case. - (* unit *) value_case; trivial. - (* nat *) value_case; iExists _ ; trivial. - (* bool *) value_case; iExists _ ; trivial. - (* nat *) value_case; simpl; eauto. - (* bool *) value_case; simpl; eauto. - (* nat bin op *) smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHHtyped1. smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHHtyped2. iDestruct