Commit 2693eb84 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Move the AsValid typeclass in classes.v and class_instances.v

parent d7db5250
......@@ -1023,6 +1023,17 @@ Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q :
Plain P ElimModal (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
Proof. by rewrite /AsValid. Qed.
Global Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid0 (P Q) (P - Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Global Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid0 (P Q) (P - Q).
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
Global Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
AsValid0 φ P AsValid φ P.
Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.
End bi_instances.
Hint Mode ElimModalAbsorbingly + ! - - : typeclass_instances.
......
......@@ -280,6 +280,19 @@ Arguments FromLaterN {_} _%nat_scope _%I _%I.
Arguments from_laterN {_} _%nat_scope _%I _%I {_}.
Hint Mode FromLaterN + - ! - : typeclass_instances.
Class AsValid {PROP : bi} (φ : Prop) (P : PROP) := as_valid : φ P.
Arguments AsValid {_} _%type _%I.
Class AsValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_valid_here : AsValid φ P.
Arguments AsValid0 {_} _%type _%I.
Existing Instance as_valid_here | 0.
Lemma as_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : φ P.
Proof. by apply as_valid. Qed.
Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P φ.
Proof. by apply as_valid. Qed.
(* We make sure that tactics that perform actions on *specific* hypotheses or
parts of the goal look through the [tc_opaque] connective, which is used to make
definitions opaque for type class search. For example, when using `iDestruct`,
......
......@@ -54,32 +54,6 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
| |- context[ environments.Esnoc _ ?x ?P ] => tac x P
end.
Class AsValid {PROP : bi} (φ : Prop) (P : PROP) := as_valid : φ P.
Arguments AsValid {_} _%type _%I.
Class AsValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_valid_here : AsValid φ P.
Arguments AsValid0 {_} _%type _%I.
Existing Instance as_valid_here | 0.
Lemma as_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : φ P.
Proof. by apply as_valid. Qed.
Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P φ.
Proof. by apply as_valid. Qed.
Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
Proof. by rewrite /AsValid. Qed.
Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid0 (P Q) (P - Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid0 (P Q) (P - Q).
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
AsValid0 φ P AsValid φ P.
Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.
(** * Start a proof *)
Tactic Notation "iStartProof" :=
lazymatch goal with
......
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