From 46151cd28b97d15137ae63b25e2dadc1adbc1656 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 1 May 2019 16:53:18 +0200
Subject: [PATCH] Allow multiple arguments in `iEval .. in` and `iSimpl in`.

---
 ProofMode.md                      |  1 +
 tests/proofmode.ref               | 10 ++++++++++
 tests/proofmode.v                 |  5 +++++
 theories/proofmode/ltac_tactics.v | 18 +++++++++++++-----
 4 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 4e8a15993..29dfbd9cf 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 b9a27dc9e..8dd4d7138 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 c5689c2eb..b8762b7ae 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 30c42ee1f..b62920a2c 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.
-- 
GitLab