Commit 26128ad3 authored by Robbert Krebbers's avatar Robbert Krebbers

Upgrade to Iris f69cdc8c.

parent 2463dae8
......@@ -3,28 +3,29 @@ From iris.proofmode Require Import tactics.
From iris_logrel.F_mu Require Import rules.
From iris.algebra Require Export upred_big_op.
Definition log_typed {Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
@env_PersistentP Σ Δ
Definition log_typed `{irisG lang Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
env_PersistentP Δ
Γ * Δ vs τ ⟧ₑ Δ e.[env_subst vs].
Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
Section fundamental.
Context {Σ : iFunctor}.
Notation D := (valC -n> iProp lang Σ).
Context `{irisG lang Σ}.
Notation D := (valC -n> iProp Σ).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply (wp_bind [ctx]);
iApply wp_wand_l;
iSplitL; [|iApply Hp; trivial]; cbn;
iIntros {v} Hv.
iIntros (v) Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ log_typed (Σ:=Σ) Γ e τ.
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ log_typed Γ e τ.
Proof.
induction 1; iIntros {Δ vs HΔ} "#HΓ"; cbn.
induction 1; iIntros (Δ vs HΔ) "#HΓ"; cbn.
- (* var *)
iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done.
iDestruct (interp_env_Some_l with "HΓ") as (v) "[% ?]"; first done.
rewrite /env_subst. simplify_option_eq. by value_case.
- (* unit *) value_case.
- (* pair *)
......@@ -33,11 +34,11 @@ Section fundamental.
value_case; eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
iApply wp_fst; eauto using to_of_val.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
iApply wp_snd; eauto using to_of_val.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn.
......@@ -48,7 +49,7 @@ Section fundamental.
- (* case *)
smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn.
iDestruct (interp_env_length with "HΓ") as %?.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; simplify_eq/=.
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 (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
......@@ -56,7 +57,7 @@ Section fundamental.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
- (* lam *)
value_case; iAlways; iIntros {w} "#Hw".
value_case; iAlways; iIntros (w) "#Hw".
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.
......@@ -67,25 +68,25 @@ Section fundamental.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case.
iAlways; iIntros { τi } "%". iApply wp_TLam; iNext.
iAlways; iIntros (τi) "%". iApply wp_tlam; iNext.
iApply IHtyped. by iApply interp_env_ren.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! ( τ' Δ)); iPureIntro; apply _|].
iIntros {w} "?". by rewrite interp_subst.
iIntros (w) "?". by rewrite interp_subst.
- (* Fold *)
iApply (@wp_bind _ _ _ [FoldCtx]);
iApply (wp_bind [FoldCtx]);
iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ vs); auto].
iIntros {v} "#Hv". value_case.
iIntros (v) "#Hv". value_case.
rewrite /= -interp_subst fixpoint_unfold /=.
iAlways; eauto.
- (* Unfold *)
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply (wp_bind [UnfoldCtx]);
iApply wp_wand_l; iSplitL; [|iApply IHtyped; trivial].
iIntros {v} "#Hv". rewrite /= fixpoint_unfold.
iIntros (v) "#Hv". rewrite /= fixpoint_unfold.
change (fixpoint _) with ( TRec τ Δ); simpl.
iDestruct "Hv" as {w} "#[% Hw]"; subst.
iApply wp_Fold; cbn; auto using to_of_val.
by rewrite -interp_subst.
iDestruct "Hv" as (w) "#[% Hw]"; subst; simpl.
iApply wp_fold. by rewrite to_of_val.
iNext. by rewrite -interp_subst.
Qed.
End fundamental.
From iris.program_logic Require Export ectx_language ectxi_language.
From iris.algebra Require Export cofe.
From iris_logrel.prelude Require Export base.
From iris.program_logic Require Import language.
Module lang.
Inductive expr :=
......@@ -76,8 +77,6 @@ Module lang.
| FoldCtx
| UnfoldCtx.
Notation ectx := (list ectx_item).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 => App e e2
......@@ -93,47 +92,35 @@ Module lang.
| FoldCtx => Fold e
| UnfoldCtx => Unfold e
end.
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
Definition state : Type := ().
Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
Inductive head_step : expr state expr state list expr Prop :=
(* β *)
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Lam e1) e2) σ e1.[e2/] σ None
head_step (App (Lam e1) e2) σ e1.[e2/] σ []
(* Products *)
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Fst (Pair e1 e2)) σ e1 σ None
head_step (Fst (Pair e1 e2)) σ e1 σ []
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Snd (Pair e1 e2)) σ e2 σ None
head_step (Snd (Pair e1 e2)) σ e2 σ []
(* Sums *)
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ None
head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ []
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ e σ None
head_step (Unfold (Fold e)) σ e σ []
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ e σ None.
(** Atomic expressions: we don't consider any atomic operations. *)
Definition atomic (e: expr) := false.
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
Inductive prim_step
(e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' e2 = fill K e2'
head_step e1' σ1 e2' σ2 ef prim_step e1 σ1 e2 σ2 ef.
head_step (TApp (TLam e)) σ e σ [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
......@@ -144,52 +131,20 @@ We could potentially make this a generic construction. *)
revert v; induction e; intros; simplify_option_eq; auto with f_equal.
Qed.
Instance: Inj (=) (=) of_val.
Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.
Instance ectx_fill_inj K : Inj (=) (=) (fill K).
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
Lemma fill_val K e : is_Some (to_val (fill K e)) is_Some (to_val e).
Proof.
intros [v' Hv']; revert v' Hv'.
induction K as [|[]]; intros; simplify_option_eq; eauto.
Qed.
Lemma fill_not_val K e : to_val e = None to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
Lemma values_head_stuck e1 σ1 e2 σ2 ef :
Lemma val_stuck e1 σ1 e2 σ2 ef :
head_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma values_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed.
Lemma atomic_not_val e : atomic e to_val e = None.
Proof. done. Qed.
Lemma atomic_fill K e : atomic (fill K e) to_val e = None K = [].
Proof. done. Qed.
Lemma atomic_head_step e1 σ1 e2 σ2 ef :
atomic e1 head_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof. done. Qed.
Lemma atomic_step e1 σ1 e2 σ2 ef :
atomic e1 prim_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof.
intros Hatomic [K e1' e2' -> -> Hstep].
assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck.
naive_solver eauto using atomic_head_step.
Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
head_step (fill_item Ki e) σ1 e2 σ2 ef is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
......@@ -204,53 +159,22 @@ We could potentially make this a generic construction. *)
end; auto.
Qed.
(* When something does a step, and another decomposition of the same expression
has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *)
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
fill K e1 = fill K' e1' to_val e1 = None head_step e1' σ1 e2 σ2 ef
K `prefix_of` K'.
Proof.
intros Hfill Hred Hnval; revert K' Hfill.
induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
destruct K' as [|Ki' K']; simplify_eq.
{ exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
[apply fill_not_val | eapply head_ctx_step_val; erewrite Hfill];
eauto using fill_not_val, head_ctx_step_val.
}
cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
eauto using fill_item_no_val_inj, values_head_stuck, fill_not_val.
Qed.
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
End lang.
(** Language *)
Program Canonical Structure lang : language := {|
expr := lang.expr; val := lang.val; state := lang.state;
Program Instance heap_ectxi_lang :
EctxiLanguage
(lang.expr) lang.val lang.ectx_item lang.state := {|
of_val := lang.of_val; to_val := lang.to_val;
atomic := lang.atomic; prim_step := lang.prim_step;
fill_item := lang.fill_item; head_step := lang.head_step
|}.
Solve Obligations with eauto using lang.to_of_val, lang.of_to_val,
lang.values_stuck, lang.atomic_not_val, lang.atomic_step.
Instance lang_ctx K : LanguageCtx lang (lang.fill K).
Proof.
split.
* eauto using lang.fill_not_val.
* intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (K ++ K') e1' e2'; rewrite ?lang.fill_app ?Heq1 ?Heq2.
* intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (lang.step_by_val
K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
rewrite lang.fill_app in Heq1; apply (inj _) in Heq1.
exists (lang.fill K' e2''); rewrite lang.fill_app; split; auto.
econstructor; eauto.
Qed.
lang.val_stuck, lang.fill_item_val, lang.fill_item_no_val_inj,
lang.head_ctx_step_val.
Instance lang_ctx_item Ki : LanguageCtx lang (lang.fill_item Ki).
Proof. change (LanguageCtx lang (lang.fill [Ki])). by apply _. Qed.
Canonical Structure lang := ectx_lang (lang.expr).
Export lang.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu Require Export lang typing.
From iris.algebra Require Import list upred_big_op.
Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context {Σ : iFunctor}.
Notation D := (valC -n> iProp lang Σ).
Context `{irisG lang Σ}.
Notation D := (valC -n> iProp Σ).
Implicit Types τi : D.
Implicit Types Δ : listC D.
Implicit Types interp : listC D D.
......@@ -45,15 +46,15 @@ Section logrel.
Global Instance interp_rec1_contractive
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
Proof.
intros n τi1 τi2 H w; cbn.
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.
apply later_contractive =>i Hi. by rewrite Hτi.
Qed.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
Next Obligation.
intros interp n Δ1 Δ2 H; apply fixpoint_ne => τi w. solve_proper.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
Qed.
Fixpoint interp (τ : type) : listC D -n> D :=
......@@ -69,11 +70,11 @@ Section logrel.
Notation "⟦ τ ⟧" := (interp τ).
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp lang Σ :=
(Δ : listC D) (vs : list val) : iProp Σ :=
(length Γ = length vs [] zip_with (λ τ, τ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp lang Σ :=
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
WP e {{ τ Δ }}%I.
Class env_PersistentP Δ :=
......@@ -97,7 +98,7 @@ Section logrel.
env_PersistentP Δ PersistentP ( Γ * Δ vs) := _.
Lemma interp_weaken Δ1 Π Δ2 τ :
τ.[iter (length Δ1) up (ren (+ length Π))] (Δ1 ++ Π ++ Δ2)
τ.[upn (length Δ1) (ren (+ length Π))] (Δ1 ++ Π ++ Δ2)
τ (Δ1 ++ Δ2).
Proof.
revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
......@@ -108,14 +109,13 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
change (uPredC (iResUR lang Σ)) with (iProp lang Σ).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
Lemma interp_subst_up Δ1 Δ2 τ τ' :
τ (Δ1 ++ interp τ' Δ2 :: Δ2)
τ.[iter (length Δ1) up (τ' .: ids)] (Δ1 ++ Δ2).
τ.[upn (length Δ1) (τ' .: ids)] (Δ1 ++ Δ2).
Proof.
revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl.
- done.
......@@ -126,11 +126,9 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
change (uPredC (iResUR lang Σ)) with (iProp lang Σ).
rewrite !lookup_app_r; [|lia ..].
destruct (x - length Δ1) as [|n] eqn:?; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
change (uPredC (iResUR lang Σ)) with (iProp lang Σ).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
......@@ -144,7 +142,7 @@ Section logrel.
Lemma interp_env_Some_l Δ Γ vs x τ :
Γ !! x = Some τ Γ * Δ vs v, vs !! x = Some v τ Δ v.
Proof.
iIntros {?} "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
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Γ").
......
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting.
From iris.program_logic Require Import ectx_lifting.
From iris_logrel.F_mu Require Export lang.
From iris.prelude Require Import fin_maps.
Section lang_rules.
Context {Σ : iFunctor}.
Implicit Types P : iProp lang Σ.
Implicit Types Q : val iProp lang Σ.
Context `{irisG lang Σ}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val iProp Σ.
Ltac inv_step :=
Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
| H : prim_step _ _ _ _ _ |- _ => destruct H; subst
| H : _ = fill ?K ?e |- _ =>
destruct K as [|[]];
simpl in H; first [subst e|discriminate H|injection H as H]
(* ensure that we make progress for each subgoal *)
| H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
apply values_head_stuck, (fill_not_val K) in H;
by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if e is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Ltac reshape_val e tac :=
let rec go e :=
match e with
| of_val ?v => v
| Pair ?e1 ?e2 =>
let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2)
| InjL ?e => let v := reshape_val e in constr:(InjLV v)
| InjR ?e => let v := reshape_val e in constr:(InjRV v)
end in let v := go e in first [tac v | fail 2].
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Ltac reshape_expr e tac :=
let rec go K e :=
match e with
| _ => tac (reverse K) e
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
| Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
| Fst ?e => go (FstCtx :: K) e
| Snd ?e => go (SndCtx :: K) e
| InjL ?e => go (InjLCtx :: K) e
| InjR ?e => go (InjRCtx :: K) e
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
end in go (@nil ectx_item) e.
Ltac do_step tac :=
try match goal with |- language.reducible _ _ => eexists _, _, _ end;
simpl;
match goal with
| |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
reshape_expr e1 ltac:(fun K e1' =>
eapply Ectx_step with K e1' _; [reflexivity|reflexivity|];
econstructor;
rewrite ?to_of_val; tac; fail)
| |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
econstructor;
rewrite ?to_of_val; tac; fail
end.
Local Hint Extern 1 => do_step auto.
Local Hint Extern 1 => inv_step.
Local Hint Constructors head_step.
Local Hint Resolve to_of_val.
(** Helper Lemmas for weakestpre. *)
Lemma wp_bind {E e} K Q :
WP e @ E {{ v, WP fill K (# v) @ E {{ Q }} }} WP fill K e @ E {{ Q }}.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (# v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
Lemma wp_lam E e1 e2 v Q :
to_val e2 = Some v
WP e1.[e2/] @ E {{ Q }} WP App (Lam e1) e2 @ E {{ Q }}.
Lemma wp_lam E e1 e2 v Φ :
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_step (App _ _) e1.[of_val v /] None) //=; auto.
- by rewrite right_id.
rewrite -(wp_lift_pure_det_head_step' (App _ _) e1.[of_val v /]); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_TLam E e Q : WP e @ E {{ Q }} WP TApp (TLam e) @ E {{ Q }}.
Lemma wp_tlam E e Φ : WP e @ E {{ Φ }} WP TApp (TLam e) @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_step (TApp _) e None) //=; auto.
- by rewrite right_id.
rewrite -(wp_lift_pure_det_head_step' (TApp _) e); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_Fold E e v Q :
to_val e = Some v Q v WP Unfold (Fold e) @ E {{ Q }}.
Lemma wp_fold E e v Φ :
to_val e = Some v (|={E}=> Φ v) WP Unfold (Fold e) @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Unfold _) (of_val v) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
rewrite -(wp_lift_pure_det_head_step' (Unfold _) (of_val v))
-?wp_value_pvs; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_fst E e1 v1 e2 v2 Q :
Lemma wp_fst E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Q v1 WP Fst (Pair e1 e2) @ E {{ Q }}.
(|={E}=> Φ v1) WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Fst (Pair _ _)) (of_val v1) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
intros ??. rewrite -(wp_lift_pure_det_head_step' (Fst _) e1)
-?wp_value_pvs; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_snd E e1 v1 e2 v2 Q :
Lemma wp_snd E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
Q v2 WP Snd (Pair e1 e2) @ E {{ Q }}.
(|={E}=> Φ v2) WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Snd (Pair _ _)) (of_val v2) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
intros ??. rewrite -(wp_lift_pure_det_head_step' (Snd _) e2)
-?wp_value_pvs; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_case_inl E e0 v0 e1 e2 Q :
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
to_val e0 = Some v0
WP e1.[e0/] @ E {{ Q }} WP Case (InjL e0) e1 e2 @ E {{ Q }}.
WP e1.[e0/] @ E {{ Φ }} WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjL _) _ _) (e1.[of_val v0/]) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
intros. rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (e1.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Q :
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
to_val e0 = Some v0
WP e2.[e0/] @ E {{ Q }} WP Case (InjR e0) e1 e2 @ E {{ Q }}.
WP e2.[e0/] @ E {{ Φ }} WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjR _) _ _) (e2.[of_val v0/]) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
intros. rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (e2.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
End lang_rules.
......@@ -2,22 +2,21 @@ From iris_logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Theorem soundness Σ e τ e' thp σ σ' :
log_typed (Σ:=Σ) [] e τ
rtc step ([e], σ) (e' :: thp, σ')
Theorem soundness Σ `{irisPreG lang Σ} e τ e' thp σ σ' :
( `{irisG lang Σ}, log_typed [] e τ)
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ?. eapply (wp_adequacy_reducible (λ _, True%I));
eauto using ucmra_unit_valid; last by constructor.
iIntros "_". rewrite -(empty_env_subst e).
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.
Qed.
Corollary type_soundness e τ e' thp σ σ' :
[] ⊢ₜ e : τ
rtc step ([e], σ) (e' :: thp, σ')
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
set (Σ := #[]).
intros Htyped. eapply (@soundness (globalF Σ)), fundamental, Htyped.
intros ??. set (Σ := #[irisΣ lang]).
eapply (soundness Σ); eauto using fundamental.
Qed.
......@@ -10,20 +10,20 @@ Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next leve
Section fundamental.
Context `{heapG Σ}.
Notation D := (valC -n> iPropG lang Σ).
Notation D := (valC -n> iProp Σ).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply (wp_bind [ctx]);
iApply wp_wand_l;
iSplitL; [|iApply Hp; trivial]; [iIntros {v} Hv|iSplit; trivial]; cbn.
iSplitL; [|iApply Hp; trivial]; [iIntros (v) Hv|iSplit; trivial]; cbn.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ Γ e : τ.
Proof.
induction 1; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=".
induction 1; iIntros (Δ vs HΔ) "#[Hheap HΓ] /=".
- (* var *)
iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done.
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 *)
......@@ -32,11 +32,11 @@ Section fundamental.
value_case; eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
iApply wp_fst; eauto using to_of_val.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
iDestruct "Hv" as (w1