From f0e57c42485a94945cd35d24b8aa34056334ebbd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Sep 2017 13:06:14 +0200
Subject: [PATCH] Use the sink modality in the proof mode.
Whenever we iSpecialize something whose conclusion is persistent, we now have
to prove all the premises under the sink modality. This is strictly more powerful,
as we now have to use just some of the hypotheses to prove the premises, instead of
all.
---
theories/proofmode/class_instances.v | 8 ++++++++
theories/proofmode/classes.v | 6 ++++++
theories/proofmode/coq_tactics.v | 22 +++++++++++-----------
theories/proofmode/tactics.v | 5 +++--
4 files changed, 28 insertions(+), 13 deletions(-)
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index efc72d909..4449a272b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -27,6 +27,14 @@ Proof. intros. by rewrite /FromBare bare_elim. Qed.
Global Instance from_bare_default P : FromBare (â– P) P | 100.
Proof. by rewrite /FromBare. Qed.
+(* IntoSink *)
+Global Instance into_sink_True : @IntoSink PROP True emp | 0.
+Proof. by rewrite /IntoSink -sink_True_emp sink_pure. Qed.
+Global Instance into_sink_absorbing P : Absorbing P → IntoSink P P | 1.
+Proof. intros. by rewrite /IntoSink absorbing_sink. Qed.
+Global Instance into_sink_default P : IntoSink (â–² P) P | 100.
+Proof. by rewrite /IntoSink. Qed.
+
(* FromAssumption *)
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
Proof. by rewrite /FromAssumption /= bare_persistently_if_elim. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 7263098d0..ca815691f 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -68,6 +68,12 @@ Arguments from_bare {_} _%I _%type_scope {_}.
Hint Mode FromBare + ! - : typeclass_instances.
Hint Mode FromBare + - ! : typeclass_instances.
+Class IntoSink {PROP : bi} (P Q : PROP) := into_sink : P ⊢ ▲ Q.
+Arguments IntoSink {_} _%I _%I.
+Arguments into_sink {_} _%I _%I {_}.
+Hint Mode IntoSink + ! - : typeclass_instances.
+Hint Mode IntoSink + - ! : typeclass_instances.
+
Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
into_internal_eq : P ⊢ x ≡ y.
Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 3697b33f6..a555a196b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -684,18 +684,20 @@ Proof.
by rewrite emp_wand wand_elim_r.
Qed.
-Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
+Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P1' P2 R Q :
envs_lookup_delete j Δ = Some (q, R, Δ') →
IntoWand q true R P1 P2 →
Persistent P1 →
+ IntoSink P1' P1 →
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
- (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
+ (Δ' ⊢ P1') → (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
- intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+ intros [? ->]%envs_lookup_delete_Some ???? HP1 <-.
rewrite envs_lookup_sound //.
rewrite -(idemp bi_and (envs_delete _ _ _)).
rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
- rewrite {1}HP1 (persistent_persistently_2 P1) persistently_and_bare_sep_l assoc.
+ rewrite {1}HP1 (into_sink P1') (persistent_persistently_2 P1) sink_persistently.
+ rewrite persistently_and_bare_sep_l assoc.
rewrite -bare_persistently_if_idemp -bare_persistently_idemp.
rewrite (bare_persistently_bare_persistently_if q) bare_persistently_if_sep_2.
by rewrite into_wand wand_elim_l wand_elim_r.
@@ -703,20 +705,18 @@ Qed.
Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
envs_lookup j Δ = Some (q,P) →
- (Δ ⊢ R) →
+ (Δ ⊢ ▲ R) →
IntoPersistent false R R' →
- (if q then TCTrue else TCAnd (PositiveBI PROP) (Affine R)) →
+ (if q then TCTrue else AffineBI PROP) →
envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
(Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
rewrite envs_replace_singleton_sound //; destruct q; simpl.
- - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R).
+ - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R) sink_persistently.
+ by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
+ - rewrite (absorbing_sink R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
- - destruct Hpos.
- rewrite -(affine_bare R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
- rewrite bare_and_lr bare_sep sep_elim_r bare_elim.
- by rewrite persistently_and_bare_sep_l wand_elim_r.
Qed.
Lemma tac_revert Δ Δ' i p P Q :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4329266a7..c6c174b99 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -459,12 +459,13 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
|done_if d (*goal*)
|go H1 pats]
| SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
- eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
+ eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _ _;
[env_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|apply _ ||
let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
+ |apply _
|env_reflexivity
|iFrame Hs_frame; done_if d (*goal*)
|go H1 pats]
@@ -535,7 +536,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
lazymatch eval compute in
(p && bool_decide (pat ≠[]) && negb (existsb spec_pat_modal pat)) with
| true =>
- (* FIXME: do something reasonable when the BI is not positive *)
+ (* FIXME: do something reasonable when the BI is not affine *)
eapply tac_specialize_persistent_helper with _ H _ _ _ _;
[env_reflexivity || fail "iSpecialize:" H "not found"
|iSpecializePat H pat; last (iExact H)
--
GitLab