Commit 9b14f90a authored by Ralf Jung's avatar Ralf Jung

fix into_wand for monpred proofmode

parent daeeaf05
......@@ -91,10 +91,18 @@ Section tests.
P - ⎡◇ 𝓟⎤ - ⎡◇ 𝓠⎤ - (𝓟 𝓠) .
Proof. iIntros "#H1 H2 H3". iModIntro _ %I. by iSplitL "H2". Qed.
(* This is a hack to avoid avoid coq bug #5735: sections variables
ignore hint modes. So we assume the instances in a way that
cannot be used by type class resolution, and then declare the
instance. as such. *)
Lemma test_into_wand_embed 𝓟 𝓠 :
(𝓟 - 𝓠)
⎡𝓟⎤ @{monPredSI} ⎡𝓠⎤.
Proof.
iIntros (HPQ) "HP".
iMod (HPQ with "[-]") as "$"; last by auto.
iAssumption.
Qed.
(* This is a hack to avoid avoid coq bug #5735: sections variables ignore hint
modes. So we assume the instances in a way that cannot be used by type
class resolution, and then separately declare the instance as such. *)
Context (FU0 : BiFUpd PROP * unit).
Instance FU : BiFUpd PROP := fst FU0.
......
......@@ -396,8 +396,9 @@ Global Instance into_wand_persistently_false q R P Q :
Absorbing R IntoWand false q R P Q IntoWand false q (<pers> R) P Q.
Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q (PP QQ RR : PROP) (P : PROP') :
IntoWand p q RR PP QQ
IntoEmbed P PP
IntoWand p q RR PP QQ IntoWand p q RR P QQ.
IntoWand p q RR P QQ.
Proof.
rewrite /IntoEmbed /IntoWand !embed_intuitionistically_if_2=> -> ->.
apply bi.wand_intro_l.
......
......@@ -482,12 +482,14 @@ Proof. apply _. Qed.
(** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
embeddings using [iModIntro].
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤] *)
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤].
Also used backwards, i.e. Input [Q] and output [P]. *)
Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
into_embed : P Q.
Arguments IntoEmbed {_ _ _} _%I _%I.
Arguments into_embed {_ _ _} _%I _%I {_}.
Hint Mode IntoEmbed + + + ! - : typeclass_instances.
Hint Mode IntoEmbed + + + - ! : typeclass_instances.
(* We use two type classes for [AsEmpValid], in order to avoid loops in
typeclass search. Indeed, the [as_emp_valid_embed] instance would try
......
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