Commit f0e57c42 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan

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.
parent b0119c33
......@@ -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.
......
......@@ -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.
......
......@@ -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 :
......
......@@ -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)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment