Commit cec228f6 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/later_proper' into 'master'

add later_ne; make later_proper match the other _proper lemmas

See merge request FP/iris-coq!81
parents 342b79a4 6a4c6279
...@@ -672,9 +672,9 @@ Proof. ...@@ -672,9 +672,9 @@ Proof.
Qed. Qed.
(* Later derived *) (* Later derived *)
Lemma later_proper P Q : (P Q) P Q. Lemma later_proper' P Q : (P Q) P Q.
Proof. by intros ->. Qed. Proof. by intros ->. Qed.
Hint Resolve later_mono later_proper. Hint Resolve later_mono later_proper'.
Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M). Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed. Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' : Global Instance later_flip_mono' :
......
...@@ -307,7 +307,8 @@ Proof. ...@@ -307,7 +307,8 @@ Proof.
unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega. unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
apply HPQ; eauto using cmra_validN_S. apply HPQ; eauto using cmra_validN_S.
Qed. Qed.
Global Instance later_proper' : Definition later_ne : NonExpansive (@uPred_later M) := _.
Global Instance later_proper :
Proper (() ==> ()) (@uPred_later M) := ne_proper _. Proper (() ==> ()) (@uPred_later M) := ne_proper _.
Global Instance plainly_ne : NonExpansive (@uPred_plainly M). Global Instance plainly_ne : NonExpansive (@uPred_plainly M).
Proof. Proof.
......
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