Commit 6456f1f9 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents 652aebfc 2cbcc992
Pipeline #3960 passed with stage
in 2 minutes and 38 seconds
...@@ -50,6 +50,8 @@ Qed. ...@@ -50,6 +50,8 @@ Qed.
Canonical Structure dec_agreeR : cmraT := Canonical Structure dec_agreeR : cmraT :=
discreteR (dec_agree A) dec_agree_ra_mixin. discreteR (dec_agree A) dec_agree_ra_mixin.
Global Instance dec_agree_cmra_discrete : CMRADiscrete dec_agreeR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance dec_agree_total : CMRATotal dec_agreeR. Global Instance dec_agree_total : CMRATotal dec_agreeR.
Proof. intros x. by exists x. Qed. Proof. intros x. by exists x. Qed.
......
...@@ -10,16 +10,18 @@ Context {M : ucmraT}. ...@@ -10,16 +10,18 @@ Context {M : ucmraT}.
Implicit Types P Q R : uPred M. Implicit Types P Q R : uPred M.
(* FromAssumption *) (* FromAssumption *)
Global Instance from_assumption_False p P : FromAssumption p False P. Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
Global Instance from_assumption_exact p P : FromAssumption p P P.
Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed. Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
Global Instance from_assumption_always_l p P Q : Global Instance from_assumption_False p P : FromAssumption p False P | 1.
FromAssumption p P Q FromAssumption p ( P) Q. Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
Global Instance from_assumption_always_r P Q : Global Instance from_assumption_always_r P Q :
FromAssumption true P Q FromAssumption true P ( Q). FromAssumption true P Q FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed. 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 : Global Instance from_assumption_later p P Q :
FromAssumption p P Q FromAssumption p P ( Q)%I. FromAssumption p P Q FromAssumption p P ( Q)%I.
Proof. rewrite /FromAssumption=>->. apply later_intro. Qed. Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
......
...@@ -5,7 +5,9 @@ Import uPred. ...@@ -5,7 +5,9 @@ Import uPred.
Class FromAssumption {M} (p : bool) (P Q : uPred M) := Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
from_assumption : ?p P Q. from_assumption : ?p P Q.
Arguments from_assumption {_} _ _ _ {_}. 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 ⌜φ⌝. Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P ⌜φ⌝.
Arguments into_pure {_} _ _ {_}. Arguments into_pure {_} _ _ {_}.
......
...@@ -441,7 +441,7 @@ Tactic Notation "iApply" open_constr(lem) := ...@@ -441,7 +441,7 @@ Tactic Notation "iApply" open_constr(lem) :=
|lazy beta (* reduce betas created by instantiation *)] |lazy beta (* reduce betas created by instantiation *)]
|iSpecializePat H "[]"; last go H] in |iSpecializePat H "[]"; last go H] in
iPoseProofCore lem as false true (fun H => iPoseProofCore lem as false true (fun H =>
first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]). first [iExact H|go H|iTypeOf H (fun _ Q => fail "iApply: cannot apply" Q)]).
(** * Revert *) (** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) := Local Tactic Notation "iForallRevert" ident(x) :=
......
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