Commit 4ef79ca8 authored by David Swasey's avatar David Swasey
Browse files

Add wp tactics, based on `heap_lang`.

parent 29bd9d7f
......@@ -40,8 +40,10 @@ theories/logrel/prelude/base.v
#theories/logrel/F_mu_ref/soundness_binary.v
theories/logrel/F_mu_ref_conc/lang.v
theories/logrel/F_mu_ref_conc/rules.v
theories/logrel/F_mu_ref_conc/proofmode.v
theories/logrel/F_mu_ref_conc/typing.v
theories/logrel/F_mu_ref_conc/logrel_unary.v
theories/logrel/F_mu_ref_conc/tactics_unary.v
theories/logrel/F_mu_ref_conc/fundamental_unary.v
theories/logrel/F_mu_ref_conc/soundness_unary.v
#theories/logrel/F_mu_ref_conc/rules_binary.v
......
......@@ -2,30 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris_examples.logrel.F_mu_ref_conc Require Import rules typing.
From iris_examples.logrel.F_mu_ref_conc Require Import fundamental_unary.
(** Syntactic sugar. *)
Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
Definition Let (e1 : expr) (e2: {bind expr}) := App (Lam e2) e1.
Definition LetCtx (e2 : expr) := AppRCtx (LamV e2).
(** Simple bind tactics. *)
(* These tactics are a bit *too* simple. They render the following
proof scripts more cluttered than they need to be wrt values and
evaluation contexts. For an approach that scales better, see the
heap language bundled with Iris. *)
Local Tactic Notation "wp_bind" uconstr(ctx) :=
iApply (wp_bind (fill ctx)).
Local Tactic Notation "wp_pure" :=
iApply wp_pure_step_later; first done; iNext.
Local Tactic Notation "use_bind_pure" uconstr(ctx) :=
wp_bind ctx; wp_pure; rewrite ?[fill _ _]/=.
Local Tactic Notation "use_bind" uconstr(ctx) uconstr(Hp) ident(v) constr(Hv) :=
wp_bind ctx; iApply Hp; first done; iNext; iIntros (v) Hv;
rewrite ?[fill _ _]/=.
From iris_examples.logrel.F_mu_ref_conc Require Import tactics_unary.
(** Symbol ADT *)
......@@ -107,10 +84,8 @@ Section symbol_proof.
Lemma type_inc Δ γ l :
symbol_ctx γ l τinc (SymbolV γ :: Δ) (LamV (FAI (Loc l))).
Proof.
iIntros "#Hctx /=". iAlways. iIntros (v) "->".
wp_pure. asimpl.
iInv N as (n) ">[Hl Hc]" "Hclose".
iApply (wp_fai with "Hl"). iIntros "!> Hl".
iIntros "#Hctx /=". iAlways. iIntros (v) "->". wp_app.
iInv N as (n) ">[Hl Hc]" "Hclose". wp_fai.
iMod (Counter_inc with "Hc") as "[Hc Hs]".
iMod ("Hclose" with "[Hl Hc]"); last by auto.
iExists (S n). by iFrame.
......@@ -122,27 +97,21 @@ Section symbol_proof.
LamV $ Assert $ BinOp Lt (Var 0) (Load (Loc l)).
Proof.
iIntros "#Hctx /=". iAlways. iIntros (v) "Hv".
iDestruct "Hv" as (s) "[-> Hs]". asimpl.
wp_pure. asimpl. rewrite -(of_to_val (#n s) (#nv s)) //.
wp_bind [BinOpRCtx _ _; AssertCtx]; simpl.
iDestruct "Hv" as (s) "[-> Hs]". wp_app. wp_bind (Load _).
iInv N as (n) ">[Hl Hc]" "Hclose".
iDestruct (Symbol_obs with "[$Hc $Hs]") as "%".
iApply (wp_load with "Hl"). iIntros "!> Hl".
iDestruct (Symbol_obs with "[$Hc $Hs]") as "%". wp_load.
iMod ("Hclose" with "[Hl Hc]"). { iExists n. by iFrame. }
iModIntro. use_bind_pure [AssertCtx]; simpl.
destruct (lt_dec _ _); last done.
iApply wp_value. wp_pure. by iApply wp_value.
iModIntro. wp_op. destruct (lt_dec _ _)=>//. by wp_assert.
Qed.
Lemma type_symbol Γ : Γ symbol : τsymbol.
Proof.
iIntros (Δ vs _) "_". rewrite/symbol.
use_bind [LetCtx (Pair inc check); PackCtx] wp_alloc l "Hl".
iIntros (Δ vs _) "_". rewrite/interp_expr.
asimpl; wp_alloc l as "Hl".
iMod (Counter_alloc 0) as (γ) "Hc".
iMod (inv_alloc N _ (symbol_inv γ l) with "[Hl Hc]") as "#Hctx".
{ iNext. iExists 0. by iFrame. }
use_bind_pure [PackCtx]; asimpl.
iApply wp_value. iApply wp_value. iAlways.
wp_let; asimpl. iAlways.
iExists _, (SymbolV γ); iSplit; auto.
iSplit; first by iPureIntro; apply _.
iExists _, _; iSplit; auto. iSplit.
......
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_unary.
From iris_examples.logrel.F_mu_ref_conc Require Import rules.
From iris_examples.logrel.F_mu_ref_conc Require Import tactics_unary.
From iris.base_logic Require Export big_op invariants.
From iris.program_logic Require Export lifting.
From iris.proofmode Require Import tactics.
......@@ -14,8 +14,8 @@ Section typed_interp.
Notation D := (valC -n> iProp Σ).
Implicit Types e : expr.
Local Tactic Notation "use_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind (fill [ctx]));
Local Tactic Notation "use_bind" uconstr(e) ident(v) constr(Hv) uconstr(Hp) :=
unary_bind e;
iApply (wp_wand with "[-]"); [iApply Hp; trivial|]; cbn;
iIntros (v) Hv.
......@@ -27,22 +27,22 @@ Section typed_interp.
Qed.
Lemma compat_unit Γ : Γ Unit : TUnit.
Proof. iIntros (Δ vs HΔ) "#HΓ /=". by iApply wp_value. Qed.
Proof. iIntros (Δ vs HΔ) "#HΓ /=". by wp_value. Qed.
Lemma compat_nat Γ n : Γ #n n : TNat.
Proof. iIntros (Δ vs HΔ) "#HΓ /=". iApply wp_value. simpl. eauto. Qed.
Proof. iIntros (Δ vs HΔ) "#HΓ /=". wp_value. simpl. eauto. Qed.
Lemma compat_bool Γ b : Γ # b : TBool.
Proof. iIntros (Δ vs HΔ) "#HΓ /=". iApply wp_value. simpl. eauto. Qed.
Proof. iIntros (Δ vs HΔ) "#HΓ /=". wp_value. simpl. eauto. Qed.
Lemma compat_binop Γ op e1 e2 :
Γ e1 : TNat Γ e2 : TNat Γ BinOp op e1 e2 : binop_res_type op.
Proof.
iIntros (e1Typed e2Typed Δ vs HΔ) "#HΓ /=".
use_bind (BinOpLCtx _ _) v "#Hv" e1Typed.
use_bind (BinOpRCtx _ _) v' "# Hv'" e2Typed.
use_bind (e1.[_]) v "#Hv" e1Typed.
use_bind (e2.[_]) v' "# Hv'" e2Typed.
iDestruct "Hv" as (n) "%"; iDestruct "Hv'" as (n') "%"; simplify_eq/=.
iApply wp_pure_step_later; auto. iNext. iApply wp_value.
wp_op.
destruct op; simpl; try destruct eq_nat_dec;
try destruct le_dec; try destruct lt_dec; eauto 10.
Qed.
......@@ -51,39 +51,39 @@ Section typed_interp.
Γ e1 : τ1 Γ e2 : τ2 Γ Pair e1 e2 : TProd τ1 τ2.
Proof.
iIntros (e1Typed e2Typed Δ vs HΔ) "#HΓ /=".
use_bind (PairLCtx _) v "#Hv" e1Typed.
use_bind (PairRCtx _) v' "# Hv'" e2Typed.
iApply wp_value; eauto.
use_bind (e1.[_]) v "#Hv" e1Typed.
use_bind (e2.[_]) v' "# Hv'" e2Typed.
wp_value. eauto.
Qed.
Lemma compat_fst Γ e τ1 τ2 : Γ e : TProd τ1 τ2 Γ Fst e : τ1.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind FstCtx v "# Hv" eTyped; cbn.
use_bind (e.[_]) v "# Hv" eTyped.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
iApply wp_pure_step_later; auto. by iApply wp_value.
by wp_proj.
Qed.
Lemma compat_snd Γ e τ1 τ2 : Γ e : TProd τ1 τ2 Γ Snd e : τ2.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind SndCtx v "# Hv" eTyped; cbn.
use_bind (e.[_]) v "# Hv" eTyped.
iDestruct "Hv" as (w1 w2) "#[% [H2 H3]]"; subst.
iApply wp_pure_step_later; auto. by iApply wp_value.
by wp_proj.
Qed.
Lemma compat_injl Γ e τ1 τ2 : Γ e : τ1 Γ InjL e : TSum τ1 τ2.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind InjLCtx v "# Hv" eTyped; cbn.
iApply wp_value; eauto.
use_bind (e.[_]) v "# Hv" eTyped.
wp_value. eauto.
Qed.
Lemma compat_injr Γ e τ1 τ2 : Γ e : τ2 Γ InjR e : TSum τ1 τ2.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind InjRCtx v "# Hv" eTyped; cbn.
iApply wp_value; eauto.
use_bind (e.[_]) v "# Hv" eTyped.
wp_value. eauto.
Qed.
Lemma compat_case Γ e0 e1 e2 τ1 τ2 τ3
......@@ -93,13 +93,13 @@ Section typed_interp.
Γ Case e0 e1 e2 : τ3.
Proof.
iIntros (e0Typed e1Typed e2Typed Δ vs HΔ) "#HΓ /=".
use_bind (CaseCtx _ _) v "#Hv" e0Typed; cbn.
use_bind (e0.[_]) v "#Hv" e0Typed.
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 1 using to_of_val; asimpl. iNext.
- wp_case. asimpl.
erewrite n_closed_subst_head_simpl by naive_solver.
iApply (e1Typed Δ (w :: vs)). iApply interp_env_cons; auto.
- iApply wp_pure_step_later; auto 1 using to_of_val; asimpl. iNext.
- wp_case. asimpl.
erewrite n_closed_subst_head_simpl by naive_solver.
iApply (e2Typed Δ (w :: vs)). iApply interp_env_cons; auto.
Qed.
......@@ -108,10 +108,9 @@ Section typed_interp.
Γ e0 : TBool Γ e1 : τ Γ e2 : τ Γ If e0 e1 e2 : τ.
Proof.
iIntros (e0Typed e1Typed e2Typed Δ vs HΔ) "#HΓ /=".
use_bind (IfCtx _ _) v "#Hv" e0Typed; cbn.
iDestruct "Hv" as ([]) "%"; subst; simpl;
[iApply wp_pure_step_later .. ]; auto; iNext;
[iApply e1Typed| iApply e2Typed]; auto.
use_bind (e0.[_]) v "#Hv" e0Typed.
iDestruct "Hv" as ([]) "%"; subst; wp_if.
by iApply e1Typed. by iApply e2Typed.
Qed.
Lemma compat_rec Γ e τ1 τ2
......@@ -119,10 +118,10 @@ Section typed_interp.
TArrow τ1 τ2 :: τ1 :: Γ e : τ2 Γ Rec e : TArrow τ1 τ2.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
iApply wp_value. simpl. iAlways. iLöb as "IH". iIntros (w) "#Hw".
wp_value. simpl. iAlways. iLöb as "IH". iIntros (w) "#Hw".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
asimpl. change (Rec _) with (of_val (RecV e.[upn 2 (env_subst vs)])) at 2.
wp_app. asimpl.
change (Rec _) with (of_val (RecV e.[upn 2 (env_subst vs)])) at 2.
erewrite n_closed_subst_head_simpl_2 by naive_solver.
iApply (eTyped Δ (_ :: w :: vs)).
iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto.
......@@ -132,8 +131,8 @@ Section typed_interp.
Γ e1 : TArrow τ1 τ2 Γ e2 : τ1 Γ App e1 e2 : τ2.
Proof.
iIntros (e1Typed e2Typed Δ vs HΔ) "#HΓ /=".
use_bind (AppLCtx _) v "#Hv" e1Typed.
use_bind (AppRCtx _) w "#Hw" e2Typed.
use_bind (e1.[_]) v "#Hv" e1Typed.
use_bind (e2.[_]) w "#Hw" e2Typed.
by iApply "Hv".
Qed.
......@@ -141,15 +140,14 @@ Section typed_interp.
subst (ren (+1)) <$> Γ e : τ Γ TLam e : TForall τ.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
iApply wp_value.
iAlways; iIntros (τi) "%". iApply wp_pure_step_later; auto; iNext.
iApply eTyped. by iApply interp_env_ren.
wp_value. simpl. iAlways. iIntros (τi) "%".
wp_tapp. iApply eTyped. by iApply interp_env_ren.
Qed.
Lemma compat_tapp Γ e τ τ' : Γ e : TForall τ Γ TApp e : τ.[τ'/].
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind TAppCtx v "#Hv" eTyped; cbn.
use_bind (e.[_]) v "#Hv" eTyped.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! ( τ' Δ)); iPureIntro; apply _|]; cbn.
iIntros (w) "?". by iApply interp_subst.
Qed.
......@@ -157,10 +155,9 @@ Section typed_interp.
Lemma compat_pack Γ e τ τ' : Γ e : τ.[τ'/] Γ Pack e : TExist τ.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind PackCtx v "#Hv" eTyped; cbn.
iApply wp_value. iAlways. iExists v, ( τ' Δ).
iSplit; first done. iSplit; first by iPureIntro=>?; apply _.
by iApply interp_subst.
use_bind (e.[_]) v "#Hv" eTyped.
wp_value. iAlways. iExists v, ( τ' Δ). iSplit; [|iSplit].
done. by iPureIntro=>?; apply _. by iApply interp_subst.
Qed.
Lemma compat_unpack Γ e0 e1 τ τ1
......@@ -169,10 +166,9 @@ Section typed_interp.
Γ Unpack e0 e1 : τ1.
Proof.
iIntros (e0Typed e1Typed Δ vs HΔ) "#HΓ /=".
use_bind (UnpackCtx _) v "#Hv" e0Typed; cbn.
use_bind (e0.[_]) v "#Hv" e0Typed.
iDestruct "Hv" as (w τi) "(% & % & Hw)"; subst.
iApply wp_pure_step_later; auto 1 using to_of_val; asimpl.
rewrite -/of_val. iNext.
wp_unpack. asimpl.
iDestruct (interp_env_length with "HΓ") as %?.
erewrite n_closed_subst_head_simpl; [|done|solve_length].
iApply interp_expr_unused.
......@@ -184,38 +180,34 @@ Section typed_interp.
Lemma compat_fold Γ e τ : Γ e : τ.[TRec τ/] Γ Fold e : TRec τ.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
iApply (wp_bind (fill [FoldCtx]));
iApply wp_wand_l; iSplitL; [|iApply (eTyped Δ vs); auto].
iIntros (v) "#Hv". iApply wp_value.
use_bind (e.[_]) v "#Hv" eTyped.
wp_value.
rewrite /= -interp_subst fixpoint_unfold /=.
iAlways; eauto.
iAlways. eauto.
Qed.
Lemma compat_unfold Γ e τ : Γ e : TRec τ Γ Unfold e : τ.[TRec τ/].
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
iApply (wp_bind (fill [UnfoldCtx]));
iApply wp_wand_l; iSplitL; [|iApply eTyped; auto].
unary_bind (e.[_]). iApply wp_wand_l; iSplitL; last by iApply eTyped.
iIntros (v) "#Hv". rewrite /= fixpoint_unfold.
change (fixpoint _) with ( TRec τ Δ); simpl.
iDestruct "Hv" as (w) "#[% Hw]"; subst.
iApply wp_pure_step_later; cbn; auto using to_of_val.
iNext. iApply wp_value. by iApply interp_subst.
wp_unfold. by iApply interp_subst.
Qed.
Lemma compat_fork Γ e : Γ e : TUnit Γ Fork e : TUnit.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
iApply wp_fork. iNext; iSplitL; trivial.
iApply wp_wand_l. iSplitL; [|iApply eTyped; auto]; auto.
iApply wp_fork. iNext. iSplitL; trivial.
iApply wp_wand_l; iSplitL; last by iApply eTyped. auto.
Qed.
Lemma compat_alloc Γ e τ : Γ e : τ Γ Alloc e : Tref τ.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind AllocCtx v "#Hv" eTyped; cbn. iClear "HΓ". iApply wp_fupd.
iApply wp_alloc; auto 1 using to_of_val.
iNext; iIntros (l) "Hl".
use_bind (e.[_]) v "#Hv" eTyped. iClear "HΓ". iApply wp_fupd.
wp_alloc l as "Hl".
iMod (inv_alloc _ with "[Hl]") as "HN";
[| iModIntro; iExists _; iSplit; trivial]; eauto.
Qed.
......@@ -223,27 +215,21 @@ Section typed_interp.
Lemma compat_load Γ e τ : Γ e : Tref τ Γ Load e : τ.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind LoadCtx v "#Hv" eTyped; cbn. iClear "HΓ".
use_bind (e.[_]) v "#Hv" eTyped. iClear "HΓ".
iDestruct "Hv" as (l) "[% #Hv]"; subst.
iApply wp_atomic.
iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
iApply (wp_load with "Hw1").
iModIntro. iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
wp_load. iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
Qed.
Lemma compat_store Γ e1 e2 τ :
Γ e1 : Tref τ Γ e2 : τ Γ Store e1 e2 : TUnit.
Proof.
iIntros (e1Typed e2Typed Δ vs HΔ) "#HΓ /=".
use_bind (StoreLCtx _) v "#Hv" e1Typed; cbn.
use_bind (StoreRCtx _) w "#Hw" e2Typed; cbn. iClear "HΓ".
use_bind (e1.[_]) v "#Hv" e1Typed.
use_bind (e2.[_]) w "#Hw" e2Typed. iClear "HΓ".
iDestruct "Hv" as (l) "[% #Hv]"; subst.
iApply wp_atomic.
iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
iApply (wp_store with "Hz1"); auto using to_of_val.
iModIntro. iNext.
iIntros "Hz1". iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
wp_store. iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
Qed.
Lemma compat_cas Γ e1 e2 e3 τ :
......@@ -251,31 +237,24 @@ Section typed_interp.
Γ CAS e1 e2 e3 : TBool.
Proof.
iIntros (? e1Typed e2Typed e3Typed Δ vs HΔ) "#HΓ /=".
use_bind (CasLCtx _ _) v1 "#Hv1" e1Typed; cbn.
use_bind (CasMCtx _ _) v2 "#Hv2" e2Typed; cbn.
use_bind (CasRCtx _ _) v3 "#Hv3" e3Typed; cbn. iClear "HΓ".
use_bind (e1.[_]) v1 "#Hv1" e1Typed.
use_bind (e2.[_]) v2 "#Hv2" e2Typed.
use_bind (e3.[_]) v3 "#Hv3" e3Typed. iClear "HΓ".
iDestruct "Hv1" as (l) "[% Hv1]"; subst.
iApply wp_atomic.
iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
destruct (decide (v2 = w)) as [|Hneq]; subst.
+ iApply (wp_cas_suc with "Hw1"); auto using to_of_val.
iModIntro. iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
+ iApply (wp_cas_fail with "Hw1"); auto using to_of_val.
iModIntro. iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
+ wp_cas_suc. iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
+ wp_cas_fail. iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
Qed.
Lemma compat_fai Γ e : Γ e : Tref TNat Γ FAI e : TNat.
Proof.
iIntros (eTyped Δ vs HΔ) "#HΓ /=".
use_bind FAICtx v "#Hv" eTyped; cbn. iClear "HΓ".
use_bind (e.[_]) v "#Hv" eTyped. iClear "HΓ".
iDestruct "Hv" as (l) "[% #Hv]"; subst.
iApply wp_atomic.
iInv (logN .@ l) as (w) "[Hw1 >Hw2]" "Hclose".
iDestruct "Hw2" as (n) "%"; subst.
iApply (wp_fai with "Hw1"). iModIntro. iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1]"); eauto.
wp_fai. iMod ("Hclose" with "[Hw1]"); eauto.
iExists (#nv S n); eauto.
Qed.
......
......@@ -361,3 +361,22 @@ Ltac solve_atomic :=
Hint Extern 0 (Atomic _ _) => solve_atomic.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
(** Syntactic sugar. *)
Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
Definition Let (e1 : expr) (e2: {bind expr}) := App (Lam e2) e1.
Definition LetCtx (e2 : expr) := AppRCtx (LamV e2).
Definition Seq (e1 : expr) (e2 : expr) := Let e1 (e2.[ren(+1)]).
Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
(* These don't help after `asimpl` and they interfere with notation `$`.
Notation Lam e := (Rec e.[ren(+1)]).
Notation LamV e := (RecV e.[ren(+1)]).
Notation Let e1 e2 := (App (Lam e2) e1).
Notation LetCtx e2 := (AppRCtx (LamV e2)).
Notation Seq e1 e2 := (Let e1 (e2.[ren(+1)])).
Notation SeqCtx e2 := (LetCtx (e2.[ren(+1)])).
Notation Skip := (Seq Unit Unit).
*)
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris_examples.logrel.F_mu_ref_conc Require Export rules.
Set Default Proof Using "Type".
Import uPred.
(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds. *)
Ltac reshape_val e tac :=
let rec go e :=
lazymatch e with
| of_val ?v => v
| Rec ?e => constr:(RecV e)
| TLam ?e => constr:(TLamV e)
| Unit => constr:(UnitV)
| Nat ?n => constr:(NatV n)
| Bool ?b => constr:(BoolV b)
| Pair ?e1 ?e2 =>
let v1 := go e1 in let v2 := go e2 in constr:(PairV v1 v2)
| InjL ?e => let v := go e in constr:(InjLV v)
| InjR ?e => let v := go e in constr:(InjRV v)
| Fold ?e => let v := go e in constr:(FoldV v)
| Pack ?e => let v := go e in constr:(PackV v)
| Loc ?l => constr:(LocV l)
end in let v := go e in tac v.
Ltac reshape_expr e tac :=
let rec go K e :=
match e with
| _ => tac K e
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| TApp ?e => go (TAppCtx :: K) e
| Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
| Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
| BinOp ?op ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
| BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
| Fst ?e => go (FstCtx :: K) e
| Snd ?e => go (SndCtx :: K) e
| InjL ?e => go (InjLCtx :: K) e
| InjR ?e => go (InjRCtx :: K) e
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
| If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
| Assert ?e => go (AssertCtx :: K) e
| Fold ?e => go (FoldCtx :: K) e
| Unfold ?e => go (UnfoldCtx :: K) e
| Pack ?e => go (PackCtx :: K) e
| Unpack ?e ?e1 => go (UnpackCtx e1 :: K) e
| Alloc ?e => go (AllocCtx :: K) e
| Load ?e => go (LoadCtx :: K) e
| Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
| Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
| CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
[ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
| go (CasMCtx v0 e2 :: K) e1 ])
| CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
| FAI ?e => go (FAICtx :: K) e
end in go (@nil ectx_item) e.
Lemma tac_wp_expr_eval `{heapIG Σ} Δ s E Φ e e' :
e = e'
envs_entails Δ (WP e' @ s; E {{ Φ }}) envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed.
Ltac wp_expr_eval t :=
try iStartProof;
try (eapply tac_wp_expr_eval; [t; reflexivity|]).
Ltac wp_expr_simpl := wp_expr_eval simpl.
(*Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.*)
Lemma tac_wp_pure `{heapIG Σ} Δ Δ' s E e1 e2 φ Φ :
PureExec φ e1 e2
φ
IntoLaterNEnvs 1 Δ Δ'
envs_entails Δ' (WP e2 @ s; E {{ Φ }})
envs_entails Δ (WP e1 @ s; E {{ Φ }}).
Proof.
rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -wp_pure_step_later //.
Qed.
Lemma tac_wp_value `{heapIG Σ} Δ s E Φ e v :
IntoVal e v
envs_entails Δ (Φ v) envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
Ltac wp_value := wp_value_head.
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
let e := eval simpl in e in
reshape_expr e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure _ _ _ _ (fill K e'));
[apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
|wp_expr_simpl(*_subst*); try wp_value_head (* new goal *)
])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'"
end.
Tactic Notation "wp_app" := wp_pure (App _ _).
Tactic Notation "wp_rec" := wp_app.
Tactic Notation "wp_lam" := wp_rec.
Tactic Notation "wp_let" := wp_lam.
Tactic Notation "wp_seq" := wp_lam.
Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
Tactic Notation "wp_match" := wp_case; wp_let.
Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _).
Tactic Notation "wp_op" := (*wp_unop ||*) wp_binop.
Tactic Notation "wp_if" := wp_pure (If _ _ _).
Tactic Notation "wp_if_true" := wp_pure (If (Bool true) _ _).
Tactic Notation "wp_if_false" := wp_pure (If (Bool false) _ _).
Tactic Notation "wp_assert" := wp_pure (Assert (Bool true)).
Tactic Notation "wp_unfold" := wp_pure (Unfold _).
Tactic Notation "wp_tapp" := wp_pure (TApp _).
Tactic Notation "wp_unpack" := wp_pure (Unpack _ _).