Commit 61046375 authored by Ralf Jung's avatar Ralf Jung

get rid of Core typeclass

parent cbbb2896
......@@ -176,13 +176,9 @@ Hint Mode CmraTotal ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
core. *)
Class Core (A : Type) := core : A A.
Hint Mode Core ! : typeclass_instances.
Definition core `{PCore A} (x : A) : A := default x (pcore x).
Instance: Params (@core) 2 := {}.
Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
Arguments core' _ _ _ /.
(** * CMRAs with a unit element *)
Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.
......@@ -479,7 +475,7 @@ Section total_core.
Lemma cmra_pcore_core x : pcore x = Some (core x).
Proof.
rewrite /core /core'. destruct (cmra_total x) as [cx ->]. done.
rewrite /core. destruct (cmra_total x) as [cx ->]. done.
Qed.
Lemma cmra_core_l x : core x x x.
Proof.
......@@ -769,7 +765,7 @@ Section cmra_morphism.
Local Set Default Proof Using "Type*".
Context {A B : cmraT} (f : A B) `{!CmraMorphism f}.
Lemma cmra_morphism_core x : f (core x) core (f x).
Proof. unfold core, core'. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x y f x f y.
Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
Lemma cmra_morphism_monotoneN n x y : x {n} y f x {n} f y.
......@@ -1037,9 +1033,7 @@ Section mnat.
Qed.
Lemma mnat_ra_mixin : RAMixin mnat.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
- solve_proper.
apply ra_total_mixin; apply _ || eauto.
- intros x y z. apply Nat.max_assoc.
- intros x y. apply Nat.max_comm.
- intros x. apply Max.max_idempotent.
......@@ -1162,7 +1156,7 @@ Section prod.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
Proof.
rewrite /core /core' {1}/pcore /=.
rewrite /core {1}/pcore /=.
rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
Qed.
......
From iris.algebra Require Export cmra updates.
Set Default Proof Using "Type".
Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
Record DraMixin A `{Equiv A, PCore A, Disjoint A, Op A, Valid A} := {
(* setoids *)
mixin_dra_equivalence : Equivalence (@{A});
mixin_dra_op_proper : Proper ((@{A}) ==> () ==> ()) ();
......@@ -29,7 +29,7 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
Structure draT := DraT {
dra_car :> Type;
dra_equiv : Equiv dra_car;
dra_core : Core dra_car;
dra_pcore : PCore dra_car;
dra_disjoint : Disjoint dra_car;
dra_op : Op dra_car;
dra_valid : Valid dra_car;
......@@ -38,13 +38,13 @@ Structure draT := DraT {
Arguments DraT _ {_ _ _ _ _} _.
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_core : simpl never.
Arguments dra_pcore : simpl never.
Arguments dra_disjoint : simpl never.
Arguments dra_op : simpl never.
Arguments dra_valid : simpl never.
Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
(** Lifting properties from the mixin *)
Section dra_mixin.
......
......@@ -28,13 +28,8 @@ Section gset.
Lemma gset_ra_mixin : RAMixin (gset K).
Proof.
apply ra_total_mixin; eauto.
- solve_proper.
- solve_proper.
- solve_proper.
- intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
- intros X1 X2. by rewrite !gset_op_union comm_L.
- intros X. by rewrite gset_core_self idemp_L.
apply ra_total_mixin; apply _ || eauto; [].
intros X. by rewrite gset_core_self idemp_L.
Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
......
......@@ -196,8 +196,8 @@ Instance sts_valid : Valid (car sts) := λ x,
| auth s T => tok s ## T
| frag S' T => closed S' T s, s S'
end.
Instance sts_core : Core (car sts) := λ x,
match x with
Instance sts_core : PCore (car sts) := λ x,
Some match x with
| frag S' _ => frag (up_set S' )
| auth s _ => frag (up s )
end.
......@@ -394,7 +394,7 @@ Qed.
Global Instance sts_frag_core_id S : CoreId (sts_frag S ).
Proof.
constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
constructor; split=> //= [[??]]. by rewrite /dra.dra_pcore /= sts.up_closed.
Qed.
(** Inclusion *)
......
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