Commit 8c4d7b2f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add missing Propers for uPred_valid.

parent d9e87db3
...@@ -319,12 +319,13 @@ Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed. ...@@ -319,12 +319,13 @@ Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed.
Global Instance always_proper : Global Instance always_proper :
Proper (() ==> ()) (@uPred_always M) := ne_proper _. Proper (() ==> ()) (@uPred_always M) := ne_proper _.
Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M). Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
Proof. Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
by intros a1 a2 Ha n' x; split; intros [a' ?]; exists a'; simpl; first Global Instance ownM_proper: Proper (() ==> ()) (@uPred_ownM M) := ne_proper _.
[rewrite -(dist_le _ _ _ _ Ha); last lia Global Instance valid_ne {A : cmraT} n :
|rewrite (dist_le _ _ _ _ Ha); last lia]. Proper (dist n ==> dist n) (@uPred_valid M A).
Qed. Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
Global Instance ownM_proper : Proper (() ==> ()) (@uPred_ownM M) := ne_proper _. Global Instance valid_proper {A : cmraT} :
Proper (() ==> ()) (@uPred_valid M A) := ne_proper _.
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M). Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed. Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper : Global Instance iff_proper :
......
Supports Markdown
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