Commit d4a9c75d authored by Robbert Krebbers's avatar Robbert Krebbers

Enable primitive projections for OFEs.

parent a5063f60
......@@ -154,7 +154,7 @@ Proof.
- by split; simpl; rewrite ?cmra_core_l.
- by split; simpl; rewrite ?cmra_core_idemp.
- intros ??; rewrite! auth_included; intros [??].
by split; simpl; apply cmra_core_mono.
by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
- assert ( n (a b1 b2 : A), b1 b2 {n} a b1 {n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[[a1|]|] b1] [[[a2|]|] b2]; rewrite auth_validN_eq;
......@@ -208,7 +208,7 @@ Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op () (Auth None).
MonoidHomomorphism op op () (@Auth A None).
Proof. by split; [split; try apply _|]. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b a b.
......
......@@ -1230,7 +1230,7 @@ Qed.
(** ** CMRA for the option type *)
Section option.
Context {A : cmraT}.
Implicit Types a : A.
Implicit Types x y : A.
Local Arguments core _ _ !_ /.
Local Arguments pcore _ _ !_ /.
......@@ -1242,11 +1242,11 @@ Section option.
Arguments option_pcore !_ /.
Instance option_op : Op (option A) := union_with (λ x y, Some (x y)).
Definition Some_valid a : Some a a := reflexivity _.
Definition Some_validN a n : {n} Some a {n} a := reflexivity _.
Definition Some_op a b : Some (a b) = Some a Some b := eq_refl.
Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
Definition Some_valid x : Some x x := reflexivity _.
Definition Some_validN x n : {n} Some x {n} x := reflexivity _.
Definition Some_op x y : Some (x y) = Some x Some y := eq_refl.
Lemma Some_core `{CmraTotal A} x : Some (core x) = core (Some x).
Proof. rewrite /core /=. by destruct (cmra_total x) as [? ->]. Qed.
Lemma Some_op_opM x my : Some x my = Some (x ? my).
Proof. by destruct my. Qed.
......
......@@ -318,7 +318,10 @@ Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) :
( c, cFunctorContractive (F c)) cFunctorContractive (iprodCF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
by apply iprodC_map_ne=>c; apply cFunctor_contractive.
(* FIXME: when using `apply` we get
Anomaly "Uncaught exception Retyping.RetypeError(4)." Please report at http://coq.inria.fr/bugs/.
*)
apply: iprodC_map_ne=>c. by apply cFunctor_contractive.
Qed.
Program Definition iprodURF `{Finite C} (F : C urFunctor) : urFunctor := {|
......
From iris.algebra Require Export base.
Set Default Proof Using "Type".
Set Primitive Projections.
(** This files defines (a shallow embedding of) the category of OFEs:
Complete ordered families of equivalences. This is a cartesian closed
......@@ -33,25 +34,20 @@ Tactic Notation "ofe_subst" :=
| H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
end.
Section mixin.
Local Set Primitive Projections.
Record OfeMixin A `{Equiv A, Dist A} := {
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.
Record OfeMixin A `{Equiv A, Dist A} := {
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
}.
(** Bundeled version *)
Structure ofeT := OfeT' {
Structure ofeT := OfeT {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car;
_ : Type
ofe_mixin : OfeMixin ofe_car
}.
Arguments OfeT' _ {_ _} _ _.
Notation OfeT A m := (OfeT' A m A).
Arguments OfeT _ {_ _} _.
Add Printing Constructor ofeT.
Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
......@@ -1057,7 +1053,7 @@ Proof.
Qed.
(** Later *)
Inductive later (A : Type) : Type := Next { later_car : A }.
Record later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Next {_} _.
Arguments later_car {_} _.
......
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