Commit 0b462620 authored by Robbert Krebbers's avatar Robbert Krebbers

Define `iAssert` using `iSpecialize`.

This made the definition much simpler, and provides support for all
specialization patterns (although most are not very useful in
combination with `iAssert`).
parent 23ed2310
......@@ -913,40 +913,12 @@ Proof.
by rewrite -{1}persistently_idemp !affinely_persistently_elim impl_elim_r.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
AddModal P' P Q
envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
envs_entails Δ1 P' envs_entails Δ2' Q envs_entails Δ Q.
Proof.
rewrite envs_entails_eq=>??? HP HQ. rewrite envs_split_sound //.
rewrite (envs_app_singleton_sound Δ2) //; simpl. by rewrite HP HQ.
Qed.
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' neg js j P P' Q :
envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2)
Persistent P
FromAffinely P' P
envs_app false (Esnoc Enil j P') Δ = Some Δ'
envs_entails Δ1 P envs_entails Δ' Q envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ???? HP <-.
rewrite -(idemp bi_and (of_envs Δ)) {1}envs_split_sound //.
rewrite HP. rewrite (persistent_persistently_2 P) sep_elim_l.
rewrite persistently_and_affinely_sep_l -affinely_idemp.
rewrite affinely_persistently_elim from_affinely envs_app_singleton_sound //=.
by rewrite wand_elim_r.
Qed.
Lemma tac_assert_pure Δ Δ' j P P' φ Q :
FromPure true P φ
FromAffinely P' P
envs_app false (Esnoc Enil j P') Δ = Some Δ'
φ envs_entails Δ' Q envs_entails Δ Q.
Lemma tac_assert Δ Δ' j P Q :
envs_app true (Esnoc Enil j (P - P)%I) Δ = Some Δ'
envs_entails Δ' Q envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ???? <-. rewrite envs_app_singleton_sound //=.
rewrite -(from_affinely P') -(from_pure _ P) pure_True //.
by rewrite affinely_idemp affinely_True_emp affinely_emp emp_wand.
rewrite envs_entails_eq=> ? <-. rewrite (envs_app_singleton_sound Δ) //; simpl.
by rewrite -(entails_wand P) // affinely_persistently_emp emp_wand.
Qed.
Lemma tac_pose_proof Δ Δ' j P Q :
......@@ -1244,7 +1216,7 @@ Lemma tac_next Δ Δ' n Q Q' :
envs_entails Δ' Q' envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ?? HQ.
by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
Qed.
Lemma tac_löb Δ Δ' i Q :
......
......@@ -1687,56 +1687,15 @@ only contains `#` or `%` patterns at the top-level, and [false] otherwise. *)
Tactic Notation "iAssertCore" open_constr(Q)
"with" constr(Hs) "as" constr(p) tactic(tac) :=
iStartProof;
let p := intro_pat_persistent p in
let pats := spec_pat.parse Hs in
lazymatch pats with
| [_] => idtac
| _ => fail "iAssert: exactly one specialization pattern should be given"
end;
let H := iFresh in
let Hs := spec_pat.parse Hs in
lazymatch Hs with
| [SPureGoal ?d] =>
eapply tac_assert_pure with _ H Q _ _;
[apply _ || fail "iAssert:" Q "not pure"
|apply _
|env_reflexivity
|done_if d (*goal*)
|tac H]
| [SGoal (SpecGoal GPersistent _ ?Hs_frame [] ?d)] =>
eapply tac_assert_persistent with _ _ _ true [] H Q _;
[env_reflexivity
|apply _ || fail "iAssert:" Q "not persistent"
|apply _
|env_reflexivity
|iFrame Hs_frame; done_if d (*goal*)
|tac H]
| [SGoal (SpecGoal GPersistent false ?Hs_frame _ ?d)] =>
fail "iAssert: cannot select hypotheses for persistent proposition"
| [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d)] =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
let p' := eval cbv in (match m with GModal => false | _ => p end) in
lazymatch p' with
| false =>
eapply tac_assert with _ _ _ lr Hs' H Q _;
[lazymatch m with
| GSpatial => apply add_modal_id
| GModal => apply _ || fail "iAssert: goal not a modality"
end
|env_reflexivity ||
let Hs' := iMissingHyps Hs' in
fail "iAssert: hypotheses" Hs' "not found"
|env_reflexivity
|iFrame Hs_frame; done_if d (*goal*)
|tac H]
| true =>
eapply tac_assert_persistent with _ _ _ lr Hs' H Q _;
[env_reflexivity ||
let Hs' := iMissingHyps Hs' in
fail "iAssert: hypotheses" Hs' "not found"
|apply _ || fail "iAssert:" Q "not persistent"
|apply _
|env_reflexivity
|done_if d (*goal*)
|tac H]
end
| ?pat => fail "iAssert: invalid pattern" pat
end.
eapply tac_assert with _ H Q;
[env_reflexivity
|iSpecializeCore H with hnil pats as p; [..|tac H]].
Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
let p := intro_pat_persistent p in
......
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