Commit 1fcbf679 authored by Robbert Krebbers's avatar Robbert Krebbers

Strengthen `tac_specialize_assert` to put the result in the intuitionistic context.

The result of `iSpecialize ("H" with "[H1 .. Hn]")` was always put in the
spatial context. This commit strenghtens this tactic by putting the result
in the intuitionistic context if the following conditions hold:

1. The hypothesis `H` is persistent.
2. All the hypotheses `H1 .. Hn` are intuitionistic (or similarly, in case
   `[-H1 .. Hn]` is used, if all remaining hypotheses are intuitionistic).
3. If the pattern `[> ..]` for adding a modality is not used.
parent c7842c94
......@@ -286,13 +286,14 @@ Proof.
- by rewrite HR assoc !wand_elim_r.
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)
''(Δ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] *)
| 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.
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.
Lemma tac_unlock_emp Δ Q : envs_entails Δ Q envs_entails Δ (emp locked 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"
|iSolveTC || fail "iSpecialize: goal not a modality"
lazymatch goal with
| |- False =>
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