Commit da93f357 authored by Ralf Jung's avatar Ralf Jung
Browse files

use ! when possible to avoid overzealous generalization

parent 38abc449
Pipeline #15240 passed with stage
in 12 minutes and 24 seconds
......@@ -12,7 +12,7 @@ Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{invG Σ, cinvG Σ}.
Context `{!invG Σ, !cinvG Σ}.
Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
......@@ -23,7 +23,7 @@ End defs.
Instance: Params (@cinv) 5 := {}.
Section proofs.
Context `{invG Σ, cinvG Σ}.
Context `{!invG Σ, !cinvG Σ}.
Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
Proof. rewrite /cinv_own; apply _. Qed.
......
......@@ -7,14 +7,14 @@ Set Default Proof Using "Type".
Export invG.
Import uPred.
Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ownE E1 == (wsat ownE E2 P))%I.
Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. by eexists. Qed.
Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
uPred_fupd_aux.(seal_eq).
Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
Proof.
split.
- rewrite uPred_fupd_eq. solve_proper.
......@@ -32,13 +32,13 @@ Proof.
iIntros "!> !>". by iApply "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
Proof.
split.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
......@@ -59,8 +59,8 @@ Proof.
by iFrame.
Qed.
Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
( `{Hinv: invG Σ}, (|={,E}=> P)%I) ( P)%I.
Lemma fupd_plain_soundness `{!invPreG Σ} E (P: iProp Σ) `{!Plain P}:
( `{Hinv: !invG Σ}, (|={,E}=> P)%I) ( P)%I.
Proof.
iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
iPoseProof (Hfupd Hinv) as "H".
......@@ -68,8 +68,8 @@ Proof.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.
Lemma step_fupdN_soundness `{invPreG Σ} φ n :
( `{Hinv: invG Σ}, (|={,}=>^n |={,}=> φ : iProp Σ)%I)
Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
( `{Hinv: !invG Σ}, (|={,}=>^n |={,}=> φ : iProp Σ)%I)
φ.
Proof.
intros Hiter.
......@@ -86,8 +86,8 @@ Proof.
iNext. by iMod "Hφ".
Qed.
Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
( `{Hinv: invG Σ}, (|={,}=>^n φ : iProp Σ)%I)
Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
( `{Hinv: !invG Σ}, (|={,}=>^n φ : iProp Σ)%I)
φ.
Proof.
iIntros (Hiter). eapply (step_fupdN_soundness _ n).
......
......@@ -28,7 +28,7 @@ Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
Proof. solve_inG. Qed.
Section definitions.
Context `{hG : gen_heapG L V Σ}.
Context `{Countable L, hG : !gen_heapG L V Σ}.
Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
own (gen_heap_name hG) ( (to_gen_heap σ)).
......@@ -72,7 +72,7 @@ Section to_gen_heap.
Proof. by rewrite /to_gen_heap fmap_delete. Qed.
End to_gen_heap.
Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
(|==> _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
......@@ -81,7 +81,7 @@ Proof.
Qed.
Section gen_heap.
Context `{gen_heapG L V Σ}.
Context `{Countable L, !gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
......
......@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Import uPred.
(** Derived forms and lemmas about them. *)
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
( i P', i (N:coPset) (P' P) ownI i P')%I.
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
......@@ -16,7 +16,7 @@ Instance: Params (@inv) 3 := {}.
Typeclasses Opaque inv.
Section inv.
Context `{invG Σ}.
Context `{!invG Σ}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.
......
......@@ -16,7 +16,7 @@ Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{invG Σ, na_invG Σ}.
Context `{!invG Σ, !na_invG Σ}.
Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
own p (CoPset E, GSet ).
......@@ -30,7 +30,7 @@ Instance: Params (@na_inv) 3 := {}.
Typeclasses Opaque na_own na_inv.
Section proofs.
Context `{invG Σ, na_invG Σ}.
Context `{!invG Σ, !na_invG Σ}.
Global Instance na_own_timeless p E : Timeless (na_own p E).
Proof. rewrite /na_own; apply _. Qed.
......
......@@ -47,11 +47,11 @@ Ltac solve_inG :=
split; (assumption || by apply _).
(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4 := {}.
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Definition own_aux : seal (@own_def). by eexists. Qed.
Definition own {Σ A i} := own_aux.(unseal) Σ A i.
......@@ -61,7 +61,7 @@ Typeclasses Opaque own.
(** * Properties about ghost ownership *)
Section global.
Context `{inG Σ A}.
Context `{Hin: !inG Σ A}.
Implicit Types a : A.
(** ** Properties of [iRes_singleton] *)
......@@ -113,9 +113,9 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
Lemma later_own γ a : own γ a - ( b, own γ b (a b)).
Proof.
rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
assert (NonExpansive (λ r : iResUR Σ, r (inG_id H) !! γ)).
assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
{ intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
rewrite (f_equiv (λ r : iResUR Σ, r (inG_id H) !! γ) _ r).
rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
rewrite {1}/iRes_singleton ofe_fun_lookup_singleton lookup_singleton.
rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
{ by rewrite and_elim_r /sbi_except_0 -or_intro_l. }
......@@ -125,7 +125,7 @@ Proof.
cmra_transport Heq (cmra_transport (eq_sym Heq) a) = a) as ->
by (by intros ?? ->).
apply ownM_mono=> /=.
exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id H))) r).
exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
intros i'. rewrite ofe_fun_lookup_op.
destruct (decide (i' = inG_id _)) as [->|?].
+ rewrite ofe_fun_lookup_insert ofe_fun_lookup_singleton.
......@@ -196,7 +196,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Proof.
rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, ofe_fun_singleton_update_empty.
......@@ -206,13 +206,13 @@ Proof.
Qed.
(** Big op class instances *)
Instance own_cmra_sep_homomorphism `{inG Σ (A:ucmraT)} :
Instance own_cmra_sep_homomorphism `{!inG Σ (A:ucmraT)} :
WeakMonoidHomomorphism op uPred_sep () (own γ).
Proof. split; try apply _. apply own_op. Qed.
(** Proofmode class instances *)
Section proofmode_classes.
Context `{inG Σ A}.
Context `{!inG Σ A}.
Implicit Types a b : A.
Global Instance into_sep_own γ a b1 b2 :
......
......@@ -17,14 +17,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
subG (savedAnythingΣ F) Σ savedAnythingG Σ F.
Proof. solve_inG. Qed.
Definition saved_anything_own `{savedAnythingG Σ F}
Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ)) : iProp Σ :=
own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything.
Context `{savedAnythingG Σ F}.
Context `{!savedAnythingG Σ F}.
Implicit Types x y : F (iProp Σ).
Implicit Types γ : gname.
......@@ -65,22 +65,22 @@ End saved_anything.
Notation savedPropG Σ := (savedAnythingG Σ ( )).
Notation savedPropΣ := (savedAnythingΣ ( )).
Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
Definition saved_prop_own `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
saved_anything_own (F := ) γ (Next P).
Instance saved_prop_own_contractive `{savedPropG Σ} γ :
Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
Contractive (saved_prop_own γ).
Proof. solve_contractive. Qed.
Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
Lemma saved_prop_alloc_strong `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
(|==> γ, ⌜γ G saved_prop_own γ P)%I.
Proof. iApply saved_anything_alloc_strong. Qed.
Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
(|==> γ, saved_prop_own γ P)%I.
Proof. iApply saved_anything_alloc. Qed.
Lemma saved_prop_agree `{savedPropG Σ} γ P Q :
Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
saved_prop_own γ P - saved_prop_own γ Q - (P Q).
Proof.
iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
......@@ -90,25 +90,25 @@ Qed.
Notation savedPredG Σ A := (savedAnythingG Σ (A -c> )).
Notation savedPredΣ A := (savedAnythingΣ (A -c> )).
Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A iProp Σ) :=
Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A iProp Σ) :=
saved_anything_own (F := A -c> ) γ (CofeMor Next Φ).
Instance saved_pred_own_contractive `{savedPredG Σ A} γ :
Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
Contractive (saved_pred_own γ : (A -c> iProp Σ) iProp Σ).
Proof.
solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
Qed.
Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A iProp Σ) :
Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (G : gset gname) (Φ : A iProp Σ) :
(|==> γ, ⌜γ G saved_pred_own γ Φ)%I.
Proof. iApply saved_anything_alloc_strong. Qed.
Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A iProp Σ) :
Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A iProp Σ) :
(|==> γ, saved_pred_own γ Φ)%I.
Proof. iApply saved_anything_alloc. Qed.
(* We put the `x` on the outside to make this lemma easier to apply. *)
Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
saved_pred_own γ Φ - saved_pred_own γ Ψ - (Φ x Ψ x).
Proof.
unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
......
......@@ -16,7 +16,7 @@ Instance subG_stsΣ Σ sts :
Proof. solve_inG. Qed.
Section definitions.
Context `{stsG Σ sts} (γ : gname).
Context `{!stsG Σ sts} (γ : gname).
Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
own γ (sts_frag S T).
......@@ -57,7 +57,7 @@ Instance: Params (@sts_own) 5 := {}.
Instance: Params (@sts_ctx) 6 := {}.
Section sts.
Context `{invG Σ, stsG Σ sts}.
Context `{!invG Σ, !stsG Σ sts}.
Implicit Types φ : sts.state sts iProp Σ.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.
......
......@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
( (P - |={E1,E2}=> Q))%I.
Arguments vs {_ _} _ _ _%I _%I.
......@@ -22,7 +22,7 @@ Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
format "P ={ E }=> Q") : stdpp_scope.
Section vs.
Context `{invG Σ}.
Context `{!invG Σ}.
Implicit Types P Q R : iProp Σ.
Implicit Types N : namespace.
......
......@@ -35,30 +35,30 @@ Import invG.
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
to_agree (Next (iProp_unfold P)).
Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name ( {[ i := invariant_unfold P ]}).
Arguments ownI {_ _} _ _%I.
Typeclasses Opaque ownI.
Instance: Params (@invariant_unfold) 1 := {}.
Instance: Params (@ownI) 3 := {}.
Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
Definition ownE `{!invG Σ} (E : coPset) : iProp Σ :=
own enabled_name (CoPset E).
Typeclasses Opaque ownE.
Instance: Params (@ownE) 3 := {}.
Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
Definition ownD `{!invG Σ} (E : gset positive) : iProp Σ :=
own disabled_name (GSet E).
Typeclasses Opaque ownD.
Instance: Params (@ownD) 3 := {}.
Definition wsat `{invG Σ} : iProp Σ :=
Definition wsat `{!invG Σ} : iProp Σ :=
locked ( I : gmap positive (iProp Σ),
own invariant_name ( (invariant_unfold <$> I : gmap _ _))
[ map] i Q I, Q ownD {[i]} ownE {[i]})%I.
Section wsat.
Context `{invG Σ}.
Context `{!invG Σ}.
Implicit Types P : iProp Σ.
(* Invariants *)
......@@ -194,7 +194,7 @@ Qed.
End wsat.
(* Allocation of an initial world *)
Lemma wsat_alloc `{invPreG Σ} : (|==> _ : invG Σ, wsat ownE )%I.
Lemma wsat_alloc `{!invPreG Σ} : (|==> _ : invG Σ, wsat ownE )%I.
Proof.
iIntros.
iMod (own_alloc ( ( : gmap _ _))) as (γI) "HI"; first done.
......
......@@ -8,7 +8,7 @@ Section class_instances.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
@IntoPure (uPredI M) ( a) ( a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
......
......@@ -693,7 +693,7 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
NonExpansive Ψ a b Ψ a Ψ b.
Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
Lemma fun_ext `{B : A ofeT} (g1 g2 : ofe_fun B) :
Lemma fun_ext {A} {B : A ofeT} (g1 g2 : ofe_fun B) :
( i, g1 i g2 i) g1 g2.
Proof. by unseal. Qed.
Lemma sig_eq {A : ofeT} (P : A Prop) (x y : sigC P) :
......@@ -797,7 +797,7 @@ Proof. unseal. by destruct mx. Qed.
Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : a ⌜✓ a.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
Lemma ofe_fun_validI `{B : A ucmraT} (g : ofe_fun B) : g i, g i.
Lemma ofe_fun_validI {A} {B : A ucmraT} (g : ofe_fun B) : g i, g i.
Proof. by unseal. Qed.
(** Consistency/soundness statement *)
......
......@@ -14,8 +14,8 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
( `{!heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
......
......@@ -9,7 +9,7 @@ Definition assert : val :=
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Lemma twp_assert `{heapG Σ} E (Φ : val iProp Σ) e :
Lemma twp_assert `{!heapG Σ} E (Φ : val iProp Σ) e :
WP e @ E [{ v, v = #true Φ #() }] -
WP assert (LamV BAnon e)%V @ E [{ Φ }].
Proof.
......@@ -17,7 +17,7 @@ Proof.
wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e :
Lemma wp_assert `{!heapG Σ} E (Φ : val iProp Σ) e :
WP e @ E {{ v, v = #true Φ #() }} -
WP assert (LamV BAnon e)%V @ E {{ Φ }}.
Proof.
......
......@@ -14,7 +14,7 @@ Class heapG Σ := HeapG {
heapG_proph_mapG :> proph_mapG proph_id val Σ
}.
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ κs _ :=
(gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I;
......@@ -117,7 +117,7 @@ Instance pure_injrc (v : val) :
PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.
......@@ -152,7 +152,7 @@ Instance pure_case_inr v e1 e2 :
Proof. solve_pure_exec. Qed.
Section lifting.
Context `{heapG Σ}.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types efs : list expr.
......
......@@ -7,11 +7,11 @@ From iris.heap_lang Require Import notation.
Set Default Proof Using "Type".
Import uPred.
Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
Lemma tac_wp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
( (e'':=e'), e = e'')
envs_entails Δ (WP e' @ s; E {{ Φ }}) envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed.
Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
Lemma tac_twp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
( (e'':=e'), e = e'')
envs_entails Δ (WP e' @ s; E [{ Φ }]) envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. by intros ->. Qed.
......@@ -28,7 +28,7 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
| _ => fail "wp_expr_eval: not a 'wp'"
end.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
MaybeIntoLaterNEnvs n Δ Δ'
......@@ -38,7 +38,7 @@ Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
Lemma tac_twp_pure `{!heapG Σ} Δ s E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
envs_entails Δ (WP e2 @ s; E [{ Φ }])
......@@ -47,10 +47,10 @@ Proof.
rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
Qed.
Lemma tac_wp_value `{heapG Σ} Δ s E Φ v :
Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
envs_entails Δ (Φ v) envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
Lemma tac_twp_value `{heapG Σ} Δ s E Φ v :
Lemma tac_twp_value `{!heapG Σ} Δ s E Φ v :
envs_entails Δ (Φ v) envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
......@@ -135,12 +135,12 @@ Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "wp_pair" := wp_pure (Pair _ _).
Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
Lemma tac_wp_bind `{!heapG Σ} K Δ s E Φ e f :
f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I
envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
Lemma tac_twp_bind `{heapG Σ} K Δ s E Φ e f :
Lemma tac_twp_bind `{!heapG Σ} K Δ s E Φ e f :
f = (λ e, fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I
envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
......@@ -171,7 +171,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
(** Heap tactics *)
Section heap.