From 61e8aadd58880bd892c866edf20cc4da8e3dab50 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Sep 2016 10:28:16 +0200
Subject: [PATCH] =?UTF-8?q?Consistent=20syntax=20for=20generalization=20in?=
 =?UTF-8?q?=20iL=C3=B6b=20and=20iInduction.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

As proposed by JH Jourdan in issue 34.
---
 ProofMode.md               | 13 +++++----
 program_logic/weakestpre.v |  4 +--
 proofmode/tactics.v        | 56 ++++++++++++++++++++++++++++----------
 tests/heap_lang.v          |  2 +-
 tests/list_reverse.v       |  2 +-
 tests/tree_sum.v           |  2 +-
 6 files changed, 53 insertions(+), 26 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 7942e7683..de5340bf9 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -101,15 +101,16 @@ Separating logic specific tactics
 The later modality
 ------------------
 - `iNext` : introduce a later by stripping laters from all hypotheses.
-- `iLöb (x1 ... xn) as "IH"` : perform Löb induction by generalizing over the
-  Coq level variables `x1 ... xn` and the entire spatial context.
+- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction while generalizing
+  over the Coq level variables `x1 ... xn` and the entire spatial context.
 
 Induction
 ---------
-- `iInduction x as cpat "IH"` : perform induction on the Coq term `x`. The Coq
-  introduction pattern is used to name the introduced variables. The induction
-  hypotheses are inserted into the persistent context and given fresh names
-  prefixed `IH`.
+- `iInduction x as cpat "IH" forall (x1 ... xn)` : perform induction on the Coq
+  term `x`. The Coq introduction pattern is used to name the introduced
+  variables. The induction hypotheses are inserted into the persistent context
+  and given fresh names prefixed `IH`. The tactic generalizes over the Coq level
+  variables `x1 ... xn` and the entire spatial context.
 
 Rewriting
 ---------
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 38665fe9f..8d9119a44 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -91,7 +91,7 @@ Qed.
 Lemma wp_strong_mono E1 E2 e Φ Ψ :
   E1 ⊆ E2 → (∀ v, Φ v ={E2}=★ Ψ v) ★ WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}.
 Proof.
-  iIntros (?) "[HΦ H]". iLöb (e) as "IH". rewrite !wp_unfold /wp_pre.
+  iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
   iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight].
   { iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
     iApply ("HΦ" with "==>[-]"). by iApply (pvs_mask_mono E1 _). }
@@ -148,7 +148,7 @@ Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
   WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
 Proof.
-  iIntros "H". iLöb (E e Φ) as "IH". rewrite wp_unfold /wp_pre.
+  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
   iDestruct "H" as "[Hv|[% H]]".
   { iDestruct "Hv" as (v) "[Hev Hv]"; iDestruct "Hev" as % <-%of_to_val.
     by iApply pvs_wp. }
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 79643ca90..754ba2e55 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -899,9 +899,34 @@ Tactic Notation "iInductionCore" constr(x)
     end in
   induction x as pat; fix_ihs.
 
-Tactic Notation "iInduction" constr(x)
-    "as" simple_intropattern(pat) constr(IH) :=
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) :=
   iRevertIntros with (iInductionCore x as pat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ")" :=
+  iRevertIntros(x1) with (iInductionCore x as pat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ")" :=
+  iRevertIntros(x1 x2) with (iInductionCore x as pat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ident(x3) ")" :=
+  iRevertIntros(x1 x2 x3) with (iInductionCore x as pat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" :=
+  iRevertIntros(x1 x2 x3 x4) with (iInductionCore x as pat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+      "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")" :=
+  iRevertIntros(x1 x2 x3 x4 x5) with (iInductionCore x as aat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ")" :=
+  iRevertIntros(x1 x2 x3 x4 x5 x6) with (iInductionCore x as pat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
+    ident(x7) ")" :=
+  iRevertIntros(x1 x2 x3 x4 x5 x6 x7) with (iInductionCore x as pat IH).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
+    "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
+    ident(x7) ident(x8) ")" :=
+  iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) with (iInductionCore x as pat IH).
 
 (** * Löb Induction *)
 Tactic Notation "iLöbCore" "as" constr (IH) :=
@@ -911,26 +936,27 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
 
 Tactic Notation "iLöb" "as" constr (IH) :=
   iRevertIntros with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ")" "as" constr (IH) :=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" :=
   iRevertIntros(x1) with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ident(x2) ")" "as" constr (IH) :=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")" :=
   iRevertIntros(x1 x2) with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ")" "as" constr (IH) :=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
+    ident(x3) ")" :=
   iRevertIntros(x1 x2 x3) with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" "as"
-    constr (IH):=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
+    ident(x3) ident(x4) ")" :=
   iRevertIntros(x1 x2 x3 x4) with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ")" "as" constr (IH) :=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
+    ident(x3) ident(x4) ident(x5) ")" :=
   iRevertIntros(x1 x2 x3 x4 x5) with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ")" "as" constr (IH) :=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
+    ident(x3) ident(x4) ident(x5) ident(x6) ")" :=
   iRevertIntros(x1 x2 x3 x4 x5 x6) with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ")" "as" constr (IH) :=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
+    ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" :=
   iRevertIntros(x1 x2 x3 x4 x5 x6 x7) with (iLöbCore as IH).
-Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ident(x8) ")" "as" constr (IH) :=
+Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
+    ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" :=
   iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) with (iLöbCore as IH).
 
 (** * Assert *)
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index fec490322..3a1a31fd2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -44,7 +44,7 @@ Section LiftingTests.
     n1 < n2 →
     Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
-    iIntros (Hn) "HΦ". iLöb (n1 Hn) as "IH".
+    iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
     wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - iApply ("IH" with "[%] HΦ"). omega.
     - iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 4ab90f4c5..2e130b39e 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -32,7 +32,7 @@ Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp Σ) :
   ⊢ WP rev hd acc {{ Φ }}.
 Proof.
   iIntros "(#Hh & Hxs & Hys & HΦ)".
-  iLöb (hd acc xs ys Φ) as "IH". wp_rec. wp_let.
+  iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
   destruct xs as [|x xs]; iSimplifyEq.
   - wp_match. by iApply "HΦ".
   - iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 73a023c11..63cafec1f 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -41,7 +41,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) :
   ⊢ WP sum_loop v #l {{ Φ }}.
 Proof.
   iIntros "(#Hh & Hl & Ht & HΦ)".
-  iLöb (v t l n Φ) as "IH". wp_rec. wp_let.
+  iLöb as "IH" forall (v t l n Φ). wp_rec. wp_let.
   destruct t as [n'|tl tr]; simpl in *.
   - iDestruct "Ht" as "%"; subst.
     wp_match. wp_load. wp_op. wp_store.
-- 
GitLab