Commit 46151cd2 authored by Dan Frumin's avatar Dan Frumin

Allow multiple arguments in `iEval .. in` and `iSimpl in`.

parent cdc564bf
...@@ -160,6 +160,7 @@ Rewriting / simplification ...@@ -160,6 +160,7 @@ Rewriting / simplification
with the resulting `P`, which in turn becomes the new proof mode goal / with the resulting `P`, which in turn becomes the new proof mode goal /
hypothesis `H`. hypothesis `H`.
Note that parentheses around `tac` are needed. 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 / - `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
hypothesis `H`. This is a shorthand for `iEval (simpl)`. hypothesis `H`. This is a shorthand for `iEval (simpl)`.
......
...@@ -101,6 +101,16 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi ...@@ -101,6 +101,16 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
--------------------------------------∗ --------------------------------------∗
⌜S (S (S x)) = y⌝ ⌜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" "test_iFrame_later_1"
: string : string
1 subgoal 1 subgoal
......
...@@ -473,6 +473,11 @@ Check "test_iSimpl_in". ...@@ -473,6 +473,11 @@ Check "test_iSimpl_in".
Lemma test_iSimpl_in x y : (3 + x)%nat = y - S (S (S x)) = y : PROP. 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. 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. Lemma test_iIntros_pure_neg : ( ¬False : PROP)%I.
Proof. by iIntros (?). Qed. Proof. by iIntros (?). Qed.
......
...@@ -114,13 +114,21 @@ Tactic Notation "iEval" tactic(t) := ...@@ -114,13 +114,21 @@ Tactic Notation "iEval" tactic(t) :=
[let x := fresh in intros x; t; unfold x; reflexivity [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) := Tactic Notation "iEval" tactic(t) "in" constr(H) :=
iStartProof; iStartProof;
eapply tac_eval_in with _ H _ _ _; let Hs := words H in iEval_go t Hs.
[pm_reflexivity || fail "iEval:" H "not found"
|let x := fresh in intros x; t; unfold x; reflexivity
|pm_reflexivity
|].
Tactic Notation "iSimpl" := iEval (simpl). Tactic Notation "iSimpl" := iEval (simpl).
Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H. Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment