Commit a71965c4 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue #95.

parent baa7a380
......@@ -492,12 +492,15 @@ Qed.
(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
env_spatial_is_nil Δ = true
(if env_spatial_is_nil Δ then Unit else PersistentP P)
envs_app false (Esnoc Enil i P) Δ = Some Δ'
(Δ' Q) Δ P Q.
Proof.
intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
by rewrite right_id always_wand_impl always_elim HQ.
intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
- rewrite (persistentP Δ) envs_app_sound //; simpl.
by rewrite right_id always_wand_impl always_elim.
- apply impl_intro_l. rewrite envs_app_sound //; simpl.
by rewrite always_and_sep_l right_id wand_elim_r.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
IntoPersistentP P P'
......
......@@ -299,8 +299,10 @@ Local Tactic Notation "iIntro" constr(H) :=
first
[ (* (?Q → _) *)
eapply tac_impl_intro with _ H; (* (i:=H) *)
[reflexivity || fail 1 "iIntro: introducing" H
"into non-empty spatial context"
[env_cbv; apply _ ||
let P := lazymatch goal with |- PersistentP ?P => P end in
fail 1 "iIntro: introducing non-persistent" H ":" P
"into non-empty spatial context"
|env_reflexivity || fail "iIntro:" H "not fresh"
|]
| (* (_ -∗ _) *)
......
......@@ -77,6 +77,9 @@ Proof.
done.
Qed.
Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P Q P Q)%I.
Proof. iIntros "H1 H2". by iFrame. Qed.
Lemma test_fast_iIntros P Q :
( x y z : nat,
x = plus 0 x y = 0 z = 0 P Q foo (x x))%I.
......
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