Commit 307d0084 authored by Robbert Krebbers's avatar Robbert Krebbers

Have the `[$]` pattern succeed if the premise is `True` or `emp`.

In the same way that `iFrame` would succeed on said goals.
parent ad005c0c
......@@ -817,6 +817,10 @@ Proof.
apply wand_intro_l. by rewrite assoc !wand_elim_r.
Qed.
Lemma tac_unlock_emp Δ Q : envs_entails Δ Q envs_entails Δ (emp locked Q).
Proof. rewrite envs_entails_eq=> ->. by rewrite -lock left_id. Qed.
Lemma tac_unlock_True Δ Q : envs_entails Δ Q envs_entails Δ (True locked Q).
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.
......
......@@ -553,8 +553,11 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
| GSpatial => apply add_modal_id
| GModal => apply _ || fail "iSpecialize: goal not a modality"
end
|iFrame "∗ #"; apply tac_unlock ||
fail "iSpecialize: premise cannot be solved by framing"
|first
[apply tac_unlock_emp
|apply tac_unlock_True
|iFrame "∗ #"; apply tac_unlock
|fail "iSpecialize: premise cannot be solved by framing"]
|reflexivity]; iIntro H1; go H1 pats
end in let pats := spec_pat.parse pat in go H pats.
......
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