Commit 0dff154c authored by Robbert's avatar Robbert

Merge branch 'ralf/total-core' into 'master'

Try getting rid of total Core typeclass

See merge request !294
parents 4dc1ebda 52be2278
......@@ -39,6 +39,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
explicitly (since TC search is performed less eagerly), and in few cases it is
needed to unfold definitions explicitly (due to new unification algorithm
behaving differently).
* Removed `Core` type class for defining the total core; it is now always
defined in terms of the partial core. The only user of this type class was the
STS RA.
## Iris 3.2.0 (released 2019-08-29)
......
......@@ -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