...
 
Commits (5)
......@@ -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 =>
......
......@@ -193,4 +193,12 @@ Section tests_iprop.
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.
......@@ -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.
......@@ -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.
......
......@@ -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.
......
......@@ -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 :
......
......@@ -720,58 +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), φ]
for which we have an instance [AsEmpValid φ ?Q].
Examples of such [φ]s are
- [bi_emp_valid P], in which case [Q] is unified with [P].
- [P1 ⊢ P2], in which case [Q] is unified with [P1 -∗ P2].
- [P1 ⊣⊢ P2], in which case [Q] is unified with [P1 ↔ P2].
The tactic instantiates each dependent argument [x_i : A_i] with an evar and
generates a goal [A_i] for each non-dependent argument [x_i : A_i].
For example, if the initial goal is [bi_emp_valid ?Q] and [t] has type
[∀ x, P x → R x], then it generates an evar [?x] for [x], a subgoal [P ?x],
and unifies [?Q] with [R 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 =>
......@@ -787,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 =>
......
......@@ -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.
......