...
 
Commits (1)
......@@ -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
"iPoseProofCoreLem (open_constr) as (tactic3)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: 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 =>
......
......@@ -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.
......@@ -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.
......
......@@ -744,9 +744,7 @@ Local Ltac iIntoEmpValid t :=
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 := fresh in evar (e:T);
let e' := eval unfold e in e in clear e; iIntoEmpValid (t e')
end
in
......@@ -769,7 +767,7 @@ Local Ltac iIntoEmpValid 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,9 +783,9 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
| _ => idtac
end.
Tactic Notation "iPoseProofCoreLem" constr(lem) "as" tactic3(tac) :=
Tactic Notation "iPoseProofCoreLem" open_constr(lem) "as" tactic3(tac) :=
let Hnew := iFresh in
eapply tac_pose_proof with Hnew _; (* (j:=H) *)
notypeclasses refine (tac_pose_proof _ Hnew _ _ _ _);
[iIntoEmpValid lem
|pm_reduce;
lazymatch goal with
......