Commit f987ca78 authored by Robbert Krebbers's avatar Robbert Krebbers

Let iSpecialize with a hypotheses behave like iAssumption.

For example, when having `H : ▷ P → Q` and `HP : P`, we can now
do `iSpecialize ("H" with "HP")`. This is achieved by putting a
`FromAssumption` premise in the base instance for `IntoWand`.
parent 56f0afb2
......@@ -248,8 +248,9 @@ Global Instance from_later_exist {A} n (Φ Ψ : A → uPred M) :
Proof. intros ?. rewrite /FromLaterN laterN_exist=> ?. by apply exist_mono. Qed.
(* IntoWand *)
Global Instance wand_weaken_exact P Q : WandWeaken P Q P Q.
Proof. done. Qed.
Global Instance wand_weaken_assumption P1 P2 Q :
FromAssumption false P2 P1 WandWeaken P1 Q P2 Q | 0.
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
Global Instance wand_weaken_later P Q P' Q' :
WandWeaken P Q P' Q' WandWeaken' P Q ( P') ( Q').
Proof.
......
......@@ -78,8 +78,6 @@ Class WandWeaken' {M} (P Q P' Q' : uPred M) :=
wand_weaken' :> WandWeaken P Q P' Q'.
Hint Mode WandWeaken' + - - ! - : typeclass_instances.
Hint Mode WandWeaken' + - - - ! : typeclass_instances.
Instance wand_weaken_exact {M} (P Q : uPred M) : WandWeaken P Q P Q | 1000.
Proof. done. Qed.
Class IntoWand {M} (R P Q : uPred M) := into_wand : R P - Q.
Arguments into_wand {_} _ _ _ {_}.
......
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