From 80fcebca3b9afd4722be10bcf1cb95564b65d223 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Feb 2018 21:57:55 +0100
Subject: [PATCH] iIntoValid : for specialization, first try with [hnf] and
then with [cbv zeta].
---
theories/bi/derived_laws.v | 2 +-
theories/proofmode/tactics.v | 33 +++++++++++++++++++++++----------
2 files changed, 24 insertions(+), 11 deletions(-)
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 41c7e56d3..9f669b010 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -35,7 +35,7 @@ Lemma entails_equiv_l P Q R : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
Proof. by intros ->. Qed.
Lemma entails_equiv_r P Q R : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
Proof. by intros ? <-. Qed.
- Global Instance bi_valid_proper : Proper ((⊣⊢) ==> iff) (@bi_valid PROP).
+Global Instance bi_valid_proper : Proper ((⊣⊢) ==> iff) (@bi_valid PROP).
Proof. solve_proper. Qed.
Global Instance bi_valid_mono : Proper ((⊢) ==> impl) (@bi_valid PROP).
Proof. solve_proper. Qed.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index bb779984e..18c780e64 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -620,8 +620,28 @@ The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [P] for non-dependent arguments [x_i : P]. *)
Tactic Notation "iIntoValid" open_constr(t) :=
let rec go t :=
+ (* We try two reduction tactics for the type of t before trying to
+ specialize it. We first try the head normal form in order to
+ unfold all the definition that could hide an entailment. Then,
+ we try the much weaker [eval cbv zeta], because entailment is
+ not necessarilly opaque, and could be unfolded by [hnf].
+
+ However, for calling type class search, we only use [cbv zeta]
+ in order to make sure we do not unfold [bi_valid]. *)
let tT := type of t in
- let tT := eval cbv zeta in tT in (* In the case tT contains let-bindings. *)
+ first
+ [ let tT' := eval hnf in tT in go_specilize t tT'
+ | let tT' := eval cbv zeta in tT in go_specilize t tT'
+ | let tT' := eval cbv zeta in tT in
+ eapply (as_valid_1 tT);
+ (* Doing [apply _] here fails because that will try to solve all evars
+ whose type is a typeclass, in dependency order (according to Matthieu).
+ If one fails, it aborts. However, we rely on progress on the main goal
+ ([AsValid ...]) to unify some of these evars and hence enable progress
+ elsewhere. With [typeclasses eauto], that seems to work better. *)
+ [solve [ typeclasses eauto with typeclass_instances ] ||
+ fail "iPoseProof: not a BI assertion"|exact t]]
+ with go_specilize t tT :=
lazymatch tT with (* We do not use hnf of tT, because, if
entailment is not opaque, then it would
unfold it. *)
@@ -631,15 +651,8 @@ Tactic Notation "iIntoValid" open_constr(t) :=
(* This is a workarround for Coq bug #6583. *)
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; go (t e')
- | _ =>
- eapply (as_valid_1 tT);
- (* Doing [apply _] here fails because that will try to solve all evars
- whose type is a typeclass, in dependency order (according to Matthieu).
- If one fails, it aborts. However, we rely on progress on the main goal
- ([AsValid ...]) to unify some of these evars and hence enable progress
- elsewhere. With [typeclasses eauto], that seems to work better. *)
- [solve [ typeclasses eauto with typeclass_instances ] || fail "iPoseProof: not a BI assertion"|exact t]
- end in
+ end
+ in
go t.
(* The tactic [tac] is called with a temporary fresh name [H]. The argument
--
GitLab