Commit 6d66d9d1 authored by Robbert Krebbers's avatar Robbert Krebbers

Support ■ (∀ _, _) and ■ (_ → _) in iIntros.

parent d4a687a8
Pipeline #3023 passed with stage
in 10 minutes and 5 seconds
......@@ -475,6 +475,9 @@ Proof.
intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Qed.
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
(φ Δ ψ) Δ (φ ψ).
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ (φ Δ Q) Δ P Q.
Proof.
intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
......@@ -777,6 +780,10 @@ Qed.
Lemma tac_forall_intro {A} Δ (Φ : A uPred M) : ( a, Δ Φ a) Δ a, Φ a.
Proof. apply forall_intro. Qed.
Lemma tac_pure_forall_intro {A} Δ (φ : A Prop) :
( a, Δ φ a) Δ a, φ a.
Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
Class ForallSpecialize {As} (xs : hlist As)
(P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P Φ xs.
Arguments forall_specialize {_} _ _ _ {_}.
......
......@@ -684,7 +684,9 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
apply _ || fail "iIntro:" P "not pure"|]
|(* (?P -∗ _) *) eapply tac_wand_intro_pure;
[let P := match goal with |- IntoPure ?P _ => P end in
apply _ || fail "iIntro:" P "not pure"|]];
apply _ || fail "iIntro:" P "not pure"|]
|(* (■ ∀ _, _) *) apply tac_pure_forall_intro
|(* (■ (_ → _)) *) apply tac_pure_impl_intro];
intros x.
Local Tactic Notation "iIntro" constr(H) := first
......
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