Commit 211c2363 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve `iIntros "_"`.

In the following ways:
- When having `P → Q` it will now also work when the spatial context
  is non-empty.
- When having `∀ x : A, Q` it will now do an `iIntros (_)`.
parent 7f04cf65
...@@ -483,6 +483,8 @@ Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ...@@ -483,6 +483,8 @@ Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ
Proof. Proof.
intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l. intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Qed. Qed.
Lemma tac_impl_intro_drop Δ P Q : (Δ Q) Δ P Q.
Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
Lemma tac_wand_intro Δ Δ' i P Q : Lemma tac_wand_intro Δ Δ' i P Q :
envs_app false (Esnoc Enil i P) Δ = Some Δ' (Δ' Q) Δ P - Q. envs_app false (Esnoc Enil i P) Δ = Some Δ' (Δ' Q) Δ P - Q.
...@@ -501,6 +503,8 @@ Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ...@@ -501,6 +503,8 @@ Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ
Proof. Proof.
intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l. intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Qed. Qed.
Lemma tac_wand_intro_drop Δ P Q : (Δ Q) Δ P - Q.
Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed.
(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact], (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
but it is doing some work to keep the order of hypotheses preserved. *) but it is doing some work to keep the order of hypotheses preserved. *)
......
...@@ -773,6 +773,14 @@ Local Tactic Notation "iIntro" "#" constr(H) := ...@@ -773,6 +773,14 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
|env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|] |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
| fail 1 "iIntro: nothing to introduce" ]. | fail 1 "iIntro: nothing to introduce" ].
Local Tactic Notation "iIntro" "_" :=
try iStartProof;
first
[ (* (?Q _) *) apply tac_impl_intro_drop
| (* (_ - _) *) apply tac_wand_intro_drop
| (* ( _, _) *) iIntro (_)
| fail 1 "iIntro: nothing to introduce" ].
Local Tactic Notation "iIntroForall" := Local Tactic Notation "iIntroForall" :=
try iStartProof; try iStartProof;
lazymatch goal with lazymatch goal with
...@@ -795,6 +803,7 @@ Tactic Notation "iIntros" constr(pat) := ...@@ -795,6 +803,7 @@ Tactic Notation "iIntros" constr(pat) :=
(* Optimizations to avoid generating fresh names *) (* Optimizations to avoid generating fresh names *)
| IPureElim :: ?pats => iIntro (?); go pats | IPureElim :: ?pats => iIntro (?); go pats
| IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats | IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats
| IDrop :: ?pats => iIntro _; go pats
| IName ?H :: ?pats => iIntro H; go pats | IName ?H :: ?pats => iIntro H; go pats
(* Introduction patterns that can only occur at the top-level *) (* Introduction patterns that can only occur at the top-level *)
| IPureIntro :: ?pats => iPureIntro; go pats | IPureIntro :: ?pats => iPureIntro; go 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