Commit f2d12f84 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'gen_proofmode' of into gen_proofmode

parents abd4de45 fdc94f14
......@@ -5,7 +5,7 @@ Import uPred.
(** The "core" of an assertion is its maximal persistent part. *)
Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
( Q, (Q Q) (P Q) Q)%I.
( Q, (P Q) Q)%I.
Instance: Params (@coreP) 1.
Typeclasses Opaque coreP.
......@@ -14,15 +14,10 @@ Section core.
Implicit Types P Q : uPred M.
Lemma coreP_intro P : P - coreP P.
Proof. rewrite /coreP. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
Proof. rewrite /coreP. iIntros "HP" (Q) "HPQ". by iApply "HPQ". Qed.
Global Instance coreP_persistent P : Persistent (coreP P).
rewrite /coreP /Persistent. iIntros "HC" (Q). rewrite !affine_affinely.
iApply persistently_impl_plainly. iIntros "#HQ".
iApply persistently_impl_plainly. iIntros "#HPQ".
iApply "HQ". by iApply "HC"; rewrite !affine_affinely.
Proof. rewrite /coreP /Persistent. iIntros "#HC" (Q) "!#". iApply "HC". Qed.
Global Instance coreP_ne : NonExpansive (@coreP M).
Proof. solve_proper. Qed.
......@@ -30,13 +25,12 @@ Section core.
Proof. solve_proper. Qed.
Global Instance coreP_mono : Proper (() ==> ()) (@coreP M).
rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q) "#HQ #HPQ".
iApply ("H" $! Q with "[]"); first done. by rewrite HP.
Proof. solve_proper. Qed.
Lemma coreP_elim P : Persistent P coreP P - P.
Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P with "[]"). auto.
Lemma coreP_wand P Q : (coreP P Q) (P Q).
......@@ -44,6 +38,6 @@ Section core.
- iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
iAlways. by iApply HP.
- iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
iDestruct (coreP_elim with "HcQ") as "#HQ". done.
by iDestruct (coreP_elim with "HcQ") as "#HQ".
End core.
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Export gmap gset coPset.
From iris.algebra Require Import gset coPset.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......@@ -630,8 +630,8 @@ Tactic Notation "iIntoValid" open_constr(t) :=
in order to make sure we do not unfold [bi_valid]. *)
let tT := type of t in
[ let tT' := eval hnf in tT in go_specilize t tT'
| let tT' := eval cbv zeta in tT in go_specilize t tT'
[ let tT' := eval hnf in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in
eapply (as_valid_1 tT);
(* Doing [apply _] here fails because that will try to solve all evars
......@@ -641,7 +641,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
elsewhere. With [typeclasses eauto], that seems to work better. *)
[solve [ typeclasses eauto with typeclass_instances ] ||
fail "iPoseProof: not a BI assertion"|exact t]]
with go_specilize t tT :=
with go_specialize t tT :=
lazymatch tT with (* We do not use hnf of tT, because, if
entailment is not opaque, then it would
unfold it. *)
......@@ -1903,5 +1903,4 @@ Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro.
Hint Extern 2 (envs_entails _ (_ _)) => progress iFrame : iFrame.
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