Commit 01db92e2 authored by Robbert Krebbers's avatar Robbert Krebbers

Update to new version of Iris.

parent e045456d
......@@ -8,43 +8,10 @@ Import uPred.
Section typed_interp.
Context {Σ : iFunctor}.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_ : ?A, _) => let W := fresh "W" in evar (W : A); iExists W; unfold W; clear W
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => iNext
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => eapply (@always_intro _ _ _ _)
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial]; cbn;
eapply (@always_intro _ _ _ _);
iApply wp_wand_l;
iSplitL; [|iApply Hp; trivial]; cbn;
iIntros {v} Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
......@@ -53,8 +20,8 @@ Section typed_interp.
(Htyped : typed Γ e τ)
(HΔ : context_interp_Persistent Δ)
: List.length Γ = List.length vs
Π∧ zip_with (λ τ v, interp τ Δ v) Γ vs
WP (e.[env_subst vs]) @ {{ λ v, (@interp Σ) τ Δ v }}.
[] zip_with (λ τ v, interp τ Δ v) Γ vs
WP e.[env_subst vs] {{ λ v, (@interp Σ) τ Δ v }}.
Proof.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#HΓ"; cbn.
......@@ -69,75 +36,66 @@ Section typed_interp.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
value_case; eauto 10 with itauto.
value_case; eauto 10.
- (* fst *)
smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H; cbn.
iApply wp_fst; try iNext; eauto using to_of_val; cbn.
iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
iApply wp_fst; eauto using to_of_val.
- (* snd *)
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
iApply wp_snd; try iNext; eauto using to_of_val.
iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst.
iApply wp_snd; eauto using to_of_val.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
value_case; iLeft; auto with itauto.
value_case; eauto.
- (* injr *)
smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn.
value_case; iRight; auto with itauto.
value_case; eauto.
- (* case *)
smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
iDestruct "Hv" as "[Hv|Hv]";
iDestruct "Hv" as {w} "[% Hw]"; rewrite H;
[iApply wp_case_inl|iApply wp_case_inr];
auto 1 using to_of_val;
asimpl;
[specialize (IHHtyped2 Δ HΔ (w::vs)) |
specialize (IHHtyped3 Δ HΔ (w::vs))];
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
[iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto.
iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; subst.
+ iApply wp_case_inl; auto 1 using to_of_val; asimpl.
specialize (IHHtyped2 Δ HΔ (w::vs)).
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
iNext; iApply IHHtyped2; cbn; auto.
+ iApply wp_case_inr; auto 1 using to_of_val; asimpl.
specialize (IHHtyped3 Δ HΔ (w::vs)).
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
iNext; iApply IHHtyped3; cbn; auto.
- (* lam *)
value_case; apply (always_intro _ _); iIntros {w} "#Hw".
value_case; iAlways; iIntros {w} "#Hw".
iApply wp_lam; auto 1 using to_of_val.
asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
iNext; iApply (IHHtyped Δ HΔ (w :: vs)); cbn; auto with itauto.
iNext; iApply (IHHtyped Δ HΔ (w :: vs)); cbn; auto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto with itauto.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case.
iIntros {τi}; destruct τi as [τi τiPr]. iAlways.
iApply wp_TLam; iNext; simpl in *.
iIntros { [τi τiPr] } "!". iApply wp_TLam; iNext; simpl in *.
iApply IHHtyped; [rewrite map_length|]; trivial.
iRevert "HΓ".
rewrite zip_with_context_interp_subst.
iIntros "#HΓ"; trivial.
rewrite zip_with_context_interp_subst; trivial.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
iSpecialize ("Hv" $! ((interp τ' Δ) _)); cbn.
unshelve iSpecialize ("Hv" $! ((interp τ' Δ) _)); try apply _; cbn.
iApply always_elim. iApply always_mono; [|trivial].
apply wp_mono => w. by rewrite interp_subst.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
iApply wp_impl_l.
iSplit; [eapply (@always_intro _ _ _ _)|
iApply (IHHtyped (extend_context_interp ((interp (TRec τ)) Δ) Δ));
iApply wp_wand_l.
iSplitL; [|iApply (IHHtyped (extend_context_interp ((interp (TRec τ)) Δ) Δ));
trivial].
+ iIntros {v} "#Hv".
value_case.
change (fixpoint _) with (interp (TRec τ) Δ) at 1; trivial.
rewrite fixpoint_unfold; cbn.
auto with itauto.
iAlways; eauto.
+ iRevert "HΓ"; rewrite zip_with_context_interp_subst; iIntros "#HΓ"; trivial.
- (* Unfold *)
iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_impl_l;
iSplit; [eapply (@always_intro _ _ _ _)|
iApply IHHtyped;
trivial].
iApply wp_wand_l; iSplitL; [|iApply IHHtyped; trivial].
iIntros {v}.
cbn [interp interp_rec cofe_mor_car].
rewrite fixpoint_unfold.
......@@ -146,9 +104,5 @@ Section typed_interp.
iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
iApply wp_Fold; cbn; auto using to_of_val.
rewrite -interp_subst; trivial.
(* unshelving *)
Unshelve.
cbn; typeclasses eauto.
Qed.
End typed_interp.
\ No newline at end of file
End typed_interp.
......@@ -221,6 +221,9 @@ other words, [e] also contains the reducible expression *)
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 *)
......
......@@ -10,31 +10,28 @@ Section logrel.
Context {Σ : iFunctor}.
Notation "# v" := (of_val v) (at level 20).
Canonical Structure leibniz_val := leibnizC val.
Canonical Structure leibniz_var := leibnizC var.
Class Val_to_IProp_Persistent (f : leibniz_val -n> iProp lang Σ) :=
val_to_iprop_persistent : v : val, PersistentP ((cofe_mor_car _ _ f) v).
Class Val_to_IProp_Persistent (f : valC -n> iProp lang Σ) :=
val_to_iprop_persistent : v : val, PersistentP (f v).
Arguments Val_to_IProp_Persistent /.
(** Just to get nicer closed forms, we define extend_context_interp in three steps. *)
Program Definition extend_context_interp_fun1
(τi : leibniz_val -n> iProp lang Σ)
(f : leibniz_var -n> leibniz_val -n> iProp lang Σ) :
(leibniz_var -n> leibniz_val -n> iProp lang Σ) :=
(τi : valC -n> iProp lang Σ)
(f : varC -n> valC -n> iProp lang Σ) :
(varC -n> valC -n> iProp lang Σ) :=
{| cofe_mor_car :=
λ x,
match x return leibniz_val -n> iProp lang Σ with
match x return valC -n> iProp lang Σ with
| O => τi
| S x' => f x'
end
|}.
Program Definition extend_context_interp_fun2
(τi : leibniz_val -n> iProp lang Σ) :
(leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
(leibniz_var -n> leibniz_val -n> iProp lang Σ) :=
(τi : valC -n> iProp lang Σ) :
(varC -n> valC -n> iProp lang Σ) -n>
(varC -n> valC -n> iProp lang Σ) :=
{|
cofe_mor_car := λ f, extend_context_interp_fun1 τi f
|}.
......@@ -42,9 +39,9 @@ Section logrel.
Proof. intros ???? Hfg x; destruct x; cbn; trivial. Qed.
Program Definition extend_context_interp :
(leibniz_val -n> iProp lang Σ) -n>
(leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
(leibniz_var -n> leibniz_val -n> iProp lang Σ) :=
(valC -n> iProp lang Σ) -n>
(varC -n> valC -n> iProp lang Σ) -n>
(varC -n> valC -n> iProp lang Σ) :=
{|
cofe_mor_car := λ τi, extend_context_interp_fun2 τi
|}.
......@@ -52,10 +49,10 @@ Section logrel.
Proof. intros n g h H Δ x y. destruct x; cbn; auto. Qed.
Program Definition extend_context_interp_apply :
((leibniz_var -n> leibniz_val -n> iProp lang Σ)) -n>
((leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
leibniz_val -n> iProp lang Σ) -n>
(leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ) :=
((varC -n> valC -n> iProp lang Σ)) -n>
((varC -n> valC -n> iProp lang Σ) -n>
valC -n> iProp lang Σ) -n>
(valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ) :=
{|
cofe_mor_car := λ Δ,
{|
......@@ -79,14 +76,14 @@ Section logrel.
destruct y; trivial.
Qed.
Definition interp_unit : leibniz_val -n> iProp lang Σ :=
Definition interp_unit : valC -n> iProp lang Σ :=
{|
cofe_mor_car := λ w, (w = UnitV)%I
|}.
Program Definition interp_prod :
(leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ) -n>
leibniz_val -n> iProp lang Σ :=
(valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ) -n>
valC -n> iProp lang Σ :=
{|
cofe_mor_car :=
λ τ1i,
......@@ -105,8 +102,8 @@ Section logrel.
try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.
Program Definition interp_sum :
(leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ) -n>
leibniz_val -n> iProp lang Σ :=
(valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ) -n>
valC -n> iProp lang Σ :=
{|
cofe_mor_car :=
λ τ1i,
......@@ -126,8 +123,8 @@ Section logrel.
try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.
Program Definition interp_arrow :
(leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ) -n>
leibniz_val -n> iProp lang Σ :=
(valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ) -n>
valC -n> iProp lang Σ :=
{|
cofe_mor_car :=
λ τ1i,
......@@ -136,7 +133,7 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, ( v, τ1i v WP (App (# w) (# v)) @ {{τ2i}})%I
λ w, ( v, τ1i v WP App (# w) (# v) {{τ2i}})%I
|}
|}
|}.
......@@ -148,17 +145,17 @@ Section logrel.
try match goal with [H : _ {_} _|- _] => rewrite H end; trivial.
Program Definition interp_forall :
((leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ)) -n>
leibniz_val -n> iProp lang Σ :=
((valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ)) -n>
valC -n> iProp lang Σ :=
{|
cofe_mor_car :=
λ τi,
{|
cofe_mor_car :=
λ w,
( (τ'i : {f : (leibniz_val -n> iProp lang Σ) |
( (τ'i : {f : (valC -n> iProp lang Σ) |
Val_to_IProp_Persistent f}),
(WP TApp (# w) @ {{λ v, (τi (`τ'i) v)}}))%I
WP TApp (# w) {{λ v, (τi (`τ'i) v)}})%I
|}
|}.
Next Obligation.
......@@ -173,9 +170,9 @@ Section logrel.
Qed.
Program Definition interp_rec_pre :
((leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ)) -n>
(leibniz_val -n> iProp lang Σ) -n>
(leibniz_val -n> iProp lang Σ) :=
((valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ)) -n>
(valC -n> iProp lang Σ) -n>
(valC -n> iProp lang Σ) :=
{|
cofe_mor_car :=
λ τi,
......@@ -202,7 +199,7 @@ Section logrel.
Qed.
Global Instance interp_rec_pre_contr
(τi : (leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ))
(τi : (valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ))
:
Contractive (interp_rec_pre τi).
Proof.
......@@ -213,8 +210,8 @@ Section logrel.
Qed.
Program Definition interp_rec :
((leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ)) -n>
(leibniz_val -n> iProp lang Σ)
((valC -n> iProp lang Σ) -n> (valC -n> iProp lang Σ)) -n>
(valC -n> iProp lang Σ)
:=
{|
cofe_mor_car := λ τi, fixpoint (interp_rec_pre τi)
......@@ -223,7 +220,7 @@ Section logrel.
Proof. intros n f g H; apply fixpoint_ne => z; rewrite H; trivial. Qed.
Program Fixpoint interp (τ : type) {struct τ}
: (leibniz_var -n> (leibniz_val -n> iProp lang Σ)) -n> leibniz_val -n> iProp lang Σ
: (varC -n> (valC -n> iProp lang Σ)) -n> valC -n> iProp lang Σ
:=
match τ with
| TUnit => {| cofe_mor_car := λ Δ, interp_unit |}
......@@ -232,7 +229,7 @@ Section logrel.
| TSum τ1 τ2 => {| cofe_mor_car := λ Δ,interp_sum (interp τ1 Δ) (interp τ2 Δ)|}
| TArrow τ1 τ2 => {|cofe_mor_car := λ Δ, interp_arrow (interp τ1 Δ) (interp τ2 Δ)|}
| TVar v => {| cofe_mor_car :=
λ Δ : (leibniz_var -n> (leibniz_val -n> iProp lang Σ)), (Δ v) |}
λ Δ : (varC -n> (valC -n> iProp lang Σ)), (Δ v) |}
| TForall τ' =>
{| cofe_mor_car := λ Δ,
interp_forall (extend_context_interp_apply Δ (interp τ'))|}
......@@ -243,18 +240,18 @@ Section logrel.
Solve Obligations with
repeat intros ?; match goal with [H : _ {_} _|- _] => rewrite H end; trivial.
Class context_interp_Persistent (Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ) :=
Class context_interp_Persistent (Δ : varC -n> valC -n> iProp lang Σ) :=
contextinterppersistent : v : var, Val_to_IProp_Persistent (Δ v).
Global Instance Val_to_IProp_Persistent_Persistent
(f : leibniz_val -n> iProp lang Σ)
(f : valC -n> iProp lang Σ)
{Hf : Val_to_IProp_Persistent f}
(v : val)
: PersistentP (f v).
Proof. apply Hf. Qed.
Global Instance interp_Persistent
τ (Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
τ (Δ : varC -n> valC -n> iProp lang Σ)
{HΔ : context_interp_Persistent Δ}
: Val_to_IProp_Persistent (interp τ Δ).
Proof.
......@@ -267,7 +264,7 @@ Section logrel.
Global Instance Persistent_context_interp_rel Δ Γ vs
{HΔ : context_interp_Persistent Δ}
: PersistentP (Π∧ zip_with(λ τ v, interp τ Δ v) Γ vs)%I.
: PersistentP ([] zip_with(λ τ v, interp τ Δ v) Γ vs)%I.
Proof. typeclasses eauto. Qed.
Global Program Instance extend_context_interp_Persistent f Δ
......@@ -294,7 +291,7 @@ Section logrel.
Lemma interp_unused_contex_irrel
(m n : nat)
(Δ Δ' : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(Δ Δ' : varC -n> valC -n> iProp lang Σ)
(HΔ : v, Δ (if lt_dec v m then v else (n + v))
Δ' (if lt_dec v m then v else (n + v)))
(τ : type)
......@@ -341,8 +338,8 @@ Section logrel.
Qed.
Program Definition hop_context_interp (m n : nat) :
(leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
(leibniz_var -n> leibniz_val -n> iProp lang Σ) :=
(varC -n> valC -n> iProp lang Σ) -n>
(varC -n> valC -n> iProp lang Σ) :=
{| cofe_mor_car :=
λ Δ,
{| cofe_mor_car := λ v, if lt_dec v m then Δ v else Δ (v - n) |}
......@@ -355,8 +352,8 @@ Section logrel.
Qed.
Lemma extend_bofore_hop_context_interp (m n : nat)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(τi : leibniz_val -n> iProp lang Σ)
(Δ : varC -n> valC -n> iProp lang Σ)
(τi : valC -n> iProp lang Σ)
(v : var)
:
(extend_context_interp τi (hop_context_interp m n Δ)
......@@ -375,7 +372,7 @@ Section logrel.
Lemma interp_subst_weaken
(m n : nat)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(Δ : varC -n> valC -n> iProp lang Σ)
(τ : type)
: interp τ Δ interp τ.[iter m up (ren (+n))] (hop_context_interp m n Δ).
Proof.
......@@ -412,8 +409,8 @@ Section logrel.
Qed.
Lemma interp_ren_S (τ : type)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(τi : leibniz_val -n> iProp lang Σ)
(Δ : varC -n> valC -n> iProp lang Σ)
(τi : valC -n> iProp lang Σ)
: interp τ Δ interp τ.[ren (+1)] (extend_context_interp τi Δ).
Proof.
rewrite (interp_subst_weaken 0 1).
......@@ -424,9 +421,9 @@ Section logrel.
Local Opaque eq_nat_dec.
Program Definition context_interp_insert (m : nat) :
(leibniz_val -n> iProp lang Σ) -n>
(leibniz_var -n> leibniz_val -n> iProp lang Σ) -n>
(leibniz_var -n> leibniz_val -n> iProp lang Σ) :=
(valC -n> iProp lang Σ) -n>
(varC -n> valC -n> iProp lang Σ) -n>
(varC -n> valC -n> iProp lang Σ) :=
{| cofe_mor_car :=
λ τi,
{| cofe_mor_car :=
......@@ -451,9 +448,9 @@ Section logrel.
Qed.
Lemma extend_context_interp_insert (m : nat)
(τi : leibniz_val -n> iProp lang Σ)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(Ti : leibniz_val -n> iProp lang Σ)
(τi : valC -n> iProp lang Σ)
(Δ : varC -n> valC -n> iProp lang Σ)
(Ti : valC -n> iProp lang Σ)
:
(extend_context_interp Ti (context_interp_insert m τi Δ))
(context_interp_insert (S m) τi (extend_context_interp Ti Δ)).
......@@ -466,8 +463,8 @@ Section logrel.
Qed.
Lemma context_interp_insert_O_extend
(τi : leibniz_val -n> iProp lang Σ)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(τi : valC -n> iProp lang Σ)
(Δ : varC -n> valC -n> iProp lang Σ)
:
(context_interp_insert O τi Δ)
(extend_context_interp τi Δ).
......@@ -498,7 +495,7 @@ Section logrel.
Lemma interp_subst_iter_up
(m : nat)
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(Δ : varC -n> valC -n> iProp lang Σ)
(τ : type)
(τ' : type)
: interp τ (context_interp_insert m (interp τ'.[ren (+m)] Δ) Δ)
......@@ -532,7 +529,7 @@ Section logrel.
Qed.
Lemma interp_subst
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ)
(Δ : varC -n> valC -n> iProp lang Σ)
(τ : type)
(τ' : type)
: interp τ (extend_context_interp (interp τ' Δ) Δ) interp τ.[τ'/] Δ.
......@@ -543,10 +540,10 @@ Section logrel.
Qed.
Lemma zip_with_context_interp_subst
(Δ : leibniz_var -n> leibniz_val -n> iProp lang Σ) (Γ : list type)
(vs : list leibniz_val) (τi : leibniz_val -n> iProp lang Σ) :
((Π∧ zip_with (λ τ v, interp τ Δ v) Γ vs)%I)
(Π∧ zip_with (λ τ v, interp τ (extend_context_interp τi Δ) v)
(Δ : varC -n> valC -n> iProp lang Σ) (Γ : list type)
(vs : list valC) (τi : valC -n> iProp lang Σ) :
(([] zip_with (λ τ v, interp τ Δ v) Γ vs)%I)
([] zip_with (λ τ v, interp τ (extend_context_interp τi Δ) v)
(map (λ t : type, t.[ren (+1)]) Γ) vs)%I.
Proof.
revert Δ vs τi.
......@@ -556,5 +553,4 @@ Section logrel.
- apply interp_ren_S.
- apply IHΓ.
Qed.
End logrel.
\ No newline at end of file
End logrel.
......@@ -2,7 +2,6 @@ Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu.lang.
Section lang_rules.
Context {Σ : iFunctor}.
Implicit Types P : iProp lang Σ.
......
......@@ -12,12 +12,12 @@ Section Soundness.
Definition Σ := #[].
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof.
replace (env_subst []) with (@ids expr _) by reflexivity.
asimpl; trivial.
Qed.
Definition free_type_context :
leibniz_var -n> leibniz_val -n> iProp lang (globalF Σ) :=
Definition free_type_context : varC -n> valC -n> iProp lang (globalF Σ) :=
{|
cofe_mor_car :=
λ x,
......@@ -50,7 +50,7 @@ Section Soundness.
edestruct(@wp_adequacy_reducible lang (globalF Σ)
(interp τ free_type_context)
e e' (e' :: thp) tt ) as [Ha|Ha];
eauto using cmra_unit_valid; try tauto.
eauto using ucmra_unit_valid; try tauto.
- iIntros "H". iApply H1.
- constructor.
Qed.
......
......@@ -58,14 +58,13 @@ Proof.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option (Var x) (of_val <$> vs !! x).
from_option id (Var x) (of_val <$> vs !! x).
Notation "# v" := (of_val v) (at level 20).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)]
.
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
......@@ -73,11 +72,9 @@ Proof.
by rewrite Hv.
Qed.
Local Opaque eq_nat_dec.
Lemma iter_up_subst_type (m : nat) (τ : type) (x : var)
:
Lemma iter_up_subst_type (m : nat) (τ : type) (x : var) :
(iter m up (τ .: ids) x) =
if lt_dec x m then ids x else
if eq_nat_dec x m then τ.[ren (+m)] else ids (x - 1).
......
......@@ -12,61 +12,23 @@ Import uPred.
Section typed_interp.
Context {Σ : gFunctors} `{i : heapG Σ} `{L : namespace}.
Implicit Types P Q R : iPropG lang Σ.
Notation "# v" := (of_val v) (at level 20).
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_ : ?A, _) => let W := fresh "W" in evar (W : A); iExists W; unfold W; clear W
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => iNext
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => eapply (@always_intro _ _ _ _)
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial];
[apply (always_intro _ _); iIntros {v} Hv|iSplit; trivial]; cbn.
iApply wp_wand_l;
iSplitL; [|iApply Hp; trivial]; [iIntros {v} Hv|iSplit; trivial]; cbn.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].