diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v index 29882b430f48636e440f3cbfbec518a4ad739d40..77406583c647c5dbe4fa06ccac6b5c11a82709a7 100644 --- a/proofmode/coq_tactics.v +++ b/proofmode/coq_tactics.v @@ -292,10 +292,7 @@ Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q. Proof. by rewrite -(False_elim Q). Qed. (** * Pure *) -Lemma tac_pure_intro Δ (φ : Prop) : φ → Δ ⊢ ■φ. -Proof. apply const_intro. Qed. - -Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊢ ■φ. +Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊣⊢ ■φ. Arguments to_pure : clear implicits. Global Instance to_pure_const φ : ToPure (■φ) φ. Proof. done. Qed. @@ -305,6 +302,9 @@ Proof. intros; red. by rewrite timeless_eq. Qed. Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure (✓ a) (✓ a). Proof. intros; red. by rewrite discrete_valid. Qed. +Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ → φ → Δ ⊢ Q. +Proof. intros ->. apply const_intro. Qed. + Lemma tac_pure Δ Δ' i p P φ Q : envs_lookup_delete i Δ = Some (p, P, Δ') → ToPure P φ → (φ → Δ' ⊢ Q) → Δ ⊢ Q. diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 222ae275c1813b6b65858e428e83495213b5df1a..4bfb81df087be0c687bde5673536236196b368b9 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -113,7 +113,10 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := apply _ || fail "iPure:" H ":" P "not pure" |intros pat]. -Tactic Notation "iPureIntro" := apply uPred.const_intro. +Tactic Notation "iPureIntro" := + eapply tac_pure_intro; + [let P := match goal with |- ToPure ?P _ => P end in + apply _ || fail "iPureIntro:" P "not pure"|]. (** * Specialize *) Record iTrm {X As} := @@ -751,5 +754,5 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) := iRewriteCore true t in H. (* Make sure that by and done solve trivial things in proof mode *) -Hint Extern 0 (of_envs _ ⊢ _) => by apply tac_pure_intro. +Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro. Hint Extern 0 (of_envs _ ⊢ _) => iAssumption. diff --git a/tests/proofmode.v b/tests/proofmode.v index b5e863c38821c2af64307339865001332c549afe..8146ab1158e1e817638df0621ba6604ad016a421 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -72,9 +72,10 @@ Proof. Qed. Lemma demo_6 (M : cmraT) (P Q : uPred M) : - True ⊢ (∀ x y z, x = 0 → y = 0 → z = 0 → P → □ Q → foo False). + True ⊢ (∀ x y z : nat, + x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x)). Proof. iIntros {a} "*". iIntros "#Hfoo **". - by iIntros "%". + by iIntros "# _". Qed.