Commit 2cbcc992 authored by Robbert Krebbers's avatar Robbert Krebbers

Change Hint Mode for FromAssumption.

There is no need to restrict the type class using Hint Mode, we have
a default instance that will always be used first. In case of evars,
the default instance should apply.

The reason for this change is that `iAssumption` should be able to
prove `H : ?e |- P` and `H : P |- ?e`. The former Hint Mode prevented
it from doing that.
parent b81b27d3
......@@ -10,16 +10,18 @@ Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
(* FromAssumption *)
Global Instance from_assumption_False p P : FromAssumption p False P.
Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
Global Instance from_assumption_exact p P : FromAssumption p P P.
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
Global Instance from_assumption_always_l p P Q :
FromAssumption p P Q FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
Global Instance from_assumption_False p P : FromAssumption p False P | 1.
Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
Global Instance from_assumption_always_r P Q :
FromAssumption true P Q FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
Global Instance from_assumption_always_l p P Q :
FromAssumption p P Q FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
Global Instance from_assumption_later p P Q :
FromAssumption p P Q FromAssumption p P ( Q)%I.
Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
......
......@@ -5,7 +5,9 @@ Import uPred.
Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
from_assumption : ?p P Q.
Arguments from_assumption {_} _ _ _ {_}.
Hint Mode FromAssumption + + ! - : typeclass_instances.
(* No need to restrict Hint Mode, we have a default instance that will always
be used in case of evars *)
Hint Mode FromAssumption + + - - : typeclass_instances.
Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P ⌜φ⌝.
Arguments into_pure {_} _ _ {_}.
......
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