...
 
Commits (28)
......@@ -30,20 +30,23 @@ variables:
build-coq.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
CI_COQCHK: "1"
build-coq.8.10.1:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.1"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
TIMING_CONF: "coq-8.10.1"
tags:
- fp-timing
build-coq.8.10.0:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version 8.10.0"
build-coq.8.9.1:
......@@ -55,12 +58,6 @@ build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
DOC_OPTS: "--external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
......
......@@ -26,6 +26,8 @@ a feature branch instead.
* Wait for CI to publish a new std++ version on the opam archive, then run
`opam update iris-dev`.
* In Iris, change the `opam` file to depend on the new version.
(In case you do not use opam yourself, you can see recently published versions
[in this repository](https://gitlab.mpi-sws.org/iris/opam/commits/master).)
* Run `make build-dep` (in Iris) to install the new version of std++.
You may have to do `make clean` as Coq will likely complain about .vo file
mismatches.
......
......@@ -9,7 +9,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
rm -f Makefile.coq .lia.cache
.PHONY: clean
# Create Coq Makefile.
......
......@@ -24,16 +24,19 @@ PROJECTS = [
{ 'name': 'lambda-rust', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'lambda-rust', 'branch': 'ci/weak_mem', 'vars': ['STDPP_REV', 'IRIS_REV', 'ORC11_REV', 'GPFSL_REV'] }, # covers GPFSL and ORC11
{ 'name': 'iron', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'fairis', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'ora', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'reloc', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'c', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'tutorial-popl18', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'spygame', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] }, # these do not work, for some reason
{ 'name': 'time-credits', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
{ 'name': 'actris', 'branch': 'master', 'vars': ['STDPP_REV', 'IRIS_REV'] },
]
for project in PROJECTS:
print("Triggering build for {}{}...".format(project['name'], '' if project['branch'] == 'master' else ':'+project['branch']))
url = "https://gitlab.mpi-sws.org/api/v4/projects/iris%2F{}/pipeline".format(project['name'])
id = str(project['id']) if 'id' in project else "iris%2F{}".format(project['name'])
url = "https://gitlab.mpi-sws.org/api/v4/projects/{}/pipeline".format(id)
json = {
'ref': project['branch'],
'variables': list(map(lambda var: { 'key': var, 'value': os.environ.get(var, "master") }, project['vars'])),
......
......@@ -578,13 +578,13 @@ Tactic failure: iStartProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
"iPoseProofCoreLem (open_constr) as (tactic3)" and
"iIntoEmpValid", last call failed.
Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
......@@ -604,7 +604,7 @@ Tactic failure: iPoseProof: "Hx" not found.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
fun Htmp =>
......
......@@ -6,6 +6,12 @@ Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_eauto_emp_isplit_biwand P : emp P - P.
Proof. eauto 6. Qed.
Lemma test_eauto_isplit_biwand P : (P - P)%I.
Proof. eauto. Qed.
Check "demo_0".
Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P).
Proof.
......@@ -158,7 +164,7 @@ Proof.
iIntros "H".
let H1 := iFresh in
let H2 := iFresh in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
iDestruct "H" as pat.
iFrame.
Qed.
......
......@@ -220,6 +220,11 @@ Section iris_tests.
iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
eauto.
Qed.
Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
x' x
own γ x - own γ x'.
Proof. intros. by iApply own_mono. Qed.
End iris_tests.
Section monpred_tests.
......
......@@ -68,12 +68,12 @@ Tactic failure: iFrame: cannot frame (P i).
Σ : gFunctors
invG0 : invG Σ
N : namespace
P : iProp Σ
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> P) ⎤
"H2" : ⎡ ▷ <pers> P
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟
--------------------------------------□
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
1 subgoal
......@@ -81,12 +81,12 @@ Tactic failure: iFrame: cannot frame (P i).
Σ : gFunctors
invG0 : invG Σ
N : namespace
P : iProp Σ
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> P) ⎤
"H2" : ⎡ ▷ <pers> P
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟
--------------------------------------□
"Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
"Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P
|={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟
......@@ -174,22 +174,31 @@ Section tests_iprop.
Context {I : biIndex} `{!invG Σ}.
Local Notation monPred := (monPred I (iPropI Σ)).
Implicit Types P : iProp Σ.
Implicit Types P Q R : monPred.
Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
Lemma test_iInv_0 N P:
embed (B:=monPred) (inv N (<pers> P)) ={}= ⎡▷ P.
Lemma test_iInv_0 N 𝓟 :
embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟.
Proof.
iIntros "#H".
iInv N as "#H2". Show.
iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
Qed.
Lemma test_iInv_0_with_close N P:
embed (B:=monPred) (inv N (<pers> P)) ={}= ⎡▷ P.
Lemma test_iInv_0_with_close N 𝓟 :
embed (B:=monPred) (inv N (<pers> 𝓟)) ={}= ⎡▷ 𝓟.
Proof.
iIntros "#H".
iInv N as "#H2" "Hclose". Show.
iMod ("Hclose" with "H2").
iModIntro. iModIntro. by iNext.
Qed.
Lemma test_iPoseProof `{inG Σ A} P γ (x y : A) :
x ~~> y P own γ x == own γ y.
Proof.
iIntros (?) "[_ Hγ]".
iPoseProof (own_update with "Hγ") as "H"; first done.
by iMod "H".
Qed.
End tests_iprop.
......@@ -622,7 +622,7 @@ Qed.
Global Instance id_free_op_r x y : IdFree y Cancelable x IdFree (x y).
Proof.
intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
eapply (id_free0_r y); [by eapply cmra_validN_op_r |symmetry; eauto].
Qed.
Global Instance id_free_op_l x y : IdFree x Cancelable y IdFree (x y).
Proof. intros. rewrite comm. apply _. Qed.
......
......@@ -271,7 +271,7 @@ Proof.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox").
iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
- iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
......@@ -279,7 +279,7 @@ Proof.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox").
iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
Qed.
......@@ -296,14 +296,14 @@ Proof.
iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox")
as (γ ?) "[#Hslice Hbox]"; first done.
iExists γ. iIntros "{$% $#} !>". iNext.
iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox").
iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
- iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
{ by simplify_map_eq. }
iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iIntros "{$% $#} !>". iNext.
iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox").
iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed.
End box.
......
......@@ -93,5 +93,5 @@ Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
Proof.
iIntros (Hiter). eapply (step_fupdN_soundness _ n).
iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
iApply (step_fupdN_wand with "Hiter"). by iApply (fupd_mask_weaken _ _ _).
iApply (step_fupdN_wand with "Hiter"). by iApply fupd_mask_weaken.
Qed.
......@@ -11,6 +11,10 @@ higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) :=
InG { inG_id : gid Σ; inG_prf : A = gFunctors_lookup Σ inG_id (iPrePropO Σ) _ }.
Arguments inG_id {_ _} _.
(** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
not want Coq to pick one arbitrarily. *)
Hint Mode inG - ! : typeclass_instances.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPrePropO Σ) _).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
......@@ -90,7 +94,7 @@ Proof. intros a1 a2. apply own_mono. Qed.
Lemma own_valid γ a : own γ a a.
Proof.
rewrite !own_eq /own_def ownM_valid /iRes_singleton.
rewrite discrete_fun_validI (forall_elim (inG_id _)) discrete_fun_lookup_singleton.
rewrite discrete_fun_validI (forall_elim (inG_id Hin)) discrete_fun_lookup_singleton.
rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
(* implicit arguments differ a bit *)
by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
......@@ -113,7 +117,7 @@ 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 Hin) !! γ)).
{ intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
{ intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id Hin)). }
rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton.
rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
......@@ -126,7 +130,7 @@ Proof.
apply ownM_mono=> /=.
exists (discrete_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
intros i'. rewrite discrete_fun_lookup_op.
destruct (decide (i' = inG_id _)) as [->|?].
destruct (decide (i' = inG_id Hin)) as [->|?].
+ rewrite discrete_fun_lookup_insert discrete_fun_lookup_singleton.
intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
* by rewrite lookup_singleton lookup_delete Hb.
......@@ -149,7 +153,7 @@ Proof.
intros HP Ha.
rewrite -(bupd_mono ( m, ⌜∃ γ, P γ m = iRes_singleton γ a uPred_ownM m)%I).
- rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
eapply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty (inG_id _));
eapply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty (inG_id Hin));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
......@@ -205,7 +209,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 γ (ε:A))%I.
Proof.
rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, discrete_fun_singleton_update_empty.
......
......@@ -95,7 +95,8 @@ Proof. iApply saved_anything_alloc. Qed.
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").
iIntros "HP HQ". iApply later_equivI.
iApply (saved_anything_agree (F := ) with "HP HQ").
Qed.
(* Saved predicates. *)
......@@ -129,6 +130,6 @@ 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.
iDestruct (saved_anything_agree with "HΦ HΨ") as "Heq".
iDestruct (saved_anything_agree (F := A -d> ) with "HΦ HΨ") as "Heq".
by iDestruct (discrete_fun_equivI with "Heq") as "?".
Qed.
......@@ -108,7 +108,7 @@ Section greatest.
F (bi_greatest_fixpoint F) x bi_greatest_fixpoint F x.
Proof.
iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
iSplit; last done. iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
iSplit; last done. iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed.
......
......@@ -76,7 +76,7 @@ Proof.
iMod (fupd_plain_mask with "H") as %?; eauto.
Qed.
Lemma wptp_strong_adequacy Φ κs' s n e1 t1 κs e2 t2 σ1 σ2 :
Lemma wptp_strong_adequacy Φ κs' s n e1 t1 κs t2 σ1 σ2 :
nsteps n (e1 :: t1, σ1) κs (t2, σ2)
state_interp σ1 (κs ++ κs') (length t1) -
WP e1 @ s; {{ Φ }} -
......
......@@ -4,6 +4,13 @@ From iris.proofmode Require Import base modality_instances classes ltac_tactics.
Set Default Proof Using "Type".
Import bi.
(** The follow lemma is not an instance, but defined using a [Hint Extern] to
enable the better unification algorithm. *)
Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Hint Extern 0 (FromAssumption _ _ _) =>
notypeclasses refine (from_assumption_exact _ _) : typeclass_instances.
Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
......@@ -59,9 +66,6 @@ Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 10
Proof. by rewrite /IntoAbsorbingly. Qed.
(** FromAssumption *)
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Global Instance from_assumption_persistently_r P Q :
FromAssumption true P Q KnownRFromAssumption true P (<pers> Q).
Proof.
......
......@@ -498,9 +498,9 @@ Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid : φ bi_emp_valid P.
Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_here : AsEmpValid φ P.
as_emp_valid_0 : AsEmpValid φ P.
Arguments AsEmpValid0 {_} _%type _%I.
Existing Instance as_emp_valid_here | 0.
Existing Instance as_emp_valid_0 | 0.
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
φ bi_emp_valid P.
......
......@@ -452,8 +452,19 @@ Proof.
by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
Qed.
Lemma tac_pose_proof Δ j P Q :
P
Definition IntoEmpValid (φ : Type) (P : PROP) := φ bi_emp_valid P.
Lemma into_emp_valid_here φ P : AsEmpValid φ P IntoEmpValid φ P.
Proof. by intros [??]. Qed.
Lemma into_emp_valid_impl (φ ψ : Type) P :
φ IntoEmpValid ψ P IntoEmpValid (φ ψ) P.
Proof. rewrite /IntoEmpValid; auto. Qed.
Lemma into_emp_valid_forall {A} (φ : A Type) P x :
IntoEmpValid (φ x) P IntoEmpValid ( x : A, φ x) P.
Proof. rewrite /IntoEmpValid; auto. Qed.
Lemma tac_pose_proof Δ j (φ : Prop) P Q :
φ
IntoEmpValid φ P
match envs_app true (Esnoc Enil j P) Δ with
| None => False
| Some Δ' => envs_entails Δ' Q
......@@ -461,8 +472,8 @@ Lemma tac_pose_proof Δ j P Q :
envs_entails Δ Q.
Proof.
destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=.
by rewrite -HP /= intuitionistically_emp emp_wand.
rewrite envs_entails_eq => ? HP <-. rewrite envs_app_singleton_sound //=.
by rewrite -HP //= intuitionistically_emp emp_wand.
Qed.
Lemma tac_pose_proof_hyp Δ i j Q :
......
......@@ -70,7 +70,7 @@ Tactic Notation "iStartProof" :=
| |- envs_entails _ _ => idtac
| |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
[iSolveTC || fail "iStartProof: not a BI assertion"
|apply tac_start]
|notypeclasses refine (tac_start _ _)]
end.
(* Same as above, with 2 differences :
......@@ -720,56 +720,9 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
(ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
(* The tactic [iIntoEmpValid] tactic solves a goal [bi_emp_valid Q]. The
argument [t] must be a Coq term whose type is of the following shape:
[∀ (x_1 : A_1) .. (x_n : A_n), φ]
and so that we have an instance `AsValid φ Q`.
Examples of such [φ]s are
- [bi_emp_valid P], in which case [Q] should be [P]
- [P1 ⊢ P2], in which case [Q] should be [P1 -∗ P2]
- [P1 ⊣⊢ P2], in which case [Q] should be [P1 ↔ P2]
The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [R] for each non-dependent argument [x_i : R]. For example, if the
original goal was [Q] and [t] has type [∀ x, P x → Q], then it generates an evar
[?x] for [x] and a subgoal [P ?x]. *)
Local Ltac iIntoEmpValid t :=
let 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. *)
| ?P ?Q => let H := fresh in assert P as H; [|iIntoEmpValid uconstr:(t H); clear H]
| _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
(* This is a workarround for Coq bug #6583. *)
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; iIntoEmpValid (t e')
end
in
(* We try two reduction tactics for the type of t before trying to
specialize it. We first try the head normal form in order to
unfold all the definition that could hide an entailment. Then,
we try the much weaker [eval cbv zeta], because entailment is
not necessarilly opaque, and could be unfolded by [hnf].
However, for calling type class search, we only use [cbv zeta]
in order to make sure we do not unfold [bi_emp_valid]. *)
let tT := type of t in
first
[ 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
notypeclasses refine (as_emp_valid_1 tT _ _);
[iSolveTC || fail 1 "iPoseProof: not a BI assertion"
|exact t]].
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
let Δ := iGetCtx in
eapply tac_pose_proof_hyp with H Hnew;
notypeclasses refine (tac_pose_proof_hyp _ H Hnew _ _);
pm_reduce;
lazymatch goal with
| |- False =>
......@@ -785,10 +738,26 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
| _ => idtac
end.
Tactic Notation "iPoseProofCoreLem" constr(lem) "as" tactic3(tac) :=
Ltac iIntoEmpValid_go := first
[(* Case [φ ψ] *)
notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
[(*goal for [φ] *)|iIntoEmpValid_go]
|(* Case [ x : A, φ] *)
notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
|(* Case [P Q], [P ⊣⊢ Q], [bi_emp_valid P] *)
notypeclasses refine (into_emp_valid_here _ _ _)].
(** Factor out the base case of the loop to avoid needless backtracking *)
Ltac iIntoEmpValid :=
iIntoEmpValid_go;
[.. (* goals for premises *)
|iSolveTC ||
let φ := lazymatch goal with |- AsEmpValid ?φ _ => φ end in
fail "iPoseProof:" φ "not a BI assertion"].
Tactic Notation "iPoseProofCoreLem" open_constr(lem) "as" tactic3(tac) :=
let Hnew := iFresh in
eapply tac_pose_proof with Hnew _; (* (j:=H) *)
[iIntoEmpValid lem
notypeclasses refine (tac_pose_proof _ Hnew _ _ _ lem _ _);
[iIntoEmpValid
|pm_reduce;
lazymatch goal with
| |- False =>
......@@ -3151,6 +3120,7 @@ Tactic Notation "iAccu" :=
(** Automation *)
Hint Extern 0 (_ _) => iStartProof : core.
Hint Extern 0 (bi_emp_valid _) => iStartProof : core.
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
......@@ -3184,6 +3154,7 @@ Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?) : core.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit : core.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit : core.
Hint Extern 1 (envs_entails _ (_ - _)) => iSplit : core.
Hint Extern 1 (envs_entails _ ( _)) => iNext : core.
Hint Extern 1 (envs_entails _ ( _)) => iAlways : core.
Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways : core.
......
......@@ -6,7 +6,7 @@ Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
(P : monPred I PROP) (𝓟 : PROP) :=
make_monPred_at : P i ⊣⊢ 𝓟.
Arguments MakeMonPredAt {_ _} _ _%I _%I.
Hint Mode MakeMonPredAt + + - ! - : typeclass_instances.
Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i j.
Hint Mode IsBiIndexRel + - - : typeclass_instances.
......@@ -213,7 +213,7 @@ Proof.
Qed.
Lemma into_wand_monPred_at_unknown_unknown p q R P 𝓟 Q 𝓠 i :
IntoWand p q R P Q MakeMonPredAt i P 𝓟 MakeMonPredAt i Q 𝓠
IntoWand p q R P Q MakeMonPredAt i P 𝓟 MakeMonPredAt i Q 𝓠
IntoWand p q (R i) 𝓟 𝓠.
Proof.
rewrite /IntoWand /MakeMonPredAt /bi_affinely_if /bi_persistently_if.
......