Commit aebbe02a authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

WIP switching to stdpp and moving from Cofe to Ofe.

parent 1b5e31d9
-Q . iris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
prelude/option.v
prelude/fin_map_dom.v
prelude/bset.v
prelude/fin_maps.v
prelude/vector.v
prelude/pmap.v
prelude/stringmap.v
prelude/fin_collections.v
prelude/mapset.v
prelude/proof_irrel.v
prelude/hashset.v
prelude/pretty.v
prelude/countable.v
prelude/orders.v
prelude/natmap.v
prelude/strings.v
prelude/relations.v
prelude/irelations.v
prelude/collections.v
prelude/listset.v
prelude/streams.v
prelude/gmap.v
prelude/base.v
prelude/tactics.v
prelude/prelude.v
prelude/listset_nodup.v
prelude/finite.v
prelude/numbers.v
prelude/nmap.v
prelude/zmap.v
prelude/coPset.v
prelude/lexico.v
prelude/set.v
prelude/decidable.v
prelude/list.v
prelude/error.v
prelude/functions.v
prelude/hlist.v
prelude/sorting.v
algebra/irelations.v
algebra/relations.v
algebra/step.v
algebra/cmra.v
algebra/cmra_big_op.v
......@@ -46,6 +9,7 @@ algebra/cmra_tactics.v
algebra/sts.v
algebra/auth.v
algebra/gmap.v
algebra/ofe.v
algebra/cofe.v
algebra/base.v
algebra/dra.v
......
From mathcomp Require Export ssreflect.
From iris.prelude Require Export prelude.
From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
Set Default Proof Using "Type".
(* Reset options set by the ssreflect plugin to their defaults *)
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
\ No newline at end of file
Global Unset Asymmetric Patterns.
Ltac done := stdpp.tactics.done.
\ No newline at end of file
From iris.algebra Require Export cofe step.
From iris.algebra Require Export ofe step.
Class PCore (A : Type) := pcore : A option A.
Instance: Params (@pcore) 2.
Class Op (A : Type) := op : A A A.
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.
(* The inclusion quantifies over [A], not [option A]. This means we do not get
reflexivity. However, if we used [option A], the following would no longer
......@@ -14,8 +14,8 @@ Notation "(⋅)" := op (only parsing) : C_scope.
x y x.1 y.1 x.2 y.2
*)
Definition included `{Equiv A, Op A} (x y : A) := z, y x z.
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity.
Instance: Params (@included) 3.
......@@ -26,11 +26,11 @@ Notation "✓{ n } x" := (validN n x)
Class Valid (A : Type) := valid : A Prop.
Instance: Params (@valid) 2.
Notation "✓ x" := (valid x) (at level 20) : C_scope.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := z, y {n} x z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : C_scope.
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (_ {_} _) => reflexivity.
......@@ -69,22 +69,24 @@ Structure cmraT := CMRAT' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
cmra_compl : Compl cmra_car;
cmra_pcore : PCore cmra_car;
cmra_op : Op cmra_car;
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_stepN : StepN cmra_car;
cmra_cofe_mixin : CofeMixin cmra_car;
cmra_cofe_mixin : OfeMixin cmra_car;
cmra_mixin : CMRAMixin cmra_car;
_ : Type
}.
Arguments CMRAT' _ {_ _ _ _ _ _ _ _} _ _ _.
Arguments CMRAT' _ {_ _ _ _ _ _ _} _ _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
Notation CmraT A m := (CMRAT' A (ofe_mixin_of A%type) m A) (only parsing).
Notation CMRAT A m m' := (CMRAT' A m m' A).
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
Arguments cmra_compl : simpl never.
Arguments cmra_pcore : simpl never.
Arguments cmra_op : simpl never.
Arguments cmra_valid : simpl never.
......@@ -98,9 +100,13 @@ Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Hint Extern 0 (StepN _) => eapply (@cmra_stepN _) : typeclass_instances.
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
Coercion cmra_cofeC (A : cmraT) : ofeT := OfeT A (cmra_cofe_mixin A).
Canonical Structure cmra_cofeC.
Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac A) : CMRAMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
(** Lifting properties from the mixin *)
Section cmra_mixin.
Context {A : cmraT}.
......@@ -153,7 +159,7 @@ End cmra_mixin.
Definition opM {A : cmraT} (x : A) (my : option A) :=
match my with Some y => x y | None => x end.
Infix "⋅?" := opM (at level 50, left associativity) : C_scope.
Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
(** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : pcore x Some x.
......@@ -180,7 +186,9 @@ Arguments core' _ _ _ /.
Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
mixin_ucmra_unit_valid : ;
mixin_ucmra_unit_left_id : LeftId () ();
mixin_ucmra_unit_timeless : Timeless ;
(*
mixin_ucmra_unit_timeless : Discrete ;
*)
mixin_ucmra_pcore_unit : pcore Some
}.
......@@ -188,38 +196,38 @@ Structure ucmraT := UCMRAT' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
ucmra_compl : Compl ucmra_car;
ucmra_pcore : PCore ucmra_car;
ucmra_op : Op ucmra_car;
ucmra_valid : Valid ucmra_car;
ucmra_validN : ValidN ucmra_car;
ucmra_stepN : StepN ucmra_car;
ucmra_empty : Empty ucmra_car;
ucmra_cofe_mixin : CofeMixin ucmra_car;
ucmra_ofe_mixin : OfeMixin ucmra_car;
ucmra_cmra_mixin : CMRAMixin ucmra_car;
ucmra_mixin : UCMRAMixin ucmra_car;
_ : Type;
}.
Arguments UCMRAT' _ {_ _ _ _ _ _ _ _ _} _ _ _ _.
Arguments UCMRAT' _ {_ _ _ _ _ _ _ _} _ _ _ _.
Notation UcmraT A m :=
(UCMRAT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
Notation UCMRAT A m m' m'' := (UCMRAT' A m m' m'' A).
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
Arguments ucmra_compl : simpl never.
Arguments ucmra_pcore : simpl never.
Arguments ucmra_op : simpl never.
Arguments ucmra_valid : simpl never.
Arguments ucmra_validN : simpl never.
Arguments ucmra_stepN : simpl never.
Arguments ucmra_cofe_mixin : simpl never.
Arguments ucmra_ofe_mixin : simpl never.
Arguments ucmra_cmra_mixin : simpl never.
Arguments ucmra_mixin : simpl never.
Add Printing Constructor ucmraT.
Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
Coercion ucmra_cofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_cofeC.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
CMRAT A (ucmra_cofe_mixin A) (ucmra_cmra_mixin A).
CMRAT A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.
(** Lifting properties from the mixin *)
......@@ -230,17 +238,16 @@ Section ucmra_mixin.
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_left_id : LeftId () (@op A _).
Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
Global Instance ucmra_unit_timeless : Timeless ( : A).
Proof. apply (mixin_ucmra_unit_timeless _ (ucmra_mixin A)). Qed.
Lemma ucmra_pcore_unit : pcore (:A) Some .
Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
End ucmra_mixin.
(** * Discrete CMRAs *)
Class CMRADiscrete (A : cmraT) := {
cmra_discrete :> Discrete A;
cmra_discrete :> OfeDiscrete A;
cmra_discrete_valid (x : A) : {0} x x
}.
Hint Mode CMRADiscrete ! : typeclass_instances.
(** * Morphisms *)
Class CMRAMonotone {A B : cmraT} (f : A B) := {
......@@ -309,7 +316,7 @@ Proof.
by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
Qed.
Global Instance cmra_opM_ne n : Proper (dist n ==> dist n ==> dist n) (@opM A).
Proof. destruct 2; by cofe_subst. Qed.
Proof. destruct 2; by ofe_subst. Qed.
Global Instance cmra_opM_proper : Proper (() ==> () ==> ()) (@opM A).
Proof. destruct 2; by setoid_subst. Qed.
......@@ -381,7 +388,7 @@ Proof.
intros x y z [z1 Hy] [z2 Hz]; exists (z1 z2). by rewrite assoc -Hy -Hz.
Qed.
Lemma cmra_validN_includedN n x y : {n} y x {n} y {n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Proof. intros Hyv [z ?]; ofe_subst y; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_included n x y : {n} y x y {n} x.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
Lemma cmra_valid_included x y : y x y x.
......@@ -519,21 +526,21 @@ Section total_core.
End total_core.
(** ** Timeless *)
Lemma cmra_timeless_included_l x y : Timeless x {0} y x {0} y x y.
Lemma cmra_timeless_included_l x y : Discrete x {0} y x {0} y x y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy (timeless x z).
by exists z'; rewrite Hy (discrete x z).
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y x {0} y x {n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
Lemma cmra_timeless_included_r n x y : Discrete y x {0} y x {n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (discrete y). Qed.
Lemma cmra_op_timeless x1 x2 :
(x1 x2) Timeless x1 Timeless x2 Timeless (x1 x2).
(x1 x2) Discrete x1 Discrete x2 Discrete (x1 x2).
Proof.
intros ??? z Hz.
destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
{ rewrite -?Hz. by apply cmra_valid_validN. }
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
by rewrite Hz' (discrete x1 y1) // (discrete x2 y2).
Qed.
(** ** Discrete *)
......@@ -542,10 +549,10 @@ Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
Lemma cmra_discrete_included_iff `{Discrete A} n x y : x y x {n} y.
Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x y x {n} y.
Proof.
split; first by apply cmra_included_includedN.
intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
Qed.
End cmra.
......@@ -605,7 +612,7 @@ Section ucmra.
Proof. by destruct H. Qed.
Lemma ucmra_transport_stepN_adj n x y : (T x _(n) y) (x _(n) (ucmra_transport (eq_sym H) y)).
Proof. by destruct H. Qed.
Global Instance ucmra_transport_timeless x : Timeless x Timeless (T x).
Global Instance ucmra_transport_timeless x : Discrete x Discrete (T x).
Proof. by destruct H. Qed.
Global Instance ucmra_transport_persistent x : Persistent x Persistent (T x).
Proof. by destruct H. Qed.
......@@ -685,7 +692,7 @@ End cmra_monotone.
(** Functors *)
Structure rFunctor := RFunctor {
rFunctor_car : cofeT cofeT cmraT;
rFunctor_car : ofeT ofeT cmraT;
rFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
rFunctor_ne A1 A2 B1 B2 n :
......@@ -703,7 +710,7 @@ Instance: Params (@rFunctor_map) 5.
Class rFunctorContractive (F : rFunctor) :=
rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
Definition rFunctor_diag (F: rFunctor) (A: ofeT) : cmraT := rFunctor_car F A A.
Coercion rFunctor_diag : rFunctor >-> Funclass.
Program Definition constRF (B : cmraT) : rFunctor :=
......@@ -714,7 +721,7 @@ Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.
Structure urFunctor := URFunctor {
urFunctor_car : cofeT cofeT ucmraT;
urFunctor_car : ofeT ofeT ucmraT;
urFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
urFunctor_ne A1 A2 B1 B2 n :
......@@ -732,7 +739,7 @@ Instance: Params (@urFunctor_map) 5.
Class urFunctorContractive (F : urFunctor) :=
urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
Definition urFunctor_diag (F: urFunctor) (A: cofeT) : ucmraT := urFunctor_car F A A.
Definition urFunctor_diag (F: urFunctor) (A: ofeT) : ucmraT := urFunctor_car F A A.
Coercion urFunctor_diag : urFunctor >-> Funclass.
Program Definition constURF (B : ucmraT) : urFunctor :=
......@@ -765,7 +772,7 @@ Section cmra_transport.
Proof. by destruct H. Qed.
Lemma cmra_transport_stepN_adj n x y : (T x _(n) y) (x _(n) (cmra_transport (eq_sym H) y)).
Proof. by destruct H. Qed.
Global Instance cmra_transport_timeless x : Timeless x Timeless (T x).
Global Instance cmra_transport_timeless x : Discrete x Discrete (T x).
Proof. by destruct H. Qed.
Global Instance cmra_transport_persistent x : Persistent x Persistent (T x).
Proof. by destruct H. Qed.
......@@ -801,9 +808,10 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A, Step A} := {
}.
Section discrete.
Context `{Equiv A, PCore A, Op A, Valid A, Step A, @Equivalence A ()}.
Local Set Default Proof Using "Type*".
Context `{Equiv A, PCore A, Op A, Valid A, Step A} (Heq: @Equivalence A ()).
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist discrete_compl.
Existing Instances discrete_dist.
Instance discrete_validN : ValidN A := λ n x, x.
Instance discrete_stepN : StepN A := λ n x y, x y.
......@@ -816,16 +824,16 @@ Section discrete.
inversion Hequiv; subst; eauto.
- intros n x y1 y2 ??. by exists (y1,y2).
Qed.
Global Instance discrete_cmra_discrete :
(CMRADiscrete (CMRAT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin A)).
Proof. split; try apply _; auto. Qed.
End discrete.
Notation discreteR A ra_mix :=
(CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
(CmraT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
(only parsing).
Notation discreteUR A ra_mix ucmra_mix :=
(UCMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A, Step A,
@Equivalence A ()} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
Proof. split. apply _. done. Qed.
(UCMRAT A discrete_ofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
Section ra_total.
Context A `{Equiv A, PCore A, Op A, Valid A, Step A}.
......@@ -867,13 +875,13 @@ Section unit.
Instance unit_step : StepN () := λ n x y, True.
Lemma unit_cmra_mixin : CMRAMixin ().
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
Canonical Structure unitR : cmraT := CMRAT () unit_cofe_mixin unit_cmra_mixin.
Canonical Structure unitR : cmraT := CMRAT () unit_ofe_mixin unit_cmra_mixin.
Instance unit_empty : Empty () := ().
Lemma unit_ucmra_mixin : UCMRAMixin ().
Proof. done. Qed.
Canonical Structure unitUR : ucmraT :=
UCMRAT () unit_cofe_mixin unit_cmra_mixin unit_ucmra_mixin.
UCMRAT () unit_ofe_mixin unit_cmra_mixin unit_ucmra_mixin.
Global Instance unit_cmra_discrete : CMRADiscrete unitR.
Proof. done. Qed.
......@@ -908,8 +916,7 @@ Section nat.
Instance nat_empty : Empty nat := 0.
Lemma nat_ucmra_mixin : UCMRAMixin nat.
Proof. split; apply _ || done. Qed.
Canonical Structure natUR : ucmraT :=
discreteUR nat nat_ra_mixin nat_ucmra_mixin.
Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
Global Instance nat_cmra_discrete : CMRADiscrete natR.
Proof. constructor; apply _ || done. Qed.
......@@ -944,8 +951,7 @@ Section mnat.
Instance mnat_empty : Empty mnat := 0.
Lemma mnat_ucmra_mixin : UCMRAMixin mnat.
Proof. split; apply _ || done. Qed.
Canonical Structure mnatUR : ucmraT :=
discreteUR mnat mnat_ra_mixin mnat_ucmra_mixin.
Canonical Structure mnatUR : ucmraT := UcmraT mnat mnat_ucmra_mixin.
Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
Proof. constructor; apply _ || done. Qed.
......@@ -1042,8 +1048,7 @@ Section prod.
- intros n x1 x2 [Hx1 Hx2].
split; eapply cmra_stepN_S; eauto.
Qed.
Canonical Structure prodR :=
CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
Canonical Structure prodR := CmraT (prod A B) prod_cmra_mixin.
Lemma pair_op (a a' : A) (b b' : B) : (a, b) (a', b') = (a a', b b').
Proof. done. Qed.
......@@ -1079,11 +1084,9 @@ Section prod_unit.
split.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- by intros ? [??]; split; apply (timeless _).
- rewrite prod_pcore_Some'; split; apply (persistent _).
Qed.
Canonical Structure prodUR :=
UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin.
Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
Lemma pair_split (x : A) (y : B) : (x, y) (x, ) (, y).
Proof. by rewrite pair_op left_id right_id. Qed.
......@@ -1208,9 +1211,9 @@ Section option.
Proof.
apply cmra_total_mixin.
- eauto.
- by intros n [x|]; destruct 1; constructor; cofe_subst.
- destruct 1; by cofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
- by intros n [x|]; destruct 1; constructor; ofe_subst.
- destruct 1; by ofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; ofe_subst.
- intros [x|]; [apply cmra_valid_validN|done].
- intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
- by intros n.
......@@ -1240,17 +1243,15 @@ Section option.
+ by exists (None,Some x); inversion Hx'; repeat constructor.
+ exists (None,None); repeat constructor.
Qed.
Canonical Structure optionR :=
CMRAT (option A) option_cofe_mixin option_cmra_mixin.
Canonical Structure optionR := CmraT (option A) option_cmra_mixin.
Global Instance option_cmra_discrete : CMRADiscrete A CMRADiscrete optionR.
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
Instance option_empty : Empty (option A) := None.
Lemma option_ucmra_mixin : UCMRAMixin optionR.
Proof. split. done. by intros []. by inversion_clear 1. done. Qed.
Canonical Structure optionUR :=
UCMRAT (option A) option_cofe_mixin option_cmra_mixin option_ucmra_mixin.
Proof. split. done. by intros []. done. Qed.
Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
(** Misc *)
Global Instance Some_cmra_monotone : CMRAMonotone Some.
......@@ -1296,11 +1297,11 @@ Next Obligation.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply rFunctor_id.
apply option_fmap_equiv_ext=>y; apply rFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
Qed.
Instance optionURF_contractive F :
......
From iris.algebra Require Export cmra list.
From iris.prelude Require Import gmap.
From stdpp Require Import gmap.
Fixpoint big_op {A : ucmraT} (xs : list A) : A :=
match xs with [] => | x :: xs => x big_op xs end.
......@@ -34,9 +34,9 @@ Proof.
induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
by rewrite IH assoc.
Qed.
Lemma big_op_contains xs ys : xs `contains` ys big_op xs big_op ys.
Lemma big_op_contains xs ys : xs + ys big_op xs big_op ys.
Proof.
intros [xs' ->]%contains_Permutation.
intros [xs' ->]%submseteq_Permutation.
rewrite big_op_app; apply cmra_included_l.
Qed.
Lemma big_op_delete xs i x :
......@@ -68,8 +68,10 @@ Proof.
intros m2 Hm2; rewrite big_opM_insert //.
rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x)
as (y&?&Hxy); auto using lookup_insert.
rewrite Hxy -big_opM_insert; last auto using lookup_delete.
as (y&?&Hxy); auto.
{ rewrite lookup_insert. done. }
rewrite Hxy -big_opM_insert; last first.
{ eapply lookup_delete. }
by rewrite insert_delete insert_id.
Qed.
Lemma big_opM_lookup_valid n m i x : {n} big_opM m m !! i = Some x {n} x.
......
......@@ -28,7 +28,7 @@ Module ra_reflection. Section ra_reflection.
by rewrite fmap_app IH1 IH2 big_op_app.
Qed.
Lemma flatten_correct Σ e1 e2 :
flatten e1 `contains` flatten e2 eval Σ e1 eval Σ e2.
flatten e1 + flatten e2 eval Σ e1 eval Σ e2.
Proof.
by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
Qed.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections coPset.
From stdpp Require Export collections coPset.
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
......
......@@ -655,11 +655,11 @@ Next Obligation.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply cFunctor_id.
apply option_fmap_equiv_ext=>y; apply cFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
apply option_fmap_equiv_ext=>y; apply cFunctor_compose.
Qed.
Instance optionCF_contractive F :
......
From iris.algebra Require Export cmra.
From iris.prelude Require Export gmap.
From stdpp Require Export gmap.
From iris.algebra Require Import upred updates local_updates.
Section cofe.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections gmap.
From stdpp Require Export collections gmap.
Inductive gset_disj K `{Countable K} :=
| GSet : gset K gset_disj K
......
From iris.algebra Require Export cmra updates.
From iris.algebra Require Import upred.
From iris.prelude Require Import finite.
From stdpp Require Import finite.
(** * Indexed product *)
(** Need to put this in a definition to make canonical structures to work. *)
......
......@@ -12,7 +12,7 @@
**)
From Coq Require Import Wf_nat Omega.
From iris.prelude Require Export tactics base relations list collections.
From stdpp Require Export tactics base relations list collections.
(** * Definitions *)
Section definitions.
......@@ -1336,7 +1336,7 @@ Section cofair.
End erasure.
Section block.
From iris.prelude Require Export set.
From stdpp Require Export set.
Context (flatten: A B * (nat set nat)).
Context (flatten_spec_step:
i a a', R1 i a a'
......@@ -1441,7 +1441,7 @@ Section cofair.
apply glue_length.
Qed.
Lemma glue_prefix_S: a e n, prefix_of (glue a e n) (glue a e (S n)).
Lemma glue_prefix_S: a e n, prefix (glue a e n) (glue a e (S n)).
Proof.
intros a e n. revert a e; induction n; intros.