Skip to content

GitLab

Commit 61a4a07a authored by Amin Timany's avatar Amin Timany
Browse files

Add iris-logrel to examples

parent 2e5b9a6d
Hide whitespace changes
Inline Side-by-side
_CoqProject
View file @ 61a4a07a
......@@ -6,3 +6,45 @@ theories/barrier/barrier.v
theories/barrier/protocol.v
theories/barrier/example_client.v
theories/barrier/example_joining_existentials.v
theories/iris_logrel/prelude/base.v
theories/iris_logrel/stlc/lang.v
theories/iris_logrel/stlc/typing.v
theories/iris_logrel/stlc/rules.v
theories/iris_logrel/stlc/logrel.v
theories/iris_logrel/stlc/fundamental.v
theories/iris_logrel/stlc/soundness.v
theories/iris_logrel/F_mu/lang.v
theories/iris_logrel/F_mu/typing.v
theories/iris_logrel/F_mu/rules.v
theories/iris_logrel/F_mu/logrel.v
theories/iris_logrel/F_mu/fundamental.v
theories/iris_logrel/F_mu/soundness.v
theories/iris_logrel/F_mu_ref/lang.v
theories/iris_logrel/F_mu_ref/typing.v
theories/iris_logrel/F_mu_ref/rules.v
theories/iris_logrel/F_mu_ref/rules_binary.v
theories/iris_logrel/F_mu_ref/logrel.v
theories/iris_logrel/F_mu_ref/logrel_binary.v
theories/iris_logrel/F_mu_ref/fundamental.v
theories/iris_logrel/F_mu_ref/fundamental_binary.v
theories/iris_logrel/F_mu_ref/soundness.v
theories/iris_logrel/F_mu_ref/context_refinement.v
theories/iris_logrel/F_mu_ref/soundness_binary.v
theories/iris_logrel/F_mu_ref_conc/lang.v
theories/iris_logrel/F_mu_ref_conc/rules.v
theories/iris_logrel/F_mu_ref_conc/typing.v
theories/iris_logrel/F_mu_ref_conc/logrel_unary.v
theories/iris_logrel/F_mu_ref_conc/fundamental_unary.v
theories/iris_logrel/F_mu_ref_conc/rules_binary.v
theories/iris_logrel/F_mu_ref_conc/logrel_binary.v
theories/iris_logrel/F_mu_ref_conc/fundamental_binary.v
theories/iris_logrel/F_mu_ref_conc/soundness_unary.v
theories/iris_logrel/F_mu_ref_conc/context_refinement.v
theories/iris_logrel/F_mu_ref_conc/soundness_binary.v
theories/iris_logrel/F_mu_ref_conc/examples/lock.v
theories/iris_logrel/F_mu_ref_conc/examples/counter.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/refinement.v
\ No newline at end of file
theories/iris_logrel/F_mu/fundamental.v 0 → 100644
View file @ 61a4a07a
From iris_examples.iris_logrel.F_mu Require Export logrel.
From iris.program_logic Require Import lifting.
From iris.proofmode Require Import tactics.
From iris_examples.iris_logrel.F_mu Require Import rules.
From iris.base_logic Require Export big_op.
Definition log_typed `{irisG F_mu_lang Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs,
env_Persistent Δ →
⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs].
Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level).
Section fundamental.
Context `{irisG F_mu_lang Σ}.
Notation D := (valC -n> iProp Σ).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind (fill[ctx]));
iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
iIntros (v) Hv.
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 iApply wp_value.
- (* unit *) by iApply wp_value.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2.
iApply wp_value; eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
simpl. iApply wp_pure_step_later; auto. by iApply wp_value.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
simpl. iApply wp_pure_step_later; eauto. by iApply wp_value.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn.
iApply wp_value; eauto.
- (* injr *)
smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn.
iApply wp_value; 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_pure_step_later; auto; asimpl. iNext.
erewrite typed_subst_head_simpl by naive_solver.
iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+ iApply wp_pure_step_later; 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 *)
iApply wp_value; simpl; iAlways; iIntros (w) "#Hw".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; 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 *)
iApply wp_value; simpl.
iAlways; iIntros (τi) "%". iApply wp_pure_step_later; auto. 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 *)
smart_wp_bind FoldCtx v "#Hv" IHtyped; cbn. iApply wp_value.
rewrite /= -interp_subst fixpoint_unfold /=.
iAlways; eauto.
- (* Unfold *)
iApply (wp_bind (fill [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_pure_step_later; auto. iApply wp_value; iNext.
by rewrite -interp_subst.
Qed.
End fundamental.
theories/iris_logrel/F_mu/lang.v 0 → 100644
View file @ 61a4a07a
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris_examples.iris_logrel.prelude Require Export base.
Module F_mu.
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.
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Proof.
split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
End F_mu.
(** Language *)
Canonical Structure F_mu_ectxi_lang := EctxiLanguage F_mu.lang_mixin.
Canonical Structure F_mu_ectx_lang := EctxLanguageOfEctxi F_mu_ectxi_lang.
Canonical Structure F_mu_lang := LanguageOfEctx F_mu_ectx_lang.
Export F_mu.
Hint Extern 20 (PureExec _ _ _) => progress simpl : typeclass_instances.
Hint Extern 5 (IntoVal _ _) => eapply to_of_val : typeclass_instances.
Hint Extern 10 (IntoVal _ _) =>
rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
Hint Extern 5 (AsVal _) => eexists; eapply to_of_val : typeclass_instances.
Hint Extern 10 (AsVal _) =>
eexists; rewrite /IntoVal /= ?to_of_val /=; eauto : typeclass_instances.
\ No newline at end of file
theories/iris_logrel/F_mu/logrel.v 0 → 100644
View file @ 61a4a07a
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_examples.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 F_mu_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 repeat intros ?; simpl; 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 repeat intros ?; simpl; 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 repeat intros ?; simpl; solve_proper.
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
(□ ∀ τi : D,
⌜∀ v, Persistent (τi v)⌝ → WP TApp (# w) {{ interp (τi :: Δ) }})%I.
Solve Obligations with repeat intros ?; simpl; 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_Persistent Δ :=
ctx_persistent : Forall (λ τi, ∀ v, Persistent (τi v)) Δ.
Global Instance ctx_persistent_nil : env_Persistent [].
Proof. by constructor. Qed.
Global Instance ctx_persistent_cons τi Δ :
(∀ v, Persistent (τi v)) → env_Persistent Δ → env_Persistent (τi :: Δ).
Proof. by constructor. Qed.
Global Instance ctx_persistent_lookup Δ x v :
env_Persistent Δ → Persistent (ctx_lookup x Δ v).
Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
Global Instance interp_persistent τ Δ v :
env_Persistent Δ → Persistent (⟦ τ ⟧ Δ v) := _.
Proof.
revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _.
rewrite /Persistent /interp_rec fixpoint_unfold /interp_rec1 /=.
by apply persistently_intro'.
Qed.
Global Instance interp_env_base_persistent Δ Γ vs :
env_Persistent Δ → TCForall Persistent (zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs).
Proof.
intros HΔ. revert vs.
induction Γ => vs; simpl; destruct vs; constructor; apply _.
Qed.
Global Instance interp_env_persistent Γ Δ vs :
env_Persistent Δ → Persistent (⟦ Γ ⟧* Δ 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_sepL_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 Δ : (⟦ [] ⟧* Δ [])%I.
Proof. iSplit; rewrite ?zip_with_nil_r; 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 Γ).
theories/iris_logrel/F_mu/rules.v 0 → 100644
View file @ 61a4a07a
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From iris_examples.iris_logrel.F_mu Require Export lang.
From stdpp Require Import fin_maps.
Section lang_rules.
Context `{irisG F_mu_lang Σ}.
Implicit Types e : expr.
Ltac inv_head_step :=
repeat match goal with
| 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.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
unfold IntoVal, AsVal in *; subst;
repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].