From 2539f33565a71a79aa613ace11336f530f900428 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 26 Apr 2016 17:52:26 +0200 Subject: [PATCH] Move iIntro tactics arround. --- proofmode/tactics.v | 78 ++++++++++++++++++++++----------------------- 1 file changed, 38 insertions(+), 40 deletions(-) diff --git a/proofmode/tactics.v b/proofmode/tactics.v index b9551f12..68caa8b8 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -97,46 +97,6 @@ Tactic Notation "iAssumption" := (** * False *) Tactic Notation "iExFalso" := apply tac_ex_falso. -(** * Pure introduction *) -Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := - lazymatch goal with - | |- _ ⊢ (∀ _, _) => apply tac_forall_intro; intros x - | |- _ ⊢ (?P → _) => - eapply tac_impl_intro_pure; - [apply _ || fail "iIntro:" P "not pure"|]; intros x - | |- _ ⊢ (?P -★ _) => - eapply tac_wand_intro_pure; - [apply _ || fail "iIntro:" P "not pure"|]; intros x - | |- _ => intros x - end. - -(** * Introduction *) -Local Tactic Notation "iIntro" constr(H) := - lazymatch goal with - | |- _ ⊢ (?Q → _) => - eapply tac_impl_intro with _ H; (* (i:=H) *) - [reflexivity || fail "iIntro: introducing " H ":" Q - "into non-empty spatial context" - |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] - | |- _ ⊢ (_ -★ _) => - eapply tac_wand_intro with _ H; (* (i:=H) *) - [env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] - | _ => fail "iIntro: nothing to introduce" - end. - -Local Tactic Notation "iIntro" "#" constr(H) := - lazymatch goal with - | |- _ ⊢ (?P → _) => - eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *) - [apply _ || fail "iIntro: " P " not persistent" - |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] - | |- _ ⊢ (?P -★ _) => - eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *) - [apply _ || fail "iIntro: " P " not persistent" - |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] - | _ => fail "iIntro: nothing to introduce" - end. - (** * Making hypotheses persistent or pure *) Local Tactic Notation "iPersistent" constr(H) := eapply tac_persistent with _ H _ _ _; (* (i:=H) *) @@ -685,6 +645,44 @@ Tactic Notation "iNext":= apply _ || fail "iNext:" P "does not contain laters"|]. (** * Introduction tactic *) +Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := + lazymatch goal with + | |- _ ⊢ (∀ _, _) => apply tac_forall_intro; intros x + | |- _ ⊢ (?P → _) => + eapply tac_impl_intro_pure; + [apply _ || fail "iIntro:" P "not pure"|]; intros x + | |- _ ⊢ (?P -★ _) => + eapply tac_wand_intro_pure; + [apply _ || fail "iIntro:" P "not pure"|]; intros x + | |- _ => intros x + end. + +Local Tactic Notation "iIntro" constr(H) := + lazymatch goal with + | |- _ ⊢ (?Q → _) => + eapply tac_impl_intro with _ H; (* (i:=H) *) + [reflexivity || fail "iIntro: introducing " H ":" Q + "into non-empty spatial context" + |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] + | |- _ ⊢ (_ -★ _) => + eapply tac_wand_intro with _ H; (* (i:=H) *) + [env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] + | _ => fail "iIntro: nothing to introduce" + end. + +Local Tactic Notation "iIntro" "#" constr(H) := + lazymatch goal with + | |- _ ⊢ (?P → _) => + eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *) + [apply _ || fail "iIntro: " P " not persistent" + |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] + | |- _ ⊢ (?P -★ _) => + eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *) + [apply _ || fail "iIntro: " P " not persistent" + |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|] + | _ => fail "iIntro: nothing to introduce" + end. + Tactic Notation "iIntros" constr(pat) := let rec go pats := lazymatch pats with -- GitLab