Skip to content

R
ReLoC-v1
Commit 2f06623a authored by Dan Frumin's avatar Dan Frumin Committed by Dan Frumin
Browse files
Options

Initial port of the codebase to explicit name. 

We are switich away from De Bruijn indices because
1) it's hard to read terms with De Bruijn indices
2) they are making lots of things slower
parent e5f52af7
Hide whitespace changes
Inline Side-by-side
Showing with 2718 additions and 4550 deletions
F_mu/fundamental.v deleted 100644 → 0
View file @ e5f52af7
From iris_logrel.F_mu Require Export logrel.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu Require Import rules.
From iris.base_logic Require Export big_op.
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 `{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_wand with "[-]"); [iApply Hp; trivial|]; cbn;
iIntros (v) Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ.
Proof.
induction 1; iIntros (Δ vs HΔ) "#HΓ"; cbn.
- (* var *)
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" IHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
value_case; eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
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.
iApply wp_snd; eauto using to_of_val.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn.
value_case; eauto.
- (* injr *)
smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn.
value_case; eauto.
- (* 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/=.
+ 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.
+ iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto.
- (* lam *)
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.
iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case.
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.
- (* Fold *)
iApply (wp_bind [FoldCtx]);
iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ 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 IHtyped; trivial].
iIntros (v) "#Hv". rewrite /= fixpoint_unfold.
change (fixpoint _) with (⟦ TRec τ ⟧ Δ); simpl.
iDestruct "Hv" as (w) "#[% Hw]"; subst; simpl.
iApply wp_fold. by rewrite to_of_val.
iNext. by rewrite -interp_subst.
Qed.
End fundamental.
F_mu/lang.v deleted 100644 → 0
View file @ e5f52af7
From iris.program_logic Require Export ectx_language ectxi_language.
From iris.algebra Require Export ofe.
From iris_logrel.prelude Require Export base.
Module lang.
Inductive expr :=
| Var (x : var)
| Lam (e : {bind 1 of expr})
| App (e1 e2 : expr)
(* Unit *)
| Unit
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
(* Recursive Types *)
| Fold (e : expr)
| Unfold (e : expr)
(* Polymorphic Types *)
| TLam (e : expr)
| TApp (e : expr).
Instance Ids_expr : Ids expr. derive. Defined.
Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
Inductive val :=
| LamV (e : {bind 1 of expr})
| TLamV (e : {bind 1 of expr})
| UnitV
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
| FoldV (v : val).
Fixpoint of_val (v : val) : expr :=
match v with
| LamV e => Lam e
| TLamV e => TLam e
| UnitV => Unit
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| FoldV v => Fold (of_val v)
end.
Notation "# v" := (of_val v) (at level 20).
Fixpoint to_val (e : expr) : option val :=
match e with
| Lam e => Some (LamV e)
| TLam e => Some (TLamV e)
| Unit => Some UnitV
| Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
| InjL e => InjLV <$> to_val e
| InjR e => InjRV <$> to_val e
| Fold e => v ← to_val e; Some (FoldV v)
| _ => None
end.
(** Evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
| TAppCtx
| PairLCtx (e2 : expr)
| PairRCtx (v1 : val)
| FstCtx
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
| FoldCtx
| UnfoldCtx.
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 => App e e2
| AppRCtx v1 => App (of_val v1) e
| TAppCtx => TApp e
| PairLCtx e2 => Pair e e2
| PairRCtx v1 => Pair (of_val v1) e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| FoldCtx => Fold e
| UnfoldCtx => Unfold e
end.
Definition state : Type := ().
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/] σ []
(* Products *)
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
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 σ []
(* Sums *)
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
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/] σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v →
head_step (Unfold (Fold e)) σ e σ []
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ e σ [].
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof. by induction v; simplify_option_eq. Qed.
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof.
revert v; induction e; intros; simplify_option_eq; auto with f_equal.
Qed.
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.
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 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.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
Proof.
destruct Ki1, Ki2; intros; try discriminate; simplify_eq;
repeat match goal with
| H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
end; auto.
Qed.
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
End lang.
(** Language *)
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;
fill_item := lang.fill_item; head_step := lang.head_step
|}.
Solve Obligations with eauto using lang.to_of_val, lang.of_to_val,
lang.val_stuck, lang.fill_item_val, lang.fill_item_no_val_inj,
lang.head_ctx_step_val.
Canonical Structure lang := ectx_lang (lang.expr).
Export lang.
F_mu/logrel.v deleted 100644 → 0
View file @ e5f52af7
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.
From iris.base_logic Require Import big_op.
Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context `{irisG lang Σ}.
Notation D := (valC -n> iProp Σ).
Implicit Types τi : D.
Implicit Types Δ : listC D.
Implicit Types interp : listC D → D.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
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.
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.
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.
Solve Obligations with solve_proper.
Program Definition interp_arrow
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(□ ∀ v, interp1 Δ v → WP App (# w) (# v) {{ interp2 Δ }})%I.
Solve Obligations with solve_proper.
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.
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.
Global Instance interp_rec1_contractive
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
Proof. by solve_contractive. 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.
Qed.
Fixpoint interp (τ : type) : listC D -n> D :=
match τ return _ with
| TUnit => interp_unit
| TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2)
| TSum τ1 τ2 => interp_sum (interp τ1) (interp τ2)
| TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2)
| TVar x => ctx_lookup x
| TForall τ' => interp_forall (interp τ')
| TRec τ' => interp_rec (interp τ')
end%I.
Notation "⟦ τ ⟧" := (interp τ).
Definition interp_env (Γ : list type)
(Δ : 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 Σ :=
WP e {{ ⟦ τ ⟧ Δ }}%I.
Class env_PersistentP Δ :=
ctx_persistentP : Forall (λ τi, ∀ v, PersistentP (τi v)) Δ.
Global Instance ctx_persistent_nil : env_PersistentP [].
Proof. by constructor. Qed.
Global Instance ctx_persistent_cons τi Δ :
(∀ v, PersistentP (τi v)) → env_PersistentP Δ → env_PersistentP (τi :: Δ).
Proof. by constructor. Qed.
Global Instance ctx_persistent_lookup Δ x v :
env_PersistentP Δ → PersistentP (ctx_lookup x Δ v).
Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
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 τ :
⟦ τ.[upn (length Δ1) (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.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi w /=.
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.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
Lemma interp_subst_up Δ1 Δ2 τ τ' :
⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2)
≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2).
Proof.
revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl.
- done.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
- apply fixpoint_proper=> τi w /=.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
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.
- 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⌝.
Proof. by iIntros "[% ?]". Qed.
Lemma interp_env_Some_l Δ Γ vs x τ :
Γ !! 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].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
iExists v; iSplit. done. iApply (big_sep_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 sep_proper; [apply pure_proper; omega|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
⟦ subst (ren (+1)) <$> Γ ⟧* (τi :: Δ) vs ⊣⊢ ⟦ Γ ⟧* Δ vs.
Proof.
apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
Qed.
End logrel.
Notation "⟦ τ ⟧" := (interp τ).
Notation "⟦ τ ⟧ₑ" := (interp_expr τ).
Notation "⟦ Γ ⟧*" := (interp_env Γ).
F_mu/rules.v deleted 100644 → 0
View file @ e5f52af7
From iris.program_logic Require Export weakestpre.
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 `{irisG lang Σ}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val → iProp Σ.
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 : 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
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Local Hint Constructors head_step.
Local Hint Resolve to_of_val.
(** Helper Lemmas for weakestpre. *)
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 Φ :
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_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_no_fork (TApp _) e); eauto.
intros; inv_head_step; eauto.
Qed.
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_head_step_no_fork (Unfold _) (of_val v))
-?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_fst E e1 v1 e2 v2 Φ :
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_no_fork (Fst _) e1)
-?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_snd E e1 v1 e2 v2 Φ :
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_no_fork (Snd _) e2)
-?wp_value_fupd; eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
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_no_fork (Case _ _ _) (e1.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
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_no_fork (Case _ _ _) (e2.[e0/])); eauto.
intros; inv_head_step; eauto.
Qed.
End lang_rules.
F_mu/soundness.v deleted 100644 → 0
View file @ e5f52af7
From iris_logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
(∀ `{irisG lang Σ}, [] ⊨ 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 Σ); eauto.
iIntros (Hinv). iModIntro. iExists (λ _, True%I). iSplit=> //.
rewrite -(empty_env_subst e).
set (HΣ := IrisG _ _ Hinv (λ _, True)%I).
iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
Qed.
Corollary type_soundness e τ e' thp σ σ' :
[] ⊢ₜ e : τ →
rtc step ([e], σ) (thp, σ') → e' ∈ thp →
is_Some (to_val e') ∨ reducible e' σ'.
Proof.
intros ??. set (Σ := invΣ).
eapply (soundness Σ); eauto using fundamental.
Qed.
F_mu/typing.v deleted 100644 → 0
View file @ e5f52af7
From iris_logrel.F_mu Require Export lang.
Inductive type :=
| TUnit : type
| TProd : type → type → type
| TSum : type → type → type
| TArrow : type → type → type
| TRec (τ : {bind 1 of type})
| TVar (x : var)
| TForall (τ : {bind 1 of type}).
Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Inductive typed (Γ : list type) : expr → type → Prop :=
| Var_typed x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ
| Unit_typed : Γ ⊢ₜ Unit : TUnit
| Pair_typed e1 e2 τ1 τ2 :
Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 → Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2
| Fst_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Fst e : τ1
| Snd_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Snd e : τ2
| InjL_typed e τ1 τ2 : Γ ⊢ₜ e : τ1 → Γ ⊢ₜ InjL e : TSum τ1 τ2
| InjR_typed e τ1 τ2 : Γ ⊢ₜ e : τ2 → Γ ⊢ₜ InjR e : TSum τ1 τ2
| Case_typed e0 e1 e2 τ1 τ2 ρ :
Γ ⊢ₜ e0 : TSum τ1 τ2 → τ1 :: Γ ⊢ₜ e1 : ρ → τ2 :: Γ ⊢ₜ e2 : ρ →
Γ ⊢ₜ Case e0 e1 e2 : ρ
| Lam_typed e τ1 τ2 : τ1 :: Γ ⊢ₜ e : τ2 → Γ ⊢ₜ Lam e : TArrow τ1 τ2
| 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 τ : Γ ⊢ₜ e : τ.[TRec τ/] → Γ ⊢ₜ Fold e : TRec τ
| TUnfold e τ : Γ ⊢ₜ e : TRec τ → Γ ⊢ₜ Unfold e : τ.[TRec τ/]
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
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 (∀ 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.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
Δ ⊢ₜ e : τ → length Δ = S (length ws) →
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2. rewrite /env_subst.
eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' ?]; first omega.
by simplify_option_eq.
Qed.
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
F_mu_ref/context_refinement.v deleted 100644 → 0
View file @ e5f52af7
From iris_logrel.F_mu_ref Require Export fundamental_binary.
Inductive ctx_item :=
| CTX_Lam
| CTX_AppL (e2 : expr)
| CTX_AppR (e1 : expr)
(* Products *)
| CTX_PairL (e2 : expr)
| CTX_PairR (e1 : expr)
| CTX_Fst
| CTX_Snd
(* Sums *)
| CTX_InjL
| CTX_InjR
| CTX_CaseL (e1 : expr) (e2 : expr)
| CTX_CaseM (e0 : expr) (e2 : expr)
| CTX_CaseR (e0 : expr) (e1 : expr)
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
(* Polymorphic Types *)
| CTX_TLam
| CTX_TApp
(* Reference Types *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr).