Commit 8938309e authored by Ralf Jung's avatar Ralf Jung

use the 'separate Db' approach for all proofmode classes except for framing

parent bb060202
......@@ -257,10 +257,10 @@ Arguments authR : clear implicits.
Arguments authUR : clear implicits.
(* Proof mode class instances *)
Instance from_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
Lemma from_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
FromOp a b1 b2 FromOp ( a) ( b1) ( b2).
Proof. done. Qed.
Instance into_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
Lemma into_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
IntoOp a b1 b2 IntoOp ( a) ( b1) ( b2).
Proof. done. Qed.
......@@ -341,3 +341,5 @@ Instance authURF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
Qed.
Hint Resolve from_op_auth_frag into_op_auth_frag : proofmode.
......@@ -73,13 +73,13 @@ Section auth.
Lemma auth_own_op γ a b : auth_own γ (a b) ⊣⊢ auth_own γ a auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Global Instance from_sep_auth_own γ a b1 b2 :
Lemma from_sep_auth_own γ a b1 b2 :
FromOp a b1 b2
FromSep (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
FromSep (auth_own γ a) (auth_own γ b1) (auth_own γ b2).
Proof. rewrite /FromOp /FromSep=> <-. by rewrite auth_own_op. Qed.
Global Instance into_and_auth_own p γ a b1 b2 :
Lemma into_and_auth_own p γ a b1 b2 :
IntoOp a b1 b2
IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2).
Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) auth_own_op. Qed.
Lemma auth_own_mono γ a b : a b auth_own γ b auth_own γ a.
......@@ -148,3 +148,4 @@ Section auth.
End auth.
Arguments auth_open {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
Hint Resolve from_sep_auth_own into_and_auth_own | 90 : proofmode.
......@@ -283,3 +283,4 @@ Qed.
End box.
Typeclasses Opaque slice box.
Hint Opaque slice box : proofmode.
......@@ -114,21 +114,23 @@ Module inv. Section inv.
Lemma fupd_frame_r E P Q : fupd E P Q fupd E (P Q).
Proof. by rewrite comm fupd_frame_l comm. Qed.
Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
Lemma elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
Proof. by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed.
Global Instance elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Lemma elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Proof.
by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
Qed.
Global Instance exists_split_fupd0 {A} E P (Φ : A iProp) :
Lemma exists_split_fupd0 {A} E P (Φ : A iProp) :
FromExist P Φ FromExist (fupd E P) (λ a, fupd E (Φ a)).
Proof.
rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
apply fupd_mono. by rewrite -HP -(uPred.exist_intro a).
Qed.
Hint Resolve elim_fupd_fupd elim_fupd0_fupd1 exists_split_fupd0 : proofmode.
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition saved (γ : gname) (P : iProp) : iProp :=
i, inv i (start γ (finished γ P)).
......
......@@ -147,22 +147,22 @@ Section proofmode_classes.
Context `{invG Σ}.
Implicit Types P Q : iProp Σ.
Global Instance from_pure_fupd E P φ : FromPure P φ FromPure (|={E}=> P) φ.
Lemma from_pure_fupd E P φ : FromPure P φ FromPure (|={E}=> P) φ.
Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
Lemma from_assumption_fupd E p P Q :
FromAssumption p P (|==> Q) FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
Global Instance into_wand_fupd E1 E2 R P Q :
IntoWand R P Q IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Lemma into_wand_fupd E1 E2 R P Q :
IntoWand R P Q IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite fupd_wand_r. Qed.
Global Instance from_sep_fupd E P Q1 Q2 :
Lemma from_sep_fupd E P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep=><-. apply fupd_sep. Qed.
Global Instance or_split_fupd E1 E2 P Q1 Q2 :
Lemma or_split_fupd E1 E2 P Q1 Q2 :
FromOr P Q1 Q2 FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply fupd_mono; auto with I. Qed.
......@@ -176,27 +176,30 @@ Section proofmode_classes.
Frame R P Q Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
Lemma is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
Global Instance into_modal_fupd E P : IntoModal P (|={E}=> P).
Lemma into_modal_fupd E P : IntoModal P (|={E}=> P).
Proof. rewrite /IntoModal. apply fupd_intro. Qed.
(* Put a lower priority compared to [elim_modal_fupd_fupd], so that
it is not taken when the first parameter is not specified (in
spec. patterns). *)
Global Instance elim_modal_bupd_fupd E1 E2 P Q :
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Lemma elim_modal_bupd_fupd E1 E2 P Q :
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed.
Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
Lemma elim_modal_fupd_fupd E1 E2 E3 P Q :
ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes.
Hint Resolve from_assumption_fupd : proofmode.
Hint Resolve from_exist_fupd : proofmode.
Hint Resolve from_pure_fupd from_assumption_fupd from_sep_fupd
or_split_fupd from_exist_fupd is_except_0_fupd into_modal_fupd
elim_modal_fupd_fupd : proofmode.
(* Put a lower priority compared to [elim_modal_fupd_fupd], so that
it is not taken when the first parameter is not specified (in
spec. patterns). *)
Hint Resolve elim_modal_bupd_fupd | 10 : proofmode.
Hint Resolve into_wand_fupd | 100 : proofmode.
Hint Extern 2 (coq_tactics.of_envs _ _) =>
match goal with |- _ |={_}=> _ => iModIntro end.
......
......@@ -110,32 +110,38 @@ Section fractional.
Qed.
(** Proof mode instances *)
Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
Lemma from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
FromSep P P1 P2.
Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
Lemma from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
AsFractional P1 Φ q1 AsFractional P2 Φ q2 AsFractional P Φ (q1 + q2)
FromSep P P1 P2 | 10.
FromSep P P1 P2.
Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed.
Global Instance from_sep_fractional_half_fwd P Q Φ q :
Lemma from_sep_fractional_half_fwd P Q Φ q :
AsFractional P Φ q AsFractional Q Φ (q/2)
FromSep P Q Q | 10.
FromSep P Q Q.
Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
Global Instance from_sep_fractional_half_bwd P Q Φ q :
Lemma from_sep_fractional_half_bwd P Q Φ q :
AsFractional P Φ (q/2) AsFractional Q Φ q
FromSep Q P P.
Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
Global Instance into_and_fractional P P1 P2 Φ q1 q2 :
Lemma into_and_fractional b P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
IntoAnd false P P1 P2.
Proof. by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _]. Qed.
Global Instance into_and_fractional_half P Q Φ q :
IntoAnd b P P1 P2.
Proof.
intros H1 H2 H3. apply mk_into_and_sep. revert H1 H2 H3.
by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _].
Qed.
Lemma into_and_fractional_half b P Q Φ q :
AsFractional P Φ q AsFractional Q Φ (q/2)
IntoAnd false P Q Q | 100.
Proof. by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed.
IntoAnd b P Q Q.
Proof.
intros H1 H2. apply mk_into_and_sep. revert H1 H2.
by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _].
Qed.
(* The instance [frame_fractional] can be tried at all the nodes of
the proof search. The proof search then fails almost always on
......@@ -166,3 +172,9 @@ Section fractional.
- move=>-[-> _]->. by rewrite -fractional Qp_div_2.
Qed.
End fractional.
Hint Resolve from_sep_fractional_fwd from_sep_fractional_half_bwd into_and_fractional : proofmode.
Hint Resolve from_sep_fractional_bwd from_sep_fractional_half_fwd | 10 : proofmode.
Hint Resolve into_and_fractional_half | 100 : proofmode.
Hint Extern 0 (AsFractional _ _ _) => solve [typeclasses eauto] : proofmode.
......@@ -153,10 +153,12 @@ Section proofmode_classes.
Context `{inG Σ A}.
Implicit Types a b : A.
Global Instance into_and_own p γ a b1 b2 :
Lemma into_and_own p γ a b1 b2 :
IntoOp a b1 b2 IntoAnd p (own γ a) (own γ b1) (own γ b2).
Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
Global Instance from_sep_own γ a b1 b2 :
Lemma from_sep_own γ a b1 b2 :
FromOp a b1 b2 FromSep (own γ a) (own γ b1) (own γ b2).
Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
End proofmode_classes.
Hint Resolve into_and_own from_sep_own : proofmode.
......@@ -136,7 +136,7 @@ Proof.
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ i (invariant_unfold P)); last done.
by rewrite /= lookup_fmap HIi. }
iModIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
iModIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
iExists (<[i:=P]>I); iSplitL "Hw".
{ by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
iApply (big_sepM_insert _ I); first done.
......
......@@ -232,7 +232,7 @@ Ltac solve_atomic :=
end.
Hint Extern 10 (language.atomic _) => solve_atomic.
(* For the side-condition of elim_upd_fupd_wp_atomic *)
Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
Hint Extern 10 (language.atomic _) => solve_atomic : proofmode.
(** Substitution *)
Ltac simpl_subst :=
......
......@@ -280,24 +280,26 @@ Section proofmode_classes.
( v, Frame R (Φ v) (Ψ v)) Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
Lemma is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
Global Instance elim_modal_bupd_wp E e P Φ :
Lemma elim_modal_bupd_wp E e P Φ :
ElimModal (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
Global Instance elim_modal_fupd_wp E e P Φ :
Lemma elim_modal_fupd_wp E e P Φ :
ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
(* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
Lemma elim_modal_fupd_wp_atomic E1 E2 e P Φ :
atomic e
ElimModal (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes.
Hint Extern 0 (atomic _) => assumption : typeclass_instances.
Hint Resolve is_except_0_wp elim_modal_bupd_wp elim_modal_fupd_wp : proofmode.
Hint Resolve elim_modal_fupd_wp_atomic | 100 : proofmode.
Hint Extern 0 (atomic _) => assumption : proofmode.
This diff is collapsed.
......@@ -83,8 +83,21 @@ End classes.
(* Establish links between Hint Dbs. *)
Hint Extern 0 (FromAssumption _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoPure _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromPure _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoPersistentP _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoLaterN _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromLaterN _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoWand _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromAnd _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromSep _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoAnd _ _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromOp _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoOp _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromOr _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoOr _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromExist _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoExist _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
(* We still ned typeclass_instances for some side-conditions, but we can't generally use it or things will loop. *)
Hint Extern 0 (Inhabited _) => solve [typeclasses eauto] : proofmode.
Hint Extern 0 (IntoModal _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (ElimModal _ _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IsExcept0 _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
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