### Merge branch 'ci/primproj' into 'master'

```use primitive projections for our mixins

See merge request FP/iris-coq!69```
parents 7db2fb65 a19d201e
 ... @@ -39,27 +39,30 @@ Notation "x ≼{ n } y" := (includedN n x y) ... @@ -39,27 +39,30 @@ Notation "x ≼{ n } y" := (includedN n x y) Instance: Params (@includedN) 4. Instance: Params (@includedN) 4. Hint Extern 0 (_ ≼{_} _) => reflexivity. Hint Extern 0 (_ ≼{_} _) => reflexivity. Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { Section mixin. (* setoids *) Local Set Primitive Projections. mixin_cmra_op_ne (x : A) : NonExpansive (op x); Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { mixin_cmra_pcore_ne n x y cx : (* setoids *) x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy; mixin_cmra_op_ne (x : A) : NonExpansive (op x); mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); mixin_cmra_pcore_ne n x y cx : (* valid *) x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy; mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; (* valid *) (* monoid *) mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; mixin_cmra_assoc : Assoc (≡) (⋅); mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; mixin_cmra_comm : Comm (≡) (⋅); (* monoid *) mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x; mixin_cmra_assoc : Assoc (≡) (⋅); mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx; mixin_cmra_comm : Comm (≡) (⋅); mixin_cmra_pcore_mono x y cx : mixin_cmra_pcore_l x cx : pcore x = Some cx → cx ⋅ x ≡ x; x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy; mixin_cmra_pcore_idemp x cx : pcore x = Some cx → pcore cx ≡ Some cx; mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; mixin_cmra_pcore_mono x y cx : mixin_cmra_extend n x y1 y2 : x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy; ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 mixin_cmra_extend n x y1 y2 : }. ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 }. End mixin. (** Bundeled version *) (** Bundeled version *) Structure cmraT := CMRAT' { Structure cmraT := CMRAT' { ... ...
 ... @@ -33,11 +33,14 @@ Tactic Notation "ofe_subst" := ... @@ -33,11 +33,14 @@ Tactic Notation "ofe_subst" := | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x end. end. Record OfeMixin A `{Equiv A, Dist A} := { Section mixin. mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; Local Set Primitive Projections. mixin_dist_equivalence n : Equivalence (dist n); Record OfeMixin A `{Equiv A, Dist A} := { mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; }. mixin_dist_equivalence n : Equivalence (dist n); mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y }. End mixin. (** Bundeled version *) (** Bundeled version *) Structure ofeT := OfeT' { Structure ofeT := OfeT' { ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!