Commit 386b91b5 authored by Robbert Krebbers's avatar Robbert Krebbers

LeibnizEquiv instances for Modures.

parent 2e658fd7
......@@ -41,8 +41,8 @@ Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Σ A).
Proof.
intros σ σ' [???]; apply (timeless _), dist_le with (S n); auto with lia.
Qed.
Global Instance pst_proper : Proper (() ==> ()) (@pst Σ A).
Proof. by destruct 1. Qed.
Global Instance pst_proper : Proper (() ==> (=)) (@pst Σ A).
Proof. by destruct 1; unfold_leibniz. Qed.
Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Σ A).
Proof. by destruct 1. Qed.
Global Instance gst_proper : Proper (() ==> ()) (@gst Σ A).
......
......@@ -45,6 +45,8 @@ Canonical Structure authC := CofeT auth_cofe_mixin.
Instance Auth_timeless (x : excl A) (y : A) :
Timeless x Timeless y Timeless (Auth x y).
Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
Global Instance auth_leibniz : LeibnizEquiv A LeibnizEquiv (auth A).
Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
End cofe.
Arguments authC : clear implicits.
......
......@@ -300,6 +300,9 @@ End discrete_cofe.
Arguments discreteC _ {_ _}.
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
Proof. by intros A x y. Qed.
Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
......
......@@ -75,6 +75,8 @@ Proof. by inversion_clear 1; constructor. Qed.
Global Instance excl_timeless :
( x : A, Timeless x) x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
Global Instance excl_leibniz : LeibnizEquiv A LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
(* CMRA *)
Instance excl_valid : Valid (excl A) := λ 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