From b90b85b0ed9d754800c37a9548078d6b0e378915 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 27 Apr 2016 20:56:46 +0200 Subject: [PATCH] Make iIntros work when the implication is hidden behind a definition. --- proofmode/tactics.v | 60 ++++++++++++++++++++++----------------------- tests/proofmode.v | 8 +++++- 2 files changed, 36 insertions(+), 32 deletions(-) diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 68caa8b..2cbeaac 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 edddb37..5fb1366 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. -- GitLab