Commit 5f5f6d89 authored by Dan Frumin's avatar Dan Frumin

some simplifications

parent 9e4edf44
......@@ -96,8 +96,8 @@ Section fundamental.
smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as (l) "[% #Hv]"; subst.
iInv (logN .@ l) as (w) "[Hw1 #Hw2]" "Hclose".
iApply (wp_load with "Hw1 [Hclose]").
iNext.
iApply (wp_load with "Hw1").
iNext.
iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"); eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris_logrel.F_mu_ref_conc Require Import rules.
From iris_logrel.F_mu_ref_conc Require Import rules rules_binary.
From iris_logrel.F_mu_ref_conc Require Export lang.
Set Default Proof Using "Type".
Import lang.
......@@ -76,7 +76,6 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
end.
(* * TP tactics *)
From iris_logrel.F_mu_ref_conc Require Import rules_binary.
(* ** bind *)
Lemma tac_tp_bind_gen `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p e e' Q :
......@@ -106,10 +105,8 @@ Ltac tp_bind_helper :=
| |- fill ?K ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
lazymatch eval cbn in (K ++ K') with
| ?K'' =>
replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app)
end)
let K'' := eval cbn in (K ++ K') in
replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
| |- ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
......@@ -119,7 +116,7 @@ Ltac tp_bind_helper :=
Ltac tp_bind_helper_constr efoc :=
rewrite ?fill_app /=;
lazymatch goal with
| |- fill ?K ?e%I = fill _ _ =>
| |- fill ?K ?e = fill _ _ =>
reshape_expr e ltac:(fun K' e' =>
unify e' efoc;
lazymatch eval cbn in (K ++ K') with
......
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