Commit 9825e341 authored by Amin Timany's avatar Amin Timany

Prove fundamental lemma of stlc is proven

Change the Fμ to make the operational semantics reduce under Fold.
Fundamental lemma for Fμ is partially proven (up to App).
parent a0f07fe1
......@@ -13,7 +13,7 @@ Section typed_interp.
Canonical Structure leibniz_val := leibnizC val.
Canonical Structure leibniz_le n m := leibnizC (n m).
(*
Ltac ipropsimpl :=
repeat
match goal with
......@@ -39,95 +39,116 @@ Section typed_interp.
Local Hint Extern 3 (_ (_ _))%I => rewrite -or_intro_l : itauto.
Local Hint Extern 3 (_ (_ _))%I => rewrite -or_intro_r : itauto.
Local Hint Extern 2 (_ _)%I => etransitivity; [|rewrite -later_intro] : itauto.
Local Ltac value_case := rewrite -wp_value/= ?to_of_val //; auto 2.
*)
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
|-
(_
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial]; cbn;
eapply (@always_intro _ _ _ _);
iIntros {v} Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma typed_interp k Δ Γ vs e τ
(Htyped : typed k Γ e τ)
(Hctx : closed_ctx k Γ)
(HC : closed_type k τ)
(HΔ : VlistAlwaysStable Δ)
: length Γ = length vs
: List.length Γ = List.length vs
Π∧ zip_with (λ τ v, interp k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs
WP (e.[env_subst vs]) @ {{ λ v, (@interp Σ) k τ HC Δ v }}.
Proof.
revert Hctx HC HΔ vs.
induction Htyped; intros Hctx HC HΔ vs Hlen; cbn.
induction Htyped; intros Hctx HC HΔ vs Hlen; iIntros "#HΓ"; cbn.
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv /= -wp_value; eauto using to_of_val.
rewrite /env_subst Hv; value_case.
edestruct (zipwith_Forall_lookup _ Hctx) as [Hτ' Hτ'eq]; eauto.
etransitivity.
apply big_and_elem_of, elem_of_list_lookup_2 with x.
iApply interp_closed_irrel_turnstile.
iApply big_and_elem_of "HΓ"; eauto.
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
rewrite interp_closed_irrel; trivial.
- (* unit *) value_case.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) _ v; eauto.
(* weird!: and_alwaysstable is an instance but is not resolved! *)
smart_wp_bind (PairRCtx v) (and_persistent _ _ _ _) v'.
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.
- (* fst *)
smart_wp_bind (FstCtx) v. ipropsimpl; eauto.
apply const_elim_l; intros H; rewrite H.
rewrite -wp_fst; eauto using to_of_val, and_elim_l.
rewrite and_elim_l; rewrite interp_closed_irrel; eauto.
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; eauto using to_of_val; cbn.
iNext; iApply interp_closed_irrel_turnstile; trivial.
- (* snd *)
smart_wp_bind SndCtx v. ipropsimpl; eauto.
apply const_elim_l; intros H; rewrite H.
rewrite -wp_snd; eauto using to_of_val, and_elim_l.
rewrite and_elim_r; rewrite interp_closed_irrel; eauto.
- (* injl *) smart_wp_bind InjLCtx v; value_case; eauto 7 with itauto.
- (* injr *) smart_wp_bind InjRCtx v; value_case; eauto 7 with itauto.
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
iApply wp_snd; eauto using to_of_val.
iNext; iApply interp_closed_irrel_turnstile; trivial.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn.
value_case; iLeft; auto with itauto.
- (* injr *)
smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn.
value_case; iRight; auto with itauto.
- (* case *)
smart_wp_bind (CaseCtx _ _) _ v. cbn.
rewrite (later_intro (Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v0 : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v0) (closed_ctx_list k Γ Hctx) vs));
rewrite or_elim; [apply impl_elim_l| |].
+ rewrite exist_elim; eauto; intros v'.
apply const_elim_l; intros H; rewrite H.
rewrite -impl_intro_r //; rewrite -later_and later_mono; eauto.
rewrite -wp_case_inl; eauto using to_of_val.
asimpl.
specialize (IHHtyped2 Δ (typed_closed_ctx _ _ _ _ Htyped2) HC HΔ (v'::vs)).
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
rewrite -IHHtyped2; cbn; auto.
rewrite interp_closed_irrel type_context_closed_irrel /closed_ctx_list.
apply later_mono, and_intro; eauto 3 with itauto.
+ rewrite exist_elim; eauto; intros v'.
apply const_elim_l; intros H; rewrite H.
rewrite -impl_intro_r //; rewrite -later_and later_mono; eauto.
rewrite -wp_case_inr; eauto using to_of_val.
asimpl.
specialize (IHHtyped3 Δ (typed_closed_ctx _ _ _ _ Htyped3) HC HΔ (v'::vs)).
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto).
rewrite -IHHtyped3; cbn; auto.
rewrite interp_closed_irrel type_context_closed_irrel /closed_ctx_list.
apply later_mono, and_intro; eauto 3 with itauto.
smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
iDestruct "Hv" as "[Hv|Hv]"; eauto; iRevert "HΓ";
iApply exist_elim; eauto; cbn;
iIntros {w} "#[% Hw2] #HΓ"; rewrite H; cbn;
[iApply wp_case_inl|iApply wp_case_inr];
auto 1 using to_of_val;
asimpl;
[specialize (IHHtyped2 Δ (typed_closed_ctx _ _ _ _ Htyped2) HC HΔ (w::vs)) |
specialize (IHHtyped3 Δ (typed_closed_ctx _ _ _ _ Htyped3) HC HΔ (w::vs))];
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
[iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto;
(iSplit; [iApply interp_closed_irrel_turnstile|
iApply type_context_closed_irrel_turnstile]; trivial).
- (* lam *)
value_case; apply (always_intro _ _), forall_intro=> v /=; apply impl_intro_l.
rewrite -wp_lam ?to_of_val //=.
asimpl. erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
rewrite (later_intro (Π∧ _)) -later_and; apply later_mono.
rewrite interp_closed_irrel type_context_closed_irrel /closed_ctx_list.
rewrite -(IHHtyped Δ (typed_closed_ctx _ _ _ _ Htyped) (closed_type_arrow_2 HC) HΔ (v :: vs));
simpl; auto with f_equal.
value_case; apply (always_intro _ _); iIntros {w} "#Hw".
iApply wp_lam; auto 1 using to_of_val.
asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
iNext; iApply (IHHtyped Δ (typed_closed_ctx _ _ _ _ Htyped) (closed_type_arrow_2 HC)
HΔ (w :: vs)); cbn; auto.
(iSplit; [iApply interp_closed_irrel_turnstile|
iApply type_context_closed_irrel_turnstile]; trivial).
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) _ v.
rewrite -(@wp_bind _ _ _ [AppRCtx v]) /=.
rewrite -wp_impl_l /=; apply and_intro.
2: etransitivity; [|apply IHHtyped2]; eauto using and_elim_r.
rewrite and_elim_l. apply always_mono.
apply forall_intro =>v'.
rewrite forall_elim.
apply impl_intro_l.
rewrite -(later_intro).
etransitivity; [apply impl_elim_r|].
apply wp_mono => w.
rewrite interp_closed_irrel; trivial.
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].
intros; apply interp_closed_irrel_turnstile.
- (* TLam *)
value_case; rewrite -exist_intro; apply and_intro; auto.
apply forall_intro =>τi;
apply (always_intro _ _).
......@@ -207,4 +228,4 @@ Section typed_interp.
all: solve [eauto 2 using typed_closed_type | try typeclasses eauto].
Qed.
End typed_interp.
\ No newline at end of file
End typed_interp.
......@@ -36,7 +36,7 @@ Module lang.
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
| FoldV (e : expr).
| FoldV (v : val).
Fixpoint of_val (v : val) : expr :=
match v with
......@@ -46,7 +46,7 @@ Module lang.
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| FoldV e => Fold e
| FoldV v => Fold (of_val v)
end.
Fixpoint to_val (e : expr) : option val :=
match e with
......@@ -56,7 +56,7 @@ Module lang.
| 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 => Some (FoldV e)
| Fold e => v to_val e; Some (FoldV v)
| _ => None
end.
......@@ -72,6 +72,7 @@ Module lang.
| InjLCtx
| InjRCtx
| CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
| FoldCtx
| UnfoldCtx.
Notation ectx := (list ectx_item).
......@@ -88,6 +89,7 @@ Module lang.
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| FoldCtx => Fold e
| UnfoldCtx => Unfold e
end.
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
......@@ -114,14 +116,15 @@ Module lang.
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
(* Recursive Types *)
| Unfold_Fold e σ :
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ e σ None
(* 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.
Definition atomic (e: expr) := false.
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
......@@ -247,4 +250,4 @@ Global Instance lang_ctx_item Ki :
LanguageCtx lang (lang.fill_item Ki).
Proof. change (LanguageCtx lang (lang.fill [Ki])). by apply _. Qed.
Export lang.
\ No newline at end of file
Export lang.
......@@ -17,7 +17,7 @@ Section logrel.
Class Val_to_IProp_AlwaysStable (f : leibniz_val -n> iProp lang Σ) :=
val_to_iprop_always_stable : v : val, Persistent ((cofe_mor_car _ _ f) v).
val_to_iprop_always_stable : v : val, PersistentP ((cofe_mor_car _ _ f) v).
Arguments val_to_iprop_always_stable /.
......@@ -242,12 +242,21 @@ Section logrel.
let H := fresh "H" in intros H; inversion H; congruence
end.
Qed.
Lemma interp_closed_irrel_turnstile
(k : nat) (τ : type) (HC HC': closed_type k τ)
(Δ : Vlist (leibniz_val -n> iProp lang Σ) k)
(v : val)
: interp k τ HC Δ v interp k τ HC' Δ v.
Proof.
rewrite interp_closed_irrel; trivial.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl k Δ τ e w ws :
typed k Δ e τ -> length Δ = S (length ws)
typed k Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)]
.
Proof.
......@@ -264,7 +273,7 @@ Section logrel.
(f : leibniz_val -n> iProp lang Σ)
{Hf : Val_to_IProp_AlwaysStable f}
(v : val)
: Persistent (f v).
: PersistentP (f v).
Proof. apply Hf. Qed.
Global Instance interp_always_stable
......@@ -273,11 +282,11 @@ Section logrel.
: Val_to_IProp_AlwaysStable (interp k τ H Δ).
Proof.
induction τ; cbn; intros v; try apply _.
- rewrite /interp_rec /Persistent fixpoint_unfold /interp_rec_pre.
- rewrite /interp_rec /PersistentP fixpoint_unfold /interp_rec_pre.
apply always_intro'; trivial.
- apply (@force_lookup_Forall
_ _
(λ f : leibniz_val -n> iProp lang Σ, Persistent (f v))).
(λ f : leibniz_val -n> iProp lang Σ, PersistentP (f v))).
apply Forall_forall => f H1.
eapply Forall_forall in HΔ; [apply HΔ|trivial].
Qed.
......@@ -285,7 +294,7 @@ Section logrel.
Global Instance alwyas_stable_Δ k Δ Γ vs
(Hctx : closed_ctx k Γ)
{HΔ : VlistAlwaysStable Δ}
: Persistent (Π∧ zip_with (λ τ v, interp k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I.
: PersistentP (Π∧ zip_with (λ τ v, interp k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I.
Proof. typeclasses eauto. Qed.
Global Instance alwyas_stable_Vlist_cons k f Δ
......@@ -318,6 +327,25 @@ Section logrel.
- apply IHΓ.
Qed.
Lemma type_context_closed_irrel_turnstile
(k : nat) (Δ : Vlist (leibniz_val -n> iProp lang Σ) k) (Γ : list type)
(vs : list leibniz_val)
(Hctx Hctx' : closed_ctx k Γ) :
(Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v0 : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v0)
(closed_ctx_list k Γ Hctx)
vs)%I
(Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v)
(closed_ctx_list k Γ Hctx')
vs)%I.
Proof.
rewrite type_context_closed_irrel; trivial.
Qed.
Local Ltac ipropsimpl :=
repeat
match goal with
......@@ -514,4 +542,4 @@ Section logrel.
- apply IHΓ.
Qed.
End logrel.
\ No newline at end of file
End logrel.
......@@ -334,7 +334,7 @@ Next Obligation.
Proof. repeat intros ?; constructor; trivial. Qed.
Next Obligation.
Proof.
repeat intros?; constructor; trivial; apply Forall2_Forall, Forall_forall; trivial.
repeat intros?; constructor; trivial. apply Forall_Forall2, Forall_forall; trivial.
Qed.
Program Definition Vlist_cons_apply {A : cofeT} {k}
......@@ -367,4 +367,4 @@ Proof.
cbn -[Vlist_cons_morph].
apply cofe_mor_car_ne; trivial.
rewrite H1; trivial.
Qed.
\ No newline at end of file
Qed.
Require Export iris.proofmode.tactics.
From iris.program_logic Require Import wsat.
Require Import iris.program_logic.weakestpre.
Require Import iris.program_logic.language.
From mathcomp Require Export ssreflect.
From iris.prelude Require Export prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
\ No newline at end of file
Ltac done := prelude.tactics.done.
Section uPred_Lemmas.
Import uPred.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
Implicit Types Φ : val Λ iProp Λ Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Definition double_exists M A ψ Q Y :=
@exist_elim M A (λ x, b : A, ψ x b)%I Q (λ x, @exist_elim M A _ Q (Y x)).
Lemma wp_impl_l E e Φ Ψ :
(( v, Φ v Ψ v) WP e @ E {{ Φ }}) WP e @ E {{ Ψ }}.
Proof.
rewrite wp_always_l; apply wp_mono=> // v.
by rewrite always_elim (forall_elim v) impl_elim_l.
Qed.
Lemma wp_impl_r E e Φ Ψ :
(WP e @ E {{ Φ }} ( v, Φ v Ψ v)) WP e @ E {{ Ψ }}.
Proof. by rewrite comm wp_impl_l. Qed.
Lemma wp_mask_weaken E1 E2 e Φ :
E1 E2 WP e @ E1 {{ Φ }} WP e @ E2 {{ Φ }}.
Proof. auto using wp_mask_frame_mono. Qed.
End uPred_Lemmas.
Require Import iris.proofmode.tactics.
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
......@@ -6,84 +7,94 @@ Import uPred.
Section typed_interp.
Context {Σ : iFunctor}.
Notation "# v" := (of_val v) (at level 20).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) uconstr(t) ident(v) :=
rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_impl_l; apply and_intro; eauto with itauto;
apply (@always_intro _ _ _ t), forall_intro=> v /=; apply impl_intro_l.
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 Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) :=
rewrite -(@wp_bind _ _ _ [ctx]) /= -wp_mono; eauto; intros v; cbn.
Local Hint Extern 1 ((_ _) _)%I => rewrite and_elim_r : itauto.
Local Hint Extern 1 ((_ _) _)%I => rewrite and_elim_l : itauto.
Local Hint Extern 1 (_ (_ _))%I => repeat eapply and_intro : itauto.
Local Hint Extern 1 (_ _)%I => rewrite -later_intro : itauto.
Local Hint Extern 1 (_ _, _)%I => rewrite -exist_intro : itauto.
Local Hint Extern 1 (_ (_ _))%I => rewrite -or_intro_l : itauto.
Local Hint Extern 1 (_ (_ _))%I => rewrite -or_intro_r : itauto.
Local Ltac value_case := rewrite -wp_value/= ?to_of_val //; auto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
_) => iNext
end : itauto.
Local Hint Extern 1 =>
match goal with
|-
(_
--------------------------------------
(_ _)) => iSplit
end : itauto.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
iApply (@wp_bind _ _ _ [ctx]);
iApply wp_impl_l;
iSplit; [| iApply Hp; trivial]; cbn;
eapply (@always_intro _ _ _ _);
iIntros {v} Hv.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma typed_interp Γ vs e τ :
typed Γ e τ length Γ = length vs
Π∧ zip_with (@interp Σ) Γ vs wp (e.[env_subst vs]) (interp τ).
Proof.
intros Htyped; revert vs.
induction Htyped; intros vs Hlen; cbn.
induction Htyped; intros vs Hlen; iIntros "#Hctx"; cbn.
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv /= -wp_value; eauto using to_of_val.
apply big_and_elem_of, elem_of_list_lookup_2 with x.
by rewrite lookup_zip_with; simplify_option_eq.
rewrite /env_subst Hv. value_case.
iApply big_and_elem_of; eauto.
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
- (* unit *) value_case.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) _ v.
(* weird!: and_alwaysstable is an instance but is not resolved! *)
smart_wp_bind (PairRCtx v) (and_persistent _ _ _ _) v'.
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.
- (* fst *)
smart_wp_bind (FstCtx) v.
rewrite exist_elim; eauto; intros v1. rewrite exist_elim; eauto; intros v2.
apply const_elim_l; intros H; rewrite H.
rewrite -wp_fst; eauto using to_of_val, and_elim_l.
smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
iApply wp_fst; eauto using to_of_val.
- (* snd *)
smart_wp_bind SndCtx v.
rewrite exist_elim; eauto; intros v1. rewrite exist_elim; eauto; intros v2.
apply const_elim_l; intros H; rewrite H.
rewrite -wp_snd; eauto using to_of_val, and_elim_r.
- (* injl *) smart_wp_bind InjLCtx v; value_case; eauto 7 with itauto.
- (* injr *) smart_wp_bind InjRCtx v; value_case; eauto 7 with itauto.
smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn.
iApply double_exists; [|trivial].
intros w w'; cbn; iIntros "#[% [H2 H3]]"; rewrite H.
iApply wp_snd; eauto using to_of_val.
- (* injl *)
smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; value_case.
iLeft; iExists v; auto with itauto.
- (* injr *)
smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; value_case.
iRight; iExists v; auto with itauto.
- (* case *)
smart_wp_bind (CaseCtx _ _) _ v.
rewrite (later_intro (Π∧ zip_with interp Γ vs)).
rewrite or_elim; [apply impl_elim_l| |];
rewrite exist_elim; eauto; [intros v1| intros v2];
apply const_elim_l; intros H; rewrite H;
rewrite -impl_intro_r //; rewrite -later_and later_mono; eauto;
[rewrite -wp_case_inl | rewrite -wp_case_inr]; eauto using to_of_val;
asimpl; [specialize (IHHtyped2 (v1::vs)) | specialize (IHHtyped3 (v2::vs))];
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto);
[rewrite -IHHtyped2 | rewrite -IHHtyped3]; cbn; auto.
smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn.
iDestruct "Hv" as "[Hv|Hv]"; eauto; iRevert "Hctx";
iApply exist_elim; eauto; cbn;
iIntros {w} "#[% Hw2] #Hctx"; rewrite H; cbn;
[iApply wp_case_inl|iApply wp_case_inr];
auto 1 using to_of_val;
asimpl; [specialize (IHHtyped2 (w::vs)) | specialize (IHHtyped3 (w::vs))];
erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
[iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto.
- (* lam *)
value_case; apply (always_intro _ _), forall_intro=> v /=; apply impl_intro_l.
rewrite -wp_lam ?to_of_val //=.
asimpl. erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
rewrite (later_intro (Π∧ _)) -later_and; apply later_mono.
apply (IHHtyped (v :: vs)); simpl; auto with f_equal.
value_case; apply (always_intro _ _); iIntros {w} "#Hw".
iApply wp_lam; auto 1 using to_of_val.
asimpl; erewrite typed_subst_head_simpl; [|eauto|cbn]; eauto.
iNext; iApply (IHHtyped (w :: vs)); cbn; auto with itauto.
- (* app *)
smart_wp_bind (AppLCtx (e2.[env_subst vs])) _ v.
rewrite -(@wp_bind _ _ _ [AppRCtx v]) /=.
rewrite -wp_impl_l /=; apply and_intro.
2: etransitivity; [|apply IHHtyped2]; eauto using and_elim_r.
rewrite and_elim_l. apply always_mono.
apply forall_intro =>v'.
rewrite forall_elim.
apply impl_intro_l.
rewrite (later_intro (interp τ1 v')).
apply impl_elim_r.
smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply "Hv"; auto with itauto.
Qed.
End typed_interp.
\ No newline at end of file
End typed_interp.
......@@ -96,7 +96,7 @@ Module lang.
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None.
(** Atomic expressions: we don't consider any atomic operations. *)
Definition atomic (e: expr) := False.
Definition atomic (e: expr) := false.
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
......@@ -222,4 +222,4 @@ Global Instance lang_ctx_item Ki :
LanguageCtx lang (lang.fill_item Ki).
Proof. change (LanguageCtx lang (lang.fill [Ki])). by apply _. Qed.
Export lang.
\ No newline at end of file
Export lang.
......@@ -19,11 +19,11 @@ Fixpoint interp (τ : type) (w : val) : iProp lang Σ :=
v, interp τ1 v wp (App (of_val w) (of_val v)) (interp τ2)
end%I.
Global Instance interp_always_stable τ v : Persistent (interp τ v).
Global Instance interp_always_stable τ v : PersistentP (interp τ v).
Proof. revert v; induction τ=> v /=; apply _. Qed.
Lemma typed_subst_invariant Γ e τ s1 s2 :
typed Γ e τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
typed Γ e τ ( x, x < List.length Γ s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Htyped; revert s1 s2.
assert ( s1 s2 x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
......@@ -35,7 +35,7 @@ Definition env_subst (vs : list val) (x : var) : expr :=
from_option (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> length Δ = S (length ws)
typed Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)]
.
Proof.
......@@ -45,4 +45,4 @@ Proof.
by rewrite Hv.
Qed.
End logrel.
\ No newline at end of file
End logrel.
......@@ -123,4 +123,4 @@ Section lang_rules.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
Qed.
End lang_rules.
\ No newline at end of file
End lang_rules.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment