From 9ea6fa453f1b9ef1cd4b5b8a167d1fab717c895e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Feb 2017 21:33:09 +0100
Subject: [PATCH] Improve `iSpecialize ("H" $! x1 .. xn)`.

Instead of doing all the instantiations by invoking a single type
class search, it now performs the instantiations by invoking
individual type class searches. This a.) gives better error messages
and b.) works when `xj` depends on `xi`.
---
 theories/proofmode/class_instances.v |  7 +++++++
 theories/proofmode/classes.v         |  5 +++++
 theories/proofmode/coq_tactics.v     | 24 ++++--------------------
 theories/proofmode/tactics.v         | 20 +++++++++++---------
 4 files changed, 27 insertions(+), 29 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 3e985fc46..b623f0d48 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -601,6 +601,13 @@ Global Instance into_exist_laterN {A} n P (Φ : A → uPred M) :
   IntoExist P Φ → Inhabited A → IntoExist (▷^n P) (λ a, ▷^n (Φ a))%I.
 Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
 
+(* IntoForall *)
+Global Instance into_forall_forall {A} (Φ : A → uPred M) : IntoForall (∀ a, Φ a) Φ.
+Proof. done. Qed.
+Global Instance into_forall_always {A} P (Φ : A → uPred M) :
+  IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
+Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
+
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (â–· P) P.
 Proof. apply later_intro. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 6efe52766..40d4fad49 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -88,6 +88,11 @@ Class IntoExist {M A} (P : uPred M) (Φ : A → uPred M) :=
 Arguments into_exist {_ _} _ _ {_}.
 Hint Mode IntoExist + - ! - : typeclass_instances.
 
+Class IntoForall {M A} (P : uPred M) (Φ : A → uPred M) :=
+  into_forall : P ⊢ ∀ x, Φ x.
+Arguments into_forall {_ _} _ _ {_}.
+Hint Mode IntoForall + - ! - : typeclass_instances.
+
 Class FromModal {M} (P Q : uPred M) := from_modal : Q ⊢ P.
 Arguments from_modal {_} _ _ {_}.
 Hint Mode FromModal + ! - : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 20b21e3a5..2cbea3f72 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -791,27 +791,13 @@ Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) :
   (∀ a, Δ ⊢ ⌜φ a⌝) → Δ ⊢ ⌜∀ a, φ a⌝.
 Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
 
-Class ForallSpecialize {As} (xs : hlist As)
-  (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P ⊢ Φ xs.
-Arguments forall_specialize {_} _ _ _ {_}.
-
-Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
-Proof. done. Qed.
-Global Instance forall_specialize_cons A As x xs Φ (Ψ : A → himpl As (uPred M)) :
-  (∀ x, ForallSpecialize xs (Φ x) (Ψ x)) →
-  ForallSpecialize (hcons x xs) (∀ x : A, Φ x) Ψ.
-Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
-Global Instance forall_specialize_always As xs P (Ψ : himpl As (uPred M)) :
-  ForallSpecialize xs P Ψ → ForallSpecialize xs (□ P) Ψ | 101.
-Proof. rewrite /ForallSpecialize=> ->. by rewrite always_elim. Qed.
-
-Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
-  envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ →
-  envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ' →
+Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q x :
+  envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
+  envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (forall_specialize _ P) wand_elim_r.
+  by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
@@ -849,5 +835,3 @@ Proof.
   rewrite right_id HΔ always_if_elim. by apply elim_modal.
 Qed.
 End tactics.
-
-Hint Mode ForallSpecialize + - - ! - : typeclass_instances.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index cd03600c6..715f44171 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -268,15 +268,17 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
 Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
 
 Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
-  match xs with
-  | hnil => idtac
-  | _ =>
-    eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
-      [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
-      |let P := match goal with |- ForallSpecialize _ ?P _ => P end in
-       apply _ || fail 1 "iSpecialize:" P "not a forall of the right arity or type"
-      |cbn [himpl hcurry]; reflexivity|]
-  end.
+  let rec go xs :=
+    match xs with
+    | hnil => idtac
+    | hcons ?x ?xs =>
+       eapply tac_forall_specialize with _ H _ _ _ x; (* (i:=H) (a:=x) *)
+         [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
+         |let P := match goal with |- IntoForall ?P _ => P end in
+          apply _ || fail 1 "iSpecialize:" P "not a forall or not a forall of the right type"
+         |env_cbv; reflexivity|go xs]
+    end in
+  go xs.
 
 Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
   let solve_to_wand H1 :=
-- 
GitLab