diff --git a/ProofMode.md b/ProofMode.md index 4e8a1599321c85be80a156960f0daffe31d01a2d..29dfbd9cf592b38621cf53102376d7d64362fefc 100644 --- a/ProofMode.md +++ b/ProofMode.md @@ -160,6 +160,7 @@ Rewriting / simplification with the resulting `P`, which in turn becomes the new proof mode goal / hypothesis `H`. Note that parentheses around `tac` are needed. + If `H` is a list of hypothesis, then `iEval` will perform `tac` on each of them. - `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal / hypothesis `H`. This is a shorthand for `iEval (simpl)`. diff --git a/tests/proofmode.ref b/tests/proofmode.ref index b9a27dc9eb3129d554629394d5179e5117e133bd..8dd4d71389a44d98c87363ad04ff85705e327ea0 100644 --- a/tests/proofmode.ref +++ b/tests/proofmode.ref @@ -101,6 +101,16 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi --------------------------------------∗ ⌜S (S (S x)) = y⌝ +1 subgoal + + PROP : sbi + x, y, z : nat + ============================ + "H1" : ⌜S (S (S x)) = y⌝ + "H2" : ⌜S y = z⌝ + --------------------------------------∗ + ⌜S (S (S x)) = y⌝ + "test_iFrame_later_1" : string 1 subgoal diff --git a/tests/proofmode.v b/tests/proofmode.v index c5689c2ebd7f95e13e309044da68525ba1bdd0c4..b8762b7aead1076ba0b88321736ed1eab919867a 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -473,6 +473,11 @@ Check "test_iSimpl_in". Lemma test_iSimpl_in x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP. Proof. iIntros "H". iSimpl in "H". Show. done. Qed. +Lemma test_iSimpl_in_2 x y z : + ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ (1 + y)%nat = z ⌝ -∗ + ⌜ S (S (S x)) = y ⌝ : PROP. +Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed. + Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I. Proof. by iIntros (?). Qed. diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v index 30c42ee1f0c9ac9ac0589b9dd3c41a489c04f6c8..b62920a2c466ff131e76c3ccb7a639eb5e7b6069 100644 --- a/theories/proofmode/ltac_tactics.v +++ b/theories/proofmode/ltac_tactics.v @@ -114,13 +114,21 @@ Tactic Notation "iEval" tactic(t) := [let x := fresh in intros x; t; unfold x; reflexivity |]. +Ltac iEval_go t Hs := + match Hs with + | [] => idtac + | ?H :: ?Hs => + let H := pretty_ident H in + eapply tac_eval_in with _ H _ _ _; + [pm_reflexivity || fail "iEval:" H "not found" + |let x := fresh in intros x; t; unfold x; reflexivity + |pm_reflexivity + |iEval_go t Hs] + end. + Tactic Notation "iEval" tactic(t) "in" constr(H) := iStartProof; - eapply tac_eval_in with _ H _ _ _; - [pm_reflexivity || fail "iEval:" H "not found" - |let x := fresh in intros x; t; unfold x; reflexivity - |pm_reflexivity - |]. + let Hs := words H in iEval_go t Hs. Tactic Notation "iSimpl" := iEval (simpl). Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.