Commit 7f04cf65 authored by Robbert Krebbers's avatar Robbert Krebbers

Proper instances for types classes over ofe and cmra elements, and upreds.

parent 272b90d7
......@@ -139,23 +139,27 @@ Infix "⋅?" := opM (at level 50, left associativity) : C_scope.
Class Persistent {A : cmraT} (x : A) := persistent : pcore x Some x.
Arguments persistent {_} _ {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x y) False.
Arguments exclusive0_l {_} _ {_} _ _.
Hint Mode Exclusive + ! : typeclass_instances.
Instance: Params (@Exclusive) 1.
(** * Cancelable elements. *)
Class Cancelable {A : cmraT} (x : A) :=
cancelableN n y z : {n}(x y) x y {n} x z y {n} z.
Arguments cancelableN {_} _ {_} _ _ _ _.
Hint Mode Cancelable + ! : typeclass_instances.
Instance: Params (@Cancelable) 1.
(** * Identity-free elements. *)
Class IdFree {A : cmraT} (x : A) :=
id_free0_r y : {0}x x y {0} x False.
Arguments id_free0_r {_} _ {_} _ _.
Hint Mode IdFree + ! : typeclass_instances.
Instance: Params (@IdFree) 1.
(** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total
......@@ -313,6 +317,15 @@ Proof. destruct 2; by ofe_subst. Qed.
Global Instance cmra_opM_proper : Proper (() ==> () ==> ()) (@opM A).
Proof. destruct 2; by setoid_subst. Qed.
Global Instance Persistent_proper : Proper (() ==> iff) (@Persistent A).
Proof. solve_proper. Qed.
Global Instance Exclusive_proper : Proper (() ==> iff) (@Exclusive A).
Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
Global Instance Cancelable_proper : Proper (() ==> iff) (@Cancelable A).
Proof. intros x y Hxy. rewrite /Cancelable. by setoid_rewrite Hxy. Qed.
Global Instance IdFree_proper : Proper (() ==> iff) (@IdFree A).
Proof. intros x y Hxy. rewrite /IdFree. by setoid_rewrite Hxy. Qed.
(** ** Op *)
Lemma cmra_opM_assoc x y mz : (x y) ? mz x (y ? mz).
Proof. destruct mz; by rewrite /= -?assoc. Qed.
......
......@@ -102,6 +102,7 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
Class Timeless {A : ofeT} (x : A) := timeless y : x {0} y x y.
Arguments timeless {_} _ {_} _ _.
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.
Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.
......@@ -152,15 +153,17 @@ Section ofe.
Qed.
Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
Global Instance Timeless_proper : Proper (() ==> iff) (@Timeless A).
Proof. intros x y Hxy. rewrite /Timeless. by setoid_rewrite Hxy. Qed.
Lemma dist_le n n' x y : x {n} y n' n x {n'} y.
Proof. induction 2; eauto using dist_S. Qed.
Lemma dist_le' n n' x y : n' n x {n} y x {n'} y.
Proof. intros; eauto using dist_le. Qed.
Instance ne_proper {B : ofeT} (f : A B)
`{!NonExpansive f} : Proper (() ==> ()) f | 100.
Instance ne_proper {B : ofeT} (f : A B) `{!NonExpansive f} :
Proper (() ==> ()) f | 100.
Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
Instance ne_proper_2 {B C : ofeT} (f : A B C)
`{!NonExpansive2 f} :
Instance ne_proper_2 {B C : ofeT} (f : A B C) `{!NonExpansive2 f} :
Proper (() ==> () ==> ()) f | 100.
Proof.
unfold Proper, respectful; setoid_rewrite equiv_dist.
......
......@@ -32,11 +32,12 @@ Typeclasses Opaque uPred_except_0.
Class TimelessP {M} (P : uPred M) := timelessP : P P.
Arguments timelessP {_} _ {_}.
Hint Mode TimelessP + ! : typeclass_instances.
Instance: Params (@TimelessP) 1.
Class PersistentP {M} (P : uPred M) := persistentP : P P.
Hint Mode PersistentP - ! : typeclass_instances.
Arguments persistentP {_} _ {_}.
Hint Mode PersistentP + ! : typeclass_instances.
Instance: Params (@PersistentP) 1.
Module uPred.
Section derived.
......@@ -746,6 +747,8 @@ Proof.
Qed.
(* Timeless instances *)
Global Instance TimelessP_proper : Proper (() ==> iff) (@TimelessP M).
Proof. solve_proper. Qed.
Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
Proof.
rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
......@@ -811,6 +814,9 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
Proof. destruct mx; apply _. Qed.
(* Derived lemmas for persistence *)
Global Instance PersistentP_proper : Proper (() ==> iff) (@PersistentP M).
Proof. solve_proper. Qed.
Lemma always_always P `{!PersistentP P} : P P.
Proof. apply (anti_symm ()); auto using always_elim. Qed.
Lemma always_if_always p P `{!PersistentP P} : ?p P P.
......
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