diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 68caa8b8742829523b47636cccb1934d98f7a83a..2cbeaac53e09aea5e206185ed615fc1fab83d3b4 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -645,43 +645,41 @@ 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 → _) => +Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first + [ (* (∀ _, _) *) apply tac_forall_intro; intros x + | (* (?P → _) *) eapply tac_impl_intro_pure; + [let P := match goal with |- ToPure ?P _ => P end in + apply _ || fail "iIntro:" P "not pure" + |intros x] + | (* (?P -★ _) *) eapply tac_wand_intro_pure; + [let P := match goal with |- ToPure ?P _ => P end in + apply _ || fail "iIntro:" P "not pure" + |intros x] + |intros x]. + +Local Tactic Notation "iIntro" constr(H) := first + [ (* (?Q → _) *) eapply tac_impl_intro with _ H; (* (i:=H) *) - [reflexivity || fail "iIntro: introducing " H ":" Q - "into non-empty spatial context" + [reflexivity || fail 1 "iIntro: introducing" H + "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. + [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|] + | fail 1 "iIntro: nothing to introduce" ]. -Local Tactic Notation "iIntro" "#" constr(H) := - lazymatch goal with - | |- _ ⊢ (?P → _) => +Local Tactic Notation "iIntro" "#" constr(H) := first + [ (* (?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 -★ _) => + [let P := match goal with |- ToPersistentP ?P _ => P end in + apply _ || fail 1 "iIntro: " P " not persistent" + |env_cbv; reflexivity || fail 1 "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. + [let P := match goal with |- ToPersistentP ?P _ => P end in + apply _ || fail 1 "iIntro: " P " not persistent" + |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|] + | fail 1 "iIntro: nothing to introduce" ]. Tactic Notation "iIntros" constr(pat) := let rec go pats := diff --git a/tests/proofmode.v b/tests/proofmode.v index edddb370780b6ae6f06eeebb45481e6c36ba1f3c..5fb1366a50720455eb6272c980b801b857eabb39 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -44,4 +44,10 @@ Qed. Lemma demo_3 (M : cmraT) (P1 P2 P3 : uPred M) : (P1 ★ P2 ★ P3) ⊢ (▷ P1 ★ ▷ (P2 ★ ∃ x, (P3 ∧ x = 0) ∨ P3)). -Proof. iIntros "(\$ & \$ & H)". iFrame "H". iNext. by iExists 0. Qed. \ No newline at end of file +Proof. iIntros "(\$ & \$ & H)". iFrame "H". iNext. by iExists 0. Qed. + +Definition foo {M} (P : uPred M) := (P → P)%I. +Definition bar {M} : uPred M := (∀ P, foo P)%I. + +Lemma demo_4 (M : cmraT) : True ⊢ @bar M. +Proof. iIntros {P} "HP". done. Qed.