Commit dba20c7f authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'robbert/iSpecialize_tweaks' into 'master'

Better handling of persistent results in `iDestruct`, `iPoseProof`, `iAssert` and friends

See merge request iris/iris!341
parents 8169d405 cecf3d62
Pipeline #23447 passed with stage
in 14 minutes and 48 seconds
......@@ -46,6 +46,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
basic proofmode support.
* Sealed the definitions of `big_opS`, `big_opMS`, `big_opM` and `big_sepM2`
to prevent undesired simplification.
* Better handling of persistent results in `iDestruct`, `iPoseProof`, `iAssert`,
and friends. See https://gitlab.mpi-sws.org/iris/iris/merge_requests/341 for
more details.
## Iris 3.2.0 (released 2019-08-29)
......
......@@ -66,6 +66,24 @@ In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr) as #",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
last call failed.
Tactic failure: iSpecialize: Q not persistent.
"test_iAssert_intuitionistic"
: string
The command has indeed failed with message:
In nested Ltac calls to "<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first done",
"<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first done",
"iAssert (open_constr) with (constr) as (constr)",
"iAssertCore (open_constr) with (constr) as (constr) (tactic3)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: (|==> P)%I not persistent.
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
......
......@@ -157,6 +157,62 @@ Lemma test_iSpecialize_Coq_entailment P Q R :
P (P - Q) Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iSpecialize_intuitionistic P Q R :
P - (P - P - P - P - P - P - Q) - R - R (P Q).
Proof.
iIntros "#HP #H HR".
(* Test that [H] remains in the intuitionistic context *)
iSpecialize ("H" with "HP").
iSpecialize ("H" with "[HP]"); first done.
iSpecialize ("H" with "[]"); first done.
iSpecialize ("H" with "[-HR]"); first done.
iSpecialize ("H" with "[#]"); first done.
iFrame "HR".
iSpecialize ("H" with "[-]"); first done.
by iFrame "#".
Qed.
Lemma test_iSpecialize_intuitionistic_2 P Q R :
P - (P - P - P - P - P - P - Q) - R - R (P Q).
Proof.
iIntros "#HP #H HR".
(* Test that [H] remains in the intuitionistic context *)
iSpecialize ("H" with "HP") as #.
iSpecialize ("H" with "[HP]") as #; first done.
iSpecialize ("H" with "[]") as #; first done.
iSpecialize ("H" with "[-HR]") as #; first done.
iSpecialize ("H" with "[#]") as #; first done.
iFrame "HR".
iSpecialize ("H" with "[-]") as #; first done.
by iFrame "#".
Qed.
Lemma test_iSpecialize_intuitionistic_3 P Q R :
P - (P - Q) - (P - <pers> Q) - (Q - R) - P (Q R).
Proof.
iIntros "HP #H1 #H2 #H3".
(* Should fail, [Q] is not persistent *)
Fail iSpecialize ("H1" with "HP") as #.
(* Should succeed, [<pers> Q] is persistent *)
iSpecialize ("H2" with "HP") as #.
(* Should succeed, despite [R] not being persistent, no spatial premises are
needed to prove [Q] *)
iSpecialize ("H3" with "H2") as #.
by iFrame "#".
Qed.
Check "test_iAssert_intuitionistic".
Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
P - |==> P.
Proof.
iIntros "#HP".
(* Test that [HPupd1] ends up in the intuitionistic context *)
iAssert (|==> P)%I with "[]" as "#HPupd1"; first done.
(* This should not work, [|==> P] is not persistent. *)
Fail iAssert (|==> P)%I with "[#]" as "#HPupd2"; first done.
done.
Qed.
Lemma test_iPure_intro_emp R `{!Affine R} :
R - emp.
Proof. iIntros "HR". by iPureIntro. Qed.
......
......@@ -17,6 +17,10 @@ the actual operations that may appear in users' proofs. *)
Lemma lazy_andb_true (b1 b2 : bool) : b1 &&& b2 = true b1 = true b2 = true.
Proof. destruct b1, b2; intuition congruence. Qed.
Definition negb (b : bool) : bool := if b then false else true.
Lemma negb_true b : negb b = true b = false.
Proof. by destruct b. Qed.
Fixpoint Pos_succ (x : positive) : positive :=
match x with
| (p~1)%positive => ((Pos_succ p)~0)%positive
......@@ -94,7 +98,10 @@ Qed.
Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
(** Copies of some [option] combinators for better reduction control. *)
(** Copies of some functions on [list] and [option] for better reduction control. *)
Fixpoint pm_app {A} (l1 l2 : list A) : list A :=
match l1 with [] => l2 | x :: l1 => x :: pm_app l1 l2 end.
Definition pm_option_bind {A B} (f : A option B) (mx : option A) : option B :=
match mx with Some x => f x | None => None end.
Arguments pm_option_bind {_ _} _ !_ /.
......
......@@ -286,13 +286,14 @@ Proof.
- by rewrite HR assoc !wand_elim_r.
Qed.
Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
envs_lookup j Δ = Some (q, R)
IntoWand q false R P1 P2 AddModal P1' P1 Q
IntoWand q false R P1 P2
(if am then AddModal P1' P1 Q else TCEq P1' P1)
match
''(Δ1,Δ2) envs_split (if neg is true then Right else Left)
js (envs_delete true j q Δ);
Δ2' envs_app false (Esnoc Enil j P2) Δ2;
js (envs_delete true j q Δ);
Δ2' envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2') (* does not preserve position of [j] *)
with
| Some (Δ1,Δ2') =>
......@@ -301,15 +302,21 @@ Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
| None => False
end envs_entails Δ Q.
Proof.
rewrite envs_entails_eq. intros ??? HQ.
rewrite envs_entails_eq. intros ?? Hmod HQ.
destruct (_ = _) as [[Δ1 Δ2']|] eqn:?; last done.
destruct HQ as [HP1 HQ].
destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_singleton_sound Δ2) //; simpl.
rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
apply wand_intro_l. by rewrite assoc !wand_elim_r.
rewrite -intuitionistically_if_idemp (into_wand q false) /=.
destruct (negb am &&& q &&& env_spatial_is_nil Δ1) eqn:Hp; simpl.
- move: Hp. rewrite !lazy_andb_true negb_true. intros [[-> ->] ?]; simpl.
destruct Hmod. rewrite env_spatial_is_nil_intuitionistically // HP1.
by rewrite assoc intuitionistically_sep_2 wand_elim_l wand_elim_r HQ.
- rewrite intuitionistically_if_elim HP1. destruct am; last destruct Hmod.
+ by rewrite assoc -(comm _ P1') -assoc wand_trans HQ.
+ by rewrite assoc wand_elim_l wand_elim_r HQ.
Qed.
Lemma tac_unlock_emp Δ Q : envs_entails Δ Q envs_entails Δ (emp locked Q).
......@@ -319,18 +326,18 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
Lemma tac_unlock Δ Q : envs_entails Δ Q envs_entails Δ (locked Q).
Proof. by unlock. Qed.
Lemma tac_specialize_frame Δ j q R P1 P2 P1' Q Q' :
Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
envs_lookup j Δ = Some (q, R)
IntoWand q false R P1 P2
AddModal P1' P1 Q
(if am then AddModal P1' P1 Q else TCEq P1' P1)
envs_entails (envs_delete true j q Δ) (P1' locked Q')
Q' = (P2 - Q)%I
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq. intros ??? HPQ ->.
rewrite envs_entails_eq. intros ?? Hmod HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
apply wand_intro_l. by rewrite assoc !wand_elim_r.
rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
Qed.
Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
......
......@@ -903,15 +903,13 @@ Ltac iSpecializePat_go H1 pats :=
fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
notypeclasses refine (tac_specialize_assert _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _);
notypeclasses refine (tac_specialize_assert _ H1 _
(if m is GModal then true else false) lr Hs' _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|lazymatch m with
| GSpatial => class_apply add_modal_id
| GModal => iSolveTC || fail "iSpecialize: goal not a modality"
end
|iSolveTC || fail "iSpecialize: goal not a modality"
|pm_reduce;
lazymatch goal with
| |- False =>
......@@ -934,15 +932,13 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reduce; solve [iFrame "∗ #"]
|pm_reduce; iSpecializePat_go H1 pats]
| SAutoFrame ?m :: ?pats =>
notypeclasses refine (tac_specialize_frame _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
notypeclasses refine (tac_specialize_frame _ H1 _
(if m is GModal then true else false) _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|lazymatch m with
| GSpatial => class_apply add_modal_id
| GModal => iSolveTC || fail "iSpecialize: goal not a modality"
end
|iSolveTC || fail "iSpecialize: goal not a modality"
|pm_reduce;
first
[notypeclasses refine (tac_unlock_emp _ _ _)
......@@ -955,15 +951,66 @@ Ltac iSpecializePat_go H1 pats :=
Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
let pats := spec_pat.parse pat in iSpecializePat_go H pats.
(** The argument [p] denotes whether the conclusion of the specialized term is
intuitionistic. If so, one can use all spatial hypotheses for both proving the
premises and the remaning goal. The argument [p] can either be a Boolean or an
introduction pattern, which will be coerced into [true] when it solely contains
`#` or `%` patterns at the top-level.
(** The tactics [iSpecialize trm as #] and [iSpecializeCore trm as true] allow
one to use the entire spatial context /twice/: the first time for proving the
premises [Q1 .. Qn] of [H : Q1 -* .. -∗ Qn -∗ R], and the second time for
proving the remaining goal. This is possible if all of the following properties
hold:
1. The conclusion [R] of the hypothesis [H] is persistent.
2. The specialization pattern [[> ..]] for wrapping a modality is not used for
any of the premises [Q1 .. Qn].
3. The BI is either affine, or the hypothesis [H] resides in the intuitionistic
context.
The copying of the context for proving the premises of [H] and the remaining
goal is implemented using the lemma [tac_specialize_intuitionistic_helper].
Since the tactic [iSpecialize .. as #] is used a helper to implement
[iDestruct .. as "#.."], [iPoseProof .. as "#.."], [iSpecialize .. as "#.."],
and friends, the behavior on violations of these conditions is as follows:
- If condition 1 is violated (i.e. the conclusion [R] of [H] is not persistent),
the tactic will fail.
- If condition 2 or 3 is violated, the tactic will fall back to consuming the
hypotheses for proving the premises [Q1 .. Qn]. That is, it will fall back to
not using [tac_specialize_intuitionistic_helper].
The function [use_tac_specialize_intuitionistic_helper Δ pat] below returns
[true] iff the specialization pattern [pat] consumes any spatial hypotheses,
and does not contain the pattern [[> ..]] (cf. condition 2). If the function
returns [false], then the conclusion can be moved in the intuitionistic context
even if conditions 1 and 3 do not hold. Therefore, in that case, we prefer
putting the conclusion to the intuitionistic context directly and not using
[tac_specialize_intuitionistic_helper], which requires conditions 1 and 3. *)
Fixpoint use_tac_specialize_intuitionistic_helper {M}
(Δ : envs M) (pats : list spec_pat) : bool :=
match pats with
| [] => false
| (SForall | SPureGoal _) :: pats =>
use_tac_specialize_intuitionistic_helper Δ pats
| SAutoFrame _ :: _ => true
| SIdent H _ :: pats =>
match envs_lookup_delete false H Δ with
| Some (false, _, Δ) => true
| Some (true, _, Δ) => use_tac_specialize_intuitionistic_helper Δ pats
| None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
end
| SGoal (SpecGoal GModal _ _ _ _) :: _ => false
| SGoal (SpecGoal GIntuitionistic _ _ _ _) :: pats =>
use_tac_specialize_intuitionistic_helper Δ pats
| SGoal (SpecGoal GSpatial neg Hs_frame Hs _) :: pats =>
match envs_split (if neg is true then Right else Left)
(if neg then Hs else pm_app Hs_frame Hs) Δ with
| Some (Δ1,Δ2) => if env_spatial_is_nil Δ1
then use_tac_specialize_intuitionistic_helper Δ2 pats
else true
| None => false (* dummy case (invalid pattern, will fail in the tactic anyway) *)
end
end.
In case the specialization pattern in [t] states that the modality of the goal
should be kept for one of the premises (i.e. [>[H1 .. Hn]] is used) then [p]
defaults to [false] (i.e. spatial hypotheses are not preserved). *)
(** The argument [p] of [iSpecializeCore] can either be a Boolean, or an
introduction pattern that is coerced into [true] when it solely contains [#] or
[%] patterns at the top-level. *)
Tactic Notation "iSpecializeCore" open_constr(H)
"with" open_constr(xs) open_constr(pat) "as" constr(p) :=
let p := intro_pat_intuitionistic p in
......@@ -976,25 +1023,17 @@ Tactic Notation "iSpecializeCore" open_constr(H)
iSpecializeArgs H xs; [..|
lazymatch type of H with
| ident =>
(* The lemma [tac_specialize_intuitionistic_helper] allows one to use the
whole spatial context for:
- proving the premises of the lemma we specialize, and,
- the remaining goal.
We can only use if all of the following properties hold:
- The result of the specialization is persistent.
- No modality is eliminated.
- If the BI is not affine, the hypothesis should be in the intuitionistic
context.
As an optimization, we do only use [tac_specialize_intuitionistic_helper]
if no implications nor wands are eliminated, i.e. [pat ≠ []]. *)
let pat := spec_pat.parse pat in
lazymatch eval compute in
(p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
let Δ := iGetCtx in
(* Check if we should use [tac_specialize_intuitionistic_helper]. Notice
that [pm_eval] does not unfold [use_tac_specialize_intuitionistic_helper],
so we should do that first. *)
let b := eval cbv [use_tac_specialize_intuitionistic_helper] in
(if p then use_tac_specialize_intuitionistic_helper Δ pat else false) in
lazymatch eval pm_eval in b with
| true =>
(* Check that if the BI is not affine, the hypothesis is in the
intuitionistic context. *)
(* Check that the BI is either affine, or the hypothesis [H] resides
in the intuitionistic context. *)
lazymatch iTypeOf H with
| Some (?q, _) =>
let PROP := iBiOfGoal in
......@@ -1003,10 +1042,11 @@ Tactic Notation "iSpecializeCore" open_constr(H)
notypeclasses refine (tac_specialize_intuitionistic_helper _ H _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity
(* This premise, [envs_lookup j Δ = Some (q,P)],
holds because [iTypeOf] succeeded *)
holds because the [iTypeOf] above succeeded *)
|pm_reduce; iSolveTC
(* This premise, [if q then TCTrue else BiAffine PROP],
holds because [q || TC_to_bool (BiAffine PROP)] is true *)
(* This premise, [if q then TCTrue else BiAffine PROP], holds
because we established that [q || TC_to_bool (BiAffine PROP)]
is true *)
|iSpecializePat H pat;
[..
|notypeclasses refine (tac_specialize_intuitionistic_helper_done _ H _ _ _);
......
......@@ -6,7 +6,8 @@ From iris.proofmode Require Import base environments.
do not reduce e.g. before unification happens in [iApply].*)
Declare Reduction pm_eval := cbv [
(* base *)
base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
base.negb base.beq
base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
(* environments *)
env_lookup env_lookup_delete env_delete env_app env_replace
env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
......@@ -15,8 +16,8 @@ Declare Reduction pm_eval := cbv [
envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
envs_split_go envs_split
env_to_prop_go env_to_prop env_to_prop_and_go env_to_prop_and
(* PM option combinators *)
pm_option_bind pm_from_option pm_option_fun
(* PM list and option functions *)
pm_app pm_option_bind pm_from_option pm_option_fun
].
Ltac pm_eval t :=
eval pm_eval in t.
......
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