Commit 6d458e00 authored by Dan Frumin's avatar Dan Frumin

Update stlc and F_mu to work with Iris 3.0

parent dad6c7ed
From iris.program_logic Require Export ectx_language ectxi_language.
From iris.algebra Require Export cofe.
From iris.algebra Require Export ofe.
From iris_logrel.prelude Require Export base.
Module lang.
......
......@@ -17,16 +17,16 @@ Section logrel.
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper_alt.
Definition interp_unit : listC D -n> D := λne Δ w, (w = UnitV)%I.
Definition interp_unit : listC D -n> D := λne Δ w, (w = UnitV)%I.
Program Definition interp_prod
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
( w1 w2, w = PairV w1 w2 interp1 Δ w1 interp2 Δ w2)%I.
( w1 w2, w = PairV w1 w2 interp1 Δ w1 interp2 Δ w2)%I.
Solve Obligations with solve_proper.
Program Definition interp_sum
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(( w1, w = InjLV w1 interp1 Δ w1) ( w2, w = InjRV w2 interp2 Δ w2))%I.
(( w1, w = InjLV w1 interp1 Δ w1) ( w2, w = InjRV w2 interp2 Δ w2))%I.
Solve Obligations with solve_proper.
Program Definition interp_arrow
......@@ -37,20 +37,17 @@ Section logrel.
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
( τi : D,
( v, PersistentP (τi v)) WP TApp (# w) {{ interp (τi :: Δ) }})%I.
⌜∀ v, PersistentP (τi v) WP TApp (# w) {{ interp (τi :: Δ) }})%I.
Solve Obligations with solve_proper.
Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
( ( v, w = FoldV v interp (τi :: Δ) v))%I.
( ( v, w = FoldV v interp (τi :: Δ) v))%I.
Global Instance interp_rec1_contractive
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
Proof.
intros n τi1 τi2 Hτi w; cbn.
apply always_ne, exist_ne; intros v; apply and_ne; trivial.
apply later_contractive =>i Hi. by rewrite Hτi.
Qed.
Proof. by solve_contractive. Qed.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
......@@ -72,7 +69,7 @@ Section logrel.
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp Σ :=
(length Γ = length vs [] zip_with (λ τ, τ Δ) Γ vs)%I.
(length Γ = length vs [] zip_with (λ τ, τ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
......@@ -110,7 +107,7 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
......@@ -130,18 +127,18 @@ Section logrel.
rewrite !lookup_app_r; [|lia ..].
destruct (x - length Δ1) as [|n] eqn:?; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
Lemma interp_subst Δ2 τ τ' : τ ( τ' Δ2 :: Δ2) τ.[τ'/] Δ2.
Proof. apply (interp_subst_up []). Qed.
Lemma interp_env_length Δ Γ vs : Γ * Δ vs length Γ = length 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.
Γ !! x = Some τ Γ * Δ vs v, vs !! x = Some v τ Δ v.
Proof.
iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
......@@ -156,7 +153,7 @@ Section logrel.
Lemma interp_env_cons Δ Γ vs τ v :
τ :: Γ * Δ (v :: vs) ⊣⊢ τ Δ v Γ * Δ vs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
Qed.
......
......@@ -33,13 +33,13 @@ Section lang_rules.
to_val e2 = Some v WP e1.[e2 /] @ E {{ Φ }} WP App (Lam e1) e2 @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_head_step' (App _ _) e1.[of_val v /]); eauto.
rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _) e1.[of_val v /]); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_tlam E e Φ : WP e @ E {{ Φ }} WP TApp (TLam e) @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step' (TApp _) e); eauto.
rewrite -(wp_lift_pure_det_head_step_no_fork (TApp _) e); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -47,7 +47,7 @@ Section lang_rules.
to_val e = Some v (|={E}=> Φ v) WP Unfold (Fold e) @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_head_step' (Unfold _) (of_val v))
rewrite -(wp_lift_pure_det_head_step_no_fork (Unfold _) (of_val v))
-?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -56,7 +56,7 @@ Section lang_rules.
to_val e1 = Some v1 to_val e2 = Some v2
(|={E}=> Φ v1) WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ??. rewrite -(wp_lift_pure_det_head_step' (Fst _) e1)
intros ??. rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1)
-?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -65,7 +65,7 @@ Section lang_rules.
to_val e1 = Some v1 to_val e2 = Some v2
(|={E}=> Φ v2) WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ??. rewrite -(wp_lift_pure_det_head_step' (Snd _) e2)
intros ??. rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2)
-?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -74,7 +74,7 @@ Section lang_rules.
to_val e0 = Some v0
WP e1.[e0/] @ E {{ Φ }} WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (e1.[e0/])); eauto.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (e1.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -82,7 +82,7 @@ Section lang_rules.
to_val e0 = Some v0
WP e2.[e0/] @ E {{ Φ }} WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (e2.[e0/])); eauto.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (e2.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
End lang_rules.
......@@ -2,14 +2,20 @@ From iris_logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Theorem soundness Σ `{irisPreG lang Σ} e τ e' thp σ σ' :
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
( `{irisG lang Σ}, log_typed [] e τ)
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??. cut (adequate e σ (λ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ); iIntros (?) "Hσ". rewrite -(empty_env_subst e).
iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto. by iApply interp_env_nil.
eapply (wp_adequacy Σ); eauto.
iIntros (Hinv).
iModIntro. iExists (λ _, True%I). iSplitR;eauto.
rewrite -(empty_env_subst e).
set (HΣ := IrisG () _ Hinv (fun _ => True)%I).
iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto.
by iApply interp_env_nil.
Qed.
Corollary type_soundness e τ e' thp σ σ' :
......@@ -17,6 +23,6 @@ Corollary type_soundness e τ e' thp σ σ' :
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros ??. set (Σ := #[irisΣ state]).
intros ??. set (Σ := invΣ).
eapply (soundness Σ); eauto using fundamental.
Qed.
......@@ -7,10 +7,10 @@ Context `{irisG lang Σ}.
Fixpoint interp (τ : type) (w : val) : iProp Σ :=
match τ with
| TUnit => w = UnitV
| TProd τ1 τ2 => w1 w2, w = PairV w1 w2 τ1 w1 τ2 w2
| TUnit => w = UnitV
| TProd τ1 τ2 => w1 w2, w = PairV w1 w2 τ1 w1 τ2 w2
| TSum τ1 τ2 =>
( w1, w = InjLV w1 τ1 w1) ( w2, w = InjRV w2 τ2 w2)
( w1, w = InjLV w1 τ1 w1) ( w2, w = InjRV w2 τ2 w2)
| TArrow τ1 τ2 => v, τ1 v WP App (# w) (# v) {{ τ2 }}
end%I
where "⟦ τ ⟧" := (interp τ).
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Import ectx_lifting.
From iris_logrel.stlc Require Export lang.
From iris.prelude Require Import fin_maps.
......@@ -33,7 +34,7 @@ Section lang_rules.
to_val e2 = Some v WP e1.[e2 /] @ E {{ Φ }} WP App (Lam e1) e2 @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_head_step' (App _ _) e1.[of_val v /]); eauto.
rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _) e1.[of_val v /]); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -41,7 +42,7 @@ Section lang_rules.
to_val e1 = Some v1 to_val e2 = Some v2
(|={E}=> Φ v1) WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ??. rewrite -(wp_lift_pure_det_head_step' (Fst _) e1)
intros ??. rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1)
-?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -50,7 +51,7 @@ Section lang_rules.
to_val e1 = Some v1 to_val e2 = Some v2
(|={E}=> Φ v2) WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros ??. rewrite -(wp_lift_pure_det_head_step' (Snd _) e2)
intros ??. rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2)
?right_id -?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -59,7 +60,7 @@ Section lang_rules.
to_val e0 = Some v0
WP e1.[e0/] @ E {{ Φ }} WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros ?. rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (e1.[e0/])); eauto.
intros ?. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (e1.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
......@@ -67,7 +68,8 @@ Section lang_rules.
to_val e0 = Some v0
WP e2.[e0/] @ E {{ Φ }} WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros ?. rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (e2.[e0/])); eauto.
intros ?. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (e2.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
End lang_rules.
......@@ -8,12 +8,20 @@ Proof.
iIntros (?) "". rewrite -(empty_env_subst e). iApply fundamental; eauto.
Qed.
Definition Σ := invΣ.
Theorem soundness e τ e' thp :
[] ⊢ₜ e : τ rtc step ([e], ()) (thp, ()) e' thp
is_Some (to_val e') reducible e' ().
Proof.
intros. set (Σ := #[irisΣ state]).
intros.
cut (adequate e () (λ _, True)); first (intros [_ Hsafe]; eauto).
eapply (wp_adequacy Σ); iIntros (?) "Hσ".
iApply wp_wand_l; iSplitR; [|by iApply wp_soundness]; eauto.
eapply (wp_adequacy Σ _). iIntros (Hinv).
iModIntro.
iExists (fun _ => True%I).
iSplitR; eauto.
set (HΣ := IrisG () _ Hinv (fun _ => True)%I).
iApply wp_wand_l.
iSplitR; [|by iApply wp_soundness]; eauto.
Qed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment