Commit c1dac1db authored by Robbert's avatar Robbert

Merge branch 'robbert/logrel' into 'master'

Remove many variants of logical relations

See merge request iris/examples!35
parents b20ca674 d5a3435d
......@@ -34,39 +34,43 @@ This repository contains the following case studies:
* [barrier](theories/barrier): Implementation and proof of a barrier as
described in ["Higher-Order Ghost State"](http://doi.acm.org/10.1145/2818638).
* [logrel](theories/logrel): Logical relations from the
[IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
- STLC
- Unary logical relations proving type safety
- F_mu (System F with recursive types)
- Unary logical relations proving type safety
- F_mu_ref (System F with recursive types and references)
- Unary logical relations proving type safety
- Binary logical relations for proving contextual refinements
- F_mu_ref_conc (System F with recursive types, references and concurrency)
- Unary logical relations proving type safety
- Binary logical relations for proving contextual refinements
- Proof of refinement for a pair of fine-grained/coarse-grained
concurrent counter implementations
- Proof of refinement for a pair of fine-grained/coarse-grained
concurrent stack implementations
* [logrel_heaplang](theories/logrel_heaplang): A unary logical relation for
semantic typing of heap lang.
* [logrel](logrel): Logical relations.
- [logrel/stlc](theories/logrel/stlc): A unary logical relation for semantic
typing STLC (simply-typed lambda calculus) with De Bruijn indices (using
Autosubst).
- [logrel/F_mu_ref_conc](theories/logrel/F_mu_ref_conc): The logical relations
for F_mu_ref_conc (System F with recursive types, references and concurrency)
with De Bruijn indices (using Autosubst) from the
[IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
+ Unary logical relations proving type safety.
+ Binary logical relations for proving contextual refinements.
+ Proof of refinement for a pair of fine-grained/coarse-grained
concurrent counter implementations.
+ Proof of refinement for a pair of fine-grained/coarse-grained
concurrent stack implementations.
- [logrel/heaplang](theories/logrel/heaplang): A unary logical relation for
semantic typing of heap lang (by Robbert Krebbers).
* [logatom](theories/logrel_heaplang): Proofs of various logically atomic specifications:
- Elimination Stack (by Ralf Jung)
- Conditional increment (inspired by [this paper](https://people.mpi-sws.org/~dreyer/papers/relcon/paper.pdf)) and RDCSS (as in [this paper](https://timharris.uk/papers/2002-disc.pdf)) (by Marianna Rapoport, Rodolphe Lepigre and Gaurav Parthasarathy)
- [Herlihy-Wing-Queue](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf) (by Rodolphe Lepigre)
- Atomic Snapshot (by Marianna Rapoport)
- Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre)
- Flat Combiner (by Zhen Zhang, also see [this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs))
- Elimination Stack (by Ralf Jung).
- Conditional increment (inspired by [this paper](https://people.mpi-sws.org/~dreyer/papers/relcon/paper.pdf))
and RDCSS (as in [this paper](https://timharris.uk/papers/2002-disc.pdf))
(by Marianna Rapoport, Rodolphe Lepigre and Gaurav Parthasarathy).
- [Herlihy-Wing-Queue](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)
(by Rodolphe Lepigre).
- Atomic Snapshot (by Marianna Rapoport).
- Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre).
- Flat Combiner (by Zhen Zhang, also see
[this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs)).
* [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
algorithm by Amin Timany.
algorithm (by Amin Timany).
* [concurrent-stacks](theories/concurrent_stacks): Proof of an implementation of
concurrent stacks with helping by Daniel Gratzer et. al., as described in the
[report](http://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf).
* [lecture-notes](theories/lecture_notes): Coq examples for the
[Iris lecture notes](http://iris-project.org/tutorial-material.html).
* [hocap](theories/hocap): Formalisations of the concurrent bag and concurrent runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283). See the associated [README](theories/hocap/README.md).
* [hocap](theories/hocap): Formalizations of the concurrent bag and concurrent
runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283)
(by Dan Frumin). See the associated [README](theories/hocap/README.md).
## For Developers: How to update the Iris dependency
......
......@@ -37,30 +37,14 @@ theories/concurrent_stacks/concurrent_stack2.v
theories/concurrent_stacks/concurrent_stack3.v
theories/concurrent_stacks/concurrent_stack4.v
theories/logrel/prelude/base.v
theories/logrel/stlc/lang.v
theories/logrel/stlc/typing.v
theories/logrel/stlc/rules.v
theories/logrel/stlc/typing.v
theories/logrel/stlc/logrel.v
theories/logrel/stlc/fundamental.v
theories/logrel/stlc/soundness.v
theories/logrel/F_mu/lang.v
theories/logrel/F_mu/typing.v
theories/logrel/F_mu/rules.v
theories/logrel/F_mu/logrel.v
theories/logrel/F_mu/fundamental.v
theories/logrel/F_mu/soundness.v
theories/logrel/F_mu_ref/lang.v
theories/logrel/F_mu_ref/typing.v
theories/logrel/F_mu_ref/rules.v
theories/logrel/F_mu_ref/rules_binary.v
theories/logrel/F_mu_ref/logrel.v
theories/logrel/F_mu_ref/logrel_binary.v
theories/logrel/F_mu_ref/fundamental.v
theories/logrel/F_mu_ref/fundamental_binary.v
theories/logrel/F_mu_ref/soundness.v
theories/logrel/F_mu_ref/context_refinement.v
theories/logrel/F_mu_ref/soundness_binary.v
theories/logrel/stlc/fundamental.v
theories/logrel/F_mu_ref_conc/base.v
theories/logrel/F_mu_ref_conc/lang.v
theories/logrel/F_mu_ref_conc/rules.v
theories/logrel/F_mu_ref_conc/typing.v
......@@ -80,9 +64,9 @@ theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel_heaplang/ltyping.v
theories/logrel_heaplang/ltyping_safety.v
theories/logrel_heaplang/lib/symbol_adt.v
theories/logrel/heaplang/ltyping.v
theories/logrel/heaplang/ltyping_safety.v
theories/logrel/heaplang/lib/symbol_adt.v
theories/hocap/abstract_bag.v
theories/hocap/cg_bag.v
......
From iris_examples.logrel.F_mu Require Export logrel.
From iris.program_logic Require Import lifting.
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu Require Import rules.
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 := (valO -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.
erewrite env_subst_lookup; eauto. 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.
iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto.
+ iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
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.
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_interp_rec1_eq /=.
iAlways; eauto.
- (* Unfold *)
iApply (wp_bind (fill [UnfoldCtx]));
iApply wp_wand_l; iSplitL; [|iApply IHtyped; trivial].
iIntros (v) "#Hv /=". rewrite /= fixpoint_interp_rec1_eq.
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.
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris_examples.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 list Empty_set 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 stateO := leibnizO state.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO 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 of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (IntoVal _ _) =>
rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
Hint Extern 5 (AsVal _) => eexists; eapply of_to_val; fast_done : typeclass_instances.
Hint Extern 10 (AsVal _) =>
eexists; rewrite /IntoVal; eapply of_to_val; rewrite /= !to_of_val /=; solve [ eauto ] : typeclass_instances.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_examples.logrel.F_mu Require Export lang typing.
From iris.algebra Require Import list.
Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context `{irisG F_mu_lang Σ}.
Notation D := (valO -n> iPropO Σ).
Implicit Types τi : D.
Implicit Types Δ : listO D.
Implicit Types interp : listO D D.
Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper.
Definition interp_unit : listO D -n> D := λne Δ w, (w = UnitV)%I.
Program Definition interp_prod
(interp1 interp2 : listO D -n> D) : listO 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 : listO D -n> D) : listO 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 : listO D -n> D) : listO 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 : listO D -n> D) : listO 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 : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w,
( ( v, w = FoldV v interp (τi :: Δ) v))%I.
Global Instance interp_rec1_contractive
(interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
Proof. by solve_contractive. Qed.
Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
fixpoint (interp_rec1 interp Δ) x interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
Program Definition interp_rec (interp : listO D -n> D) : listO 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) : listO 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)
(Δ : listO D) (vs : list val) : iProp Σ :=
(length Γ = length vs [] zip_with (λ τ, τ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listO 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 fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently.
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. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
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. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..].
case EQ: (x - length Δ1) => [|n]; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
Lemma interp_subst Δ2 τ τ' v : τ ( τ' Δ2 :: Δ2) v τ.[τ'/] Δ2 v.
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 Δ : [] * Δ [].
Proof. iSplit; rewrite ?zip_with_nil_r; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.