From accf80a6dfc349cb1ffa5fc3e18ef93afc5b662d Mon Sep 17 00:00:00 2001
From: Simon Spies <simonspies@icloud.com>
Date: Sun, 11 Sep 2022 15:05:56 +0200
Subject: [PATCH] index as type class
---
theories/algebra/agree.v | 22 +-
theories/algebra/big_op.v | 14 +-
theories/algebra/cmra.v | 291 ++++++------
theories/algebra/cmra_big_op.v | 8 +-
theories/algebra/cofe_solver.v | 124 +++---
theories/algebra/excl.v | 28 +-
theories/algebra/finite.v | 18 +
theories/algebra/frac.v | 8 +-
theories/algebra/gmap.v | 73 +--
theories/algebra/local_updates.v | 22 +-
theories/algebra/monoid.v | 14 +-
theories/algebra/numbers.v | 78 ++--
theories/algebra/ofe.v | 471 ++++++++++----------
theories/algebra/proofmode_classes.v | 20 +-
theories/algebra/truncation.v | 78 ++--
theories/algebra/updates.v | 14 +-
theories/algebra/wf_IR.v | 22 +-
theories/stepindex/existential_properties.v | 15 +-
theories/stepindex/stepindex.v | 140 +++---
19 files changed, 732 insertions(+), 728 deletions(-)
create mode 100644 theories/algebra/finite.v
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 1c373216..faf0a138 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -50,17 +50,17 @@ Proof.
Qed.
Section agree.
-Context {SI} {A : ofe SI}.
+Context `{SI: indexT} {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : agree A.
(* OFE *)
-Local Instance agree_dist : Dist SI (agree A) := λ n x y,
+Local Instance agree_dist : Dist (agree A) := λ n x y,
(∀ a, a ∈ agree_car x → ∃ b, b ∈ agree_car y ∧ a ≡{n}≡ b) ∧
(∀ b, b ∈ agree_car y → ∃ a, a ∈ agree_car x ∧ a ≡{n}≡ b).
Local Instance agree_equiv : Equiv (agree A) := λ x y, ∀ n, x ≡{n}≡ y.
-Definition agree_ofe_mixin : OfeMixin SI (agree A).
+Definition agree_ofe_mixin : OfeMixin (agree A).
Proof.
split.
- done.
@@ -79,7 +79,7 @@ Canonical Structure agreeO := Ofe (agree A) agree_ofe_mixin.
(* CMRA *)
(* agree_validN is carefully written such that, when applied to a singleton, it
is convertible to True. This makes working with agreement much more pleasant. *)
-Local Instance agree_validN_instance : ValidN SI (agree A) := λ n x,
+Local Instance agree_validN_instance : ValidN (agree A) := λ n x,
match agree_car x with
| [a] => True
| _ => ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b
@@ -136,7 +136,7 @@ Proof.
- destruct (elem_of_agree x1); naive_solver.
Qed.
-Definition agree_cmra_mixin : CmraMixin SI (agree A).
+Definition agree_cmra_mixin : CmraMixin (agree A).
Proof.
apply cmra_total_mixin; try apply _ || by eauto.
- intros α β x; rewrite !agree_validN_def; eauto using dist_le.
@@ -147,7 +147,7 @@ Proof.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
-Canonical Structure agreeR : cmra SI := Cmra SI (agree A) agree_cmra_mixin.
+Canonical Structure agreeR : cmra := Cmra (agree A) agree_cmra_mixin.
Global Instance agree_cmra_total : CmraTotal agreeR.
Proof. rewrite /CmraTotal; eauto. Qed.
@@ -275,7 +275,7 @@ Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
Proof. by apply agree_eq. Qed.
Section agree_map.
- Context {SI} {A B : ofe SI} (f : A → B) {Hf: NonExpansive f}.
+ Context `{SI: indexT} {A B : ofe} (f : A → B) {Hf: NonExpansive f}.
Local Instance agree_map_ne : NonExpansive (agree_map f).
Proof using Type*.
@@ -305,15 +305,15 @@ Section agree_map.
Qed.
End agree_map.
-Definition agreeO_map {SI} {A B: ofe SI} (f : A -n> B) : agreeO A -n> agreeO B :=
+Definition agreeO_map `{SI: indexT} {A B: ofe} (f : A -n> B) : agreeO A -n> agreeO B :=
OfeMor (agree_map f : agreeO A → agreeO B).
-Global Instance agreeO_map_ne {SI} A B : NonExpansive (@agreeO_map SI A B).
+Global Instance agreeO_map_ne `{SI: indexT} A B : NonExpansive (@agreeO_map SI A B).
Proof.
intros n f g Hfg x; split=> b /=;
setoid_rewrite elem_of_list_fmap; naive_solver.
Qed.
-Program Definition agreeRF {SI} (F : oFunctor SI) : rFunctor SI := {|
+Program Definition agreeRF `{SI: indexT} (F : oFunctor) : rFunctor := {|
rFunctor_car A B := agreeR (oFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := agreeO_map (oFunctor_map F fg)
|}.
@@ -329,7 +329,7 @@ Next Obligation.
apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
Qed.
-Global Instance agreeRF_contractive {SI} (F : oFunctor SI):
+Global Instance agreeRF_contractive `{SI: indexT} (F : oFunctor):
oFunctorContractive F → rFunctorContractive (agreeRF F).
Proof.
intros ? A1 A2 B1 B2 n ???; simpl.
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 29354953..4b1b53cc 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -20,14 +20,14 @@ Since these big operators are like quantifiers, they have the same precedence as
[∀] and [∃]. *)
(** * Big ops over lists *)
-Fixpoint big_opL {SI} {M: ofe SI} {o: M → M → M} `{!Monoid o} {A} (f : nat → A → M) (xs : list A) : M :=
+Fixpoint big_opL `{SI: indexT} {M: ofe} {o: M → M → M} `{!Monoid o} {A} (f : nat → A → M) (xs : list A) : M :=
match xs with
| [] => monoid_unit
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
Global Instance: Params (@big_opL) 5 := {}.
Global Arguments big_opL {SI} {M} o {_ A} _ !_ /.
-Typeclasses Opaque big_opL.
+Global Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope.
@@ -35,7 +35,7 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity,
format "[^ o list] x ∈ l , P") : stdpp_scope.
-Definition big_opM_def {SI} {M: ofe SI} {o: M → M → M} `{!Monoid o} `{Countable K} {A} (f : K → A → M)
+Definition big_opM_def `{SI: indexT} {M: ofe} {o: M → M → M} `{!Monoid o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, uncurry f) (map_to_list m).
Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
@@ -49,7 +49,7 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity,
format "[^ o map] x ∈ m , P") : stdpp_scope.
-Definition big_opS_def {SI} {M: ofe SI} {o: M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
+Definition big_opS_def `{SI: indexT} {M: ofe} {o: M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
@@ -60,7 +60,7 @@ Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o set] x ∈ X , P") : stdpp_scope.
-Definition big_opMS_def {SI} {M: ofe SI} {o: M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
+Definition big_opMS_def `{SI: indexT} {M: ofe} {o: M → M → M} `{!Monoid o} `{Countable A} (f : A → M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
Definition big_opMS := big_opMS_aux.(unseal).
@@ -73,7 +73,7 @@ Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(** * Properties about big ops *)
Section big_op.
-Context {SI} {M: ofe SI} {o: M → M → M} `{!Monoid o}.
+Context `{SI: indexT} {M: ofe} {o: M → M → M} `{!Monoid o}.
Implicit Types xs : list M.
Infix "`o`" := o (at level 50, left associativity).
@@ -655,7 +655,7 @@ End gmultiset.
End big_op.
Section homomorphisms.
- Context {SI} {M1 M2: ofe SI} {o1: M1 → M1 → M1} {o2: M2 → M2 → M2} `{!Monoid o1, !Monoid o2}.
+ Context `{SI: indexT} {M1 M2: ofe} {o1: M1 → M1 → M1} {o2: M2 → M2 → M2} `{!Monoid o1, !Monoid o2}.
Infix "`o1`" := o1 (at level 50, left associativity).
Infix "`o2`" := o2 (at level 50, left associativity).
(** The ssreflect rewrite tactic only works for relations that have a
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 65340b22..640dc1f8 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -24,7 +24,7 @@ Notation "(≼)" := included (only parsing) : stdpp_scope.
Global Hint Extern 0 (_ ≼ _) => reflexivity : core.
Global Instance: Params (@included) 3 := {}.
-Class ValidN (SI: indexT) (A : Type) := validN : SI → A → Prop.
+Class ValidN `{SI: indexT} (A : Type) := validN : index → A → Prop.
Global Hint Mode ValidN - ! : typeclass_instances.
Global Instance: Params (@validN) 4 := {}.
Notation "✓{ α } x" := (validN α x)
@@ -35,7 +35,7 @@ Global Hint Mode Valid ! : typeclass_instances.
Global Instance: Params (@valid) 2 := {}.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
-Definition includedN {SI: indexT} `{Dist SI A, Op A} (α : SI) (x y : A) := ∃ z, y ≡{α}≡ x ⋅ z.
+Definition includedN `{SI: indexT} `{!Dist A, Op A} (α : index) (x y : A) := ∃ z, y ≡{α}≡ x ⋅ z.
Notation "x ≼{ α } y" := (includedN α x y)
(at level 70, α at next level, format "x ≼{ α } y") : stdpp_scope.
Global Instance: Params (@includedN) 5 := {}.
@@ -43,7 +43,7 @@ Global Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
Section mixin.
Local Set Primitive Projections.
- Record CmraMixin {SI: indexT} A `{Dist SI A, Equiv A, PCore A, Op A, Valid A, ValidN SI A} := {
+ Record CmraMixin `{SI: indexT} A `{!Dist A, Equiv A, PCore A, Op A, Valid A, !ValidN A} := {
(* setoids *)
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne α (x y : A) cx :
@@ -65,25 +65,25 @@ Section mixin.
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{α}≡ y1 ∧ z2 ≡{α}≡ y2 } }
}.
End mixin.
-Arguments CmraMixin _ _ {_ _ _ _ _ _}.
+Arguments CmraMixin {_} _ {_ _ _ _ _ _}.
(** Bundled version *)
-Structure cmra (SI: indexT) := Cmra' {
+Structure cmra `{SI: indexT} := Cmra' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
- cmra_dist : Dist SI cmra_car;
+ cmra_dist : Dist cmra_car;
cmra_pcore : PCore cmra_car;
cmra_op : Op cmra_car;
cmra_valid : Valid cmra_car;
- cmra_validN : ValidN SI cmra_car;
- cmra_ofe_mixin : OfeMixin SI cmra_car;
- cmra_mixin : CmraMixin SI cmra_car;
+ cmra_validN : ValidN cmra_car;
+ cmra_ofe_mixin : OfeMixin cmra_car;
+ cmra_mixin : CmraMixin cmra_car;
}.
Global Arguments Cmra' {_} _ {_ _ _ _ _ _} _ _.
(* Given [m : CmraMixin A], the notation [Cmra 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 Cmra SI A m := (Cmra' A (ofe_mixin_of SI A%type) m) (only parsing).
+Notation Cmra A m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).
Global Arguments cmra_car {_} : simpl never.
Global Arguments cmra_equiv {_} : simpl never.
@@ -98,17 +98,17 @@ Add Printing Constructor cmra.
Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _ _) : typeclass_instances.
Global Hint Extern 0 (Op _) => eapply (@cmra_op _ _) : typeclass_instances.
Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _ _) : typeclass_instances.
-Global Hint Extern 0 (ValidN _ _) => eapply (@cmra_validN _ _) : typeclass_instances.
-Coercion cmra_ofeO {SI: indexT} (A : cmra SI) : ofe SI := Ofe A (cmra_ofe_mixin A).
+Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _ _) : typeclass_instances.
+Coercion cmra_ofeO `{SI: indexT} (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeO.
-Definition cmra_mixin_of' {SI: indexT} A {Ac : cmra SI} (f : Ac → A) : CmraMixin SI Ac := cmra_mixin Ac.
+Definition cmra_mixin_of' `{SI: indexT} A {Ac : cmra} (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 {SI: indexT} {A : cmra SI}.
+ Context `{SI: indexT} {A : cmra}.
Implicit Types x y : A.
Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
@@ -140,38 +140,38 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
End cmra_mixin.
-Definition opM {SI: indexT} {A : cmra SI} (x : A) (my : option A) :=
+Definition opM `{SI: indexT} {A : cmra} (x : A) (my : option A) :=
match my with Some y => x ⋅ y | None => x end.
Infix "⋅?" := opM (at level 50, left associativity) : stdpp_scope.
(** * CoreId elements *)
-Class CoreId {SI: indexT} {A : cmra SI} (x : A) := core_id : pcore x ≡ Some x.
+Class CoreId `{SI: indexT} {A : cmra} (x : A) := core_id : pcore x ≡ Some x.
Global Arguments core_id {_ _} _ {_}.
Global Hint Mode CoreId - + ! : typeclass_instances.
Global Instance: Params (@CoreId) 2 := {}.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
-Class Exclusive {SI: indexT} {A : cmra SI} (x : A) := exclusive0_l y : ✓{zero} (x ⋅ y) → False.
+Class Exclusive `{SI: indexT} {A : cmra} (x : A) := exclusive0_l y : ✓{zero} (x ⋅ y) → False.
Global Arguments exclusive0_l {_ _} _ {_} _ _.
Global Hint Mode Exclusive - + ! : typeclass_instances.
Global Instance: Params (@Exclusive) 2 := {}.
(** * Cancelable elements. *)
-Class Cancelable {SI: indexT} {A : cmra SI} (x : A) :=
+Class Cancelable `{SI: indexT} {A : cmra} (x : A) :=
cancelableN α y z : ✓{α}(x ⋅ y) → x ⋅ y ≡{α}≡ x ⋅ z → y ≡{α}≡ z.
Global Arguments cancelableN {_ _} _ {_} _ _ _ _.
Global Hint Mode Cancelable - + ! : typeclass_instances.
Global Instance: Params (@Cancelable) 2 := {}.
(** * Identity-free elements. *)
-Class IdFree {SI: indexT} {A : cmra SI} (x : A) :=
+Class IdFree `{SI: indexT} {A : cmra} (x : A) :=
id_free0_r y : ✓{zero}x → x ⋅ y ≡{zero}≡ x → False.
Global Arguments id_free0_r {_ _} {_} _ {_} _ _.
Global Hint Mode IdFree - + ! : typeclass_instances.
Global Instance: Params (@IdFree) 2 := {}.
(** * CMRAs whose core is total *)
-Class CmraTotal {SI: indexT} (A : cmra SI) := cmra_total (x : A) : is_Some (pcore x).
+Class CmraTotal `{SI: indexT} (A : cmra) := cmra_total (x : A) : is_Some (pcore x).
Global Hint Mode CmraTotal - ! : typeclass_instances.
(** The function [core] returns a dummy when used on CMRAs without total
@@ -184,29 +184,29 @@ Global Instance: Params (@core) 2 := {}.
Class Unit (A : Type) := ε : A.
Global Arguments ε {_ _}.
-Record UcmraMixin {SI: indexT} A `{Dist SI A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
+Record UcmraMixin `{SI: indexT} A `{!Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
mixin_ucmra_unit_valid : ✓ (ε : A);
mixin_ucmra_unit_left_id : LeftId (≡) ε (⋅);
mixin_ucmra_pcore_unit : pcore ε ≡ Some ε
}.
-Arguments UcmraMixin _ _ {_ _ _ _ _ _}.
+Arguments UcmraMixin {_} _ {_ _ _ _ _ _}.
-Structure ucmra (SI: indexT) := Ucmra' {
+Structure ucmra `{SI: indexT} := Ucmra' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
- ucmra_dist : Dist SI ucmra_car;
+ ucmra_dist : Dist ucmra_car;
ucmra_pcore : PCore ucmra_car;
ucmra_op : Op ucmra_car;
ucmra_valid : Valid ucmra_car;
- ucmra_validN : ValidN SI ucmra_car;
+ ucmra_validN : ValidN ucmra_car;
ucmra_unit : Unit ucmra_car;
- ucmra_ofe_mixin : OfeMixin SI ucmra_car;
- ucmra_cmra_mixin : CmraMixin SI ucmra_car;
- ucmra_mixin : UcmraMixin SI ucmra_car;
+ ucmra_ofe_mixin : OfeMixin ucmra_car;
+ ucmra_cmra_mixin : CmraMixin ucmra_car;
+ ucmra_mixin : UcmraMixin ucmra_car;
}.
Global Arguments Ucmra' {_} _ {_ _ _ _ _ _ _} _ _ _.
-Notation Ucmra SI A m :=
- (Ucmra' A (ofe_mixin_of SI A%type) (cmra_mixin_of A%type) m) (only parsing).
+Notation Ucmra A m :=
+ (Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Global Arguments ucmra_car {_} : simpl never.
Global Arguments ucmra_equiv {_} : simpl never.
@@ -220,15 +220,15 @@ Global Arguments ucmra_cmra_mixin {_} : simpl never.
Global Arguments ucmra_mixin {_} : simpl never.
Add Printing Constructor ucmra.
Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
-Coercion ucmra_ofeO {SI: indexT} (A : ucmra SI) : ofe SI := Ofe A (ucmra_ofe_mixin A).
+Coercion ucmra_ofeO `{SI: indexT} (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeO.
-Coercion ucmra_cmraR {SI: indexT} (A : ucmra SI) : cmra SI :=
+Coercion ucmra_cmraR `{SI: indexT} (A : ucmra) : cmra :=
Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.
(** Lifting properties from the mixin *)
Section ucmra_mixin.
- Context {SI: indexT} {A : ucmra SI}.
+ Context `{SI: indexT} {A : ucmra}.
Implicit Types x y : A.
Lemma ucmra_unit_valid : ✓ (ε : A).
Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
@@ -239,14 +239,14 @@ Section ucmra_mixin.
End ucmra_mixin.
(** * Discrete CMRAs *)
-Class CmraDiscrete {SI: indexT} (A : cmra SI) := {
+Class CmraDiscrete `{SI: indexT} (A : cmra) := {
cmra_discrete_ofe_discrete :> OfeDiscrete A;
cmra_discrete_valid (x : A) : ✓{zero} x → ✓ x
}.
Global Hint Mode CmraDiscrete - ! : typeclass_instances.
(** * Morphisms *)
-Class CmraMorphism {SI: indexT} {A B : cmra SI} (f : A → B) := {
+Class CmraMorphism `{SI: indexT} {A B : cmra} (f : A → B) := {
cmra_morphism_ne :> NonExpansive f;
cmra_morphism_validN α x : ✓{α} x → ✓{α} f x;
cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
@@ -258,7 +258,7 @@ Arguments cmra_morphism_op {_ _ _} _ {_} _ _.
(** * Properties **)
Section cmra.
-Context {SI: indexT} {A : cmra SI}.
+Context `{SI: indexT} {A : cmra}.
Implicit Types x y z : A.
Implicit Types xs ys zs : list A.
@@ -562,19 +562,19 @@ Proof.
Qed.
(** ** Discrete *)
-Lemma cmra_discrete_valid_iff `{CmraDiscrete SI A} α x : ✓ x ↔ ✓{α} x.
+Lemma cmra_discrete_valid_iff `{!CmraDiscrete A} α x : ✓ x ↔ ✓{α} x.
Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le, index_zero_minimum.
Qed.
-Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete SI A} α x : ✓{zero} x ↔ ✓{α} x.
+Lemma cmra_discrete_valid_iff_0 `{!CmraDiscrete A} α x : ✓{zero} x ↔ ✓{α} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
-Lemma cmra_discrete_included_iff `{OfeDiscrete SI A} α x y : x ≼ y ↔ x ≼{α} y.
+Lemma cmra_discrete_included_iff `{!OfeDiscrete A} α x y : x ≼ y ↔ x ≼{α} y.
Proof.
split; first by apply cmra_included_includedN.
intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
Qed.
-Lemma cmra_discrete_included_iff_0 `{OfeDiscrete SI A} α x y : x ≼{zero} y ↔ x ≼{α} y.
+Lemma cmra_discrete_included_iff_0 `{!OfeDiscrete A} α x y : x ≼{zero} y ↔ x ≼{α} y.
Proof. by rewrite -!cmra_discrete_included_iff. Qed.
(** Cancelable elements *)
@@ -582,7 +582,7 @@ Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable SI A).
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
Lemma cancelable x `{!Cancelable x} y z : ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z.
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
-Lemma discrete_cancelable x `{CmraDiscrete SI A}:
+Lemma discrete_cancelable x `{!CmraDiscrete A}:
(∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x.
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
@@ -612,7 +612,7 @@ Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
Lemma id_free_l x `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
Proof. rewrite comm. eauto using id_free_r. Qed.
-Lemma discrete_id_free x `{CmraDiscrete SI A}:
+Lemma discrete_id_free x `{!CmraDiscrete A}:
(∀ y, ✓ x → x ⋅ y ≡ x → False) → IdFree x.
Proof.
intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
@@ -630,7 +630,7 @@ End cmra.
(** * Properties about CMRAs with a unit element **)
Section ucmra.
- Context {SI: indexT} {A : ucmra SI}.
+ Context `{SI: indexT} {A : ucmra}.
Implicit Types x y z : A.
Lemma ucmra_unit_validN α : ✓{α} (ε:A).
@@ -661,7 +661,7 @@ Global Hint Immediate cmra_unit_cmra_total : core.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
Local Set Default Proof Using "Type*".
- Context {SI: indexT} {A : cmra SI} `{!LeibnizEquiv A}.
+ Context `{SI: indexT} {A : cmra} `{!LeibnizEquiv A}.
Implicit Types x y : A.
Global Instance cmra_assoc_L : Assoc (=) (@op A _).
@@ -708,7 +708,7 @@ End cmra_leibniz.
Section ucmra_leibniz.
Local Set Default Proof Using "Type*".
- Context {SI: indexT} {A : ucmra SI} `{!LeibnizEquiv A}.
+ Context `{SI: indexT} {A : ucmra} `{!LeibnizEquiv A}.
Implicit Types x y z : A.
Global Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _).
@@ -719,7 +719,7 @@ End ucmra_leibniz.
(** * Constructing a CMRA with total core *)
Section cmra_total.
- Context A {SI: indexT} `{Dist SI A, Equiv A, PCore A, Op A, Valid A, ValidN SI A}.
+ Context A `{SI: indexT} `{!Dist A, Equiv A, PCore A, Op A, Valid A, !ValidN A}.
Context (total : ∀ x : A, is_Some (pcore x)).
Context (op_ne : ∀ x : A, NonExpansive (op x)).
Context (core_ne : NonExpansive (@core A _)).
@@ -735,7 +735,7 @@ Section cmra_total.
Context (extend : ∀ α (x y1 y2 : A),
✓{α} x → x ≡{α}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{α}≡ y1 ∧ z2 ≡{α}≡ y2 } }).
- Lemma cmra_total_mixin : CmraMixin SI A.
+ Lemma cmra_total_mixin : CmraMixin A.
Proof using Type*.
split; auto.
- intros α x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
@@ -749,7 +749,7 @@ Section cmra_total.
End cmra_total.
(** * Properties about morphisms *)
-Global Instance cmra_morphism_id {SI: indexT} {A : cmra SI} : CmraMorphism (@id A).
+Global Instance cmra_morphism_id `{SI: indexT} {A : cmra} : CmraMorphism (@id A).
Proof.
split => /=.
- apply _.
@@ -757,9 +757,9 @@ Proof.
- intros. by rewrite option_fmap_id.
- done.
Qed.
-Global Instance cmra_morphism_proper {SI: indexT} {A B : cmra SI} (f : A → B) `{!CmraMorphism f} :
+Global Instance cmra_morphism_proper `{SI: indexT} {A B : cmra} (f : A → B) `{!CmraMorphism f} :
Proper ((≡) ==> (≡)) f := ne_proper _.
-Global Instance cmra_morphism_compose {SI: indexT} {A B C : cmra SI} (f : A → B) (g : B → C) :
+Global Instance cmra_morphism_compose `{SI: indexT} {A B C : cmra} (f : A → B) (g : B → C) :
CmraMorphism f → CmraMorphism g → CmraMorphism (g ∘ f).
Proof.
split.
@@ -771,7 +771,7 @@ Qed.
Section cmra_morphism.
Local Set Default Proof Using "Type*".
- Context {SI: indexT} {A B : cmra SI} (f : A → B) `{!CmraMorphism f}.
+ Context `{SI: indexT} {A B : cmra} (f : A → B) `{!CmraMorphism f}.
Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
Proof. unfold core. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
@@ -783,8 +783,8 @@ Section cmra_morphism.
End cmra_morphism.
(** OFE → CMRA Functors *)
-Record rFunctor {SI: indexT} := RFunctor {
- rFunctor_car : ∀ (A: ofe SI) (B: ofe SI), cmra SI;
+Record rFunctor `{SI: indexT} := RFunctor {
+ rFunctor_car : ∀ (A: ofe) (B: ofe), cmra;
rFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
rFunctor_map_ne A1 A2 B1 B2:
@@ -798,22 +798,21 @@ Record rFunctor {SI: indexT} := RFunctor {
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (rFunctor_map fg)
}.
-Arguments rFunctor : clear implicits.
-Existing Instances rFunctor_map_ne rFunctor_mor.
+Global Existing Instances rFunctor_map_ne rFunctor_mor.
Global Instance: Params (@rFunctor_map) 6 := {}.
Declare Scope rFunctor_scope.
Delimit Scope rFunctor_scope with RF.
Bind Scope rFunctor_scope with rFunctor.
-Class rFunctorContractive {SI: indexT} (F : rFunctor SI) :=
+Class rFunctorContractive `{SI: indexT} (F : rFunctor) :=
rFunctor_map_contractive A1 A2 B1 B2 :>
Contractive (@rFunctor_map SI F A1 A2 B1 B2).
-Definition rFunctor_apply {SI: indexT} (F: rFunctor SI) (A: ofe SI) `{!Cofe A} : cmra SI :=
+Definition rFunctor_apply `{SI: indexT} (F: rFunctor) (A: ofe) `{!Cofe A} : cmra :=
rFunctor_car F A A.
-Program Definition rFunctor_to_oFunctor {SI} (F: rFunctor SI) : oFunctor SI := {|
+Program Definition rFunctor_to_oFunctor `{SI: indexT} (F: rFunctor) : oFunctor := {|
oFunctor_car A B := rFunctor_car F A B;
oFunctor_map A1 A2 B1 B2 fg := rFunctor_map F fg
|}.
@@ -825,13 +824,13 @@ Next Obligation.
apply rFunctor_map_compose.
Qed.
-Global Instance rFunctor_to_oFunctor_contractive {SI: indexT} (F: rFunctor SI) :
+Global Instance rFunctor_to_oFunctor_contractive `{SI: indexT} (F: rFunctor) :
rFunctorContractive F → oFunctorContractive (rFunctor_to_oFunctor F).
Proof.
intros A1 A2 B1 B2 n f g Hfg. apply rFunctor_map_contractive.
Qed.
-Program Definition rFunctor_oFunctor_compose {SI} (F1 : rFunctor SI) (F2 : oFunctor SI) : rFunctor SI := {|
+Program Definition rFunctor_oFunctor_compose `{SI: indexT} (F1 : rFunctor) (F2 : oFunctor) : rFunctor := {|
rFunctor_car A B := rFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
rFunctor_map A1 A2 B1 B2 'fg :=
rFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
@@ -850,59 +849,58 @@ Next Obligation.
rewrite -rFunctor_map_compose. apply equiv_dist=> n. apply rFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_compose.
Qed.
-Global Instance rFunctor_oFunctor_compose_contractive_1 {SI} (F1 : rFunctor SI) (F2 : oFunctor SI) :
+Global Instance rFunctor_oFunctor_compose_contractive_1 `{SI: indexT} (F1 : rFunctor) (F2 : oFunctor) :
rFunctorContractive F1 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 A2 B1 B2 n [f1 g1] [f2 g2] Hfg; simpl in *.
f_contractive. intros m Hlt; specialize (Hfg m Hlt). destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.
-Global Instance rFunctor_oFunctor_compose_contractive_2 {SI} (F1 : rFunctor SI) (F2 : oFunctor SI):
+Global Instance rFunctor_oFunctor_compose_contractive_2 `{SI: indexT} (F1 : rFunctor) (F2 : oFunctor):
oFunctorContractive F2 → rFunctorContractive (rFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 A2 B1 B2 n [f1 g1] [f2 g2] Hfg; simpl in *.
f_equiv; split; simpl in *; f_contractive; intros m Hlt; specialize (Hfg m Hlt); destruct Hfg; by split.
Qed.
-Program Definition constRF {SI: indexT} (B : cmra SI) : rFunctor SI :=
+Program Definition constRF `{SI: indexT} (B : cmra) : rFunctor :=
{| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
Coercion constRF : cmra >-> rFunctor.
-Global Instance constRF_contractive {SI: indexT} (B : cmra SI): rFunctorContractive (constRF B).
+Global Instance constRF_contractive `{SI: indexT} (B : cmra): rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed.
(** OFE → UCMRA Functors *)
-Record urFunctor {SI: indexT} := URFunctor {
- urFunctor_car : ∀ A B, ucmra SI;
+Record urFunctor `{SI: indexT} := URFunctor {
+ urFunctor_car : ∀ A B, ucmra;
urFunctor_map {A1 A2 B1 B2}:
((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
- urFunctor_map_ne {A1 A2 B1 B2 : ofe SI}:
+ urFunctor_map_ne {A1 A2 B1 B2 : ofe}:
NonExpansive (@urFunctor_map A1 A2 B1 B2);
- urFunctor_map_id {A B : ofe SI} (x : urFunctor_car A B) :
+ urFunctor_map_id {A B : ofe} (x : urFunctor_car A B) :
urFunctor_map (cid,cid) x ≡ x;
- urFunctor_map_compose {A1 A2 A3 B1 B2 B3 : ofe SI}
+ urFunctor_map_compose {A1 A2 A3 B1 B2 B3 : ofe}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
- urFunctor_mor {A1 A2 B1 B2 : ofe SI}
+ urFunctor_mor {A1 A2 B1 B2 : ofe}
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (urFunctor_map fg)
}.
-Arguments urFunctor : clear implicits.
-Existing Instances urFunctor_map_ne urFunctor_mor.
+Global Existing Instances urFunctor_map_ne urFunctor_mor.
Global Instance: Params (@urFunctor_map) 6 := {}.
Declare Scope urFunctor_scope.
Delimit Scope urFunctor_scope with URF.
Bind Scope urFunctor_scope with urFunctor.
-Class urFunctorContractive {SI: indexT} (F : urFunctor SI) :=
+Class urFunctorContractive `{SI: indexT} (F : urFunctor) :=
urFunctor_map_contractive A1 A2 B1 B2 :>
Contractive (@urFunctor_map SI F A1 A2 B1 B2).
-Definition urFunctor_apply {SI: indexT} (F: urFunctor SI) (A: ofe SI) `{!Cofe A} : ucmra SI :=
+Definition urFunctor_apply `{SI: indexT} (F: urFunctor) (A: ofe) `{!Cofe A} : ucmra :=
urFunctor_car F A A.
-Program Definition urFunctor_to_rFunctor {SI} (F: urFunctor SI) : rFunctor SI := {|
+Program Definition urFunctor_to_rFunctor `{SI: indexT} (F: urFunctor) : rFunctor := {|
rFunctor_car A B := urFunctor_car F A B;
rFunctor_map A1 A2 B1 B2 fg := urFunctor_map F fg
|}.
@@ -914,13 +912,13 @@ Next Obligation.
apply urFunctor_map_compose.
Qed.
-Global Instance urFunctor_to_rFunctor_contractive {SI} (F: urFunctor SI) :
+Global Instance urFunctor_to_rFunctor_contractive `{SI: indexT} (F: urFunctor) :
urFunctorContractive F → rFunctorContractive (urFunctor_to_rFunctor F).
Proof.
intros ? A1 A2 B1 B2 n f g Hfg. apply urFunctor_map_contractive. done.
Qed.
-Program Definition urFunctor_oFunctor_compose {SI} (F1 : urFunctor SI) (F2 : oFunctor SI) : urFunctor SI := {|
+Program Definition urFunctor_oFunctor_compose `{SI: indexT} (F1 : urFunctor) (F2 : oFunctor) : urFunctor := {|
urFunctor_car A B := urFunctor_car F1 (oFunctor_car F2 B A) (oFunctor_car F2 A B);
urFunctor_map A1 A2 B1 B2 'fg :=
urFunctor_map F1 (oFunctor_map F2 (fg.2,fg.1),oFunctor_map F2 fg)
@@ -939,37 +937,37 @@ Next Obligation.
rewrite -urFunctor_map_compose. apply equiv_dist=> n. apply urFunctor_map_ne.
split=> y /=; by rewrite !oFunctor_map_compose.
Qed.
-Global Instance urFunctor_oFunctor_compose_contractive_1 {SI} (F1 : urFunctor SI) (F2 : oFunctor SI):
+Global Instance urFunctor_oFunctor_compose_contractive_1 `{SI: indexT} (F1 : urFunctor) (F2 : oFunctor):
urFunctorContractive F1 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 A2 B1 B2 n [f1 g1] [f2 g2] Hfg; simpl in *.
f_contractive; intros m Hlt; specialize (Hfg m Hlt); destruct Hfg; split; simpl in *; apply oFunctor_map_ne; by split.
Qed.
-Global Instance urFunctor_oFunctor_compose_contractive_2 {SI} (F1 : urFunctor SI) (F2 : oFunctor SI):
+Global Instance urFunctor_oFunctor_compose_contractive_2 `{SI: indexT} (F1 : urFunctor) (F2 : oFunctor):
oFunctorContractive F2 → urFunctorContractive (urFunctor_oFunctor_compose F1 F2).
Proof.
intros ? A1 A2 B1 B2 n [f1 g1] [f2 g2] Hfg; simpl in *.
f_equiv; split; simpl in *; f_contractive; intros m Hlt; specialize (Hfg m Hlt); destruct Hfg; by split.
Qed.
-Program Definition constURF {SI: indexT} (B : ucmra SI) : urFunctor SI :=
+Program Definition constURF `{SI: indexT} (B : ucmra) : urFunctor :=
{| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
Coercion constURF : ucmra >-> urFunctor.
-Global Instance constURF_contractive {SI: indexT} (B: ucmra SI) : urFunctorContractive (constURF B).
+Global Instance constURF_contractive `{SI: indexT} (B: ucmra) : urFunctorContractive (constURF B).
Proof. rewrite /urFunctorContractive; apply _. Qed.
(** * Transporting a CMRA equality *)
-Definition cmra_transport {SI: indexT} {A B : cmra SI} (H : A = B) (x : A) : B :=
+Definition cmra_transport `{SI: indexT} {A B : cmra} (H : A = B) (x : A) : B :=
eq_rect A id x _ H.
- Lemma cmra_transport_trans {SI: indexT} {A B C : cmra SI} (H1 : A = B) (H2 : B = C) x :
+ Lemma cmra_transport_trans `{SI: indexT} {A B C : cmra} (H1 : A = B) (H2 : B = C) x :
cmra_transport H2 (cmra_transport H1 x) = cmra_transport (eq_trans H1 H2) x.
Proof. by destruct H2. Qed.
Section cmra_transport.
- Context {SI: indexT} {A B : cmra SI} (H : A = B).
+ Context `{SI: indexT} {A B : cmra} (H : A = B).
Notation T := (cmra_transport H).
Global Instance cmra_transport_ne : NonExpansive T.
Proof. by intros ???; destruct H. Qed.
@@ -1009,12 +1007,12 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
Section discrete.
Local Set Default Proof Using "Type*".
- Context {SI: indexT} `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A (≡)).
+ Context `{SI: indexT} `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A (≡)).
Context (ra_mix : RAMixin A).
Existing Instances discrete_dist.
- Local Instance discrete_validN : ValidN SI A := λ α x, ✓ x.
- Definition discrete_cmra_mixin : CmraMixin SI A.
+ Local Instance discrete_validN : ValidN A := λ α x, ✓ x.
+ Definition discrete_cmra_mixin : CmraMixin A.
Proof.
destruct ra_mix; split; try done.
- intros x; split; first done. by move=> /(_ zero).
@@ -1029,8 +1027,8 @@ End discrete.
(** A smart constructor for the discrete RA over a carrier [A]. It uses
[ofe_discrete_equivalence_of A] to make sure the same [Equivalence] proof is
used as when constructing the OFE. *)
-Notation discreteR SI A ra_mix :=
- (Cmra SI A (@discrete_cmra_mixin SI A _ _ _ _ (discrete_ofe_equivalence_of SI A%type) ra_mix))
+Notation discreteR A ra_mix :=
+ (Cmra A (@discrete_cmra_mixin _ A _ _ _ _ (discrete_ofe_equivalence_of A%type) ra_mix))
(only parsing).
Section ra_total.
@@ -1061,19 +1059,19 @@ End ra_total.
(** ** CMRA for the unit type *)
Section unit.
- Variable (SI: indexT).
+ Context `{SI: indexT}.
Local Instance unit_valid : Valid unit := λ x, True.
- Local Instance unit_validN : ValidN SI unit := λ α x, True.
+ Local Instance unit_validN : ValidN unit := λ α x, True.
Local Instance unit_pcore : PCore unit := λ x, Some x.
Local Instance unit_op : Op unit := λ x y, ().
- Lemma unit_cmra_mixin : @CmraMixin SI unit (@unit_dist SI) unit_equiv _ _ _ _.
+ Lemma unit_cmra_mixin : CmraMixin unit.
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
- Canonical Structure unitR : cmra SI := Cmra SI unit unit_cmra_mixin.
+ Canonical Structure unitR : cmra := Cmra unit unit_cmra_mixin.
Instance unit_unit_instance : Unit unit := ().
- Lemma unit_ucmra_mixin : @UcmraMixin SI () (@unit_dist SI) unit_equiv _ _ _ _.
+ Lemma unit_ucmra_mixin : UcmraMixin unit.
Proof. done. Qed.
- Canonical Structure unitUR : ucmra SI := Ucmra SI unit unit_ucmra_mixin.
+ Canonical Structure unitUR : ucmra := Ucmra unit unit_ucmra_mixin.
Global Instance unit_cmra_discrete : CmraDiscrete unitR.
Proof. done. Qed.
@@ -1085,15 +1083,15 @@ End unit.
(** ** CMRA for the empty type *)
Section empty.
- Context {SI: indexT}.
+ Context `{SI: indexT}.
Local Instance Empty_set_valid_instance : Valid Empty_set := λ x, False.
- Local Instance Empty_set_validN_instance : ValidN SI Empty_set := λ n x, False.
+ Local Instance Empty_set_validN_instance : ValidN Empty_set := λ n x, False.
Local Instance Empty_set_pcore_instance : PCore Empty_set := λ x, Some x.
Local Instance Empty_set_op_instance : Op Empty_set := λ x y, x.
- Lemma Empty_set_cmra_mixin : CmraMixin SI (Empty_setO SI).
+ Lemma Empty_set_cmra_mixin : CmraMixin Empty_setO.
Proof. apply discrete_cmra_mixin, ra_total_mixin; by (intros [] || done). Qed.
- Canonical Structure Empty_setR : cmra SI := Cmra SI Empty_set Empty_set_cmra_mixin.
+ Canonical Structure Empty_setR : cmra := Cmra Empty_set Empty_set_cmra_mixin.
Global Instance Empty_set_cmra_discrete : CmraDiscrete Empty_setR.
Proof. done. Qed.
@@ -1102,11 +1100,10 @@ Section empty.
Global Instance Empty_set_cancelable (x : Empty_set) : Cancelable x.
Proof. by constructor. Qed.
End empty.
-Global Arguments Empty_setR : clear implicits.
(** ** Product *)
Section prod.
- Context {SI: indexT} {A B : cmra SI}.
+ Context `{SI: indexT} {A B : cmra}.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_/.
@@ -1115,7 +1112,7 @@ Section prod.
c1 ← pcore (x.1); c2 ← pcore (x.2); Some (c1, c2).
Local Arguments prod_pcore_instance !_ /.
Local Instance prod_valid_instance : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
- Local Instance prod_validN_instance : ValidN SI (A * B) := λ α x, ✓{α} x.1 ∧ ✓{α} x.2.
+ Local Instance prod_validN_instance : ValidN (A * B) := λ α x, ✓{α} x.1 ∧ ✓{α} x.2.
Lemma prod_pcore_Some (x cx : A * B) :
pcore x = Some cx ↔ pcore (x.1) = Some (cx.1) ∧ pcore (x.2) = Some (cx.2).
@@ -1140,7 +1137,7 @@ Section prod.
intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
Qed.
- Definition prod_cmra_mixin : CmraMixin SI (A * B).
+ Definition prod_cmra_mixin : CmraMixin (A * B).
Proof.
split; try apply _.
- by intros α x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
@@ -1169,7 +1166,7 @@ Section prod.
destruct (cmra_extend α (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
by exists (z11,z21), (z12,z22).
Qed.
- Canonical Structure prodR := Cmra SI (prod A B) prod_cmra_mixin.
+ Canonical Structure prodR := Cmra (prod A B) prod_cmra_mixin.
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
Proof. done. Qed.
@@ -1231,17 +1228,17 @@ Global Hint Extern 4 (CoreId _) =>
Global Arguments prodR {_} _ _.
Section prod_unit.
- Context {SI: indexT} {A B : ucmra SI}.
+ Context `{SI: indexT} {A B : ucmra}.
Local Instance prod_unit_instance `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
- Lemma prod_ucmra_mixin : UcmraMixin SI (A * B).
+ Lemma prod_ucmra_mixin : UcmraMixin (A * B).
Proof.
split.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- rewrite prod_pcore_Some'; split; apply (core_id _).
Qed.
- Canonical Structure prodUR := Ucmra SI (prod A B) prod_ucmra_mixin.
+ Canonical Structure prodUR := Ucmra (prod A B) prod_ucmra_mixin.
Lemma pair_split (a : A) (b : B) : (a, b) ≡ (a, ε) ⋅ (ε, b).
Proof. by rewrite -pair_op left_id right_id. Qed.
@@ -1267,7 +1264,7 @@ End prod_unit.
Global Arguments prodUR {_} _ _.
-Global Instance prod_map_cmra_morphism {SI: indexT} {A A' B B' : cmra SI} (f : A → A') (g : B → B') :
+Global Instance prod_map_cmra_morphism `{SI: indexT} {A A' B B' : cmra} (f : A → A') (g : B → B') :
CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
Proof.
split; first apply _.
@@ -1282,7 +1279,7 @@ Proof.
- intros. by rewrite /prod_map /= !cmra_morphism_op.
Qed.
-Program Definition prodRF {SI: indexT} (F1 F2 : rFunctor SI) : rFunctor SI := {|
+Program Definition prodRF `{SI: indexT} (F1 F2 : rFunctor) : rFunctor := {|
rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
rFunctor_map A1 A2 B1 B2 fg :=
prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
@@ -1297,7 +1294,7 @@ Next Obligation.
Qed.
Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
-Global Instance prodRF_contractive {SI: indexT} (F1 F2 : rFunctor SI):
+Global Instance prodRF_contractive `{SI: indexT} (F1 F2 : rFunctor):
rFunctorContractive F1 → rFunctorContractive F2 →
rFunctorContractive (prodRF F1 F2).
Proof.
@@ -1305,7 +1302,7 @@ Proof.
by apply prodO_map_ne; apply rFunctor_map_contractive.
Qed.
-Program Definition prodURF {SI} (F1 F2 : urFunctor SI) : urFunctor SI := {|
+Program Definition prodURF `{SI: indexT} (F1 F2 : urFunctor) : urFunctor := {|
urFunctor_car A B := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
urFunctor_map A1 A2 B1 B2 fg :=
prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
@@ -1320,7 +1317,7 @@ Next Obligation.
Qed.
Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
-Global Instance prodURF_contractive {SI} (F1 F2 : urFunctor SI):
+Global Instance prodURF_contractive `{SI: indexT} (F1 F2 : urFunctor):
urFunctorContractive F1 → urFunctorContractive F2 →
urFunctorContractive (prodURF F1 F2).
Proof.
@@ -1330,7 +1327,7 @@ Qed.
(** ** CMRA for the option type *)
Section option.
- Context {SI: indexT} {A : cmra SI}.
+ Context `{SI: indexT} {A : cmra}.
Implicit Types a b : A.
Implicit Types ma mb : option A.
Local Arguments core _ _ !_ /.
@@ -1338,7 +1335,7 @@ Section option.
Local Instance option_valid_instance : Valid (option A) := λ ma,
match ma with Some a => ✓ a | None => True end.
- Local Instance option_validN_instance : ValidN SI (option A) := λ α ma,
+ Local Instance option_validN_instance : ValidN (option A) := λ α ma,
match ma with Some a => ✓{α} a | None => True end.
Local Instance option_pcore_instance : PCore (option A) := λ ma, Some (ma ≫= pcore).
Local Arguments option_pcore_instance !_ /.
@@ -1347,7 +1344,7 @@ Section option.
Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
Definition Some_validN a α : ✓{α} Some a ↔ ✓{α} a := reflexivity _.
Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
- Lemma Some_core `{CmraTotal SI A} a : Some (core a) = core (Some a).
+ Lemma Some_core `{!CmraTotal A} a : Some (core a) = core (Some a).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
Lemma Some_op_opM a ma : Some a ⋅ ma = Some (a ⋅? ma).
Proof. by destruct ma. Qed.
@@ -1396,7 +1393,7 @@ Section option.
right. exists a, b. by rewrite {3}Hab.
Qed.
- Lemma option_cmra_mixin : CmraMixin SI (option A).
+ Lemma option_cmra_mixin : CmraMixin (option A).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -1428,15 +1425,15 @@ Section option.
+ by exists None, (Some a); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
- Canonical Structure optionR := Cmra SI (option A) option_cmra_mixin.
+ Canonical Structure optionR := Cmra (option A) option_cmra_mixin.
Global Instance option_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
Instance option_unit_instance : Unit (option A) := None.
- Lemma option_ucmra_mixin : UcmraMixin SI optionR.
+ Lemma option_ucmra_mixin : UcmraMixin optionR.
Proof. split; [done| |done]. by intros []. Qed.
- Canonical Structure optionUR := Ucmra SI (option A) option_ucmra_mixin.
+ Canonical Structure optionUR := Ucmra (option A) option_ucmra_mixin.
(** Misc *)
Lemma op_None ma mb : ma ⋅ mb = None ↔ ma = None ∧ mb = None.
@@ -1483,9 +1480,9 @@ Section option.
Lemma Some_included_2 a b : a ≼ b → Some a ≼ Some b.
Proof. rewrite Some_included; eauto. Qed.
- Lemma Some_includedN_total `{CmraTotal SI A} α a b : Some a ≼{α} Some b ↔ a ≼{α} b.
+ Lemma Some_includedN_total `{!CmraTotal A} α a b : Some a ≼{α} Some b ↔ a ≼{α} b.
Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
- Lemma Some_included_total `{CmraTotal SI A} a b : Some a ≼ Some b ↔ a ≼ b.
+ Lemma Some_included_total `{!CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
Proof. rewrite Some_included. split; [|by eauto]. by intros [->|?]. Qed.
Lemma Some_includedN_exclusive α a `{!Exclusive a} b :
@@ -1521,32 +1518,32 @@ Global Arguments optionR {_} _.
Global Arguments optionUR {_} _.
Section option_prod.
- Context {SI: indexT} {A B : cmra SI}.
+ Context `{SI: indexT} {A B : cmra}.
Implicit Types a : A.
Implicit Types b : B.
Lemma Some_pair_includedN α a1 a2 b1 b2 :
Some (a1,b1) ≼{α} Some (a2,b2) → Some a1 ≼{α} Some a2 ∧ Some b1 ≼{α} Some b2.
Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed.
- Lemma Some_pair_includedN_total_1 `{CmraTotal SI A} α a1 a2 b1 b2 :
+ Lemma Some_pair_includedN_total_1 `{!CmraTotal A} α a1 a2 b1 b2 :
Some (a1,b1) ≼{α} Some (a2,b2) → a1 ≼{α} a2 ∧ Some b1 ≼{α} Some b2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ a1). Qed.
- Lemma Some_pair_includedN_total_2 `{CmraTotal SI B} α a1 a2 b1 b2 :
+ Lemma Some_pair_includedN_total_2 `{!CmraTotal B} α a1 a2 b1 b2 :
Some (a1,b1) ≼{α} Some (a2,b2) → Some a1 ≼{α} Some a2 ∧ b1 ≼{α} b2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ b1). Qed.
Lemma Some_pair_included a1 a2 b1 b2 :
Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ Some b1 ≼ Some b2.
Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.
- Lemma Some_pair_included_total_1 `{CmraTotal SI A} a1 a2 b1 b2 :
+ Lemma Some_pair_included_total_1 `{!CmraTotal A} a1 a2 b1 b2 :
Some (a1,b1) ≼ Some (a2,b2) → a1 ≼ a2 ∧ Some b1 ≼ Some b2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total a1). Qed.
- Lemma Some_pair_included_total_2 `{CmraTotal SI B} a1 a2 b1 b2 :
+ Lemma Some_pair_included_total_2 `{!CmraTotal B} a1 a2 b1 b2 :
Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ b1 ≼ b2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
End option_prod.
-Lemma option_fmap_mono {SI} {A B : cmra SI} (f : A → B) ma mb :
+Lemma option_fmap_mono `{SI: indexT} {A B : cmra} (f : A → B) ma mb :
Proper ((≡) ==> (≡)) f →
(∀ a b, a ≼ b → f a ≼ f b) →
ma ≼ mb → f <$> ma ≼ f <$> mb.
@@ -1554,7 +1551,7 @@ Proof.
intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
Qed.
-Global Instance option_fmap_cmra_morphism {SI} {A B : cmra SI} (f: A → B) `{!CmraMorphism f} :
+Global Instance option_fmap_cmra_morphism `{SI: indexT} {A B : cmra} (f: A → B) `{!CmraMorphism f} :
CmraMorphism (fmap f : option A → option B).
Proof.
split; first apply _.
@@ -1563,7 +1560,7 @@ Proof.
- move=> [a|] [b|] //=. by rewrite (cmra_morphism_op f).
Qed.
-Program Definition optionURF {SI} (F : rFunctor SI) : urFunctor SI := {|
+Program Definition optionURF `{SI: indexT} (F : rFunctor) : urFunctor := {|
urFunctor_car A B := optionUR (rFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := optionO_map (rFunctor_map F fg)
|}.
@@ -1579,31 +1576,31 @@ Next Obligation.
apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
Qed.
-Global Instance optionURF_contractive {SI} (F : rFunctor SI):
+Global Instance optionURF_contractive `{SI: indexT} (F : rFunctor):
rFunctorContractive F → urFunctorContractive (optionURF F).
Proof.
by intros ? A1 A2 B1 B2 α f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
Qed.
-Program Definition optionRF {SI} (F : rFunctor SI) : rFunctor SI := {|
+Program Definition optionRF `{SI: indexT} (F : rFunctor) : rFunctor := {|
rFunctor_car A B := optionR (rFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := optionO_map (rFunctor_map F fg)
|}.
Solve Obligations with (intros; apply optionURF).
-Global Instance optionRF_contractive {SI} (F: rFunctor SI) :
+Global Instance optionRF_contractive `{SI: indexT} (F: rFunctor) :
rFunctorContractive F → rFunctorContractive (optionRF F).
Proof. apply optionURF_contractive. Qed.
(* Dependently-typed functions over a discrete domain *)
Section discrete_fun_cmra.
- Context {SI: indexT} `{B : A → ucmra SI}.
+ Context `{SI: indexT} `{B : A → ucmra}.
Implicit Types f g : discrete_fun B.
Local Instance discrete_fun_op_instance : Op (discrete_fun B) := λ f g x, f x ⋅ g x.
Local Instance discrete_fun_pcore_instance : PCore (discrete_fun B) := λ f, Some (λ x, core (f x)).
Local Instance discrete_fun_valid_instance : Valid (discrete_fun B) := λ f, ∀ x, ✓ f x.
- Local Instance discrete_fun_validN_instance : ValidN SI (discrete_fun B) := λ α f, ∀ x, ✓{α} f x.
+ Local Instance discrete_fun_validN_instance : ValidN (discrete_fun B) := λ α f, ∀ x, ✓{α} f x.
Definition discrete_fun_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
Definition discrete_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
@@ -1617,7 +1614,7 @@ Section discrete_fun_cmra.
intros [h ?]%finite_choice; by exists h.
Qed.
- Lemma discrete_fun_cmra_mixin : CmraMixin SI (discrete_fun B).
+ Lemma discrete_fun_cmra_mixin : CmraMixin (discrete_fun B).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -1643,19 +1640,19 @@ Section discrete_fun_cmra.
split; [|split]=>x; [rewrite discrete_fun_lookup_op| |];
by destruct (FUN x) as (?&?&?&?&?).
Qed.
- Canonical Structure discrete_funR := Cmra SI (discrete_fun B) discrete_fun_cmra_mixin.
+ Canonical Structure discrete_funR := Cmra (discrete_fun B) discrete_fun_cmra_mixin.
Instance discrete_fun_unit_instance : Unit (discrete_fun B) := λ x, ε.
Definition discrete_fun_lookup_empty x : ε x = ε := eq_refl.
- Lemma discrete_fun_ucmra_mixin : UcmraMixin SI (discrete_fun B).
+ Lemma discrete_fun_ucmra_mixin : UcmraMixin (discrete_fun B).
Proof.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite discrete_fun_lookup_op left_id.
- constructor=> x. apply core_id_core, _.
Qed.
- Canonical Structure discrete_funUR := Ucmra SI (discrete_fun B) discrete_fun_ucmra_mixin.
+ Canonical Structure discrete_funUR := Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.
Global Instance discrete_fun_unit_discrete :
(∀ i, Discrete (ε : B i)) → Discrete (ε : discrete_fun B).
@@ -1665,7 +1662,7 @@ End discrete_fun_cmra.
Global Arguments discrete_funR {_ _} _.
Global Arguments discrete_funUR {_ _} _.
-Global Instance discrete_fun_map_cmra_morphism {SI A} {B1 B2 : A → ucmra SI} (f : ∀ x, B1 x → B2 x) :
+Global Instance discrete_fun_map_cmra_morphism `{SI: indexT} {A} {B1 B2 : A → ucmra} (f : ∀ x, B1 x → B2 x) :
(∀ x, CmraMorphism (f x)) → CmraMorphism (discrete_fun_map f).
Proof.
split; first apply _.
@@ -1674,7 +1671,7 @@ Proof.
- intros g1 g2 i. by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
Qed.
-Program Definition discrete_funURF {SI C} (F : C → urFunctor SI) : urFunctor SI := {|
+Program Definition discrete_funURF `{SI: indexT} {C} (F : C → urFunctor) : urFunctor := {|
urFunctor_car A B := discrete_funUR (λ c, urFunctor_car (F c) A B);
urFunctor_map A1 A2 B1 B2 fg := discrete_funO_map (λ c, urFunctor_map (F c) fg)
|}.
@@ -1689,7 +1686,7 @@ Next Obligation.
intros SI C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
apply discrete_fun_map_ext=>y; apply urFunctor_map_compose.
Qed.
-Instance discrete_funURF_contractive {SI C} (F : C → urFunctor SI) :
+Global Instance discrete_funURF_contractive `{SI: indexT} {C} (F : C → urFunctor) :
(∀ c, urFunctorContractive (F c)) → urFunctorContractive (discrete_funURF F).
Proof.
intros ? A1 A2 B1 B2 α ?? g.
@@ -1698,8 +1695,8 @@ Qed.
(** * Constructing a camera [B] through a bijection with [A] that
is mostly an isomorphism but restricts validity. *)
-Lemma iso_cmra_mixin_restrict {SI} {A : cmra SI} {B : Type}
- `{!Dist SI B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN SI B}
+Lemma iso_cmra_mixin_restrict `{SI: indexT} {A : cmra} {B : Type}
+ `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
(f : A → B) (g : B → A)
(* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
(g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
@@ -1716,7 +1713,7 @@ Lemma iso_cmra_mixin_restrict {SI} {A : cmra SI} {B : Type}
(valid_rvalidN : ∀ y : B, ✓ y ↔ ∀ n, ✓{n} y)
(validN_le: ∀ n m (y : B), ✓{n} y → m ⪯ n → ✓{m} y)
(validN_op_l : ∀ n (y1 y2 : B), ✓{n} (y1 ⋅ y2) → ✓{n} y1) :
- CmraMixin SI B.
+ CmraMixin B.
Proof.
split.
- intros y n z1 z2 Hz%g_dist. apply g_dist. by rewrite !g_op Hz.
@@ -1756,8 +1753,8 @@ Proof.
Qed.
(** * Constructing a camera through an isomorphism *)
-Lemma iso_cmra_mixin {SI} {A : cmra SI} {B : Type}
- `{!Dist SI B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN SI B}
+Lemma iso_cmra_mixin `{SI: indexT} {A : cmra} {B : Type}
+ `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
(f : A → B) (g : B → A)
(* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
(g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
@@ -1769,7 +1766,7 @@ Lemma iso_cmra_mixin {SI} {A : cmra SI} {B : Type}
(g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
(g_valid : ∀ y, ✓ (g y) ↔ ✓ y)
(g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
- CmraMixin SI B.
+ CmraMixin B.
Proof.
apply (iso_cmra_mixin_restrict f g); auto.
- by intros n y ?%g_validN.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index eb08dc95..7c75f239 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -3,14 +3,14 @@ From iris.algebra Require Export big_op cmra.
From iris.prelude Require Import options.
(** Option *)
-Lemma big_opL_None {SI} {M : cmra SI} {A} (f : nat → A → option M) l :
+Lemma big_opL_None `{SI: indexT} {M : cmra} {A} (f : nat → A → option M) l :
([^op list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
Proof.
revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
- intros [??] [|k] y ?; naive_solver.
- intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
Qed.
-Lemma big_opM_None {SI} {M : cmra SI} `{Countable K} {A} (f : K → A → option M) m :
+Lemma big_opM_None `{SI: indexT} {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
Proof.
induction m as [|i x m ? IH] using map_ind=> /=.
@@ -21,13 +21,13 @@ Proof.
- apply (Hm i). by simplify_map_eq.
- intros k y ?. apply (Hm k). by simplify_map_eq.
Qed.
-Lemma big_opS_None {SI} {M : cmra SI} `{Countable A} (f : A → option M) X :
+Lemma big_opS_None `{SI: indexT} {M : cmra} `{Countable A} (f : A → option M) X :
([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
Proof.
induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
Qed.
-Lemma big_opMS_None {SI} {M : cmra SI} `{Countable A} (f : A → option M) X :
+Lemma big_opMS_None `{SI: indexT} {M : cmra} `{Countable A} (f : A → option M) X :
([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
Proof.
induction X as [|x X IH] using gmultiset_ind.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 2bb7c7e0..44df8a4b 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -7,17 +7,17 @@ Require Coq.Logic.ProofIrrelevance.
Section cofe.
Context (SI : indexT).
(* Shorthand notation to avoid making a distinction between Cofes and ofes *)
- Definition COFE := { C : ofe SI & Cofe C }.
- Global Coercion projCOFE (C: COFE) : ofe SI := (projT1 C).
+ Definition COFE := { C : ofe & Cofe C }.
+ Global Coercion projCOFE (C: COFE) : ofe := (projT1 C).
Global Instance COFE_cofe (C: COFE) : Cofe C := projT2 C.
- Definition cofe (A: ofe SI) `{C: Cofe SI A} := existT A C.
+ Definition cofe (A: ofe) `{C: !Cofe A} := existT A C.
End cofe.
Definition proj_id {SI} {A B : COFE SI} (Heq : A = B) : projCOFE _ A = projCOFE _ B.
Proof. by rewrite Heq. Qed.
(* non-expansive maps commute with bounded limits only in a restricted way *)
-Lemma bounded_ne_bcompl {SI : indexT} {A B : ofe SI} {Hc : Cofe A} {Hb : Cofe B} (f : A -n> B):
+Lemma bounded_ne_bcompl `{SI : indexT} {A B : ofe} {Hc : Cofe A} {Hb : Cofe B} (f : A -n> B):
∀ β (c : bchain _ β) Hβ γ (Hγ : γ ≺ β), f (bcompl Hβ c) ≡{γ}≡ bcompl Hβ (bchain_map f c).
Proof.
intros β c Hβ γ Hγ.
@@ -27,8 +27,8 @@ Proof.
- rewrite conv_bcompl /bchain_map. cbn. reflexivity.
Qed.
-Record solution {SI} (F : oFunctor SI) := Solution {
- solution_car :> ofe SI;
+Record solution `{SI: indexT} (F : oFunctor) := Solution {
+ solution_car :> ofe;
solution_cofe : Cofe solution_car;
solution_unfold : solution_car -n> F solution_car;
solution_fold : F solution_car -n> solution_car;
@@ -38,18 +38,18 @@ Record solution {SI} (F : oFunctor SI) := Solution {
Arguments solution_unfold {_} _.
Arguments solution_fold {_} _.
-Existing Instance solution_cofe.
+Global Existing Instance solution_cofe.
Module solver. Section solver.
-Context (SI : indexT) (F : oFunctor SI) `{Fcontr : oFunctorContractive SI F}.
-Context `{Fcofe : ∀ (T1 T2 : ofe SI), Cofe (oFunctor_car F T1 T2)}.
-Context `{Ftrunc : ∀ (T1 T2 : ofe SI), Truncatable (oFunctor_car F T1 T2)}.
-Context `{Funique : ∀ (T1 T2 : ofe SI), BcomplUniqueLim (oFunctor_car F T1 T2)}.
+Context `{SI : indexT} (F : oFunctor) `{Fcontr : !oFunctorContractive F}.
+Context `{Fcofe : !∀ (T1 T2 : ofe), Cofe (oFunctor_car F T1 T2)}.
+Context `{Ftrunc : !∀ (T1 T2 : ofe), Truncatable (oFunctor_car F T1 T2)}.
+Context `{Funique : !∀ (T1 T2 : ofe), BcomplUniqueLim (oFunctor_car F T1 T2)}.
Notation map := (oFunctor_map F).
-Context (inh_Funit : F (unitO SI)).
+Context (inh_Funit : F (unitO)).
(* a version of the functor which directly integrates the Cofe instance *)
-Definition G (A: ofe SI): COFE SI := cofe SI (F A).
+Definition G (A: ofe): COFE SI := cofe SI (F A).
(** We are using proof irrelevance very much.
Currently, that doesn't matter much, however, as we need PE for a different reason anyways.
@@ -60,14 +60,14 @@ Import ProofIrrelevance.
Local Instance all_ProofIrrel (A : Prop) : ProofIrrel A.
Proof. intros a b. apply proof_irrelevance. Qed.
-Lemma map_compose {A1 A2 A3 B1 B2 B3 : ofe SI}
+Lemma map_compose {A1 A2 A3 B1 B2 B3 : ofe}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) :
map (g, g') ◎ map (f, f') ≡ map (f ◎ g, g' ◎ f').
Proof. intros x. cbn. by setoid_rewrite <- oFunctor_map_compose. Qed.
(* Specialized version so that for dist (in principle, the previous lemma can be used,
but this one is cheaper for rewriting due to TC inference *)
-Lemma map_compose_dist {A1 A2 A3 B1 B2 B3 : ofe SI}
+Lemma map_compose_dist {A1 A2 A3 B1 B2 B3 : ofe}
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) α:
map (g, g') ◎ map (f, f') ≡{α}≡ map (f ◎ g, g' ◎ f').
Proof. apply equiv_dist, map_compose. Qed.
@@ -89,9 +89,9 @@ Ltac map_compose_tac :=
Instance map_proper A1 A2 B1 B2: Proper (equiv ==> equiv) (@oFunctor_map _ F A1 A2 B1 B2).
Proof using Fcontr. by intros ?? ->. Qed.
-Instance ccompose_proper (A B C : ofe SI) : Proper (equiv ==> equiv ==> equiv) (@ccompose _ A B C).
+Instance ccompose_proper (A B C : ofe) : Proper (equiv ==> equiv ==> equiv) (@ccompose _ A B C).
Proof. apply ne_proper_2. apply _. Qed.
-Instance ccompose_proper' (A B C : ofe SI) n : Proper (dist n ==> dist n ==> dist n) (@ccompose _ A B C).
+Instance ccompose_proper' (A B C : ofe) n : Proper (dist n ==> dist n ==> dist n) (@ccompose _ A B C).
Proof. apply _. Qed.
@@ -125,7 +125,7 @@ Ltac merge_truncs :=
(** a typeclass for registering equalities between OFEs, used for the transport infrastructure *)
(* most of the times, we give instances explicitly (as transitivity and symmetry would make life hard for TC inference), but having it as a typeclass is still sensible for a few uses *)
-Class ofe_eq (X Y : ofe SI) := ofe_equal : X = Y.
+Class ofe_eq (X Y : ofe) := ofe_equal : X = Y.
Hint Mode ofe_eq + + : typeclass_instances.
Arguments ofe_eq : simpl never.
@@ -138,7 +138,7 @@ Lemma ofe_eq_symm {X Y} (H : ofe_eq X Y) : ofe_eq Y X.
Proof. intros. by rewrite H. Qed.
Lemma ofe_eq_trans {X Y Z} (H1 : ofe_eq X Y) (H2 : ofe_eq Y Z) : ofe_eq X Z.
Proof. intros. by rewrite H1 H2. Qed.
-Lemma ofe_eq_funct {X Y : ofe SI} {α α'} (Heq : α = α') (H : ofe_eq X Y) :
+Lemma ofe_eq_funct {X Y : ofe} {α α'} (Heq : α = α') (H : ofe_eq X Y) :
ofe_eq ([G X]_{α}) ([G Y]_{α'}).
Proof. by rewrite H Heq. Qed.
@@ -146,7 +146,7 @@ Proof. by rewrite H Heq. Qed.
Hint Resolve ofe_eq_funct : ofe_eq.
-Program Definition transport_id (X Y : ofe SI) {H : ofe_eq X Y} : X -n> Y := λne x, _ .
+Program Definition transport_id (X Y : ofe) {H : ofe_eq X Y} : X -n> Y := λne x, _ .
Next Obligation. intros X Y Heq x. rewrite <- Heq. exact x. Defined.
Next Obligation. intros. intros x y H1. destruct H. apply H1. Defined.
Arguments transport_id : simpl never.
@@ -155,22 +155,22 @@ Arguments transport_id : simpl never.
the category of OFEs with transport_id arrows is thin if assuming proof irrelevance. Thus checking if
any two transports are equal reduces to type-checking.
*)
-Lemma transport_id_compose (X Y Z : ofe SI) {Heq1 : ofe_eq X Y} {Heq2 : ofe_eq Y Z} :
+Lemma transport_id_compose (X Y Z : ofe) {Heq1 : ofe_eq X Y} {Heq2 : ofe_eq Y Z} :
transport_id Y Z ◎ transport_id X Y ≡ @transport_id X Z (ofe_eq_trans Heq1 Heq2).
Proof.
intros x; cbn. destruct Heq1, Heq2.
by rewrite (proof_irrel (ofe_eq_trans eq_refl eq_refl) eq_refl ).
Qed.
-Lemma transport_id_identity (X : ofe SI) {Heq : ofe_eq X X} : @transport_id X X Heq ≡ cid.
+Lemma transport_id_identity (X : ofe) {Heq : ofe_eq X X} : @transport_id X X Heq ≡ cid.
Proof. intros x; cbn. by rewrite (proof_irrel Heq eq_refl). Qed.
-Lemma transport_id_pi (X Y : ofe SI) {Heq1 : ofe_eq X Y} {Heq2 : ofe_eq X Y}:
+Lemma transport_id_pi (X Y : ofe) {Heq1 : ofe_eq X Y} {Heq2 : ofe_eq X Y}:
@transport_id X Y Heq1 ≡ @transport_id X Y Heq2.
Proof. by rewrite (proof_irrel Heq1 Heq2). Qed.
(* commutation of transports with truncation/expansion *)
-Lemma transport_id_truncate (Y Z : ofe SI) γ γ' (Heq : γ = γ') I:
+Lemma transport_id_truncate (Y Z : ofe) γ γ' (Heq : γ = γ') I:
@transport_id ([G Z]_{γ}) ([G Y]_{γ'}) (ofe_eq_funct Heq I) ◎ ofe_trunc_truncate γ
≡ ofe_trunc_truncate γ' ◎ map (@transport_id Y Z (ofe_eq_symm I), transport_id Z Y).
Proof using Fcontr.
@@ -178,7 +178,7 @@ Proof using Fcontr.
intros x; cbn. by rewrite oFunctor_map_id.
Qed.
-Lemma transport_id_truncate_symm (Y Z : ofe SI) γ γ' (Heq : γ = γ') (I : ofe_eq Y Z):
+Lemma transport_id_truncate_symm (Y Z : ofe) γ γ' (Heq : γ = γ') (I : ofe_eq Y Z):
@transport_id ([G Z]_{γ}) ([G Y]_{γ'}) (ofe_eq_funct Heq (ofe_eq_symm I)) ◎ ofe_trunc_truncate γ
≡ ofe_trunc_truncate γ' ◎ map (@transport_id Y Z I, @transport_id Z Y (ofe_eq_symm I)).
Proof using Fcontr.
@@ -186,7 +186,7 @@ Proof using Fcontr.
intros x; cbn. by rewrite oFunctor_map_id.
Qed.
-Lemma transport_id_truncate' (Y Z : ofe SI) γ γ' (Heq : γ = γ') I0 I1 I2:
+Lemma transport_id_truncate' (Y Z : ofe) γ γ' (Heq : γ = γ') I0 I1 I2:
@transport_id ([G Z]_{γ}) ([G Y]_{γ'}) I0 ◎ ofe_trunc_truncate γ
≡ ofe_trunc_truncate γ' ◎ map (@transport_id Y Z I1, @transport_id Z Y I2).
Proof using Fcontr.
@@ -195,7 +195,7 @@ Proof using Fcontr.
subst. apply transport_id_truncate.
Qed.
-Lemma transport_id_expand (Y Z : ofe SI) γ γ' (Heq : γ' = γ) I:
+Lemma transport_id_expand (Y Z : ofe) γ γ' (Heq : γ' = γ) I:
map(@transport_id Y Z (ofe_eq_symm I), transport_id Z Y) ◎ ofe_trunc_expand γ'
≡ ofe_trunc_expand γ ◎ @transport_id ([G Z]_{γ'}) ([G Y]_{γ}) (ofe_eq_funct Heq I).
Proof using Fcontr.
@@ -203,7 +203,7 @@ Proof using Fcontr.
intros x; cbn. by rewrite oFunctor_map_id.
Qed.
-Lemma transport_id_expand_symm (Y Z : ofe SI) γ γ' (Heq : γ' = γ) (I : ofe_eq Y Z):
+Lemma transport_id_expand_symm (Y Z : ofe) γ γ' (Heq : γ' = γ) (I : ofe_eq Y Z):
map(@transport_id Y Z I, @transport_id Z Y (ofe_eq_symm I)) ◎ ofe_trunc_expand γ'
≡ ofe_trunc_expand γ ◎ @transport_id ([G Z]_{γ'}) ([G Y]_{γ}) (ofe_eq_funct Heq (ofe_eq_symm I)).
Proof using Fcontr.
@@ -211,7 +211,7 @@ Proof using Fcontr.
intros x; cbn. by rewrite oFunctor_map_id.
Qed.
-Lemma transport_id_expand' (Y Z : ofe SI) γ γ' (Heq : γ' = γ) I0 I1 I2:
+Lemma transport_id_expand' (Y Z : ofe) γ γ' (Heq : γ' = γ) I0 I1 I2:
map(@transport_id Y Z I1, @transport_id Z Y I2) ◎ ofe_trunc_expand γ'
≡ ofe_trunc_expand γ ◎ @transport_id ([G Z]_{γ'}) ([G Y]_{γ}) I0.
Proof using Fcontr.
@@ -367,8 +367,8 @@ Ltac clear_transports := compose_transports; clear_id_transports; cbn -[trunc_ma
(* shortcut definition for the often-used fold/unfold pattern *)
-Definition unfold_transport {Y Z: ofe SI} (Heq : ofe_eq Y Z) := transport_id Y Z.
-Definition fold_transport {Y Z : ofe SI} (Heq : ofe_eq Y Z) := @transport_id Z Y (ofe_eq_symm Heq).
+Definition unfold_transport {Y Z: ofe} (Heq : ofe_eq Y Z) := transport_id Y Z.
+Definition fold_transport {Y Z : ofe} (Heq : ofe_eq Y Z) := @transport_id Z Y (ofe_eq_symm Heq).
(** casts between OFEs commute with bcompl *)
(*the COFEs really need to be equal so that the limits are also equal *)
@@ -384,7 +384,7 @@ Qed.
(** A record for the inductive hypothesis.
Parameterised by a predicate P (instead of an ordinal β and specialising to the predicate ⪯ β) as we have different instantiations (with ≺ β and True) for the two limit cases.
*)
-Record is_bounded_approx {P : SI -> Prop} {X : ∀ α, P α → COFE SI}
+Record is_bounded_approx {P : index -> Prop} {X : ∀ α, P α → COFE SI}
{e : ∀ α₁ α₂ (Hα₁ : P α₁) (Hα₂ : P α₂), α₁ ≺ α₂ → X α₁ Hα₁ -n> X α₂ Hα₂}
{p : ∀ α₁ α₂ (Hα₁ : P α₁) (Hα₂ : P α₂), α₁ ≺ α₂ → X α₂ Hα₂ -n> X α₁ Hα₁}
{ϕ : ∀ α (Hα : P α), X α Hα -n> [G (X α Hα)]_{succ α}}
@@ -431,7 +431,7 @@ Record is_bounded_approx {P : SI -> Prop} {X : ∀ α, P α → COFE SI}
}.
Arguments is_bounded_approx {_} _ _ _ _ _.
-Record bounded_approx {P : SI → Prop} := mk_bounded_approx
+Record bounded_approx {P : index → Prop} := mk_bounded_approx
{
bounded_approx_X : ∀ α, P α → COFE SI;
bounded_approx_e : ∀ α₁ α₂ (Hα₁ : P α₁) (Hα₂ : P α₂), α₁ ≺ α₂ → bounded_approx_X α₁ Hα₁ -n> bounded_approx_X α₂ Hα₂;
@@ -463,7 +463,7 @@ Arguments bounded_approx _ : clear implicits.
We implement this by requiring actual Leibniz equality between the OFEs and wrapping this equality in fold_transport, unfold_transport for easier handling.
That way, we can use the type cast like isomorphisms (without nasty eq_rect stuff), but can still prove properties using the information that the transports are just typecasts.
*)
-Inductive approx_agree {P0 P1 : SI → Prop} {A0 : bounded_approx P0} {A1 : bounded_approx P1} : Type :=
+Inductive approx_agree {P0 P1 : index → Prop} {A0 : bounded_approx P0} {A1 : bounded_approx P1} : Type :=
{
agree_eq : ∀ γ (H0 : P0 γ) (H1 : P1 γ), projCOFE _ (bounded_approx_X A0 γ H0) = projCOFE _ (bounded_approx_X A1 γ H1);
@@ -524,7 +524,7 @@ Qed.
thus A0 and A2 can only agree on P0 ∧ P1 ∧ P2.
This is captured by the requirement P0 → P2 → P1
*)
-Lemma approx_agree_transitive (P0 P1 P2 : SI → Prop) A0 A1 A2: (∀ γ, P0 γ → P2 γ → P1 γ)
+Lemma approx_agree_transitive (P0 P1 P2 : index → Prop) A0 A1 A2: (∀ γ, P0 γ → P2 γ → P1 γ)
→ @approx_agree P0 P1 A0 A1 → @approx_agree P1 P2 A1 A2 → @approx_agree P0 P2 A0 A2.
Proof with (intros x; cbn; unfold fold_transport, unfold_transport; clear_transports; equalise_pi).
intros Hs Hag0 Hag1.
@@ -545,7 +545,7 @@ Proof with (intros x; cbn; unfold fold_transport, unfold_transport; clear_transp
rewrite (agree_ψ_nat Hag1 _ _ _)...
Qed.
-Lemma bounded_approx_eq {P : SI → Prop} (A : bounded_approx P) α Hα Hsα :
+Lemma bounded_approx_eq {P : index → Prop} (A : bounded_approx P) α Hα Hsα :
projCOFE _ (bounded_approx_X A (succ α) Hsα) = [G (bounded_approx_X A α Hα)]_{succ α}.
Proof. eapply approx_eq, A. Defined.
@@ -556,7 +556,7 @@ Fact agree_transport_functorial P0 P1 P2 (A0 : bounded_approx P0) (A1 : bounded_
Proof. rewrite transport_id_compose. apply transport_id_pi. Qed.
(** * One-step Extensions *)
-Record extension {γ : SI} {A : bounded_approx (λ γ', γ' ≺ γ)} :=
+Record extension {γ : index} {A : bounded_approx (λ γ', γ' ≺ γ)} :=
{
ext_Xγ : COFE SI;
ext_eγ : ∀ γ0 (Hγ0 : γ0 ≺ γ), bounded_approx_X A γ0 Hγ0 -n> ext_Xγ;
@@ -660,7 +660,7 @@ Proof with (unfold fold_transport, unfold_transport; intros x; cbn; clear_transp
Qed.
(** * Base case *)
-Lemma zero_e_p (α₁ α₂ : SI) : α₁ ⪯ zero → α₂ ⪯ zero → α₁ ≺ α₂ → False.
+Lemma zero_e_p (α₁ α₂ : index) : α₁ ⪯ zero → α₂ ⪯ zero → α₁ ≺ α₂ → False.
Proof.
intros Hα₁ Hα₂ Hlt.
destruct Hα₁ as [ -> | H%index_lt_zero_is_normal]; [ | easy].
@@ -673,7 +673,7 @@ Qed.
Notation "'[' f ']^{' a '}_{' b '}'" := (trunc_map a b f).
Section base_case.
- Let X0' : COFE SI := cofe _ (unitO SI).
+ Let X0' : COFE SI := cofe _ (unitO).
Let X0 : COFE SI := cofe _ ([ G X0']_{zero}).
Let ϕ0' : X0' -n> X0 := λne _, ⌊inh_Funit⌋_{zero}.
@@ -741,7 +741,7 @@ Ltac autorew :=
(** * Successor case *)
Section succ_case_X.
- Context (β : SI).
+ Context (β : index).
Context (IH : @bounded_approx (λ γ, γ ≺ succ β)).
Let X := bounded_approx_X IH.
@@ -818,7 +818,7 @@ Section succ_case_X.
Definition sψ' : [G sX']_{succ (succ β)} -n> sX' :=
trunc_map (succ (succ β)) (succ β) (map (ϕ β β_refl, ψ β β_refl)).
- Lemma dist_later_succ (A : ofe SI) (x y : A) γ : dist_later (succ γ) x y ↔ x ≡{γ}≡ y.
+ Lemma dist_later_succ (A : ofe) (x y : A) γ : dist_later (succ γ) x y ↔ x ≡{γ}≡ y.
Proof.
split; intros Hd.
- eauto with index.
@@ -1067,12 +1067,12 @@ Qed.
(* this is needed for the limit case construction *)
Section inverse_limit.
(* for every index γ satisfying P, we have an OFE X_γ *)
- Context {P : SI → Prop}.
- Context (X : ∀ β, P β → ofe SI).
+ Context {P : index → Prop}.
+ Context (X : ∀ β, P β → ofe).
- Definition btowerO : ofe SI := discrete_funO (λ β: SI, discrete_funO (λ (H : P β), X β H)).
+ Definition btowerO : ofe := discrete_funO (λ β: index, discrete_funO (λ (H : P β), X β H)).
- Program Definition proj_tower (β :SI) (Hβ : P β) := λne (t : btowerO), t β Hβ.
+ Program Definition proj_tower (β :index) (Hβ : P β) := λne (t : btowerO), t β Hβ.
Next Obligation.
intros β Hβ α' x y Heq. unfold btowerO in *. apply Heq.
Qed.
@@ -1123,7 +1123,7 @@ Section inv_lim_extensional.
Import Coq.Logic.PropExtensionality.
Import Coq.Logic.FunctionalExtensionality.
- Lemma sigO_extensional (A : ofe SI) (P1 P2 : A → Prop) : (∀ x, P1 x ↔ P2 x) → sigO P1 = sigO P2.
+ Lemma sigO_extensional (A : ofe) (P1 P2 : A → Prop) : (∀ x, P1 x ↔ P2 x) → sigO P1 = sigO P2.
Proof.
intros Hext. unfold sigO.
assert (P1 = P2).
@@ -1132,7 +1132,7 @@ Section inv_lim_extensional.
Defined.
Context
- {P : SI → Prop} (X1 X2 : ∀ β, P β → ofe SI)
+ {P : index → Prop} (X1 X2 : ∀ β, P β → ofe)
(p1 : ∀ γ γ' Hγ Hγ' (Hlt : γ ≺ γ'), X1 γ' Hγ' -n> X1 γ Hγ)
(p2 : ∀ γ γ' Hγ Hγ' (Hlt : γ ≺ γ'), X2 γ' Hγ' -n> X2 γ Hγ)
(Heq : ∀ γ Hγ, X1 γ Hγ = X2 γ Hγ).
@@ -1177,10 +1177,10 @@ Section inv_lim_extensional.
set (e := y p1 Heq Hmorph). generalize e. clear e y.
(* we need to prove that the two predicates we instantiate sigO with are the same *)
assert ((λ f : btowerO X2,
- ∀ (γ0 γ1 : SI) (Hγ0γ1 : γ0 ≺ γ1) (Hγ0 : P γ0) (Hγ1 : P γ1),
+ ∀ (γ0 γ1 : index) (Hγ0γ1 : γ0 ≺ γ1) (Hγ0 : P γ0) (Hγ1 : P γ1),
p1 γ0 γ1 Hγ0 Hγ1 Hγ0γ1 (f γ1 Hγ1) ≡ f γ0 Hγ0)
= (λ f : btowerO X2,
- ∀ (γ0 γ1 : SI) (Hγ0γ1 : γ0 ≺ γ1) (Hγ0 : P γ0) (Hγ1 : P γ1),
+ ∀ (γ0 γ1 : index) (Hγ0γ1 : γ0 ≺ γ1) (Hγ0 : P γ0) (Hγ1 : P γ1),
p2 γ0 γ1 Hγ0 Hγ1 Hγ0γ1 (f γ1 Hγ1) ≡ f γ0 Hγ0)).
{
apply functional_extensionality_dep; intros.
@@ -1213,17 +1213,17 @@ End inv_lim_extensional.
Section limit_case.
(* We assume an already merged approximation.
Later on, when we combine the cases, we use the above merged_agree lemma + transitivity of approx_agree to show that the new approximation we define in the limit case agrees with the original, unmerged approximations*)
- Context (β : limit_idx SI) (IH : @bounded_approx (λ γ, γ ≺ β)).
+ Context (β : limit_idx) (IH : @bounded_approx (λ γ, γ ≺ β)).
Let X α (H: α ≺ β) := bounded_approx_X IH α H.
Let e := bounded_approx_e IH.
Let p := bounded_approx_p IH.
(* we apply the functor F to every Xα and then truncate at α -- thus FX α is equal to X (α + 1) *)
- Definition FX : ∀ α, α ≺ β → ofe SI := λ α Hα, [G (X α Hα)]_{succ α}.
+ Definition FX : ∀ α, α ≺ β → ofe := λ α Hα, [G (X α Hα)]_{succ α}.
Instance FX_cofe α Hα : Cofe (FX α Hα) := _.
- Instance lX_truncated (α: SI) Hlt : OfeTruncated (X α Hlt) α.
+ Instance lX_truncated (α: index) Hlt : OfeTruncated (X α Hlt) α.
Proof. eapply approx_X_truncated, IH. Qed.
Instance Xeq α Hlt Hslt : ofe_eq (X (succ α) Hslt) (FX α Hlt).
Proof. eapply approx_eq, IH. Defined.
@@ -1611,7 +1611,7 @@ Section limit_case.
destruct x as [x Hx], y as [y Hy].
cbn. specialize (Heq γ Hγ).
cbn in Heq. rewrite ofe_truncated_dist. rewrite index_min_r.
- 2: { transitivity (β : SI); eauto with index. }
+ 2: { transitivity (β : index); eauto with index. }
eapply dist_mono; [apply Heq | by apply limit_index_is_limit, Hγ].
- intros Heq γ Hγ. eapply dist_mono'; first apply (Heq γ). auto.
Qed.
@@ -1658,7 +1658,7 @@ Section limit_case.
reflexivity.
}
setoid_rewrite (ofe_trunc_truncate_expand_id _) at 1. cbn.
- change x with ((λ (γ : SI) (Hγ : γ ≺ β), x) γ' Hγ') at 1.
+ change x with ((λ (γ : index) (Hγ : γ ≺ β), x) γ' Hγ') at 1.
reflexivity.
}
rewrite bcompl_bchain_const; auto.
@@ -1791,7 +1791,7 @@ Section limit_case.
End limit_case.
Section limit_coherent.
- Context (β : limit_idx SI) (A0 A1 : bounded_approx (λ γ, γ ≺ β)) (H : approx_agree A0 A1).
+ Context (β : limit_idx) (A0 A1 : bounded_approx (λ γ, γ ≺ β)) (H : approx_agree A0 A1).
Lemma FX_eq γ Hγ: FX β A0 γ Hγ = FX β A1 γ Hγ.
Proof using H. unfold FX. by rewrite (agree_eq H _ _ _). Qed.
@@ -2248,7 +2248,7 @@ End final_limit.
(** * Mergin an extension to an approximation *)
Section merge_extension.
- Context (β: SI).
+ Context (β: index).
Context (A : bounded_approx (λ γ, γ ≺ β)).
Context (E : extension A).
@@ -2824,7 +2824,7 @@ Section merge_extension.
Lemma extended_approx_agree : approx_agree A extended_approx.
Proof.
- assert (Heq : ∀ (γ : SI) (H0 : γ ≺ β) (H1 : γ ⪯ β), bounded_approx_X A γ H0 = bounded_approx_X extended_approx γ H1).
+ assert (Heq : ∀ (γ : index) (H0 : γ ≺ β) (H1 : γ ⪯ β), bounded_approx_X A γ H0 = bounded_approx_X extended_approx γ H1).
{ intros. cbn. unfold X'. destruct le_lt_eq_dec as [H2 | H2]; first by pi_clear.
subst; index_contra_solve.
}
@@ -2854,7 +2854,7 @@ Lemma extension_coherent β (A0 A1 : bounded_approx (λ γ, γ ≺ β))
→ approx_agree (extended_approx β A0 E0 succ_or_limit) (extended_approx β A1 E1 succ_or_limit).
Proof with (unfold fold_transport, unfold_transport; intros x; cbn; clear_transports; equalise_pi).
intros H Hag.
- unshelve refine ( let X_eq : ∀ (γ : SI) (H0 H1 : γ ⪯ β), projCOFE _ (X' β A0 E0 γ H0) = projCOFE _ (X' β A1 E1 γ H1) := _ in _).
+ unshelve refine ( let X_eq : ∀ (γ : index) (H0 H1 : γ ⪯ β), projCOFE _ (X' β A0 E0 γ H0) = projCOFE _ (X' β A1 E1 γ H1) := _ in _).
{ intros. unfold X'. pi_clear. destruct le_lt_eq_dec as [H2 | H2]; [apply H | apply Hag]. }
exists X_eq.
- intros.
@@ -2889,7 +2889,7 @@ Qed.
(** * Proving that we can merge approximations in limit cases *)
Section merge.
- Context (P : SI → Prop).
+ Context (P : index → Prop).
Context (IH : ∀ α, P α → bounded_approx (λ γ, γ ⪯ α)).
Context (IH_agree : ∀ α0 α1 Hα0 Hα1, approx_agree (IH α0 Hα0) (IH α1 Hα1)).
@@ -3098,7 +3098,7 @@ Section merge.
Lemma merged_agree γ Hγ: approx_agree (IH γ Hγ) merged_approx.
Proof with (unfold fold_transport, unfold_transport; intros x; cbn; clear_transports; equalise_pi).
- assert (X_eq : ∀ (γ0 : SI) (H0 : γ0 ⪯ γ) (H1 : P γ0), projCOFE _ (bounded_approx_X (IH γ Hγ) γ0 H0) = projCOFE _ (mX γ0 H1)).
+ assert (X_eq : ∀ (γ0 : index) (H0 : γ0 ⪯ γ) (H1 : P γ0), projCOFE _ (bounded_approx_X (IH γ Hγ) γ0 H0) = projCOFE _ (mX γ0 H1)).
{ intros. unfold mX. apply agree_eq, IH_agree. }
exists X_eq; intros; cbn.
- rewrite (agree_bcompl_nat (IH_agree γ γ0 Hγ H1) _ _ _ _ _ _).
@@ -3112,14 +3112,14 @@ Section merge.
End merge.
(* we have to show that merging two coherent & agreeing chains of approximations results in two agreeing approximations *)
-Lemma merge_coherent_agree (P : SI → Prop) (IH1 IH2 : ∀ α, P α → bounded_approx (λ γ, γ ⪯ α))
+Lemma merge_coherent_agree (P : index → Prop) (IH1 IH2 : ∀ α, P α → bounded_approx (λ γ, γ ⪯ α))
(H1 : ∀ α0 α1 Hα0 Hα1, approx_agree (IH1 α0 Hα0) (IH1 α1 Hα1))
(H2 : ∀ α0 α1 Hα0 Hα1, approx_agree (IH2 α0 Hα0) (IH2 α1 Hα1)):
(∀ α Hα, approx_agree (IH1 α Hα) (IH2 α Hα))
→ approx_agree (merged_approx P IH1 H1) (merged_approx P IH2 H2).
Proof with (unfold fold_transport, unfold_transport; intros x; cbn; clear_transports; equalise_pi).
intros IH_agree.
- assert (X_eq : ∀ (γ : SI) (H0 H3 : P γ), projCOFE _ (mX P IH1 γ H0) = projCOFE _ (mX P IH2 γ H3)).
+ assert (X_eq : ∀ (γ : index) (H0 H3 : P γ), projCOFE _ (mX P IH1 γ H0) = projCOFE _ (mX P IH2 γ H3)).
{ intros. unfold mX. pi_clear. apply IH_agree. }
exists X_eq; intros; cbn.
- repeat pi_clear. rewrite (agree_bcompl_nat (IH_agree γ H3) _ _ _ _ _ _ ).
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 12d8fe8d..d22f6218 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -21,7 +21,7 @@ Global Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a => Some a | _ => None end.
Section excl.
-Context {SI} {A : ofe SI}.
+Context `{SI: indexT} {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : excl A.
@@ -30,7 +30,7 @@ Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
| ExclBot_equiv : ExclBot ≡ ExclBot.
Existing Instance excl_equiv.
-Inductive excl_dist : Dist SI (excl A) :=
+Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
| ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
Existing Instance excl_dist.
@@ -44,13 +44,13 @@ Proof. by inversion_clear 1. Qed.
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed.
-Definition excl_ofe_mixin : OfeMixin SI (excl A).
+Definition excl_ofe_mixin : OfeMixin (excl A).
Proof.
apply (iso_ofe_mixin (maybe Excl)).
- by intros [a|] [b|]; split; inversion_clear 1; constructor.
- by intros n [a|] [b|]; split; inversion_clear 1; constructor.
Qed.
-Canonical Structure exclO : ofe SI := Ofe (excl A) excl_ofe_mixin.
+Canonical Structure exclO : ofe := Ofe (excl A) excl_ofe_mixin.
Global Instance excl_cofe `{!Cofe A} : Cofe exclO.
Proof.
@@ -72,12 +72,12 @@ Proof. by inversion_clear 1; constructor. Qed.
(* CMRA *)
Local Instance excl_valid_instance : Valid (excl A) := λ x,
match x with Excl _ => True | ExclBot => False end.
-Local Instance excl_validN_instance : ValidN SI (excl A) := λ n x,
+Local Instance excl_validN_instance : ValidN (excl A) := λ n x,
match x with Excl _ => True | ExclBot => False end.
Local Instance excl_pcore_instance : PCore (excl A) := λ _, None.
Local Instance excl_op_instance : Op (excl A) := λ x y, ExclBot.
-Lemma excl_cmra_mixin : CmraMixin SI (excl A).
+Lemma excl_cmra_mixin : CmraMixin (excl A).
Proof.
split; try discriminate.
- by intros [] n; destruct 1; constructor.
@@ -89,7 +89,7 @@ Proof.
- by intros n [?|] [?|].
- intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto.
Qed.
-Canonical Structure exclR := Cmra SI (excl A) excl_cmra_mixin.
+Canonical Structure exclR := Cmra (excl A) excl_cmra_mixin.
Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
Proof. split; first apply _. by intros []. Qed.
@@ -125,21 +125,21 @@ Proof. by destruct x. Qed.
Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
excl_map (g ∘ f) x = excl_map g (excl_map f x).
Proof. by destruct x. Qed.
-Lemma excl_map_ext {SI} {A B : ofe SI} (f g : A → B) x :
+Lemma excl_map_ext `{SI: indexT} {A B : ofe} (f g : A → B) x :
(∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
Proof. by destruct x; constructor. Qed.
-Global Instance excl_map_ne {SI} {A B : ofe SI} n :
+Global Instance excl_map_ne `{SI: indexT} {A B : ofe} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Global Instance excl_map_cmra_morphism {SI} {A B : ofe SI} (f : A → B) :
+Global Instance excl_map_cmra_morphism `{SI: indexT} {A B : ofe} (f : A → B) :
NonExpansive f → CmraMorphism (excl_map f).
Proof. split; try done; try apply _. by intros n [a|]. Qed.
-Definition exclO_map {SI} {A B: ofe SI} (f : A -n> B) : exclO A -n> exclO B :=
+Definition exclO_map `{SI: indexT} {A B: ofe} (f : A -n> B) : exclO A -n> exclO B :=
OfeMor (excl_map f).
-Global Instance exclO_map_ne {SI} (A B: ofe SI) : NonExpansive (@exclO_map SI A B).
+Global Instance exclO_map_ne `{SI: indexT} (A B: ofe) : NonExpansive (@exclO_map SI A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
-Program Definition exclRF {SI} (F : oFunctor SI) : rFunctor SI := {|
+Program Definition exclRF `{SI: indexT} (F : oFunctor) : rFunctor := {|
rFunctor_car A B := (exclR (oFunctor_car F A B));
rFunctor_map A1 A2 B1 B2 fg := exclO_map (oFunctor_map F fg)
|}.
@@ -155,7 +155,7 @@ Next Obligation.
apply excl_map_ext=>y; apply oFunctor_map_compose.
Qed.
-Global Instance exclRF_contractive {SI} (F: oFunctor SI) :
+Global Instance exclRF_contractive `{SI: indexT} (F: oFunctor) :
oFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_contractive.
diff --git a/theories/algebra/finite.v b/theories/algebra/finite.v
new file mode 100644
index 00000000..1f7561b1
--- /dev/null
+++ b/theories/algebra/finite.v
@@ -0,0 +1,18 @@
+From iris.stepindex Require Export stepindex.
+From iris.stepindex Require Import existential_properties.
+
+
+Global Existing Instance natI | 0.
+
+
+Global Instance fininte_bounded_existential_nat: FiniteBoundedExistential natI.
+Proof.
+ intros P [|n] Hdown Hex.
+ - exists true. simpl. intros ?; lia.
+ - destruct (Hex n) as [x HP].
+ + apply: index_succ_greater.
+ + exists x. simpl; intros m Hm.
+ assert (m = n ∨ m < n) as [->|] by lia; eauto.
+Qed.
+
+
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 657b7a70..a1286a73 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -13,8 +13,8 @@ From iris.prelude Require Import options.
Notation frac := Qp (only parsing).
Section frac.
- Context {SI: indexT}.
- Canonical Structure fracO := leibnizO SI frac.
+ Context `{SI: indexT}.
+ Canonical Structure fracO := leibnizO frac.
Local Instance frac_valid_instance : Valid frac := λ x, (x ≤ 1)%Qp.
Local Instance frac_pcore_instance : PCore frac := λ _, None.
@@ -36,7 +36,7 @@ Section frac.
intros p q. rewrite !frac_valid' frac_op'=> ?.
trans (p + q)%Qp; last done. apply Qp.le_add_l.
Qed.
- Canonical Structure fracR := discreteR SI frac frac_ra_mixin.
+ Canonical Structure fracR := discreteR frac frac_ra_mixin.
Global Instance frac_cmra_discrete : CmraDiscrete fracR.
Proof. apply discrete_cmra_discrete. Qed.
@@ -54,5 +54,3 @@ Section frac.
Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp frac_op' Qp.div_2. Qed.
End frac.
-Arguments fracR : clear implicits.
-Arguments fracO : clear implicits.
\ No newline at end of file
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 4b090f3c..ef76b3c5 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -4,13 +4,13 @@ From iris.algebra Require Import updates local_updates proofmode_classes big_op.
From iris.prelude Require Import options.
Section ofe.
-Context {K} `{Countable K} {SI} {A : ofe SI}.
+Context `{SI: indexT} {K} `{Countable K} {A : ofe}.
Implicit Types m : gmap K A.
Implicit Types i : K.
-Local Instance gmap_dist : Dist SI (gmap K A) := λ n m1 m2,
+Local Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
∀ i, m1 !! i ≡{n}≡ m2 !! i.
-Definition gmap_ofe_mixin : OfeMixin SI (gmap K A).
+Definition gmap_ofe_mixin : OfeMixin (gmap K A).
Proof.
split.
- intros m1 m2; split.
@@ -22,7 +22,7 @@ Proof.
+ by intros m1 m2 m3 ?? k; trans (m2 !! k).
- intros n n' m1 m2 ? k ?; eapply dist_le; eauto.
Qed.
-Canonical Structure gmapO : ofe SI := Ofe (gmap K A) gmap_ofe_mixin.
+Canonical Structure gmapO : ofe := Ofe (gmap K A) gmap_ofe_mixin.
Program Definition gmap_chain (c: chain gmapO) (k: K) : chain (optionO A) :=
@@ -32,12 +32,12 @@ Program Definition gmap_bchain {α} (c: bchain gmapO α) (k: K) : bchain (option
mkbchain _ _ _ (λ β Hβ, c β Hβ !! k) _.
Next Obligation. intros α c k β γ Hβγ Hβ Hγ; by apply c. Qed.
-Definition gmap_compl `{Cofe SI A} : (chain gmapO) → gmapO := λ c,
+Definition gmap_compl `{!Cofe A} : (chain gmapO) → gmapO := λ c,
map_imap (λ i _, compl (gmap_chain c i)) (c zero).
-Definition gmap_lbcompl `{Cofe SI A} : ∀ α Hα , (bchain gmapO α) → gmapO := λ α Hα c,
+Definition gmap_lbcompl `{!Cofe A} : ∀ α Hα , (bchain gmapO α) → gmapO := λ α Hα c,
map_imap (λ i _, lbcompl Hα (gmap_bchain c i)) (c zero (proper_limit_not_zero Hα)).
-Global Program Instance gmap_cofe `{Cofe SI A} : Cofe gmapO :=
+Global Program Instance gmap_cofe `{!Cofe A} : Cofe gmapO :=
{| compl := gmap_compl; lbcompl := gmap_lbcompl |}.
Next Obligation.
intros ? n c k. rewrite /gmap_compl map_lookup_imap.
@@ -118,27 +118,27 @@ Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
(** Internalized properties *)
End ofe.
-Global Arguments gmapO _ {_ _ _} _.
+Global Arguments gmapO {_} _ {_ _} _.
(** Non-expansiveness of higher-order map functions and big-ops *)
-Global Instance merge_ne {SI} `{Countable K} {A B C : ofe SI} n :
+Global Instance merge_ne `{SI: indexT} `{Countable K} {A B C : ofe} n :
Proper (((dist (A:=option A) n) ==> (dist (A:=option B) n) ==> (dist (A:=option C) n)) ==>
(dist n) ==> (dist n) ==> (dist n)) (merge (M:=gmap K)).
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
Qed.
-Global Instance union_with_proper {SI} `{Countable K} {A : ofe SI} n :
+Global Instance union_with_proper `{SI: indexT} `{Countable K} {A : ofe} n :
Proper (((dist n) ==> (dist n) ==> (dist n)) ==>
(dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
-Global Instance map_fmap_proper {SI} `{Countable K} {A B : ofe SI} (f : A → B) n :
+Global Instance map_fmap_proper `{SI: indexT} `{Countable K} {A B : ofe} (f : A → B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
-Global Instance map_zip_with_proper {SI} `{Countable K} {A B C : ofe SI} (f : A → B → C) n :
+Global Instance map_zip_with_proper `{SI: indexT} `{Countable K} {A B C : ofe} (f : A → B → C) n :
Proper (dist n ==> dist n ==> dist n) f →
Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
Proof.
@@ -146,7 +146,7 @@ Proof.
destruct 1; destruct 1; repeat f_equiv; constructor || done.
Qed.
-Lemma big_opM_ne_2 {SI} `{Monoid SI M o} `{Countable K} {A : ofe SI} (f g : K → A → M) m1 m2 n :
+Lemma big_opM_ne_2 `{SI: indexT} `{Monoid M o} `{Countable K} {A : ofe} (f g : K → A → M) m1 m2 n :
m1 ≡{n}≡ m2 →
(∀ k y1 y2,
m1 !! k = Some y1 → m2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
@@ -161,14 +161,14 @@ Qed.
(* CMRA *)
Section cmra.
-Context `{Countable K} {SI} {A : cmra SI}.
+Context `{SI: indexT} `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Local Instance gmap_unit_instance : Unit (gmap K A) := (∅ : gmap K A).
Local Instance gmap_op_instance : Op (gmap K A) := merge op.
Local Instance gmap_pcore_instance : PCore (gmap K A) := λ m, Some (omap pcore m).
Local Instance gmap_valid_instance : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
-Local Instance gmap_validN_instance : ValidN SI (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
+Local Instance gmap_validN_instance : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
Proof. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
@@ -209,7 +209,7 @@ Proof.
lookup_insert_ne // lookup_partial_alter_ne.
Qed.
-Lemma gmap_cmra_mixin : CmraMixin SI (gmap K A).
+Lemma gmap_cmra_mixin : CmraMixin (gmap K A).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -239,27 +239,27 @@ Proof.
+ revert Hz1i. case: (y1!!i)=>[?|] //.
+ revert Hz2i. case: (y2!!i)=>[?|] //.
Qed.
-Canonical Structure gmapR := Cmra SI (gmap K A) gmap_cmra_mixin.
+Canonical Structure gmapR := Cmra (gmap K A) gmap_cmra_mixin.
Global Instance gmap_cmra_discrete : CmraDiscrete A → CmraDiscrete gmapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
-Lemma gmap_ucmra_mixin : UcmraMixin SI (gmap K A).
+Lemma gmap_ucmra_mixin : UcmraMixin (gmap K A).
Proof.
split.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
-Canonical Structure gmapUR := Ucmra SI (gmap K A) gmap_ucmra_mixin.
+Canonical Structure gmapUR := Ucmra (gmap K A) gmap_ucmra_mixin.
End cmra.
-Global Arguments gmapR _ {_ _ _} _.
-Global Arguments gmapUR _ {_ _ _} _.
+Global Arguments gmapR {_} _ {_ _} _.
+Global Arguments gmapUR {_} _ {_ _} _.
Section properties.
-Context `{Countable K} {SI} {A : cmra SI}.
+Context `{SI: indexT} `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
@@ -617,7 +617,7 @@ Proof.
[done|by rewrite lookup_singleton].
Qed.
-Lemma gmap_fmap_mono {B : cmra SI} (f : A → B) m1 m2 :
+Lemma gmap_fmap_mono {B : cmra} (f : A → B) m1 m2 :
Proper ((≡) ==> (≡)) f →
(∀ x y, x ≼ y → f x ≼ f y) → m1 ≼ m2 → fmap f m1 ≼ fmap f m2.
Proof.
@@ -643,7 +643,7 @@ Qed.
End properties.
Section unital_properties.
-Context `{Countable K} {SI} {A : ucmra SI}.
+Context `{SI: indexT} `{Countable K} {A : ucmra}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
@@ -666,10 +666,10 @@ Qed.
End unital_properties.
(** Functor *)
-Global Instance gmap_fmap_ne `{Countable K} {SI} {A B : ofe SI} (f : A → B) n :
+Global Instance gmap_fmap_ne `{SI: indexT} `{Countable K} {A B : ofe} (f : A → B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
-Global Instance gmap_fmap_cmra_morphism `{Countable K} {SI} {A B : cmra SI} (f : A → B)
+Global Instance gmap_fmap_cmra_morphism `{SI: indexT} `{Countable K} {A B : cmra} (f : A → B)
`{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A → gmap K B).
Proof.
split; try apply _.
@@ -678,16 +678,16 @@ Proof.
case: (m!!i)=>//= ?. apply cmra_morphism_pcore, _.
- intros m1 m2 i. by rewrite lookup_op !lookup_fmap lookup_op cmra_morphism_op.
Qed.
-Definition gmapO_map `{Countable K} {SI} {A B: ofe SI} (f: A -n> B) :
+Definition gmapO_map `{SI: indexT} `{Countable K} {A B: ofe} (f: A -n> B) :
gmapO K A -n> gmapO K B := OfeMor (fmap f : gmapO K A → gmapO K B).
-Global Instance gmapO_map_ne `{Countable K} {SI} {A B: ofe SI} :
- NonExpansive (@gmapO_map K _ _ SI A B).
+Global Instance gmapO_map_ne `{SI: indexT} `{Countable K} {A B: ofe} :
+ NonExpansive (@gmapO_map _ K _ _ A B).
Proof.
intros n f g Hf m k; rewrite /= !lookup_fmap.
destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
-Program Definition gmapOF K `{Countable K} {SI} (F : oFunctor SI) : oFunctor SI := {|
+Program Definition gmapOF `{SI: indexT} K `{Countable K} (F : oFunctor) : oFunctor := {|
oFunctor_car A B := gmapO K (oFunctor_car F A B);
oFunctor_map A1 A2 B1 B2 fg := gmapO_map (oFunctor_map F fg)
|}.
@@ -702,13 +702,13 @@ Next Obligation.
intros K SI ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
Qed.
-Global Instance gmapOF_contractive K `{Countable K} {SI} (F: oFunctor SI) :
+Global Instance gmapOF_contractive `{SI: indexT} K `{Countable K} (F: oFunctor) :
oFunctorContractive F → oFunctorContractive (gmapOF K F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapO_map_ne, oFunctor_map_contractive.
Qed.
-Program Definition gmapURF K `{Countable K} {SI} (F : rFunctor SI) : urFunctor SI := {|
+Program Definition gmapURF `{SI: indexT} K `{Countable K} (F : rFunctor) : urFunctor := {|
urFunctor_car A B := gmapUR K (rFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := gmapO_map (rFunctor_map F fg)
|}.
@@ -723,18 +723,19 @@ Next Obligation.
intros K SI ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
Qed.
-Instance gmapURF_contractive K `{Countable K} {SI} (F: rFunctor SI) :
+Global Instance gmapURF_contractive `{SI: indexT} K `{Countable K} (F: rFunctor) :
rFunctorContractive F → urFunctorContractive (gmapURF K F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
Qed.
-Program Definition gmapRF K `{Countable K} {SI} (F : rFunctor SI) : rFunctor SI := {|
+Program Definition gmapRF `{SI: indexT} K `{Countable K} (F : rFunctor) : rFunctor := {|
rFunctor_car A B := gmapR K (rFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := gmapO_map (rFunctor_map F fg)
|}.
-Solve Obligations with (intros; apply gmapURF).
+Solve Obligations with (intros SI; intros; apply (@gmapURF SI)).
-Global Instance gmapRF_contractive K `{Countable K} {SI} (F : rFunctor SI) :
+
+Global Instance gmapRF_contractive `{SI: indexT} K `{Countable K} (F : rFunctor) :
rFunctorContractive F → rFunctorContractive (gmapRF K F).
Proof. apply gmapURF_contractive. Qed.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index b3ac96c8..54744e94 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -2,13 +2,13 @@ From iris.algebra Require Export cmra.
From iris.prelude Require Import options.
(** * Local updates *)
-Definition local_update {SI} {A : cmra SI} (x y : A * A) := ∀ n mz,
+Definition local_update `{SI: indexT} {A : cmra} (x y : A * A) := ∀ n mz,
✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
Global Instance: Params (@local_update) 2 := {}.
Infix "~l~>" := local_update (at level 70).
Section updates.
- Context {SI} {A : cmra SI}.
+ Context `{SI: indexT} {A : cmra}.
Implicit Types x y : A.
Global Instance local_update_proper :
@@ -110,7 +110,7 @@ Section updates.
End updates.
Section updates_unital.
- Context {SI} {A : ucmra SI}.
+ Context `{SI: indexT} {A : ucmra}.
Implicit Types x y : A.
Lemma local_update_unital x y x' y' :
@@ -138,10 +138,10 @@ Section updates_unital.
End updates_unital.
Section local_update_instances.
- Context {SI: indexT}.
+ Context `{SI: indexT}.
(** * Product *)
- Lemma prod_local_update {A B : cmra SI} (x y x' y' : A * B) :
+ Lemma prod_local_update {A B : cmra} (x y x' y' : A * B) :
(x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) →
(x,y) ~l~> (x',y').
Proof.
@@ -151,21 +151,21 @@ Section local_update_instances.
by destruct mz.
Qed.
- Lemma prod_local_update' {A B : cmra SI} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
+ Lemma prod_local_update' {A B : cmra} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
(x1,y1) ~l~> (x1',y1') → (x2,y2) ~l~> (x2',y2') →
((x1,x2),(y1,y2)) ~l~> ((x1',x2'),(y1',y2')).
Proof. intros. by apply prod_local_update. Qed.
- Lemma prod_local_update_1 {A B : cmra SI} (x1 y1 x1' y1' : A) (x2 y2 : B) :
+ Lemma prod_local_update_1 {A B : cmra} (x1 y1 x1' y1' : A) (x2 y2 : B) :
(x1,y1) ~l~> (x1',y1') → ((x1,x2),(y1,y2)) ~l~> ((x1',x2),(y1',y2)).
Proof. intros. by apply prod_local_update. Qed.
- Lemma prod_local_update_2 {A B : cmra SI} (x1 y1 : A) (x2 y2 x2' y2' : B) :
+ Lemma prod_local_update_2 {A B : cmra} (x1 y1 : A) (x2 y2 x2' y2' : B) :
(x2,y2) ~l~> (x2',y2') → ((x1,x2),(y1,y2)) ~l~> ((x1,x2'),(y1,y2')).
Proof. intros. by apply prod_local_update. Qed.
(** * Option *)
(* TODO: Investigate whether we can use these in proving the very similar local
updates on finmaps. *)
- Lemma option_local_update {A : cmra SI} (x y x' y' : A) :
+ Lemma option_local_update {A : cmra} (x y x' y' : A) :
(x, y) ~l~> (x',y') →
(Some x, Some y) ~l~> (Some x', Some y').
Proof.
@@ -175,7 +175,7 @@ Section local_update_instances.
split; first done. destruct mz as [?|]; constructor; auto.
Qed.
- Lemma alloc_option_local_update {A : cmra SI} (x : A) y :
+ Lemma alloc_option_local_update {A : cmra} (x : A) y :
✓ x →
(None, y) ~l~> (Some x, Some x).
Proof.
@@ -184,7 +184,7 @@ Section local_update_instances.
destruct z as [z|]; last done. destruct y; inversion Heq.
Qed.
- Lemma delete_option_local_update {A : cmra SI} (x : option A) (y : A) :
+ Lemma delete_option_local_update {A : cmra} (x : option A) (y : A) :
Exclusive y → (x, Some y) ~l~> (None, None).
Proof.
move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
diff --git a/theories/algebra/monoid.v b/theories/algebra/monoid.v
index 1884bbb8..733b1b4c 100644
--- a/theories/algebra/monoid.v
+++ b/theories/algebra/monoid.v
@@ -17,23 +17,23 @@ we do not have a canonical structure for setoids, we do not go that way.
Note that we do not declare any of the projections as type class instances. That
is because we only need them in the [big_op] file, and nowhere else. Hence, we
declare these instances locally there to avoid them being used elsewhere. *)
-Class Monoid {SI: indexT} {M : ofe SI} (o : M → M → M) := {
+Class Monoid `{SI: indexT} {M : ofe} (o : M → M → M) := {
monoid_unit : M;
monoid_ne : NonExpansive2 o;
monoid_assoc : Assoc (≡) o;
monoid_comm : Comm (≡) o;
monoid_left_id : LeftId (≡) monoid_unit o;
}.
-Lemma monoid_proper {SI: indexT} `{Monoid SI M o} : Proper ((≡) ==> (≡) ==> (≡)) o.
+Lemma monoid_proper `{SI: indexT} `{Monoid M o} : Proper ((≡) ==> (≡) ==> (≡)) o.
Proof. apply ne_proper_2, monoid_ne. Qed.
-Lemma monoid_right_id {SI: indexT} `{Monoid SI M o} : RightId (≡) monoid_unit o.
+Lemma monoid_right_id `{SI: indexT} `{Monoid M o} : RightId (≡) monoid_unit o.
Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
(** The [Homomorphism] classes give rise to generic lemmas about big operators
commuting with each other. We also consider a [WeakMonoidHomomorphism] which
does not necessarily commute with unit; an example is the [own] connective: we
only have `True ==∗ own γ ∅`, not `True ↔ own γ ∅`. *)
-Class WeakMonoidHomomorphism {SI: indexT} {M1 M2 : ofe SI}
+Class WeakMonoidHomomorphism `{SI: indexT} {M1 M2 : ofe}
(o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{!Monoid o1, !Monoid o2}
(R : relation M2) (f : M1 → M2) := {
monoid_homomorphism_rel_po : PreOrder R;
@@ -43,13 +43,13 @@ Class WeakMonoidHomomorphism {SI: indexT} {M1 M2 : ofe SI}
monoid_homomorphism x y : R (f (o1 x y)) (o2 (f x) (f y))
}.
-Class MonoidHomomorphism {SI: indexT} {M1 M2 : ofe SI}
+Class MonoidHomomorphism `{SI: indexT} {M1 M2 : ofe}
(o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{!Monoid o1, !Monoid o2}
(R : relation M2) (f : M1 → M2) := {
monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 R f;
monoid_homomorphism_unit : R (f monoid_unit) monoid_unit
}.
-Lemma weak_monoid_homomorphism_proper {SI: indexT}
- `{WeakMonoidHomomorphism SI M1 M2 o1 o2 R f} : Proper ((≡) ==> (≡)) f.
+Lemma weak_monoid_homomorphism_proper `{SI: indexT}
+ `{WeakMonoidHomomorphism M1 M2 o1 o2 R f} : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, monoid_homomorphism_ne. Qed.
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index 819a78d4..f21e686e 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -4,15 +4,15 @@ From iris.prelude Require Import options.
(** ** Natural numbers with [add] as the operation. *)
Section nat.
- Variable (SI: indexT).
+ Context `{SI: indexT}.
Local Instance nat_valid_instance : Valid nat := λ x, True.
- Local Instance nat_validN_instance : ValidN SI nat := λ α x, True.
+ Local Instance nat_validN_instance : ValidN nat := λ α x, True.
Local Instance nat_pcore_instance : PCore nat := λ x, Some 0.
Local Instance nat_op_instance : Op nat := plus.
Definition nat_op_plus x y : x ⋅ y = x + y := eq_refl.
- Lemma nat_included (x y : nat) : (x: natO SI) ≼ y ↔ x ≤ y.
+ Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
Proof. by rewrite Nat.le_sum. Qed.
- Lemma nat_ra_mixin : RAMixin (natO SI).
+ Lemma nat_ra_mixin : RAMixin nat.
Proof.
apply ra_total_mixin; try by eauto.
- solve_proper.
@@ -20,15 +20,15 @@ Section nat.
- intros x y. apply Nat.add_comm.
- by exists 0.
Qed.
- Canonical Structure natR : cmra SI := discreteR SI nat nat_ra_mixin.
+ Canonical Structure natR : cmra := discreteR nat nat_ra_mixin.
Global Instance nat_cmra_discrete : CmraDiscrete natR.
Proof. apply discrete_cmra_discrete. Qed.
Local Instance nat_unit_instance : Unit nat := 0.
- Lemma nat_ucmra_mixin : UcmraMixin SI (natO SI).
+ Lemma nat_ucmra_mixin : UcmraMixin nat.
Proof. split; apply _ || done. Qed.
- Canonical Structure natUR : ucmra SI := Ucmra SI nat nat_ucmra_mixin.
+ Canonical Structure natUR : ucmra := Ucmra nat nat_ucmra_mixin.
Global Instance nat_cancelable (x : nat) : Cancelable x.
Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
@@ -50,39 +50,39 @@ End nat.
Record max_nat := MaxNat { max_nat_car : nat }.
Add Printing Constructor max_nat.
-Canonical Structure max_natO SI := leibnizO SI max_nat.
+Canonical Structure max_natO `{SI: indexT} := leibnizO max_nat.
Section max_nat.
- Variable (SI: indexT).
+ Context `{SI: indexT}.
Local Instance max_nat_unit_instance : Unit max_nat := MaxNat 0.
Local Instance max_nat_valid_instance : Valid max_nat := λ x, True.
- Local Instance max_nat_validN_instance : ValidN SI max_nat := λ α x, True.
+ Local Instance max_nat_validN_instance : ValidN max_nat := λ α x, True.
Local Instance max_nat_pcore_instance : PCore max_nat := Some.
Local Instance max_nat_op_instance : Op max_nat := λ n m, MaxNat (max_nat_car n `max` max_nat_car m).
Definition max_nat_op_max x y : MaxNat x ⋅ MaxNat y = MaxNat (x `max` y) := eq_refl.
- Lemma max_nat_included (x y : max_nat) : (x: max_natO SI) ≼ y ↔ max_nat_car x ≤ max_nat_car y.
+ Lemma max_nat_included (x y : max_nat) : x ≼ y ↔ max_nat_car x ≤ max_nat_car y.
Proof.
split.
- intros [z ->]. simpl. lia.
- exists y. rewrite /op /max_nat_op_instance. rewrite Nat.max_r; last lia. by destruct y.
Qed.
- Lemma max_nat_ra_mixin : RAMixin (max_natO SI).
+ Lemma max_nat_ra_mixin : RAMixin max_nat.
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite max_nat_op_max. by rewrite Nat.max_assoc.
- intros [x] [y]. by rewrite max_nat_op_max Nat.max_comm.
- intros [x]. by rewrite max_nat_op_max Max.max_idempotent.
Qed.
- Canonical Structure max_natR : cmra SI := discreteR SI max_nat max_nat_ra_mixin.
+ Canonical Structure max_natR : cmra := discreteR max_nat max_nat_ra_mixin.
Global Instance max_nat_cmra_discrete : CmraDiscrete max_natR.
Proof. apply discrete_cmra_discrete. Qed.
- Lemma max_nat_ucmra_mixin : UcmraMixin SI (max_natO SI).
+ Lemma max_nat_ucmra_mixin : UcmraMixin max_nat.
Proof. split; try apply _ || done. intros [x]. done. Qed.
- Canonical Structure max_natUR : ucmra SI := Ucmra SI max_nat max_nat_ucmra_mixin.
+ Canonical Structure max_natUR : ucmra := Ucmra max_nat max_nat_ucmra_mixin.
Global Instance max_nat_core_id (x : max_nat) : CoreId x.
Proof. by constructor. Qed.
@@ -108,32 +108,32 @@ End max_nat.
Record min_nat := MinNat { min_nat_car : nat }.
Add Printing Constructor min_nat.
-Canonical Structure min_natO SI := leibnizO SI min_nat.
+Canonical Structure min_natO `{SI: indexT} := leibnizO min_nat.
Section min_nat.
- Variable (SI: indexT).
+ Context `{SI: indexT}.
Local Instance min_nat_unit_instance : Unit min_nat := MinNat 0.
Local Instance min_nat_valid_instance : Valid min_nat := λ x, True.
- Local Instance min_nat_validN_instance : ValidN SI min_nat := λ α x, True.
+ Local Instance min_nat_validN_instance : ValidN min_nat := λ α x, True.
Local Instance min_nat_pcore_instance : PCore min_nat := Some.
Local Instance min_nat_op_instance : Op min_nat := λ n m, MinNat (min_nat_car n `min` min_nat_car m).
Definition min_nat_op_min x y : MinNat x ⋅ MinNat y = MinNat (x `min` y) := eq_refl.
- Lemma min_nat_included (x y : min_nat) : (x: min_natO SI) ≼ y ↔ min_nat_car y ≤ min_nat_car x .
+ Lemma min_nat_included (x y : min_nat) : x ≼ y ↔ min_nat_car y ≤ min_nat_car x .
Proof.
split.
- intros [z ->]. simpl. lia.
- exists y. rewrite /op /min_nat_op_instance. rewrite Nat.min_r; last lia. by destruct y.
Qed.
- Lemma min_nat_ra_mixin : RAMixin (min_natO SI).
+ Lemma min_nat_ra_mixin : RAMixin min_nat.
Proof.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
- intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
- intros [x]. by rewrite min_nat_op_min Nat.min_idempotent.
Qed.
- Canonical Structure min_natR : cmra SI := discreteR SI min_nat min_nat_ra_mixin.
+ Canonical Structure min_natR : cmra := discreteR min_nat min_nat_ra_mixin.
Global Instance min_nat_cmra_discrete : CmraDiscrete min_natR.
Proof. apply discrete_cmra_discrete. Qed.
@@ -166,36 +166,34 @@ End min_nat.
(** ** Positive integers with [Pos.add] as the operation. *)
Section positive.
- Variable (SI: indexT).
+ Context {SI: indexT}.
Local Instance pos_valid_instance : Valid positive := λ x, True.
- Local Instance pos_validN_instance : ValidN SI positive := λ α x, True.
+ Local Instance pos_validN_instance : ValidN positive := λ α x, True.
Local Instance pos_pcore_instance : PCore positive := λ x, None.
Local Instance pos_op_instance : Op positive := Pos.add.
Definition pos_op_plus x y : x ⋅ y = (x + y)%positive := eq_refl.
- Lemma pos_included (x y : positive) : (x: positiveO SI) ≼ y ↔ (x < y)%positive.
+ Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
Proof. by rewrite Pos.lt_sum. Qed.
- Lemma pos_ra_mixin : RAMixin (positiveO SI).
+ Lemma pos_ra_mixin : RAMixin positive.
Proof.
split; try by eauto.
- by intros ??? ->.
- intros ???. apply Pos.add_assoc.
- intros ??. apply Pos.add_comm.
Qed.
- Canonical Structure positiveR : cmra SI := discreteR SI positive pos_ra_mixin.
+ Canonical Structure positiveR : cmra := discreteR positive pos_ra_mixin.
Global Instance pos_cmra_discrete : CmraDiscrete positiveR.
Proof. apply discrete_cmra_discrete. Qed.
- Global Instance pos_cancelable (x : positiveO SI) : Cancelable (x: positiveO SI).
+ Global Instance pos_cancelable (x: positive) : Cancelable x.
Proof.
- intros α y z Hv H.
- eapply Pos.add_reg_l, (@leibniz_equiv (positiveO SI)), H.
- eapply (@leibnizO_leibniz _ SI).
+ intros n y z ??. by eapply Pos.add_reg_l, leibniz_equiv.
Qed.
Global Instance pos_id_free (x : positive) : IdFree x.
Proof.
intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
- by eapply (@leibniz_equiv (positiveO SI) (ofe_equiv _ (positiveO SI)) _).
+ by apply leibniz_equiv.
Qed.
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
@@ -206,19 +204,19 @@ End positive.
(** Ordinals *)
Section ordinals.
- Context (SI : indexT).
+ Context `{SI : indexT}.
Local Open Scope ordinals.
- Canonical Structure ordO SI := leibnizO SI ordinals.ord.
+ Canonical Structure ordO := leibnizO ordinals.ord.
Instance ord_valid : Valid ord := λ x, True.
- Instance ord_validI : ValidN SI ord := λ α x, True.
+ Instance ord_validI : ValidN ord := λ α x, True.
Instance ord_pcore : PCore ord := λ x, Some zero.
Instance ord_op : Op ord := nadd.
Instance ord_inhabited : Inhabited ord := populate zero.
Definition ord_op_plus (x y: ord) : x ⋅ y = (x ⊕ y) := eq_refl.
- Definition ord_equiv_eq (x y: ord) : ((x: ordO SI) ≡ y) = (x = y) := eq_refl.
+ Definition ord_equiv_eq (x y: ord) : (x ≡ y) = (x = y) := eq_refl.
- Lemma ord_ra_mixin : RAMixin (ordO SI).
+ Lemma ord_ra_mixin : RAMixin ord.
Proof.
split; try by eauto.
- by intros ??? ->.
@@ -232,12 +230,12 @@ Section ordinals.
exists zero. by rewrite !ord_op_plus natural_addition_zero_left_id.
Qed.
- Canonical Structure OrdR : cmra SI := discreteR SI ord ord_ra_mixin.
+ Canonical Structure OrdR : cmra := discreteR ord ord_ra_mixin.
Global Instance ord_cmra_discrete : CmraDiscrete OrdR.
Proof. apply discrete_cmra_discrete. Qed.
- Global Instance ord_cancelable (x : ordO SI) : Cancelable (x: ordO SI).
+ Global Instance ord_cancelable (x : ord) : Cancelable x.
Proof.
intros α y z Hv H. eapply natural_addition_cancel.
rewrite natural_addition_comm [z ⊕ _]natural_addition_comm.
@@ -250,10 +248,10 @@ Section ordinals.
Qed.
Global Instance ord_unit : Unit ord := zero.
- Lemma ord_ucmra_mixin : UcmraMixin SI (ordO SI).
+ Lemma ord_ucmra_mixin : UcmraMixin ord.
Proof.
split; apply _ || done.
Qed.
- Canonical Structure OrdUR : ucmra SI := Ucmra SI ord ord_ucmra_mixin.
+ Canonical Structure OrdUR : ucmra := Ucmra ord ord_ucmra_mixin.
End ordinals.
\ No newline at end of file
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 2eee734e..459bd99c 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -12,9 +12,9 @@ Set Primitive Projections.
*)
(** Unbundeled version *)
-Class Dist (SI: indexT) A := dist : SI → relation A.
+Class Dist `{SI: indexT} A := dist : index → relation A.
-Instance: Params (@dist) 4 := {}.
+Global Instance: Params (@dist) 4 := {}.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
@@ -38,23 +38,23 @@ Tactic Notation "ofe_subst" :=
| H:@dist ?SI ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist SI A d n) x
end.
-Record OfeMixin (SI: indexT) A `{Equiv A, Dist SI A} := {
- mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ (n: SI), x ≡{n}≡ y;
- mixin_dist_equivalence (n : SI): Equivalence (dist n);
- mixin_dist_mono (n m: SI) (x y : A) : x ≡{n}≡ y → m ≺ n → x ≡{m}≡ y
+Record OfeMixin `{SI: indexT} A `{Equiv A, Dist A} := {
+ mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ (n: index), x ≡{n}≡ y;
+ mixin_dist_equivalence (n : index): Equivalence (dist n);
+ mixin_dist_mono (n m: index) (x y : A) : x ≡{n}≡ y → m ≺ n → x ≡{m}≡ y
}.
(** Bundled version *)
-Structure ofe (SI: indexT) := Ofe {
+Structure ofe `{SI: indexT} := Ofe {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
- ofe_dist : Dist SI ofe_car;
- ofe_mixin : OfeMixin SI ofe_car
+ ofe_dist : Dist ofe_car;
+ ofe_mixin : OfeMixin ofe_car
}.
Global Arguments Ofe {_} _ {_ _} _.
Add Printing Constructor ofe.
-Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _ _) : typeclass_instances.
-Global Hint Extern 0 (Dist _ _) => eapply (@ofe_dist _ _) : typeclass_instances.
+Global Hint Extern 0 (Equiv _) => eapply (ofe_equiv _) : typeclass_instances.
+Global Hint Extern 0 (Dist _) => eapply (ofe_dist _) : typeclass_instances.
Global Arguments ofe_car : simpl never.
Global Arguments ofe_equiv : simpl never.
Global Arguments ofe_dist : simpl never.
@@ -81,45 +81,46 @@ The notation [ofe_mixin_of A] that we define on top of [ofe_mixin_of' A id]
hides the [id] and normalizes the mixin to head normal form. The latter is to
ensure that we do not end up with redundant canonical projections to the mixin,
i.e. them all being of the shape [ofe_mixin_of' A id]. *)
-Definition ofe_mixin_of' SI A {Ac : ofe SI} (f : Ac → A) : OfeMixin SI Ac := ofe_mixin SI Ac.
-Notation ofe_mixin_of SI A :=
- ltac:(let H := eval hnf in (ofe_mixin_of' SI A id) in exact H) (only parsing).
+Definition ofe_mixin_of' `{SI: indexT} A {Ac : ofe} (f : Ac → A) : OfeMixin Ac := ofe_mixin Ac.
+Notation ofe_mixin_of A :=
+ ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).
(** Lifting properties from the mixin *)
Section ofe_mixin.
- Context {SI} {A : ofe SI}.
+ Context `{SI: indexT} {A : ofe}.
Implicit Types x y : A.
- Lemma equiv_dist x y : x ≡ y ↔ ∀ (n: SI), x ≡{n}≡ y.
- Proof. apply (mixin_equiv_dist _ _ (ofe_mixin SI A)). Qed.
+
+ Lemma equiv_dist x y : x ≡ y ↔ ∀ (n: index), x ≡{n}≡ y.
+ Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
Global Instance dist_equivalence n : Equivalence (@dist SI A _ n).
- Proof. apply (mixin_dist_equivalence _ _ (ofe_mixin SI A)). Qed.
- Lemma dist_mono (n m: SI) x y : x ≡{n}≡ y → m ≺ n → x ≡{m}≡ y.
- Proof. apply (mixin_dist_mono _ _ (ofe_mixin SI A)). Qed.
- Lemma dist_mono' (n m: SI) x y : x ≡{n}≡ y → m ⪯ n → x ≡{m}≡ y.
+ Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
+ Lemma dist_mono (n m: index) x y : x ≡{n}≡ y → m ≺ n → x ≡{m}≡ y.
+ Proof. apply (mixin_dist_mono _ (ofe_mixin A)). Qed.
+ Lemma dist_mono' (n m: index) x y : x ≡{n}≡ y → m ⪯ n → x ≡{m}≡ y.
Proof. intros H [-> | Hm]; [auto | by eapply dist_mono]. Qed.
End ofe_mixin.
Global Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
(** Discrete OFEs and discrete OFE elements *)
-Class Discrete {SI: indexT} {A : ofe SI} (x : A) := discrete y : x ≡{zero}≡ y → x ≡ y.
+Class Discrete `{SI: indexT} {A : ofe} (x : A) := discrete y : x ≡{zero}≡ y → x ≡ y.
Global Arguments discrete {_ _} _ {_} _ _.
Global Hint Mode Discrete - + ! : typeclass_instances.
Global Instance: Params (@Discrete) 2 := {}.
-Class OfeDiscrete {SI: indexT} (A : ofe SI) := ofe_discrete_discrete (x : A) :> Discrete x.
+Class OfeDiscrete `{SI: indexT} (A : ofe) := ofe_discrete_discrete (x : A) :> Discrete x.
Global Hint Mode OfeDiscrete - ! : typeclass_instances.
(** OFEs with a completion *)
-Record chain {SI: indexT} (A : ofe SI) := mkchain {
- chain_car :> SI → A;
+Record chain `{SI: indexT} (A : ofe) := mkchain {
+ chain_car :> index → A;
chain_cauchy n m: n ⪯ m → chain_car m ≡{n}≡ chain_car n
}.
Global Arguments chain_car {_ _} _ _.
Global Arguments chain_cauchy {_ _} _ _ _ _.
-Record bchain {SI: indexT} (A : ofe SI) (n: SI) := mkbchain {
+Record bchain `{SI: indexT} (A : ofe) (n: index) := mkbchain {
bchain_car :> ∀ m, m ≺ n → A;
bchain_cauchy m p Hm Hp: m ⪯ p → bchain_car p Hp ≡{m}≡ bchain_car m Hm
}.
@@ -127,15 +128,15 @@ Global Arguments bchain_car {_ _} _ _ _.
Global Arguments bchain_cauchy {_ _} _ _ _ _ _.
-Program Definition chain_map {SI: indexT} {A B : ofe SI} (f : A → B) `{NonExpansive f} (c : chain A) : chain B :=
+Program Definition chain_map `{SI: indexT} {A B : ofe} (f : A → B) `{NonExpansive f} (c : chain A) : chain B :=
{| chain_car n := f (c n) |}.
Next Obligation. by intros SI A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
-Program Definition bchain_map {SI: indexT} {A B : ofe SI} (f : A → B) `{NonExpansive f} {n} (c: bchain A n) : bchain B n :=
+Program Definition bchain_map `{SI: indexT} {A B : ofe} (f : A → B) `{NonExpansive f} {n} (c: bchain A n) : bchain B n :=
{| bchain_car m Hm := f (c m Hm) |}.
Next Obligation. by intros SI A B f Hf n c m p ? Hm Hp; apply Hf, bchain_cauchy. Qed.
-Class Cofe {SI: indexT} (A : ofe SI) :=
+Class Cofe `{SI: indexT} (A : ofe) :=
{
compl : chain A → A;
(** We only require a bounded limit operation for proper limit indices *)
@@ -150,7 +151,7 @@ Global Hint Mode Cofe - ! : typeclass_instances.
(** But we can derive bounded limits for all non-zero indices. *)
Section bcompl.
- Context {SI : indexT} `{Cofe SI A}.
+ Context `{SI : indexT} `{!Cofe A}.
Local Unset Program Cases.
Program Definition bcompl {α} (Hz : zero ≺ α) (b : bchain A α) : A :=
match index_dec_limit α with
@@ -179,31 +180,31 @@ End bcompl.
(* TODO: remove these lemmas *)
-Lemma chain_conv_compl {SI: indexT} `{Cofe SI A} (c: chain A) n : compl c ≡{n}≡ c n.
+Lemma chain_conv_compl `{SI: indexT} `{!Cofe A} (c: chain A) n : compl c ≡{n}≡ c n.
Proof. rewrite conv_compl; eauto using chain_cauchy. Qed.
-Lemma bchain_conv_bcompl {SI: indexT} `{Cofe SI A} n Hn (c: bchain A n) m Hm: bcompl Hn c ≡{m}≡ c m Hm.
+Lemma bchain_conv_bcompl `{SI: indexT} `{!Cofe A} n Hn (c: bchain A n) m Hm: bcompl Hn c ≡{m}≡ c m Hm.
Proof. rewrite conv_bcompl; eauto using bchain_cauchy. Qed.
-Lemma compl_chain_map {SI: indexT} `{Cofe SI A, Cofe SI B} (f : A → B) (c: chain A) `(NonExpansive f) :
+Lemma compl_chain_map `{SI: indexT} `{!Cofe A, !Cofe B} (f : A → B) (c: chain A) `(NonExpansive f) :
compl (chain_map f c) ≡ f (compl c).
Proof. apply equiv_dist=>n. by rewrite !chain_conv_compl. Qed.
-Program Definition chain_const {SI: indexT} {A : ofe SI} (a : A) : chain A :=
+Program Definition chain_const `{SI: indexT} {A : ofe} (a : A) : chain A :=
{| chain_car n := a |}.
Next Obligation. by intros ??????. Qed.
-Lemma compl_chain_const {SI: indexT} {A : ofe SI} `{!Cofe A} (a : A) :
+Lemma compl_chain_const `{SI: indexT} {A : ofe} `{!Cofe A} (a : A) :
compl (chain_const a) ≡ a.
Proof. apply equiv_dist=>n. by rewrite chain_conv_compl. Qed.
-Program Definition bchain_const {SI : indexT} {A : ofe SI} (a : A) n : bchain A n :=
+Program Definition bchain_const `{SI : indexT} {A : ofe} (a : A) n : bchain A n :=
{| bchain_car m _ := a |}.
Next Obligation.
by intros ????????.
Qed.
-Lemma bcompl_bchain_const {SI: indexT} {A : ofe SI} `{!Cofe A} (a : A) (n : SI) Hn:
+Lemma bcompl_bchain_const `{SI: indexT} {A : ofe} `{!Cofe A} (a : A) (n : index) Hn:
∀ p, p ≺ n → bcompl Hn (bchain_const a n) ≡{p}≡ a.
Proof.
intros p Hp. by unshelve rewrite bchain_conv_bcompl.
@@ -211,7 +212,7 @@ Qed.
(** General properties *)
Section ofe.
- Context {SI: indexT} {A : ofe SI}.
+ Context `{SI: indexT} {A : ofe}.
Implicit Types x y : A.
Global Instance ofe_equivalence : Equivalence ((≡) : relation A).
Proof.
@@ -243,17 +244,17 @@ Section ofe.
type class search during setoid rewriting.
Local Instances of [NonExpansive{,2}] are hence accompanied by instances of
[Proper] built using these lemmas. *)
- Lemma ne_proper {B : ofe SI} (f : A → B) `{!NonExpansive f} :
+ Lemma ne_proper {B : ofe} (f : A → B) `{!NonExpansive f} :
Proper ((≡) ==> (≡)) f.
Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
- Lemma ne_proper_2 {B C : ofe SI} (f : A → B → C) `{!NonExpansive2 f} :
+ Lemma ne_proper_2 {B C : ofe} (f : A → B → C) `{!NonExpansive2 f} :
Proper ((≡) ==> (≡) ==> (≡)) f.
Proof.
unfold Proper, respectful; setoid_rewrite equiv_dist.
by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed.
- Lemma conv_compl' `{!Cofe A} (n m: SI) (c: chain A) : n ⪯ m → compl c ≡{n}≡ c m.
+ Lemma conv_compl' `{!Cofe A} (n m: index) (c: chain A) : n ⪯ m → compl c ≡{n}≡ c m.
Proof.
transitivity (c n); first by apply chain_conv_compl. symmetry. by rewrite chain_cauchy.
Qed.
@@ -267,12 +268,12 @@ Section ofe.
End ofe.
(** Contractive functions *)
-Definition dist_later {SI: indexT} `{Dist SI A} (n : SI) (x y : A) : Prop :=
+Definition dist_later {SI: indexT} `{!Dist A} (n : index) (x y : A) : Prop :=
∀ m, m ≺ n → x ≡{m}≡ y.
Global Arguments dist_later _ _ _ !_ _ _ /.
-Global Instance dist_later_equivalence {SI} (A : ofe SI) n : Equivalence (@dist_later SI A _ n).
+Global Instance dist_later_equivalence `{SI: indexT} (A : ofe) n : Equivalence (@dist_later SI A _ n).
Proof.
split.
- now intros ???.
@@ -280,38 +281,38 @@ Proof.
- unfold dist_later; intros ??? H1 H2 ??; now rewrite H1 ?H2.
Qed.
-Lemma dist_dist_later {SI: indexT} {A : ofe SI} n (x y : A) : dist n x y → dist_later n x y.
+Lemma dist_dist_later `{SI: indexT} {A : ofe} n (x y : A) : dist n x y → dist_later n x y.
Proof. intros Heq ??; eapply dist_mono; eauto. Qed.
-Lemma dist_later_dist {SI: indexT} {A : ofe SI} n m (x y : A) : m ≺ n → dist_later n x y → dist m x y.
-Proof. intros ? H; by apply H. Qed.
+Lemma dist_later_dist `{SI: indexT} {A : ofe} n m (x y : A) : m ≺ n → dist_later n x y → dist m x y.
+Proof. intros ? H; by apply H. Qed.
(* We don't actually need this lemma (as our tactics deal with this through
other means), but technically speaking, this is the reason why
pre-composing a non-expansive function to a contractive function
preserves contractivity. *)
-Lemma ne_dist_later {SI} {A B : ofe SI} (f : A → B) :
+Lemma ne_dist_later `{SI: indexT} {A B : ofe} (f : A → B) :
NonExpansive f → ∀ n, Proper (dist_later n ==> dist_later n) f.
Proof. intros Hf ??????; by eapply Hf, H. Qed.
-Lemma dist_later_zero {SI: indexT} {A : ofe SI} (x y : A): dist_later zero x y.
+Lemma dist_later_zero `{SI: indexT} {A : ofe} (x y : A): dist_later zero x y.
Proof. intros ? [] % index_lt_zero_is_normal. Qed.
-Global Instance ne2_dist_later_l {SI} {A B C: ofe SI} (f : A → B → C) :
+Global Instance ne2_dist_later_l `{SI: indexT} {A B C: ofe} (f : A → B → C) :
NonExpansive2 f → ∀ n, Proper (dist_later n ==> dist n ==> dist_later n) f.
Proof. intros H n a b H1 c d H2 m Hm. apply H; by eauto using dist_mono. Qed.
-Global Instance ne2_dist_later_r {SI} {A B C: ofe SI} (f : A → B → C) :
+Global Instance ne2_dist_later_r `{SI: indexT} {A B C: ofe} (f : A → B → C) :
NonExpansive2 f → ∀ n, Proper (dist n ==> dist_later n ==> dist_later n) f.
Proof. intros H n a b H1 c d H2 m Hm. apply H; by eauto using dist_mono. Qed.
Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
-Instance const_contractive {SI: indexT} {A B : ofe SI} (x : A) : Contractive (@const A B x).
+Global Instance const_contractive `{SI: indexT} {A B : ofe} (x : A) : Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.
Section contractive.
Local Set Default Proof Using "Type*".
- Context {SI: indexT} {A B : ofe SI} (f : A → B) `{!Contractive f}.
+ Context `{SI: indexT} {A B : ofe} (f : A → B) `{!Contractive f}.
Implicit Types x y : A.
Lemma contractive_0 x y : f x ≡{zero}≡ f y.
@@ -352,19 +353,19 @@ Ltac solve_contractive :=
end]).
(* without smoothness, we only get uniqueness at ≺ n *)
-Lemma cofe_bcompl_weakly_unique {SI : indexT} (A : ofe SI) (HA : Cofe A) (n: SI) Hn (c d : bchain A n):
+Lemma cofe_bcompl_weakly_unique `{SI : indexT} (A : ofe) (HA : Cofe A) (n: index) Hn (c d : bchain A n):
(∀ p (Hp : p ≺ n), c p Hp ≡{p}≡ d p Hp) → dist_later n (bcompl Hn c) (bcompl Hn d).
Proof.
intros H p Hp. unshelve rewrite !conv_bcompl; [assumption | assumption | apply H].
Qed.
(** Limit preserving predicates *)
-Class LimitPreserving {SI: indexT} {A: ofe SI} `{!Cofe A} (P : A → Prop) : Prop :=
+Class LimitPreserving `{SI: indexT} {A: ofe} `{!Cofe A} (P : A → Prop) : Prop :=
limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c).
Global Hint Mode LimitPreserving - + + ! : typeclass_instances.
Section limit_preserving.
- Context {SI: indexT} {A: ofe SI}`{!Cofe A}.
+ Context {SI: indexT} {A: ofe}`{!Cofe A}.
(* These are not instances as they will never fire automatically...
but they can still be helpful in proving things to be limit preserving. *)
@@ -408,12 +409,12 @@ End limit_preserving.
(** Bounded limit preserving predicates *)
-Class BoundedLimitPreserving {SI: indexT} `{Cofe SI A} (P : A → Prop) : Prop :=
+Class BoundedLimitPreserving {SI: indexT} `{!Cofe A} (P : A → Prop) : Prop :=
bounded_limit_preserving n Hn (c: bchain A n) : (∀ m Hm, P (c m Hm)) → P (lbcompl Hn c).
Global Hint Mode BoundedLimitPreserving - + + ! : typeclass_instances.
Section bounded_limit_preserving.
- Context {SI: indexT} `{Cofe SI A}.
+ Context {SI: indexT} `{!Cofe A}.
(* These are not instances as they will never fire automatically...
but they can still be helpful in proving things to be limit preserving. *)
@@ -451,7 +452,7 @@ End bounded_limit_preserving.
(** Fixpoint *)
Section fixpoint.
- Context {SI: indexT} `{Cofe SI A} (f: A → A) `{C: Contractive f} `{In: Inhabited A}.
+ Context {SI: indexT} `{!Cofe A} (f: A → A) `{C: Contractive f} `{In: Inhabited A}.
Record is_bounded_fixpoint_chain n (ch : ∀ m, m ≺ n → A) := mk_is_bounded_fixpoint_chain
{
@@ -495,8 +496,8 @@ Section fixpoint.
Lemma bounded_fixpoint_chain_unique n (Hn: zero ≺ n) (c: bounded_fixpoint_chain n) m (Hm: zero ≺ m) (Hmn: m ⪯ n) (d: bounded_fixpoint_chain m) :
dist_later m (bcompl Hn c) (bcompl Hm d).
- Proof using A C H SI f.
- revert Hmn d. induction (index_lt_wf SI m) as [m _ IH]. intros Hmn d p Hp.
+ Proof using A C SI f.
+ revert Hmn d. induction (index_lt_wf m) as [m _ IH]. intros Hmn d p Hp.
rewrite -(fp_chain_is_fp _ d Hm p Hp). rewrite -(fp_chain_is_fp _ c Hn p _); eauto using index_lt_le_trans.
destruct (index_is_zero p) as [->|NT].
- by apply contractive_0.
@@ -512,13 +513,13 @@ Section fixpoint.
Section inductive_step.
- Local Definition patch_base_case {n: SI} (g: zero ≺ n → A) : A :=
+ Local Definition patch_base_case {n: index} (g: zero ≺ n → A) : A :=
match index_is_zero n with
| left H => inhabitant
| right NT => g NT
end.
- Program Definition bfpc : ∀ (n: SI), bounded_fixpoint_chain n :=
+ Program Definition bfpc : ∀ (n: index), bounded_fixpoint_chain n :=
index_cumulative_rec (fun _ => A) is_bounded_fixpoint_chain
(fun n IH => f (patch_base_case (fun NT => bcompl NT (get_chain n IH)))) _.
Next Obligation.
@@ -556,24 +557,24 @@ Section fixpoint.
erewrite !conv_compl. unfold fixpoint_chain; simpl.
unfold patch_base_case; destruct index_is_zero; subst.
- by apply contractive_0.
- - eapply contractive_mono; eauto. symmetry. eapply is_fp.
+ - eapply contractive_mono; eauto. symmetry. eapply is_fp.
Qed.
End fixpoint.
Section fixpoint.
- Context {SI: indexT} `{Cofe SI A} (f : A → A) `{!Contractive f} `{Inhabited A}.
+ Context {SI: indexT} `{!Cofe A} (f : A → A) `{!Contractive f} `{Inhabited A}.
Lemma fixpoint_unique (x : A) : x ≡ f x → x ≡ fixpoint f.
Proof.
- rewrite !equiv_dist=> Hx n. induction (index_lt_wf SI n) as [n _ IH].
+ rewrite !equiv_dist=> Hx n. induction (index_lt_wf n) as [n _ IH].
rewrite Hx fixpoint_unfold. eapply contractive_mono; eauto.
Qed.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
(∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
Proof.
- intros Hfg. induction (index_lt_wf SI n) as [n _ IH].
+ intros Hfg. induction (index_lt_wf n) as [n _ IH].
do 2 (rewrite fixpoint_unfold; symmetry). etransitivity; last by eapply Hfg.
eapply contractive_mono; eauto.
intros ??; eapply IH; eauto.
@@ -609,12 +610,12 @@ Global Arguments fixpoint {_ A _} f {_ _}.
(** Fixpoint of f when f^k is contractive. **)
-Definition fixpointK {SI} {A: ofe SI} `{!Cofe A, Inhabited A} k (f : A → A)
+Definition fixpointK `{SI: indexT} {A: ofe} `{!Cofe A, Inhabited A} k (f : A → A)
`{!Contractive (Nat.iter k f)} := fixpoint (Nat.iter k f).
Section fixpointK.
Local Set Default Proof Using "Type*".
- Context {SI} {A: ofe SI} `{!Cofe A, Inhabited A} (f : A → A) (k : nat).
+ Context `{SI: indexT} {A: ofe} `{!Cofe A, Inhabited A} (f : A → A) (k : nat).
Context {f_contractive : Contractive (Nat.iter k f)} {f_ne : NonExpansive f}.
(* Note than f_ne is crucial here: there are functions f such that f^2 is contractive,
but f is not non-expansive.
@@ -683,7 +684,7 @@ End fixpointK.
(** Mutual fixpoints *)
Section fixpointAB.
- Context {SI} {A B: ofe SI}`{!Cofe A, !Cofe B, !Inhabited A, !Inhabited B}.
+ Context `{SI: indexT} {A B: ofe}`{!Cofe A, !Cofe B, !Inhabited A, !Inhabited B}.
Context (fA : A → B → A).
Context (fB : A → B → B).
Context {fA_contractive : ∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
@@ -727,7 +728,7 @@ Section fixpointAB.
End fixpointAB.
Section fixpointAB_ne.
- Context {SI} {A B: ofe SI} `{!Cofe A, !Cofe B, !Inhabited A, !Inhabited B}.
+ Context `{SI: indexT} {A B: ofe} `{!Cofe A, !Cofe B, !Inhabited A, !Inhabited B}.
Context (fA fA' : A → B → A).
Context (fB fB' : A → B → B).
Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
@@ -761,25 +762,25 @@ Section fixpointAB_ne.
End fixpointAB_ne.
(** Non-expansive function space *)
-Record ofe_mor {SI} (A B : ofe SI) : Type := OfeMor {
+Record ofe_mor `{SI: indexT} (A B : ofe) : Type := OfeMor {
ofe_mor_car :> A → B;
ofe_mor_ne : NonExpansive ofe_mor_car
}.
Global Arguments OfeMor {_ _ _} _ {_}.
Add Printing Constructor ofe_mor.
-Existing Instance ofe_mor_ne.
+Global Existing Instance ofe_mor_ne.
Notation "'λne' x .. y , t" :=
(@OfeMor _ _ _ (λ x, .. (@OfeMor _ _ _ (λ y, t) _) ..) _)
(at level 200, x binder, y binder, right associativity).
Section ofe_mor.
- Context {SI: indexT} {A B : ofe SI}.
+ Context `{SI: indexT} {A B : ofe}.
Global Instance ofe_mor_proper (f : ofe_mor A B) : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, ofe_mor_ne. Qed.
Local Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, ∀ x, f x ≡ g x.
- Local Instance ofe_mor_dist : Dist SI (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
- Definition ofe_mor_ofe_mixin : OfeMixin SI (ofe_mor A B).
+ Local Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+ Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -805,7 +806,7 @@ Section ofe_mor.
Program Definition ofe_mor_bchain {n} (c : bchain ofe_morO n) (x : A) : bchain B n :=
{| bchain_car n Hn := c n Hn x |}.
Next Obligation. intros n c x m Hm i ??. by apply (bchain_cauchy n c). Qed.
- Program Definition ofe_mor_lbcompl `{Cofe SI B} n : index_is_proper_limit n → bchain ofe_morO n → ofe_morO := λ Hn c,
+ Program Definition ofe_mor_lbcompl `{!Cofe B} n : index_is_proper_limit n → bchain ofe_morO n → ofe_morO := λ Hn c,
{| ofe_mor_car x := lbcompl Hn (ofe_mor_bchain c x) |}.
Next Obligation.
intros ? n Hn c m x y Hx. eapply lbcompl_ne.
@@ -813,7 +814,7 @@ Section ofe_mor.
Qed.
- Global Program Instance ofe_mor_cofe `{Cofe SI B} : Cofe ofe_morO :=
+ Global Program Instance ofe_mor_cofe `{!Cofe B} : Cofe ofe_morO :=
{| compl := ofe_mor_compl; lbcompl := ofe_mor_lbcompl |}.
Next Obligation.
intros ? n c x; cbn. rewrite conv_compl //=.
@@ -835,48 +836,47 @@ Section ofe_mor.
Proof. done. Qed.
End ofe_mor.
-Global Arguments ofe_morO : clear implicits.
+Global Arguments ofe_morO {_} _ _.
Notation "A -n> B" :=
- (ofe_morO _ A B) (at level 99, B at level 200, right associativity).
-Global Instance ofe_mor_inhabited {SI: indexT} {A B : ofe SI} `{Inhabited B} :
+ (ofe_morO A B) (at level 99, B at level 200, right associativity).
+Global Instance ofe_mor_inhabited `{SI: indexT} {A B : ofe} `{Inhabited B} :
Inhabited (A -n> B) := populate (λne _, inhabitant).
(** Identity and composition and constant function *)
-Definition cid {SI} {A: ofe SI} : A -n> A := OfeMor id.
+Definition cid `{SI: indexT} {A: ofe} : A -n> A := OfeMor id.
Global Instance: Params (@cid) 2 := {}.
-Definition cconst {SI} {A B : ofe SI} (x : B) : A -n> B := OfeMor (const x).
+Definition cconst `{SI: indexT} {A B : ofe} (x : B) : A -n> B := OfeMor (const x).
Global Instance: Params (@cconst) 3 := {}.
-Definition ccompose {SI: indexT} {A B C: ofe SI}
+Definition ccompose `{SI: indexT} {A B C: ofe}
(f : B -n> C) (g : A -n> B) : A -n> C := OfeMor (f ∘ g).
Global Instance: Params (@ccompose) 4 := {}.
Infix "◎" := ccompose (at level 40, left associativity).
-Global Instance ccompose_ne SI {A B C: ofe SI} :
+Global Instance ccompose_ne `{SI: indexT} {A B C: ofe} :
NonExpansive2 (@ccompose SI A B C).
Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
-(* TODO: is this used anywhere? LG: yes, COFE solver. may move there*)
-Lemma ccompose_assoc {SI : indexT} {A B C D : ofe SI} (f : C -n> D) (g : B -n> C) (h : A -n> B) :
+Lemma ccompose_assoc `{SI : indexT} {A B C D : ofe} (f : C -n> D) (g : B -n> C) (h : A -n> B) :
(f ◎ g) ◎ h ≡ f ◎ (g ◎ h).
Proof. intros x. by cbn. Qed.
-Lemma ccompose_cid_l {SI : indexT} {A B : ofe SI} (f : A -n> B ) : cid ◎ f ≡ f.
+Lemma ccompose_cid_l `{SI : indexT} {A B : ofe} (f : A -n> B ) : cid ◎ f ≡ f.
Proof. intros x. by cbn. Qed.
-Lemma ccompose_cid_r {SI : indexT} {A B : ofe SI} (f : A -n> B ) : f ◎ cid ≡ f.
+Lemma ccompose_cid_r `{SI : indexT} {A B : ofe} (f : A -n> B ) : f ◎ cid ≡ f.
Proof. intros x. by cbn. Qed.
(* Function space maps *)
-Definition ofe_mor_map {SI: indexT} {A A' B B': ofe SI} (f : A' -n> A) (g : B -n> B')
+Definition ofe_mor_map `{SI: indexT} {A A' B B': ofe} (f : A' -n> A) (g : B -n> B')
(h : A -n> B) : A' -n> B' := g ◎ h ◎ f.
-Instance ofe_mor_map_ne SI {A A' B B': ofe SI} n :
+Global Instance ofe_mor_map_ne SI {A A' B B': ofe} n :
Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map SI A A' B B').
Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
-Definition ofe_morO_map {SI: indexT} {A A' B B': ofe SI} (f : A' -n> A) (g : B -n> B') :
+Definition ofe_morO_map `{SI: indexT} {A A' B B': ofe} (f : A' -n> A) (g : B -n> B') :
(A -n> B) -n> (A' -n> B') := OfeMor (ofe_mor_map f g).
-Instance ofe_morO_map_ne {SI: indexT} {A A' B B': ofe SI} :
+Global Instance ofe_morO_map_ne `{SI: indexT} {A A' B B': ofe} :
NonExpansive2 (@ofe_morO_map SI A A' B B').
Proof.
intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
@@ -885,11 +885,11 @@ Qed.
(** * Unit type *)
Section unit.
- Context {SI: indexT}.
- Local Instance unit_dist : Dist SI unit := λ _ _ _, True.
- Definition unit_ofe_mixin : OfeMixin SI unit.
+ Context `{SI: indexT}.
+ Local Instance unit_dist : Dist unit := λ _ _ _, True.
+ Definition unit_ofe_mixin : OfeMixin unit.
Proof. by repeat split. Qed.
- Canonical Structure unitO : ofe SI := Ofe unit unit_ofe_mixin.
+ Canonical Structure unitO : ofe := Ofe unit unit_ofe_mixin.
Global Program Instance unit_cofe : Cofe unitO := { compl x := () }.
Solve All Obligations with by repeat split.
@@ -897,15 +897,14 @@ Section unit.
Global Instance unit_ofe_discrete : OfeDiscrete unitO.
Proof. done. Qed.
End unit.
-Global Arguments unitO : clear implicits.
(** * Empty type *)
Section empty.
- Context {SI: indexT}.
- Local Instance Empty_set_dist : Dist SI Empty_set := λ _ _ _, True.
- Definition Empty_set_ofe_mixin : OfeMixin SI Empty_set.
+ Context `{SI: indexT}.
+ Local Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
+ Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
Proof. by repeat split; try exists zero. Qed.
- Canonical Structure Empty_setO : ofe SI := Ofe Empty_set Empty_set_ofe_mixin.
+ Canonical Structure Empty_setO : ofe := Ofe Empty_set Empty_set_ofe_mixin.
Global Program Instance Empty_set_cofe : Cofe Empty_setO :=
{ compl x := x zero; lbcompl n Hn c := c zero (proper_limit_not_zero Hn) }.
@@ -914,18 +913,17 @@ Section empty.
Global Instance Empty_set_ofe_discrete : OfeDiscrete Empty_setO.
Proof. done. Qed.
End empty.
-Global Arguments Empty_setO : clear implicits.
(** * Product type *)
Section product.
- Context {SI: indexT} {A B : ofe SI}.
+ Context `{SI: indexT} {A B : ofe}.
- Local Instance prod_dist : Dist SI (A * B) := λ n, prod_relation (dist n) (dist n).
+ Local Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
Global Instance pair_ne :
NonExpansive2 (@pair A B) := _.
Global Instance fst_ne : NonExpansive (@fst A B) := _.
Global Instance snd_ne : NonExpansive (@snd A B) := _.
- Definition prod_ofe_mixin : OfeMixin SI (A * B).
+ Definition prod_ofe_mixin : OfeMixin (A * B).
Proof.
split.
- intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
@@ -933,9 +931,9 @@ Section product.
- apply _.
- by intros n m [x1 y1] [x2 y2] [??]; split; eapply dist_mono.
Qed.
- Canonical Structure prodO : ofe SI := Ofe (A * B) prod_ofe_mixin.
+ Canonical Structure prodO : ofe := Ofe (A * B) prod_ofe_mixin.
- Global Program Instance prod_cofe `{Cofe SI A, Cofe SI B} : Cofe prodO :=
+ Global Program Instance prod_cofe `{!Cofe A, !Cofe B} : Cofe prodO :=
{ compl c := (compl (chain_map fst c), compl (chain_map snd c));
lbcompl n Hn c := (lbcompl Hn (bchain_map fst c), lbcompl Hn (bchain_map snd c)) }.
Next Obligation.
@@ -957,21 +955,21 @@ Section product.
End product.
Global Arguments prodO {_} _ _.
-Typeclasses Opaque prod_dist.
+Global Typeclasses Opaque prod_dist.
-Global Instance prod_map_ne {SI: indexT} {A A' B B' : ofe SI} n :
+Global Instance prod_map_ne `{SI: indexT} {A A' B B' : ofe} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
dist n ==> dist n) (@prod_map A A' B B').
Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.
-Definition prodO_map {SI: indexT} {A A' B B': ofe SI} (f : A -n> A') (g : B -n> B') :
+Definition prodO_map `{SI: indexT} {A A' B B': ofe} (f : A -n> A') (g : B -n> B') :
prodO A B -n> prodO A' B' := OfeMor (prod_map f g).
-Global Instance prodO_map_ne {SI: indexT} {A A' B B': ofe SI} :
+Global Instance prodO_map_ne `{SI: indexT} {A A' B B': ofe} :
NonExpansive2 (@prodO_map SI A A' B B').
Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
(** * OFE → OFE Functors *)
-Record oFunctor {SI} := OFunctor {
- oFunctor_car : ∀ A B, ofe SI;
+Record oFunctor `{SI: indexT} := OFunctor {
+ oFunctor_car : ∀ A B, ofe;
oFunctor_map {A1 A2 B1 B2}:
((A2 -n> A1) * (B1 -n> B2)) → oFunctor_car A1 B1 -n> oFunctor_car A2 B2;
oFunctor_map_ne {A1 A2 B1 B2}:
@@ -982,37 +980,36 @@ Record oFunctor {SI} := OFunctor {
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
}.
-Existing Instance oFunctor_map_ne.
-Instance: Params (@oFunctor_map) 6 := {}.
-Arguments oFunctor : clear implicits.
+Global Existing Instance oFunctor_map_ne.
+Global Instance: Params (@oFunctor_map) 6 := {}.
Declare Scope oFunctor_scope.
Delimit Scope oFunctor_scope with OF.
Bind Scope oFunctor_scope with oFunctor.
-Class oFunctorContractive {SI: indexT} (F : oFunctor SI) :=
- oFunctor_map_contractive `{A1 : ofe SI} `{A2 : ofe SI} `{B1 : ofe SI} `{B2 : ofe SI} :>
+Class oFunctorContractive `{SI: indexT} (F : oFunctor) :=
+ oFunctor_map_contractive `{A1 : ofe} `{A2 : ofe} `{B1 : ofe} `{B2 : ofe} :>
Contractive (@oFunctor_map SI F A1 A2 B1 B2).
Global Hint Mode oFunctorContractive - ! : typeclass_instances.
(** We add the coercion because there is no more Cofe argument *)
-Definition oFunctor_apply {SI: indexT} (F: oFunctor SI) (A: ofe SI) : ofe SI := oFunctor_car F A A.
+Definition oFunctor_apply `{SI: indexT} (F: oFunctor) (A: ofe) : ofe := oFunctor_car F A A.
Coercion oFunctor_apply : oFunctor >-> Funclass.
-Program Definition constOF {SI} (B : ofe SI) : oFunctor SI :=
+Program Definition constOF `{SI: indexT} (B : ofe) : oFunctor :=
{| oFunctor_car A1 A2 := B; oFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
Coercion constOF : ofe >-> oFunctor.
-Global Instance constOF_contractive {SI} B : @oFunctorContractive SI (constOF B).
+Global Instance constOF_contractive `{SI: indexT} B : oFunctorContractive (constOF B).
Proof. rewrite /oFunctorContractive; apply _. Qed.
-Program Definition idOF SI : oFunctor SI :=
+Program Definition idOF `{SI: indexT} : oFunctor :=
{| oFunctor_car A1 A2 := A2; oFunctor_map A1 A2 B1 B2 f := f.2 |}.
Solve Obligations with done.
Notation "∙" := idOF : oFunctor_scope.
-Program Definition prodOF {SI} (F1 F2 : oFunctor SI) : oFunctor SI := {|
+Program Definition prodOF `{SI: indexT} (F1 F2 : oFunctor) : oFunctor := {|
oFunctor_car A B := prodO (oFunctor_car F1 A B) (oFunctor_car F2 A B);
oFunctor_map A1 A2 B1 B2 fg :=
prodO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
@@ -1027,7 +1024,7 @@ Next Obligation.
Qed.
Notation "F1 * F2" := (prodOF F1%OF F2%OF) : oFunctor_scope.
-Instance prodOF_contractive {SI} {F1 F2 : ofe SI}:
+Global Instance prodOF_contractive `{SI: indexT} {F1 F2 : ofe}:
oFunctorContractive F1 → oFunctorContractive F2 →
oFunctorContractive (prodOF F1 F2).
Proof.
@@ -1035,7 +1032,7 @@ Proof.
by apply prodO_map_ne; apply oFunctor_map_contractive.
Qed.
-Program Definition ofe_morOF {SI: indexT} (F1 F2 : oFunctor SI) : oFunctor SI := {|
+Program Definition ofe_morOF `{SI: indexT} (F1 F2 : oFunctor) : oFunctor := {|
oFunctor_car A B := oFunctor_car F1 B A -n> oFunctor_car F2 A B;
oFunctor_map A1 A2 B1 B2 fg :=
ofe_morO_map (oFunctor_map F1 (fg.2, fg.1)) (oFunctor_map F2 fg)
@@ -1054,7 +1051,7 @@ Next Obligation.
Qed.
Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
-Global Instance ofe_morOF_Contractive {SI: indexT} (F1 F2 : oFunctor SI):
+Global Instance ofe_morOF_Contractive `{SI: indexT} (F1 F2 : oFunctor):
oFunctorContractive F1 → oFunctorContractive F2 →
oFunctorContractive (ofe_morOF F1 F2).
Proof.
@@ -1065,15 +1062,15 @@ Qed.
(** * Sum type *)
Section sum.
- Context {SI: indexT} {A B : ofe SI}.
+ Context `{SI: indexT} {A B : ofe}.
- Local Instance sum_dist : Dist SI (A + B) := λ n, sum_relation (dist n) (dist n).
+ Local Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
Global Instance inl_ne : NonExpansive (@inl A B) := _.
Global Instance inr_ne : NonExpansive (@inr A B) := _.
Global Instance inl_ne_inj n : Inj (dist n) (dist n) (@inl A B) := _.
Global Instance inr_ne_inj n : Inj (dist n) (dist n) (@inr A B) := _.
- Definition sum_ofe_mixin : OfeMixin SI (A + B).
+ Definition sum_ofe_mixin : OfeMixin (A + B).
Proof.
split.
- intros x y; split=> Hx.
@@ -1083,7 +1080,7 @@ Section sum.
- destruct 1; constructor; eapply dist_mono; eauto.
Qed.
- Canonical Structure sumO : ofe SI := Ofe (A + B) sum_ofe_mixin.
+ Canonical Structure sumO : ofe := Ofe (A + B) sum_ofe_mixin.
Program Definition inl_chain (c : chain sumO) (a : A) : chain A :=
{| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
@@ -1103,7 +1100,7 @@ Section sum.
Program Definition inr_bchain {n} (c : bchain sumO n) (b : B) : bchain B n :=
{| bchain_car n Hn := match c n Hn return _ with inr b' => b' | _ => b end |}.
Next Obligation. intros n c b m p Hm Hp Hmp; simpl. by destruct (bchain_cauchy n c m p Hm Hp Hmp). Qed.
- Definition sum_lbcompl `{Cofe SI A, Cofe SI B} n : index_is_proper_limit n → bchain sumO n → sumO :=
+ Definition sum_lbcompl `{!Cofe A, !Cofe B} n : index_is_proper_limit n → bchain sumO n → sumO :=
λ Hn c,
match c zero (proper_limit_not_zero Hn) with
| inl a => inl (lbcompl Hn (inl_bchain c a))
@@ -1142,21 +1139,21 @@ Section sum.
End sum.
Global Arguments sumO {_} _ _.
-Typeclasses Opaque sum_dist.
+Global Typeclasses Opaque sum_dist.
-Global Instance sum_map_ne {SI: indexT} {A A' B B' : ofe SI} n :
+Global Instance sum_map_ne `{SI: indexT} {A A' B B' : ofe} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
dist n ==> dist n) (@sum_map A A' B B').
Proof.
intros f f' Hf g g' Hg ??; destruct 1; constructor; [by apply Hf|by apply Hg].
Qed.
-Definition sumO_map {SI: indexT} {A A' B B': ofe SI} (f : A -n> A') (g : B -n> B') :
+Definition sumO_map `{SI: indexT} {A A' B B': ofe} (f : A -n> A') (g : B -n> B') :
sumO A B -n> sumO A' B' := OfeMor (sum_map f g).
-Global Instance sumO_map_ne {SI} {A A' B B'} :
+Global Instance sumO_map_ne `{SI: indexT} {A A' B B'} :
NonExpansive2 (@sumO_map SI A A' B B').
Proof. intros n f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.
-Program Definition sumOF {SI: indexT} (F1 F2 : oFunctor SI) : oFunctor SI := {|
+Program Definition sumOF `{SI: indexT} (F1 F2 : oFunctor) : oFunctor := {|
oFunctor_car A B := sumO (oFunctor_car F1 A B) (oFunctor_car F2 A B);
oFunctor_map A1 A2 B1 B2 fg :=
sumO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
@@ -1171,7 +1168,7 @@ Next Obligation.
Qed.
Notation "F1 + F2" := (sumOF F1%OF F2%OF) : oFunctor_scope.
-Global Instance sumOF_contractive {SI: indexT} (F1 F2 : oFunctor SI):
+Global Instance sumOF_contractive `{SI: indexT} (F1 F2 : oFunctor):
oFunctorContractive F1 → oFunctorContractive F2 →
oFunctorContractive (sumOF F1 F2).
Proof.
@@ -1181,10 +1178,10 @@ Qed.
(** * Discrete OFEs *)
Section discrete_ofe.
- Context {SI: indexT} {A: Type} `{Equiv A} (Heq : @Equivalence A (≡)).
+ Context `{SI: indexT} {A: Type} `{Equiv A} (Heq : @Equivalence A (≡)).
- Local Instance discrete_dist : Dist SI A := λ n x y, x ≡ y.
- Definition discrete_ofe_mixin : OfeMixin SI A.
+ Local Instance discrete_dist : Dist A := λ n x y, x ≡ y.
+ Definition discrete_ofe_mixin : OfeMixin A.
Proof using Type*.
split.
- intros x y; split; [done|intros Hn; apply (Hn zero)].
@@ -1215,11 +1212,11 @@ Section discrete_ofe.
End discrete_ofe.
-Notation discreteO SI A := (Ofe A (discrete_ofe_mixin _): ofe SI).
+Notation discreteO A := (Ofe A (discrete_ofe_mixin _)).
(** Force the [Equivalence] proof to be [eq_equivalence] so that it does not
find another one, like [ofe_equivalence], in the case of aliases. See also
https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
-Notation leibnizO SI A := (Ofe A (@discrete_ofe_mixin SI _ equivL eq_equivalence): ofe SI).
+Notation leibnizO A := (Ofe A (@discrete_ofe_mixin _ _ equivL eq_equivalence)).
(** In order to define a discrete CMRA with carrier [A] (in the file [cmra.v])
we need to determine the [Equivalence A] proof that was used to construct the
@@ -1229,36 +1226,38 @@ via [ofe_equivalence]).
We obtain the proof of [Equivalence A] by inferring the canonical OFE mixin
using [ofe_mixin_of A], and then check whether it is indeed a discrete OFE. This
will fail if no OFE, or an OFE other than the discrete OFE, was registered. *)
-Notation discrete_ofe_equivalence_of SI A := ltac:(
- match constr:(ofe_mixin_of SI A) with
+Notation discrete_ofe_equivalence_of A := ltac:(
+ match constr:(ofe_mixin_of A) with
| discrete_ofe_mixin ?H => exact H
end) (only parsing).
-Global Instance leibnizO_leibniz A {SI} : LeibnizEquiv (leibnizO SI A : ofe SI).
+Global Instance leibnizO_leibniz A `{SI: indexT} : LeibnizEquiv (leibnizO A).
Proof. by intros x y. Qed.
(** * Basic Coq types *)
-Canonical Structure boolO SI : ofe SI := leibnizO SI bool.
-Canonical Structure natO SI : ofe SI := leibnizO SI nat.
-Canonical Structure positiveO SI : ofe SI := leibnizO SI positive.
-Canonical Structure NO SI : ofe SI := leibnizO SI N.
-Canonical Structure ZO SI : ofe SI := leibnizO SI Z.
+Canonical Structure boolO `{SI: indexT} : ofe := leibnizO bool.
+Canonical Structure natO `{SI: indexT} : ofe := leibnizO nat.
+Canonical Structure positiveO `{SI: indexT} : ofe := leibnizO positive.
+Canonical Structure NO `{SI: indexT} : ofe := leibnizO N.
+Canonical Structure ZO `{SI: indexT} : ofe := leibnizO Z.
Section prop.
+ Context `{SI: indexT}.
+
Local Instance Prop_equiv : Equiv Prop := iff.
Local Instance Prop_equivalence : Equivalence (≡@{Prop}) := _.
- Canonical Structure PropO SI := discreteO SI Prop.
+ Canonical Structure PropO := discreteO Prop.
End prop.
(** * Option type *)
Section option.
- Context {SI: indexT} {A : ofe SI}.
+ Context `{SI: indexT} {A : ofe}.
- Local Instance option_dist : Dist SI (option A) := λ n, option_Forall2 (dist n).
+ Local Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
Proof. done. Qed.
- Definition option_ofe_mixin : OfeMixin SI (option A).
+ Definition option_ofe_mixin : OfeMixin (option A).
Proof.
split.
- intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
@@ -1278,19 +1277,19 @@ Section option.
Program Definition option_chain (c : chain optionO) (x : A) : chain A :=
{| chain_car n := default x (c n) |}.
Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
- Definition option_compl `{Cofe SI A} : (chain optionO) → optionO := λ c,
+ Definition option_compl `{!Cofe A} : (chain optionO) → optionO := λ c,
match c zero with Some x => Some (compl (option_chain c x)) | None => None end.
Program Definition option_bchain n (c : bchain optionO n) (x : A) : bchain A n :=
{| bchain_car n Hn := default x (c n Hn) |}.
Next Obligation. intros n c x m p Hm Hp Hmp; simpl. by destruct (bchain_cauchy n c m p Hm Hp Hmp). Qed.
- Definition option_lbcompl `{Cofe SI A} n (Hn: index_is_proper_limit n): (bchain optionO n) → optionO := λ c,
+ Definition option_lbcompl `{!Cofe A} n (Hn: index_is_proper_limit n): (bchain optionO n) → optionO := λ c,
match c zero (proper_limit_not_zero Hn) with
| Some x => Some (lbcompl Hn (option_bchain n c x))
| None => None
end.
- Global Program Instance option_cofe `{Cofe SI A} : Cofe optionO :=
+ Global Program Instance option_cofe `{!Cofe A} : Cofe optionO :=
{ compl := option_compl; lbcompl := option_lbcompl }.
Next Obligation.
intros ? n c; rewrite /compl /option_compl.
@@ -1340,33 +1339,33 @@ Section option.
Proof. intros ?%(dist_Some_inv_r _ _ _ y); naive_solver. Qed.
End option.
-Typeclasses Opaque option_dist.
+Global Typeclasses Opaque option_dist.
Global Arguments optionO {_} _.
-Global Instance option_fmap_ne {SI} {A B : ofe SI} n:
+Global Instance option_fmap_ne `{SI: indexT} {A B : ofe} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
Proof. intros f f' Hf ?? []; constructor; auto. Qed.
-Global Instance option_mbind_ne {SI} {A B : ofe SI} n:
+Global Instance option_mbind_ne `{SI: indexT} {A B : ofe} n:
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind option _ A B).
Proof. destruct 2; simpl; auto. Qed.
-Global Instance option_mjoin_ne {SI} {A : ofe SI} n:
+Global Instance option_mjoin_ne `{SI: indexT} {A : ofe} n:
Proper (dist n ==> dist n) (@mjoin option _ A).
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
(* TODO: why is this here *)
-Lemma fmap_Some_dist {SI} {A B : ofe SI} (f : A → B) (mx : option A) (y : B) n :
+Lemma fmap_Some_dist `{SI: indexT} {A B : ofe} (f : A → B) (mx : option A) (y : B) n :
f <$> mx ≡{n}≡ Some y ↔ ∃ x : A, mx = Some x ∧ y ≡{n}≡ f x.
Proof.
split; [|by intros (x&->&->)].
intros (?&?%fmap_Some&?)%dist_Some_inv_r'; naive_solver.
Qed.
-Definition optionO_map {SI} {A B: ofe SI} (f : A -n> B) : optionO A -n> optionO B :=
+Definition optionO_map `{SI: indexT} {A B: ofe} (f : A -n> B) : optionO A -n> optionO B :=
OfeMor (fmap f : optionO A → optionO B).
-Global Instance optionO_map_ne {SI} (A B: ofe SI) : NonExpansive (@optionO_map _ A B).
+Global Instance optionO_map_ne `{SI: indexT} (A B: ofe) : NonExpansive (@optionO_map _ A B).
Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
-Program Definition optionOF {SI: indexT} (F : oFunctor SI) : oFunctor SI := {|
+Program Definition optionOF `{SI: indexT} (F : oFunctor) : oFunctor := {|
oFunctor_car A B := optionO (oFunctor_car F A B);
oFunctor_map A1 A2 B1 B2 fg := optionO_map (oFunctor_map F fg)
|}.
@@ -1382,7 +1381,7 @@ Next Obligation.
apply option_fmap_equiv_ext=>y; apply oFunctor_map_compose.
Qed.
-Global Instance optionOF_contractive {SI} (F : oFunctor SI):
+Global Instance optionOF_contractive `{SI: indexT} (F : oFunctor):
oFunctorContractive F → oFunctorContractive (optionOF F).
Proof.
by intros ? ? A1 A2 B1 B2 n f g Hfg; apply optionO_map_ne, oFunctor_map_contractive.
@@ -1400,11 +1399,11 @@ Global Arguments later_car {_} _.
Global Instance: Params (@Next) 1 := {}.
Section later.
- Context {SI: indexT} {A : ofe SI}.
+ Context `{SI: indexT} {A : ofe}.
Local Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
- Local Instance later_dist : Dist SI (later A) := λ n x y,
+ Local Instance later_dist : Dist (later A) := λ n x y,
dist_later n (later_car x) (later_car y).
- Definition later_ofe_mixin : OfeMixin SI (later A).
+ Definition later_ofe_mixin : OfeMixin (later A).
Proof.
split.
- intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
@@ -1416,7 +1415,7 @@ Section later.
+ by intros [x] [y] [z] ??; trans y.
- intros n m [x] [y] H ? p Hp. eapply H; by transitivity m.
Qed.
- Canonical Structure laterO : ofe SI := Ofe (later A) later_ofe_mixin.
+ Canonical Structure laterO : ofe := Ofe (later A) later_ofe_mixin.
Lemma later_car_bounded_expansive (a b : laterO) n: a ≡{succ n}≡ b → later_car a ≡{n}≡ later_car b.
Proof.
@@ -1442,7 +1441,7 @@ Section later.
Global Instance Next_contractive : Contractive (@Next A).
Proof. by intros n x y. Qed.
- Global Program Instance later_cofe `{Cofe SI A} : Cofe laterO :=
+ Global Program Instance later_cofe `{!Cofe A} : Cofe laterO :=
{ compl c := Next (compl (later_chain c));
lbcompl n Hn c := Next (lbcompl Hn (later_limit_bchain c (proper_limit_is_limit Hn)))
}.
@@ -1471,7 +1470,7 @@ Section later.
(** [f] is contractive iff it can factored into [Next] and a non-expansive
function. *)
- Lemma contractive_alt {B : ofe SI} (f : A → B) :
+ Lemma contractive_alt {B : ofe} (f : A → B) :
Contractive f ↔ ∃ g : later A → B, NonExpansive g ∧ ∀ x, f x ≡ g (Next x).
Proof.
split.
@@ -1484,14 +1483,14 @@ Arguments laterO {_} _.
Definition later_map {A B} (f : A → B) (x : later A) : later B :=
Next (f (later_car x)).
-Global Instance later_map_ne {SI: indexT} {A B : ofe SI} (f : A → B) n :
+Global Instance later_map_ne {SI: indexT} {A B : ofe} (f : A → B) n :
Proper (dist_later n ==> dist_later n) f →
Proper (dist n ==> dist n) (later_map f) | 0.
Proof. intros P [x] [y] H; rewrite /later_map //=.
intros m Hm; apply P, Hm. apply H.
Qed.
-Global Instance later_map_ne' {SI: indexT} {A B : ofe SI} (f : A → B) `{NonExpansive f} : NonExpansive (later_map f).
+Global Instance later_map_ne' `{SI: indexT} {A B : ofe} (f : A → B) `{NonExpansive f} : NonExpansive (later_map f).
Proof. intros ?[x][y]H. unfold later_map; simpl.
intros ??; cbn. f_equiv. by eapply H.
Qed.
@@ -1501,15 +1500,15 @@ Proof. by destruct x. Qed.
Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
later_map (g ∘ f) x = later_map g (later_map f x).
Proof. by destruct x. Qed.
-Lemma later_map_ext {SI: indexT} {A B : ofe SI} (f g : A → B) x :
+Lemma later_map_ext `{SI: indexT} {A B : ofe} (f g : A → B) x :
(∀ x, f x ≡ g x) → later_map f x ≡ later_map g x.
Proof. destruct x; intros Hf; apply Hf. Qed.
-Definition laterO_map {SI: indexT} {A B: ofe SI} (f : A -n> B) : laterO A -n> laterO B :=
+Definition laterO_map `{SI: indexT} {A B: ofe} (f : A -n> B) : laterO A -n> laterO B :=
OfeMor (later_map f).
-Global Instance laterO_map_contractive {SI: indexT} (A B : ofe SI) : Contractive (@laterO_map SI A B).
+Global Instance laterO_map_contractive {SI: indexT} (A B : ofe) : Contractive (@laterO_map SI A B).
Proof. intros n f g ? [x] ??; simpl. by apply H. Qed.
-Program Definition laterOF {SI: indexT} (F : oFunctor SI) : oFunctor SI := {|
+Program Definition laterOF `{SI: indexT} (F : oFunctor) : oFunctor := {|
oFunctor_car A B := laterO (oFunctor_car F A B);
oFunctor_map A1 A2 B1 B2 fg := laterO_map (oFunctor_map F fg)
|}.
@@ -1527,7 +1526,7 @@ Next Obligation.
Qed.
Notation "▶ F" := (laterOF F%OF) (at level 20, right associativity) : oFunctor_scope.
-Global Instance laterOF_contractive {SI: indexT} {F :oFunctor SI} : oFunctorContractive (laterOF F).
+Global Instance laterOF_contractive `{SI: indexT} {F :oFunctor} : oFunctorContractive (laterOF F).
Proof.
intros A1 A2 B1 B2 n fg fg' Hfg. apply laterO_map_contractive.
intros ???; simpl. by eapply oFunctor_map_ne, Hfg.
@@ -1547,15 +1546,15 @@ We make [discrete_fun] a definition so that we can register it as a canonical
structure. We do not bundle the [Proper] proof to keep [discrete_fun] easier to
use. It turns out all the desired OFE and functorial properties do not rely on
this [Proper] instance. *)
-Definition discrete_fun {SI: indexT} {A} (B : A → ofe SI) := ∀ x : A, B x.
+Definition discrete_fun `{SI: indexT} {A} (B : A → ofe) := ∀ x : A, B x.
Section discrete_fun.
- Context {SI: indexT} {A : Type} {B : A → ofe SI}.
+ Context `{SI: indexT} {A : Type} {B : A → ofe}.
Implicit Types f g : discrete_fun B.
Instance discrete_fun_equiv : Equiv (discrete_fun B) := λ f g, ∀ x, f x ≡ g x.
- Instance discrete_fun_dist : Dist SI (discrete_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
- Definition discrete_fun_ofe_mixin : OfeMixin SI (discrete_fun B).
+ Instance discrete_fun_dist : Dist (discrete_fun B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
+ Definition discrete_fun_ofe_mixin : OfeMixin (discrete_fun B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
@@ -1576,7 +1575,7 @@ Section discrete_fun.
Next Obligation. intros n c x m p Hm Hp Hmp. by apply (bchain_cauchy n c _ _ Hm Hp Hmp). Qed.
- Global Program Instance discrete_fun_cofe `{∀ x, Cofe (B x)} : Cofe discrete_funO :=
+ Global Program Instance discrete_fun_cofe `{!∀ x, Cofe (B x)} : Cofe discrete_funO :=
{ compl c x := compl (discrete_fun_chain c x); lbcompl n Hn c x := lbcompl Hn (discrete_fun_bchain c x) }.
Next Obligation.
intros ? n c x. by apply conv_compl.
@@ -1606,33 +1605,33 @@ Global Arguments discrete_funO {_ _} _.
Notation "A -d> B" :=
(@discrete_funO _ A (λ _, B)) (at level 99, B at level 200, right associativity).
-Definition discrete_fun_map {SI A} {B1 B2 : A → ofe SI} (f : ∀ x, B1 x → B2 x)
+Definition discrete_fun_map `{SI: indexT} {A} {B1 B2 : A → ofe} (f : ∀ x, B1 x → B2 x)
(g : discrete_fun B1) : discrete_fun B2 := λ x, f _ (g x).
-Lemma discrete_fun_map_ext {SI A} {B1 B2 : A → ofe SI} (f1 f2 : ∀ x, B1 x → B2 x)
+Lemma discrete_fun_map_ext `{SI: indexT} {A} {B1 B2 : A → ofe} (f1 f2 : ∀ x, B1 x → B2 x)
(g : discrete_fun B1) :
(∀ x, f1 x (g x) ≡ f2 x (g x)) → discrete_fun_map f1 g ≡ discrete_fun_map f2 g.
Proof. done. Qed.
-Lemma discrete_fun_map_id {SI A} {B : A → ofe SI} (g : discrete_fun B) :
+Lemma discrete_fun_map_id `{SI: indexT} {A} {B : A → ofe} (g : discrete_fun B) :
discrete_fun_map (λ _, id) g = g.
Proof. done. Qed.
-Lemma discrete_fun_map_compose {SI A} {B1 B2 B3 : A → ofe SI}
+Lemma discrete_fun_map_compose `{SI: indexT} {A} {B1 B2 B3 : A → ofe}
(f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : discrete_fun B1) :
discrete_fun_map (λ x, f2 x ∘ f1 x) g = discrete_fun_map f2 (discrete_fun_map f1 g).
Proof. done. Qed.
-Instance discrete_fun_map_ne {SI A} {B1 B2 : A → ofe SI} (f : ∀ x, B1 x → B2 x) n :
+Global Instance discrete_fun_map_ne `{SI: indexT} {A} {B1 B2 : A → ofe} (f : ∀ x, B1 x → B2 x) n :
(∀ x, Proper (dist n ==> dist n) (f x)) →
Proper (dist n ==> dist n) (discrete_fun_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /discrete_fun_map (Hy x). Qed.
-Definition discrete_funO_map {SI A} {B1 B2 : A → ofe SI} (f : discrete_fun (λ x, B1 x -n> B2 x)) :
+Definition discrete_funO_map `{SI: indexT} {A} {B1 B2 : A → ofe} (f : discrete_fun (λ x, B1 x -n> B2 x)) :
discrete_funO B1 -n> discrete_funO B2 := OfeMor (discrete_fun_map f).
-Instance discrete_funO_map_ne {SI A} {B1 B2 : A → ofe SI} :
+Global Instance discrete_funO_map_ne `{SI: indexT} {A} {B1 B2 : A → ofe} :
NonExpansive (@discrete_funO_map SI A B1 B2).
Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
-Program Definition discrete_funOF {SI C} (F : C → oFunctor SI) : oFunctor SI := {|
+Program Definition discrete_funOF `{SI: indexT} {C} (F : C → oFunctor) : oFunctor := {|
oFunctor_car A B := discrete_funO (λ c, oFunctor_car (F c) A B);
oFunctor_map A1 A2 B1 B2 fg := discrete_funO_map (λ c, oFunctor_map (F c) fg)
|}.
@@ -1651,7 +1650,7 @@ Qed.
Notation "T -d> F" := (@discrete_funOF _ T%type (λ _, F%OF)) : oFunctor_scope.
-Global Instance discrete_funOF_contractive {SI C} (F : C → oFunctor SI) :
+Global Instance discrete_funOF_contractive {SI: indexT} {C} (F : C → oFunctor) :
(∀ c, oFunctorContractive (F c)) → oFunctorContractive (discrete_funOF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
@@ -1659,9 +1658,9 @@ Proof.
Qed.
(** * Constructing isomorphic OFEs *)
-Lemma iso_ofe_mixin {SI} {A : ofe SI} {B: Type} `{!Equiv B, !Dist SI B} (g : B → A)
+Lemma iso_ofe_mixin `{SI: indexT} {A : ofe} {B: Type} `{!Equiv B, !Dist B} (g : B → A)
(g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
- (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) : OfeMixin SI B.
+ (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) : OfeMixin B.
Proof.
split.
- intros y1 y2. rewrite g_equiv. setoid_rewrite g_dist. apply equiv_dist.
@@ -1673,7 +1672,7 @@ Proof.
Qed.
Section iso_cofe_subtype.
- Context {SI} {A B : ofe SI} `{!Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
+ Context `{SI: indexT} {A B : ofe} `{!Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
Let Hgne : NonExpansive g.
Proof. intros n y1 y2. apply g_dist. Qed.
@@ -1694,7 +1693,7 @@ Section iso_cofe_subtype.
End iso_cofe_subtype.
-Lemma iso_cofe_subtype' {SI} {A B : ofe SI} `{Cofe SI A}
+Lemma iso_cofe_subtype' `{SI: indexT} {A B : ofe} `{!Cofe A}
(P : A → Prop) (f : ∀ x, P x → B) (g : B → A)
(Pg : ∀ y, P (g y))
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
@@ -1703,20 +1702,20 @@ Lemma iso_cofe_subtype' {SI} {A B : ofe SI} `{Cofe SI A}
(Hblimit : BoundedLimitPreserving P) : Cofe B.
Proof. apply: (iso_cofe_subtype P f g)=> //; eauto. Qed.
-Definition iso_cofe {SI} {A B : ofe SI} `{!Cofe A} (f : A → B) (g : B → A)
+Definition iso_cofe `{SI: indexT} {A B : ofe} `{!Cofe A} (f : A → B) (g : B → A)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
(gf : ∀ x, g (f x) ≡ x) : Cofe B.
Proof. by apply (iso_cofe_subtype (λ _, True) (λ x _, f x) g). Qed.
(** * Sigma type *)
Section sigma.
- Context {SI} {A : ofe SI} {P : A → Prop}.
+ Context `{SI: indexT} {A : ofe} {P : A → Prop}.
Implicit Types x : sig P.
(* TODO: Find a better place for this Equiv instance. It also
should not depend on A being an OFE. *)
Local Instance sig_equiv : Equiv (sig P) := λ x1 x2, `x1 ≡ `x2.
- Local Instance sig_dist : Dist SI (sig P) := λ n x1 x2, `x1 ≡{n}≡ `x2.
+ Local Instance sig_dist : Dist (sig P) := λ n x1 x2, `x1 ≡{n}≡ `x2.
Definition sig_equiv_alt x y : x ≡ y ↔ `x ≡ `y := reflexivity _.
Definition sig_dist_alt n x y : x ≡{n}≡ y ↔ `x ≡{n}≡ `y := reflexivity _.
@@ -1727,9 +1726,9 @@ Section sigma.
Global Instance proj1_sig_ne : NonExpansive (@proj1_sig _ P).
Proof. by intros n [a Ha] [b Hb] ?. Qed.
- Definition sig_ofe_mixin : OfeMixin SI (sig P).
+ Definition sig_ofe_mixin : OfeMixin (sig P).
Proof. by apply (iso_ofe_mixin proj1_sig). Qed.
- Canonical Structure sigO : ofe SI := Ofe (sig P) sig_ofe_mixin.
+ Canonical Structure sigO : ofe := Ofe (sig P) sig_ofe_mixin.
Global Instance sig_cofe `{!Cofe A, !LimitPreserving P, !BoundedLimitPreserving P} : Cofe sigO.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
@@ -1748,7 +1747,7 @@ equality, while the second component might be any OFE. *)
Section sigT.
Import EqNotations.
- Context {SI} {A : Type} {P : A → ofe SI}.
+ Context `{SI: indexT} {A : Type} {P : A → ofe}.
Implicit Types x : sigT P.
(**
@@ -1758,7 +1757,7 @@ Section sigT.
Unlike in the topos of trees, with (C)OFEs we cannot use step-indexed equality
on the first component.
*)
- Local Instance sigT_dist : Dist SI (sigT P) := λ n x1 x2,
+ Local Instance sigT_dist : Dist (sigT P) := λ n x1 x2,
∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡{n}≡ projT2 x2.
(**
@@ -1783,7 +1782,7 @@ Section sigT.
Definition sigT_dist_proj1 n {x y} : x ≡{n}≡ y → projT1 x = projT1 y := proj1_ex.
Definition sigT_equiv_proj1 {x y} : x ≡ y → projT1 x = projT1 y := λ H, proj1_ex (H zero).
- Definition sigT_ofe_mixin : OfeMixin SI (sigT P).
+ Definition sigT_ofe_mixin : OfeMixin (sigT P).
Proof.
split => // n.
- split; hnf; setoid_rewrite sigT_dist_eq.
@@ -1798,7 +1797,7 @@ Section sigT.
exists eq_refl. by eapply dist_dist_later.
Qed.
- Canonical Structure sigTO : ofe SI := Ofe (sigT P) sigT_ofe_mixin.
+ Canonical Structure sigTO : ofe := Ofe (sigT P) sigT_ofe_mixin.
Lemma sigT_equiv_eq_alt `{!∀ a b : A, ProofIrrel (a = b)} x1 x2 :
x1 ≡ x2 ↔
@@ -1812,10 +1811,10 @@ Section sigT.
Qed.
(** [projT1] is non-expansive and proper. *)
- Global Instance projT1_ne : NonExpansive (projT1 : sigTO → leibnizO SI A).
+ Global Instance projT1_ne : NonExpansive (projT1 : sigTO → leibnizO A).
Proof. solve_proper. Qed.
- Global Instance projT1_proper : Proper ((≡) ==> (≡)) (projT1 : sigTO → leibnizO SI A).
+ Global Instance projT1_proper : Proper ((≡) ==> (≡)) (projT1 : sigTO → leibnizO A).
Proof. apply ne_proper, projT1_ne. Qed.
(** [projT2] is "non-expansive"; the properness lemma [projT2_ne] requires UIP. *)
@@ -1945,9 +1944,9 @@ End sigT.
Global Arguments sigTO {_ _} _.
Section sigTOF.
- Context {SI: indexT} {A : Type}.
+ Context `{SI: indexT} {A : Type}.
- Program Definition sigT_map {P1 P2 : A → ofe SI} :
+ Program Definition sigT_map {P1 P2 : A → ofe} :
discrete_funO (λ a, P1 a -n> P2 a) -n>
sigTO P1 -n> sigTO P2 :=
λne f xpx, existT _ (f _ (projT2 xpx)).
@@ -1959,7 +1958,7 @@ Section sigTOF.
move => ?? n f g Heq [x px] /=. exists eq_refl => /=. apply Heq.
Qed.
- Program Definition sigTOF (F : A → oFunctor SI) : oFunctor SI := {|
+ Program Definition sigTOF (F : A → oFunctor) : oFunctor := {|
oFunctor_car A B := sigTO (λ a, oFunctor_car (F a) A B);
oFunctor_map A1 A2 B1 B2 fg := sigT_map (λ a, oFunctor_map (F a) fg)
|}.
@@ -1982,42 +1981,42 @@ End sigTOF.
Global Arguments sigTOF {_ _} _%OF.
Notation "{ x & P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope.
-Notation "{ x : A & P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.
+Notation "{ x : A & P }" := (@sigTOF _ A%type (λ x, P%OF)) : oFunctor_scope.
(** * Finite COFEs *)
(** In the special case of natural numbers as step-index type, there are no bounded limits. *)
(** This case enables us to get additional COFE instances. *)
(** This is not a class since it should only be used as an easy way of constructing Cofes. *)
-Record FiniteCofe `{FiniteIndex SI} (A : ofe SI) :=
+Record FiniteCofe {SI: indexT} `{!FiniteIndex SI} (A : ofe) :=
{
fin_compl : chain A → A;
conv_fin_compl n c : fin_compl c ≡{n}≡ c n;
}.
Global Arguments fin_compl : simpl never.
-Lemma FiniteIndex_no_limit `{FiniteIndex SI} (n : SI): ¬ index_is_proper_limit n.
+Lemma FiniteIndex_no_limit {SI: indexT} `{Hfin: !FiniteIndex SI} (n : index): ¬ index_is_proper_limit n.
Proof.
intros Hlim.
- destruct Hlim as [Hlim Hnz]. destruct (H n) as [-> | [β ->]]; first by index_contra_solve.
+ destruct Hlim as [Hlim Hnz]. destruct (Hfin n) as [-> | [β ->]]; first by index_contra_solve.
by apply index_succ_not_limit in Hlim.
Qed.
-Program Definition FiniteCofe_lbcompl `{FiniteIndex SI} (A : ofe SI) {Hfin : FiniteCofe A}
- (n : SI) (Hn : index_is_proper_limit n) (c : bchain A n) : A := _.
+Program Definition FiniteCofe_lbcompl `{SI: indexT} `{!FiniteIndex SI} (A : ofe) {Hfin : FiniteCofe A}
+ (n : index) (Hn : index_is_proper_limit n) (c : bchain A n) : A := _.
Next Obligation. intros ?? A Hfin n Hlim. exfalso. by eapply FiniteIndex_no_limit. Qed.
-Program Definition FiniteCofe_is_Cofe `{FiniteIndex SI} {A : ofe SI} (Hfin : FiniteCofe A) : Cofe A :=
+Program Definition FiniteCofe_is_Cofe `{SI: indexT} `{!FiniteIndex SI} {A : ofe} (Hfin : FiniteCofe A) : Cofe A :=
{| compl := fin_compl A Hfin; lbcompl := @FiniteCofe_lbcompl _ _ A Hfin |}.
Next Obligation. intros. apply conv_fin_compl. Qed.
Next Obligation. intros. exfalso. by eapply FiniteIndex_no_limit. Qed.
Next Obligation. intros. exfalso. by eapply FiniteIndex_no_limit. Qed.
-Program Definition Cofe_is_FiniteCofe `{FiniteIndex SI} `{Cofe SI A} : FiniteCofe A := {| fin_compl := compl |}.
+Program Definition Cofe_is_FiniteCofe `{SI: indexT} `{!FiniteIndex SI} `{!Cofe A} : FiniteCofe A := {| fin_compl := compl |}.
Next Obligation. intros; apply conv_compl. Qed.
Section iso_fin_cofe_subtype.
- Context {SI} `{!FiniteIndex SI} {A B : ofe SI} `{!Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
+ Context `{SI: indexT} `{!FiniteIndex SI} {A B : ofe} `{!Cofe A} (P : A → Prop) (f : ∀ x, P x → B) (g : B → A).
Context (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2).
Let Hgne : NonExpansive g.
Proof. intros n y1 y2. apply g_dist. Qed.
@@ -2030,7 +2029,7 @@ Section iso_fin_cofe_subtype.
Next Obligation. intros n c; simpl. apply g_dist. by rewrite gf conv_compl. Qed.
End iso_fin_cofe_subtype.
-Lemma iso_finite_cofe_subtype' `{FiniteIndex SI} {A B : ofe SI} `{Cofe SI A}
+Lemma iso_finite_cofe_subtype' `{SI: indexT} `{!FiniteIndex SI} {A B : ofe} `{!Cofe A}
(P : A → Prop) (f : ∀ x, P x → B) (g : B → A)
(Pg : ∀ y, P (g y))
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
@@ -2038,13 +2037,13 @@ Lemma iso_finite_cofe_subtype' `{FiniteIndex SI} {A B : ofe SI} `{Cofe SI A}
(Hlimit : LimitPreserving P) : Cofe B.
Proof. refine (FiniteCofe_is_Cofe _). apply: (iso_finite_cofe_subtype P f g)=> //; eauto. Qed.
-Definition iso_finite_cofe `{FiniteIndex SI} {A B : ofe SI} `{!Cofe A} (f : A → B) (g : B → A)
+Definition iso_finite_cofe `{SI: indexT} `{!FiniteIndex SI} {A B : ofe} `{!Cofe A} (f : A → B) (g : B → A)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
(gf : ∀ x, g (f x) ≡ x) : Cofe B.
Proof. refine (FiniteCofe_is_Cofe _). by apply (iso_finite_cofe_subtype (λ _, True) (λ x _, f x) g). Qed.
(** * Isomorphisms between OFEs *)
-Record ofe_iso {SI} (A B : ofe SI) := OfeIso {
+Record ofe_iso `{SI: indexT} (A B : ofe) := OfeIso {
ofe_iso_1 : A -n> B;
ofe_iso_2 : B -n> A;
ofe_iso_12 y : ofe_iso_1 (ofe_iso_2 y) ≡ y;
@@ -2057,12 +2056,12 @@ Global Arguments ofe_iso_12 {_ _ _} _ _.
Global Arguments ofe_iso_21 {_ _ _} _ _.
Section ofe_iso.
- Context {SI} {A B : ofe SI}.
+ Context `{SI: indexT} {A B : ofe}.
Local Instance ofe_iso_equiv : Equiv (ofe_iso A B) := λ I1 I2,
ofe_iso_1 I1 ≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡ ofe_iso_2 I2.
- Local Instance ofe_iso_dist : Dist SI (ofe_iso A B) := λ n I1 I2,
+ Local Instance ofe_iso_dist : Dist (ofe_iso A B) := λ n I1 I2,
ofe_iso_1 I1 ≡{n}≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡{n}≡ ofe_iso_2 I2.
Global Instance ofe_iso_1_ne : NonExpansive (ofe_iso_1 (A:=A) (B:=B)).
@@ -2070,9 +2069,9 @@ Section ofe_iso.
Global Instance ofe_iso_2_ne : NonExpansive (ofe_iso_2 (A:=A) (B:=B)).
Proof. by destruct 1. Qed.
- Lemma ofe_iso_ofe_mixin : OfeMixin SI (ofe_iso A B).
+ Lemma ofe_iso_ofe_mixin : OfeMixin (ofe_iso A B).
Proof. by apply (iso_ofe_mixin (λ I, (ofe_iso_1 I, ofe_iso_2 I))). Qed.
- Canonical Structure ofe_isoO : ofe SI := Ofe (ofe_iso A B) ofe_iso_ofe_mixin.
+ Canonical Structure ofe_isoO : ofe := Ofe (ofe_iso A B) ofe_iso_ofe_mixin.
(* ≡ is not BoundedLimitPreserving, so we do not get this Cofe instance in the general case.
However, for finite Cofes this works. *)
@@ -2091,25 +2090,25 @@ Section ofe_iso.
Qed.
End ofe_iso.
-Global Arguments ofe_isoO : clear implicits.
+Global Arguments ofe_isoO {_} _ _.
-Program Definition iso_ofe_refl {SI: indexT} {A: ofe SI} : ofe_iso A A := OfeIso cid cid _ _.
+Program Definition iso_ofe_refl `{SI: indexT} {A: ofe} : ofe_iso A A := OfeIso cid cid _ _.
Solve Obligations with done.
-Definition iso_ofe_sym {SI: indexT} {A B : ofe SI} (I : ofe_iso A B) : ofe_iso B A :=
+Definition iso_ofe_sym `{SI: indexT} {A B : ofe} (I : ofe_iso A B) : ofe_iso B A :=
OfeIso (ofe_iso_2 I) (ofe_iso_1 I) (ofe_iso_21 I) (ofe_iso_12 I).
-Global Instance iso_ofe_sym_ne {SI: indexT} {A B : ofe SI} : NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
+Global Instance iso_ofe_sym_ne {SI: indexT} {A B : ofe} : NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
-Program Definition iso_ofe_trans {SI: indexT} {A B C : ofe SI}
+Program Definition iso_ofe_trans `{SI: indexT} {A B C : ofe}
(I : ofe_iso A B) (J : ofe_iso B C) : ofe_iso A C :=
OfeIso (ofe_iso_1 J ◎ ofe_iso_1 I) (ofe_iso_2 I ◎ ofe_iso_2 J) _ _.
Next Obligation. intros SI A B C I J z; simpl. by rewrite !ofe_iso_12. Qed.
Next Obligation. intros SI A B C I J z; simpl. by rewrite !ofe_iso_21. Qed.
-Global Instance iso_ofe_trans_ne {SI : indexT} {A B C : ofe SI} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (C:=C)).
+Global Instance iso_ofe_trans_ne `{SI : indexT} {A B C : ofe} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (C:=C)).
Proof. intros n I1 I2 [] J1 J2 []; split; simpl; by f_equiv. Qed.
-Program Definition iso_ofe_cong {SI : indexT} (F : oFunctor SI) `{!Cofe A, !Cofe B}
+Program Definition iso_ofe_cong `{SI : indexT} (F : oFunctor) `{!Cofe A, !Cofe B}
(I : ofe_iso A B) : ofe_iso (oFunctor_apply F A) (oFunctor_apply F B) :=
OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
(oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
@@ -2123,10 +2122,10 @@ Next Obligation.
apply equiv_dist=> n.
apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
Qed.
-Global Instance iso_ofe_cong_ne {SI : indexT} (F : oFunctor SI) `{!Cofe A, !Cofe B} :
+Global Instance iso_ofe_cong_ne `{SI : indexT} (F : oFunctor) `{!Cofe A, !Cofe B} :
NonExpansive (iso_ofe_cong F (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
-Global Instance iso_ofe_cong_contractive {SI : indexT} (F : oFunctor SI) `{!Cofe A, !Cofe B} :
+Global Instance iso_ofe_cong_contractive `{SI : indexT} (F : oFunctor) `{!Cofe A, !Cofe B} :
oFunctorContractive F → Contractive (iso_ofe_cong F (A:=A) (B:=B)).
Proof.
intros ? n I1 I2 HI; split; simpl.
diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index 449fb980..41e0e54d 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -15,36 +15,36 @@ From iris.prelude Require Import options.
[own γ (q1 + q2)] where [q1] and [q2] are fractions, we actually get
[own γ q1] and [own γ q2] instead of [own γ ((q1 + q2)/2)] twice.
*)
-Class IsOp {SI} {A : cmra SI} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
+Class IsOp `{SI: indexT} {A : cmra} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
Global Arguments is_op {_ _} _ _ _ {_}.
Global Hint Mode IsOp - + - - - : typeclass_instances.
-Global Instance is_op_op {SI} {A : cmra SI} (a b : A) : IsOp (a ⋅ b) a b | 100.
+Global Instance is_op_op `{SI: indexT} {A : cmra} (a b : A) : IsOp (a ⋅ b) a b | 100.
Proof. by rewrite /IsOp. Qed.
-Class IsOp' {SI} {A : cmra SI} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
+Class IsOp' `{SI: indexT} {A : cmra} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
Global Hint Mode IsOp' - + ! - - : typeclass_instances.
Global Hint Mode IsOp' - + - ! ! : typeclass_instances.
-Class IsOp'LR {SI} {A : cmra SI} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
-Existing Instance is_op_lr | 0.
+Class IsOp'LR `{SI: indexT} {A : cmra} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
+Global Existing Instance is_op_lr | 0.
Global Hint Mode IsOp'LR - + ! - - : typeclass_instances.
-Global Instance is_op_lr_op {SI} {A : cmra SI} (a b : A) : IsOp'LR (a ⋅ b) a b | 0.
+Global Instance is_op_lr_op `{SI: indexT} {A : cmra} (a b : A) : IsOp'LR (a ⋅ b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
(* FromOp *)
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
-Global Instance is_op_pair {SI} {A B : cmra SI} (a b1 b2 : A) (a' b1' b2' : B) :
+Global Instance is_op_pair `{SI: indexT} {A B : cmra} (a b1 b2 : A) (a' b1' b2' : B) :
IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
-Global Instance is_op_pair_core_id_l {SI} {A B : cmra SI} (a : A) (a' b1' b2' : B) :
+Global Instance is_op_pair_core_id_l `{SI: indexT} {A B : cmra} (a : A) (a' b1' b2' : B) :
CoreId a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-Global Instance is_op_pair_core_id_r {SI} {A B : cmra SI} (a b1 b2 : A) (a' : B) :
+Global Instance is_op_pair_core_id_r `{SI: indexT} {A B : cmra} (a b1 b2 : A) (a' : B) :
CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
-Global Instance is_op_Some {SI} {A : cmra SI} (a : A) b1 b2 :
+Global Instance is_op_Some `{SI: indexT} {A : cmra} (a : A) b1 b2 :
IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
diff --git a/theories/algebra/truncation.v b/theories/algebra/truncation.v
index 6bf74b73..da113dc0 100644
--- a/theories/algebra/truncation.v
+++ b/theories/algebra/truncation.v
@@ -5,14 +5,14 @@ Set Primitive Projections.
(** different notions of limit uniqueness *)
-Class BcomplUniqueLim {SI : indexT} (A : ofe SI) `{Cofe SI A} :=
- cofe_unique_lim (α : SI) Hα (c d : bchain A α) :
+Class BcomplUniqueLim `{SI : indexT} (A : ofe) `{!Cofe A} :=
+ cofe_unique_lim (α : index) Hα (c d : bchain A α) :
(∀ β (Hβ : β ≺ α), c β Hβ ≡{β}≡ d β Hβ) → lbcompl Hα c ≡{α}≡ lbcompl Hα d.
Global Hint Mode BcomplUniqueLim - ! ! : typeclass_instances.
Section pi.
Import ProofIrrelevance.
- Lemma index_dec_limit_pi {SI : indexT} (α : SI) :
+ Lemma index_dec_limit_pi `{SI : indexT} (α : index) :
∀ (Hlim : index_is_limit α), index_dec_limit α = inr Hlim.
Proof.
intros Hlim. destruct index_dec_limit as [[β ->] | H].
@@ -20,7 +20,7 @@ Section pi.
- by rewrite (proof_irrelevance _ H Hlim).
Qed.
- Lemma cofe_unique_bcompl {SI : indexT} (A : ofe SI) {Hc: Cofe A} {Hunique: BcomplUniqueLim A}:
+ Lemma cofe_unique_bcompl `{SI : indexT} (A : ofe) `{Hc: !Cofe A} {Hunique: BcomplUniqueLim A}:
∀ α Hα (c d : bchain A α), index_is_limit α →
(∀ β (Hβ : β ≺ α), c β Hβ ≡{β}≡ d β Hβ) → bcompl Hα c ≡{α}≡ bcompl Hα d.
Proof.
@@ -32,16 +32,16 @@ End pi.
(** OFEs truncated at a stepindex α*)
(* Equality at ordinals above α is fully determined by equality at α *)
-Class Truncated {SI : indexT} {A : ofe SI} (α : SI) (x : A) := truncated y β: α ⪯ β → x ≡{α}≡ y ↔ x ≡{β}≡ y.
+Class Truncated `{SI : indexT} {A : ofe} (α : index) (x : A) := truncated y β: α ⪯ β → x ≡{α}≡ y ↔ x ≡{β}≡ y.
Global Arguments truncated {_ _} _ _ {_ } _ _ _.
Global Hint Mode Truncated - + ! ! : typeclass_instances.
Global Instance : Params (@Truncated) 2 := {}.
-Class OfeTruncated {SI : indexT} (A : ofe SI) (α : SI) := ofe_truncated_truncated (x : A) :> Truncated α x.
+Class OfeTruncated `{SI : indexT} (A : ofe) (α : index) := ofe_truncated_truncated (x : A) :> Truncated α x.
Global Hint Mode OfeTruncated - + - : typeclass_instances.
Global Arguments OfeTruncated {_} _ _.
-Lemma ofe_truncated_equiv {SI : indexT} (A : ofe SI) (α : SI) {H : OfeTruncated A α} :
+Lemma ofe_truncated_equiv `{SI : indexT} (A : ofe) (α : index) {H : OfeTruncated A α} :
∀ (x y : A), x ≡ y ↔ x ≡{α}≡ y.
Proof.
intros x y. rewrite equiv_dist. split.
@@ -51,7 +51,7 @@ Proof.
+ by eapply dist_mono'.
Qed.
-Lemma ofe_truncated_dist {SI : indexT} (A : ofe SI) (α : SI) {H : OfeTruncated A α}:
+Lemma ofe_truncated_dist `{SI : indexT} (A : ofe) (α : index) `{H : !OfeTruncated A α}:
∀ (x y : A) β, x ≡{β}≡ y ↔ x ≡{index_min β α}≡ y.
Proof.
intros x y β. split; intros Heq.
@@ -60,13 +60,13 @@ Proof.
by eapply H.
Qed.
-Global Instance discrete_is_truncated {SI : indexT} (A : ofe SI) (α : SI) (H: OfeDiscrete A) : OfeTruncated A α.
+Global Instance discrete_is_truncated `{SI : indexT} (A : ofe) (α : index) `(H: !OfeDiscrete A) : OfeTruncated A α.
Proof.
intros x y β Hα. split; intros H0.
all: apply equiv_dist, ofe_discrete_discrete; (eapply dist_mono'; [apply H0 | apply index_zero_minimum]).
Qed.
-Global Instance ofe_mor_truncated {SI: indexT} {A B : ofe SI} α {H : OfeTruncated B α} : OfeTruncated (A -n> B) α.
+Global Instance ofe_mor_truncated `{SI: indexT} {A B : ofe} α `{H : !OfeTruncated B α} : OfeTruncated (A -n> B) α.
Proof.
intros f g β Hβ. split; intros Heq x.
- apply ofe_truncated_truncated; auto.
@@ -76,19 +76,19 @@ Qed.
(** Truncatable OFEs -- an OFE A is truncatable if, for every ordinal α, it admits a truncation [A]_{α} (again an OFE)
and a bounded isomorphism (equality up to α) between A and [A]_{α}
*)
-Definition boundedInverse {SI: indexT} {X1 X2: ofe SI} (f : X2 -n> X1) (g : X1 -n> X2) (α : SI) :=
+Definition boundedInverse `{SI: indexT} {X1 X2: ofe} (f : X2 -n> X1) (g : X1 -n> X2) (α : index) :=
f ◎ g ≡{α}≡ cid ∧ g ◎ f ≡{α}≡ cid.
-Lemma boundedInverse_antimono {SI : indexT} {X1 X2 : ofe SI} (f : X2 -n> X1) (g : X1 -n> X2) (α β : SI) :
+Lemma boundedInverse_antimono `{SI : indexT} {X1 X2 : ofe} (f : X2 -n> X1) (g : X1 -n> X2) (α β : index) :
α ⪯ β → boundedInverse f g β → boundedInverse f g α.
Proof. intros Hle [H1 H2]. split; eapply dist_mono'; eauto. Qed.
-Class Truncatable {SI : indexT} (A : ofe SI):=
+Class Truncatable `{SI : indexT} (A : ofe):=
{
- ofe_trunc_car (α : SI) : ofe SI;
- ofe_trunc_truncated (α : SI) : OfeTruncated (ofe_trunc_car α) α;
- ofe_trunc_truncate (α : SI) : A -n> ofe_trunc_car α;
- ofe_trunc_expand (α : SI) : ofe_trunc_car α -n> A;
- ofe_trunc_inverse (α : SI) : boundedInverse (ofe_trunc_truncate α) (ofe_trunc_expand α) α;
+ ofe_trunc_car (α : index) : ofe;
+ ofe_trunc_truncated (α : index) : OfeTruncated (ofe_trunc_car α) α;
+ ofe_trunc_truncate (α : index) : A -n> ofe_trunc_car α;
+ ofe_trunc_expand (α : index) : ofe_trunc_car α -n> A;
+ ofe_trunc_inverse (α : index) : boundedInverse (ofe_trunc_truncate α) (ofe_trunc_expand α) α;
}.
Global Hint Mode Truncatable - - : typeclass_instances.
Global Arguments ofe_trunc_car {_ _ _} _.
@@ -100,7 +100,7 @@ Notation "'⌊' a '⌋_{' α '}'" := (ofe_trunc_truncate α a) (format "'⌊' a
Notation "'⌈' a '⌉_{' α '}'" := (ofe_trunc_expand α a) (format "'⌈' a '⌉_{' α '}'").
Section truncatable_props.
- Context {SI : indexT} {A : ofe SI} {Htrunc : Truncatable A}.
+ Context `{SI : indexT} {A : ofe} `{Htrunc : !Truncatable A}.
Lemma ofe_trunc_truncate_expand_id {α} :
ofe_trunc_truncate α ◎ ofe_trunc_expand α ≡ cid.
Proof. intros x. cbn. eapply ofe_truncated_equiv; first apply Htrunc. apply ofe_trunc_inverse. Qed.
@@ -108,11 +108,11 @@ Section truncatable_props.
Lemma ofe_trunc_expand_truncate_id {α} : ofe_trunc_expand α ◎ ofe_trunc_truncate α ≡{α}≡ cid.
Proof. apply ofe_trunc_inverse. Qed.
- Global Instance Truncatable_truncated (α : SI) : OfeTruncated (ofe_trunc_car (A := A) α) α
+ Global Instance Truncatable_truncated (α : index) : OfeTruncated (ofe_trunc_car (A := A) α) α
:= (@ofe_trunc_truncated _ A _ α).
Section truncatable_cofe.
- Context (γ: SI) {Ha : Cofe A}.
+ Context (γ: index) {Ha : Cofe A}.
Program Definition trunc_chain (c : chain ([A]_{γ})) : chain A :=
mkchain _ A (λ α, ofe_trunc_expand γ (c α)) _.
@@ -155,17 +155,17 @@ Section truncatable_props.
End truncatable_props.
Section truncatable.
- Context {SI : indexT} .
+ Context `{SI : indexT} .
- Program Definition trunc_map {A : ofe SI} {HtruncA : Truncatable A} {B : ofe SI} {HtruncB : Truncatable B}
- (α β : SI) : (A -n> B) -n> ([A]_{α} -n> [B]_{β}) := λne f, ofe_trunc_truncate β ◎ f ◎ ofe_trunc_expand α.
+ Program Definition trunc_map {A : ofe} {HtruncA : Truncatable A} {B : ofe} {HtruncB : Truncatable B}
+ (α β : index) : (A -n> B) -n> ([A]_{α} -n> [B]_{β}) := λne f, ofe_trunc_truncate β ◎ f ◎ ofe_trunc_expand α.
Next Obligation.
intros A HtrucA B HtruncB α β γ f g Heq.
apply ccompose_ne; [ | reflexivity ]. apply ccompose_ne; auto.
Qed.
- Context {A : ofe SI} {HtruncA : Truncatable A}.
- Context {B : ofe SI} {HtruncB : Truncatable B}.
+ Context {A : ofe} {HtruncA : Truncatable A}.
+ Context {B : ofe} {HtruncB : Truncatable B}.
Lemma trunc_map_inv (f : A -n> B) (g : B -n> A) α β:
α ⪯ β → boundedInverse f g α → boundedInverse (trunc_map α β f) (trunc_map β α g) α.
Proof.
@@ -183,7 +183,7 @@ Section truncatable.
apply equiv_dist, ofe_trunc_truncate_expand_id.
Qed.
- Context {C : ofe SI} {HtruncC : Truncatable C}.
+ Context {C : ofe} {HtruncC : Truncatable C}.
Lemma trunc_map_compose (f : A -n> B) (g : B -n> C) α β γ :
trunc_map α β (g ◎ f) ≡{γ}≡ trunc_map γ β g ◎ trunc_map α γ f.
Proof.
@@ -196,7 +196,7 @@ End truncatable.
(** a more elementary property than Truncatable. Essentially, proto_trunc α chooses a unique representative of each equivalence class of ≡{α}≡ *)
-Class ProtoTruncatable {SI : indexT} (A : ofe SI) :=
+Class ProtoTruncatable `{SI : indexT} (A : ofe) :=
{
proto_trunc α : A -n> A;
proto_compat α (x y : A) : x ≡{α}≡ y → proto_trunc α x ≡ proto_trunc α y;
@@ -205,7 +205,7 @@ Class ProtoTruncatable {SI : indexT} (A : ofe SI) :=
Global Hint Mode ProtoTruncatable - + : typeclass_instances.
Section proto.
- Context {SI : indexT} (A : ofe SI) {Hcofe : Cofe A} {Htrunc : ProtoTruncatable A}.
+ Context `{SI : indexT} (A : ofe) `{Hcofe : !Cofe A} {Htrunc : ProtoTruncatable A}.
(** basic facts about proto truncatability *)
Fact proto_trunc_idempotent (a : A) α: proto_trunc α (proto_trunc α a) ≡ proto_trunc α a.
@@ -221,25 +221,25 @@ End proto.
(** We show that ProtoTruncatable implies Truncatable *)
(* For defining the truncated types, we wrap the OFE A in an inductive in order to not confuse typeclass inference when defining a different equivalence on it. *)
-Inductive trunc_truncation {SI : indexT} (A : ofe SI) (β : SI) := trunc_truncationC (a : A).
+Inductive trunc_truncation `{SI : indexT} (A : ofe) (β : index) := trunc_truncationC (a : A).
Section proto_truncatable.
- Context {SI : indexT} (A : ofe SI) (Htrunc : ProtoTruncatable A).
+ Context `{SI : indexT} (A : ofe) (Htrunc : ProtoTruncatable A).
Section trunc_def.
- Context (α : SI).
+ Context (α : index).
Local Definition truncembed (a : trunc_truncation A α): A := match a with trunc_truncationC _ _ a => a end.
Instance trunc_truncation_equiv : Equiv (trunc_truncation A α) := λ a b, proto_trunc α (truncembed a) ≡ proto_trunc α (truncembed b).
Lemma trunc_truncation_equiv_unfold a b : a ≡ b ↔ proto_trunc α (truncembed a) ≡ proto_trunc α (truncembed b).
Proof. tauto. Qed.
- Instance trunc_truncation_dist : Dist SI (trunc_truncation A α) :=
+ Instance trunc_truncation_dist : Dist (trunc_truncation A α) :=
λ n a b, proto_trunc α (truncembed a) ≡{n}≡ proto_trunc α (truncembed b).
Lemma trunc_truncation_dist_unfold a b n : a ≡{n}≡ b ↔ proto_trunc α (truncembed a) ≡{n}≡ proto_trunc α (truncembed b).
Proof. tauto. Qed.
- Definition trunc_truncation_ofe_mixin : OfeMixin SI (trunc_truncation A α).
+ Definition trunc_truncation_ofe_mixin : OfeMixin (trunc_truncation A α).
Proof.
split.
- setoid_rewrite trunc_truncation_dist_unfold. setoid_rewrite trunc_truncation_equiv_unfold.
@@ -250,7 +250,7 @@ Section proto_truncatable.
intros a b c -> ->. auto.
- setoid_rewrite trunc_truncation_dist_unfold. intros α' β x y Heq Hlt. eauto using dist_mono.
Qed.
- Canonical Structure tcar_truncO : ofe SI := Ofe (trunc_truncation A α) trunc_truncation_ofe_mixin.
+ Canonical Structure tcar_truncO : ofe := Ofe (trunc_truncation A α) trunc_truncation_ofe_mixin.
Program Definition tcar_trunc : A -n> tcar_truncO := λne a, trunc_truncationC A α a.
Next Obligation.
@@ -296,8 +296,8 @@ Require Coq.Logic.Classical.
Require Coq.Logic.FunctionalExtensionality.
Require Coq.Logic.PropExtensionality.
Section classical_truncation.
- Context {SI : indexT}.
- Context (A : ofe SI).
+ Context `{SI : indexT}.
+ Context (A : ofe).
(** First we show that we can get a "truncation" operation for arbitrary decidable equivalence relations.
We later instantiate this with dist and dist_later *)
@@ -366,7 +366,7 @@ Section classical_truncation.
Lemma dec_dist α (x y : A) : { x ≡{α}≡ y} + {~ x ≡{α}≡ y}.
Proof. apply binary_choice. apply classic. Qed.
- Program Definition trunc (α : SI) := λne a, choose_witness (dist α) (dec_dist α) a.
+ Program Definition trunc (α : index) := λne a, choose_witness (dist α) (dec_dist α) a.
Next Obligation.
intros α β a b Heq.
destruct (index_le_lt_dec α β) as [H1 | H1].
@@ -389,7 +389,7 @@ Section classical_truncation.
Lemma dec_dist_later α (x y : A) : { dist_later α x y} + {¬ dist_later α x y}.
Proof. apply binary_choice. apply classic. Qed.
- Program Definition trunc_dist_later (α : SI) := λne a, choose_witness (dist_later α) (dec_dist_later α) a.
+ Program Definition trunc_dist_later (α : index) := λne a, choose_witness (dist_later α) (dec_dist_later α) a.
Next Obligation.
intros α β a b Heq.
destruct (index_le_lt_dec α β) as [H1 | H1].
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 4e4a6fbd..839beb7f 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -6,18 +6,18 @@ From iris.prelude Require Import options.
make the following hold:
x ~~> P → Some c ~~> Some P
*)
-Definition cmra_updateP {SI: indexT} {A : cmra SI} (x : A) (P : A → Prop) := ∀ n mz,
+Definition cmra_updateP `{SI: indexT} {A : cmra} (x : A) (P : A → Prop) := ∀ n mz,
✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
Global Instance: Params (@cmra_updateP) 1 := {}.
Infix "~~>:" := cmra_updateP (at level 70).
-Definition cmra_update {SI: indexT} {A : cmra SI} (x y : A) := ∀ n mz,
+Definition cmra_update `{SI: indexT} {A : cmra} (x y : A) := ∀ n mz,
✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
Infix "~~>" := cmra_update (at level 70).
Global Instance: Params (@cmra_update) 1 := {}.
Section updates.
-Context {SI: indexT} {A : cmra SI}.
+Context `{SI: indexT} {A : cmra}.
Implicit Types x y : A.
Global Instance cmra_updateP_proper :
@@ -129,7 +129,7 @@ End updates.
(** * Transport *)
Section cmra_transport.
- Context {SI: indexT} {A B : cmra SI} (H : A = B).
+ Context `{SI: indexT} {A B : cmra} (H : A = B).
Notation T := (cmra_transport H).
Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
@@ -141,7 +141,7 @@ End cmra_transport.
(** * Isomorphism *)
Section iso_cmra.
- Context {SI: indexT} {A B : cmra SI} (f : A → B) (g : B → A).
+ Context `{SI: indexT} {A B : cmra} (f : A → B) (g : B → A).
Lemma iso_cmra_updateP (P : B → Prop) (Q : A → Prop) y
(gf : ∀ x, g (f x) ≡ x)
@@ -171,7 +171,7 @@ End iso_cmra.
(** * Product *)
Section prod.
- Context {SI: indexT} {A B : cmra SI}.
+ Context `{SI: indexT} {A B : cmra}.
Implicit Types x : A * B.
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
@@ -194,7 +194,7 @@ End prod.
(** * Option *)
Section option.
- Context {SI: indexT} {A : cmra SI}.
+ Context `{SI: indexT} {A : cmra}.
Implicit Types x y : A.
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
diff --git a/theories/algebra/wf_IR.v b/theories/algebra/wf_IR.v
index b3582037..09767491 100644
--- a/theories/algebra/wf_IR.v
+++ b/theories/algebra/wf_IR.v
@@ -109,13 +109,13 @@ End IR.
(** we now specialize this construction to stepindices *)
Section IR_wf_index.
Variable (SI : indexT).
- Variable (A : ∀ (P : SI → Prop), Type).
+ Variable (A : ∀ (P : index → Prop), Type).
Variable (A_agree : ∀ {P1 P2}, A P1 → A P2 → Prop).
- Variable (A_agree_transitive : ∀ (P0 P1 P2 : SI → Prop) A0 A1 A2, (∀ γ, P0 γ → P2 γ → P1 γ)
+ Variable (A_agree_transitive : ∀ (P0 P1 P2 : index → Prop) A0 A1 A2, (∀ γ, P0 γ → P2 γ → P1 γ)
→ @A_agree P0 P1 A0 A1 → @A_agree P1 P2 A1 A2 → @A_agree P0 P2 A0 A2).
Variable (A_agree_symmetric : ∀ P0 P1 A0 A1, @A_agree P0 P1 A0 A1 → @A_agree P1 P0 A1 A0).
- Implicit Type (P : SI → Prop).
+ Implicit Type (P : index → Prop).
(* we can merge previous approximations coherently *)
Variable (step_merge : ∀ P (IH : ∀ x, P x → A (λ y, y ⪯ x)), (∀ x0 x1 H0 H1, A_agree (IH x0 H0) (IH x1 H1)) → A P).
@@ -130,7 +130,7 @@ Section IR_wf_index.
Variable (step_agree : ∀ x IH, A_agree IH (step x IH) ).
Variable (step_preserve : ∀ x IH1 IH2, A_agree IH1 IH2 → A_agree (step x IH1) (step x IH2)).
- Lemma existT_index_inj2 (p : SI → Type) (x : SI) (H1 H2 : p x) : existT x H1 = existT x H2 → H1 = H2.
+ Lemma existT_index_inj2 (p : index → Type) (x : index) (H1 H2 : p x) : existT x H1 = existT x H2 → H1 = H2.
Proof.
apply inj_pair2_eq_dec. apply index_eq_dec.
Qed.
@@ -141,8 +141,8 @@ Section IR_wf_index.
- by exact (@A_agree).
- by apply step_merge.
- by exact step.
- - apply SI.
- - apply SI.
+ - apply index_lt_wf.
+ - apply _.
- apply existT_index_inj2.
- intros x1 x2. destruct (index_le_lt_dec x1 x2) as [H1 | H1].
+ by left.
@@ -161,10 +161,10 @@ End IR_wf_index.
Section IR_transfinite_index_cons.
Variable (SI : indexT).
- Variable (A : ∀ (P : SI → Prop), Type).
+ Variable (A : ∀ (P : index → Prop), Type).
Variable (A_agree : ∀ {P1 P2}, A P1 → A P2 → Prop).
Variable (A_agree_trivial : ∀ P1 P2 (A1 : A P1) (A2 : A P2), (∀ γ, P1 γ → P2 γ → False) → A_agree A1 A2).
- Variable (A_agree_transitive : ∀ (P0 P1 P2 : SI → Prop) A0 A1 A2, (∀ γ, P0 γ → P2 γ → P1 γ)
+ Variable (A_agree_transitive : ∀ (P0 P1 P2 : index → Prop) A0 A1 A2, (∀ γ, P0 γ → P2 γ → P1 γ)
→ @A_agree P0 P1 A0 A1 → @A_agree P1 P2 A1 A2 → @A_agree P0 P2 A0 A2).
Variable (A_agree_symmetric : ∀ P0 P1 A0 A1, @A_agree P0 P1 A0 A1 → @A_agree P1 P0 A1 A0).
Variable (A_agree_reflexive : ∀ P A, @A_agree P P A A).
@@ -181,7 +181,7 @@ Section IR_transfinite_index_cons.
E_agree γ ap0 ap1 ext0 ext1 H
→ A_agree (extend γ ap0 ext0 succ_or_limit) (extend γ ap1 ext1 succ_or_limit)).
- Implicit Type (P : SI → Prop).
+ Implicit Type (P : index → Prop).
(** we can merge previous approximations coherently *)
Variable (step_merge : ∀ P (IH : ∀ x, P x → A (λ y, y ⪯ x)), (∀ x0 x1 H0 H1, A_agree (IH x0 H0) (IH x1 H1)) → A P).
@@ -201,8 +201,8 @@ Section IR_transfinite_index_cons.
E_agree (succ β) IH0 IH1 (succ_step β IH0) (succ_step β IH1) H).
(** limit case *)
- Variable (limit_step : ∀ (β : limit_idx SI) (IH : A (λ y, y ≺ β)), E β IH).
- Variable (limit_extension_coherent : ∀ (β : limit_idx SI) IH0 IH1 (H : A_agree IH0 IH1),
+ Variable (limit_step : ∀ (β : limit_idx) (IH : A (λ y, y ≺ β)), E β IH).
+ Variable (limit_extension_coherent : ∀ (β : limit_idx) IH0 IH1 (H : A_agree IH0 IH1),
E_agree β IH0 IH1 (limit_step β IH0) (limit_step β IH1) H).
diff --git a/theories/stepindex/existential_properties.v b/theories/stepindex/existential_properties.v
index bfa3c142..e61eec7b 100644
--- a/theories/stepindex/existential_properties.v
+++ b/theories/stepindex/existential_properties.v
@@ -2,7 +2,7 @@ From iris.stepindex Require Export stepindex.
Polymorphic Class TypeExistentialProperty@{i} (X: Type@{i}) (SI: indexT) : Type :=
- can_commute_exists (P : X → SI → Prop) :
+ can_commute_exists (P : X → index → Prop) :
(∀ x a b, a ≺ b → P x b → P x a)
→ (∀ a, ∃ x, P x a)
→ ∃ x, ∀ a, P x a.
@@ -15,7 +15,7 @@ Notation FiniteExistential := (TypeExistentialProperty bool).
Notation CountableExistential := (TypeExistentialProperty nat).
Class FiniteBoundedExistential (SI: indexT) :=
- can_commute_fin_bounded_exists (P: bool → SI → Prop) c:
+ can_commute_fin_bounded_exists (P: bool → index → Prop) c:
(∀ x a b, a ≺ b → P x b → P x a) →
(∀ a, a ≺ c → ∃ x, P x a) → (∃ x, ∀ a, a ≺ c → P x a).
@@ -54,17 +54,6 @@ Proof.
destruct (Hsome b) as [[] ?]; auto. exfalso. apply HP; eauto.
Qed.
-Global Instance fininte_bounded_existential_nat: FiniteBoundedExistential natI.
-Proof.
- intros P [|n] Hdown Hex.
- - exists true. simpl. intros ?; lia.
- - destruct (Hex n) as [x HP]; first done.
- exists x. simpl; intros m Hm.
- assert (m = n ∨ m < n) as [->|] by lia; eauto.
-Qed.
-
-
-
diff --git a/theories/stepindex/stepindex.v b/theories/stepindex/stepindex.v
index a5a83182..5f1c5f82 100644
--- a/theories/stepindex/stepindex.v
+++ b/theories/stepindex/stepindex.v
@@ -14,89 +14,88 @@ Structure IndexMixin {A} {R: A → A → Prop} {zero: A} {succ: A → A} :=
}.
Arguments IndexMixin : clear implicits.
-Structure indexT :=
+Class indexT :=
IndexT {
- index_car :> Type;
- index_lt : relation index_car;
- index_zero : index_car;
- index_succ : index_car → index_car;
- index_mixin :> IndexMixin index_car index_lt index_zero index_succ;
+ index : Type;
+ index_lt : relation index;
+ index_zero : index;
+ index_succ : index → index;
+ index_mixin : IndexMixin index index_lt index_zero index_succ;
}.
-Notation "(≺)" := (index_lt _).
-Notation "(≻)" := (flip (index_lt _)).
+Notation "(≺)" := (index_lt).
+Notation "(≻)" := (flip (index_lt)).
-Notation zero := (index_zero _).
-Notation succ α := (index_succ _ α).
-Notation "α ≺ β" := (index_lt _ α β) (at level 80).
+Notation zero := (index_zero).
+Notation succ α := (index_succ α).
+Notation "α ≺ β" := (index_lt α β) (at level 80).
-Polymorphic Definition index_le (SI : indexT) : relation SI := rc (index_lt SI).
-Notation "(⪯)" := (index_le _).
-Notation "α ⪯ β" := (index_le _ α β) (at level 80).
+Polymorphic Definition index_le `{SI : indexT} : relation index := rc (index_lt).
+Notation "(⪯)" := (index_le).
+Notation "α ⪯ β" := (index_le α β) (at level 80).
-Instance index_le_refl {SI : indexT} : Reflexive (@index_le SI) := _.
-Instance index_lt_le_subrel {SI : indexT}: subrelation (@index_lt SI) (@index_le SI) := _.
-Lemma index_le_refl_auto {SI : indexT} (α β : SI) (H : α = β): α ⪯ β.
+Global Instance index_le_refl `{SI : indexT} : Reflexive (index_le) := _.
+Global Instance index_lt_le_subrel `{SI : indexT}: subrelation (index_lt) (index_le) := _.
+Lemma index_le_refl_auto `{SI : indexT} (α β : index) (H : α = β): α ⪯ β.
Proof. rewrite H. apply index_le_refl. Qed.
Global Hint Extern 1 (?a ⪯ ?a) => apply index_le_refl : core.
Global Hint Extern 2 (?a ⪯ ?b) => apply index_le_refl_auto : core.
Global Hint Extern 1 (?a ⪯ ?b) => apply index_lt_le_subrel : core.
-Lemma index_le_eq_or_lt {SI : indexT} (α β : SI) : α ⪯ β → α = β ∨ α ≺ β.
+Lemma index_le_eq_or_lt `{SI : indexT} (α β : index) : α ⪯ β → α = β ∨ α ≺ β.
Proof. intros [H | H]; auto. Qed.
Section index_laws.
- Context {SI : indexT}.
- Global Instance index_lt_trans : Transitive (index_lt SI).
- Proof. eapply index_mixin_lt_trans, SI. Qed.
- Lemma index_lt_wf : wf (index_lt SI).
- Proof. eapply index_mixin_lt_wf, SI. Qed.
- Lemma index_lt_eq_lt_dec (α β : SI) : (α ≺ β) + (α = β) + (β ≺ α).
- Proof. eapply index_mixin_lt_strict_total, SI. Qed.
- Lemma index_zero_least : nf (flip (index_lt SI)) zero.
- Proof. eapply index_mixin_zero_least, SI. Qed.
- Lemma index_succ_greater (α : SI) : α ≺ succ α.
- Proof. eapply index_mixin_succ_greater, SI. Qed.
- Lemma index_succ_least (α β : SI) : α ≺ β → succ α ⪯ β.
- Proof. eapply index_mixin_succ_least, SI. Qed.
- Lemma index_dec_limit (α: SI) : { β | α = succ β } + (∀ β, β ≺ α → succ β ≺ α).
- Proof. eapply index_mixin_dec_limit, SI. Qed.
+ Context `{SI : indexT}.
+ Global Instance index_lt_trans : Transitive (index_lt).
+ Proof. eapply index_mixin_lt_trans, index_mixin. Qed.
+ Lemma index_lt_wf : wf (index_lt).
+ Proof. eapply index_mixin_lt_wf, index_mixin. Qed.
+ Lemma index_lt_eq_lt_dec (α β : index) : (α ≺ β) + (α = β) + (β ≺ α).
+ Proof. eapply index_mixin_lt_strict_total, index_mixin. Qed.
+ Lemma index_zero_least : nf (flip (index_lt)) zero.
+ Proof. eapply index_mixin_zero_least, index_mixin. Qed.
+ Lemma index_succ_greater (α : index) : α ≺ succ α.
+ Proof. eapply index_mixin_succ_greater, index_mixin. Qed.
+ Lemma index_succ_least (α β : index) : α ≺ β → succ α ⪯ β.
+ Proof. eapply index_mixin_succ_least, index_mixin. Qed.
+ Lemma index_dec_limit (α: index) : { β | α = succ β } + (∀ β, β ≺ α → succ β ≺ α).
+ Proof. eapply index_mixin_dec_limit, index_mixin. Qed.
End index_laws.
-Arguments index_zero_least : clear implicits.
-Arguments index_lt_wf : clear implicits.
+(* Arguments index_zero_least : clear implicits.
+Arguments index_lt_wf : clear implicits. *)
-Definition index_is_limit {SI : indexT} (α : SI) := ∀ β, β ≺ α → succ β ≺ α.
+Definition index_is_limit {SI : indexT} (α : index) := ∀ β, β ≺ α → succ β ≺ α.
(* proper limit indices that are not zero*)
-Record index_is_proper_limit {SI : indexT} (α : SI) := mkproperlim {
+Record index_is_proper_limit {SI : indexT} (α : index) := mkproperlim {
proper_limit_is_limit : index_is_limit α;
proper_limit_not_zero : zero ≺ α;
}.
-Arguments mkproperlim {_}.
-Arguments proper_limit_not_zero {_ _}.
-Arguments proper_limit_is_limit {_ _}.
+Arguments mkproperlim {_} _ _ _.
+Arguments proper_limit_not_zero {_ _} _.
+Arguments proper_limit_is_limit {_ _} _.
Record limit_idx {SI: indexT} := _mklimitidx {
- limit_index :> SI;
+ limit_index :> index;
limit_index_is_proper :> index_is_proper_limit limit_index;
}.
-Arguments limit_idx : clear implicits.
-Arguments _mklimitidx {_}.
-Definition mklimitidx {SI : indexT} (α : SI) Hlim Hz := _mklimitidx α (mkproperlim α Hlim Hz).
+Arguments _mklimitidx {_}.
+Definition mklimitidx {SI : indexT} (α : index) Hlim Hz := _mklimitidx α (mkproperlim α Hlim Hz).
-Lemma limit_index_is_limit {SI: indexT} (α : limit_idx SI) : index_is_limit α.
+Lemma limit_index_is_limit {SI: indexT} (α : limit_idx) : index_is_limit α.
Proof. apply limit_index_is_proper. Qed.
-Lemma limit_index_not_zero {SI : indexT} (α : limit_idx SI) : zero ≺ α.
+Lemma limit_index_not_zero {SI : indexT} (α : limit_idx) : zero ≺ α.
Proof. apply limit_index_is_proper. Qed.
Section StepIndexProperties.
Context {SI: indexT}.
- Implicit Type (α β γ : SI).
+ Implicit Type (α β γ : index).
- Global Instance: Inhabited SI.
+ Global Instance: Inhabited index.
Proof. constructor. exact zero. Qed.
- Global Instance: PreOrder (@index_le SI).
+ Global Instance: PreOrder (index_le).
Proof.
split; [by constructor|].
intros ??? [] []; subst; eauto.
@@ -121,7 +120,7 @@ Section StepIndexProperties.
Lemma index_lt_zero_is_normal α: ¬ (α ≺ zero).
Proof.
- specialize (index_zero_least SI) as H.
+ specialize (index_zero_least) as H.
intros R; apply H; unfold red, flip; eauto.
Qed.
@@ -147,7 +146,7 @@ Section StepIndexProperties.
Lemma index_lt_irrefl α: ¬ (α ≺ α).
Proof.
- induction α using (well_founded_ind (index_lt_wf SI)).
+ induction α using (well_founded_ind (index_lt_wf)).
intros H1; apply H in H1 as H2; eauto.
Qed.
@@ -275,7 +274,7 @@ Section StepIndexProperties.
intros H. eapply index_lt_irrefl, H. apply index_succ_greater.
Qed.
- Lemma index_limit_not_succ (β : SI) : index_is_limit β → ∀ α, β ≠ succ α.
+ Lemma index_limit_not_succ β : index_is_limit β → ∀ α, β ≠ succ α.
Proof.
intros H α Hα. specialize (H α). rewrite Hα in H. eapply index_lt_irrefl. apply H, index_succ_greater.
Qed.
@@ -331,7 +330,7 @@ Global Hint Resolve <- index_succ_iff : core.
Section ordinal_match.
Context {SI : indexT}.
- Definition ord_match (P : SI → Type) : P zero → (∀ α, P (succ α)) → (∀ α : limit_idx SI, P α) → ∀ α, P α :=
+ Definition ord_match (P : index → Type) : P zero → (∀ α, P (succ α)) → (∀ α : limit_idx, P α) → ∀ α, P α :=
λ s f lim α,
match index_is_zero α with
| left EQ => eq_rect_r P s EQ
@@ -346,8 +345,8 @@ End ordinal_match.
Section ordinal_recursor.
Context {SI: indexT}.
- Definition index_rec (P: SI → Type): P zero → (∀ α, P α → P (succ α)) → (∀ α: limit_idx SI, (∀ β, β ≺ α → P β) → P α) → ∀ α, P α :=
- λ s f lim, Fix (index_lt_wf SI) _ (λ α IH,
+ Definition index_rec (P: index → Type): P zero → (∀ α, P α → P (succ α)) → (∀ α: limit_idx, (∀ β, β ≺ α → P β) → P α) → ∀ α, P α :=
+ λ s f lim, Fix (index_lt_wf) _ (λ α IH,
match index_is_zero α with
| left EQ => eq_rect_r P s EQ
| right NZ =>
@@ -358,7 +357,7 @@ Section ordinal_recursor.
end
).
- Lemma index_type_dec (α : SI) :
+ Lemma index_type_dec (α : index) :
(α = zero) + { α' | α = succ α'} + ( index_is_limit α).
Proof.
revert α. apply index_rec.
@@ -367,7 +366,7 @@ Section ordinal_recursor.
- intros α _. right. apply limit_index_is_limit.
Defined.
- Class index_rec_lim_ext {P: SI → Type} (lim: ∀ α: limit_idx SI, (∀ β, β ≺ α → P β) → P α) := {
+ Class index_rec_lim_ext {P: index → Type} (lim: ∀ α: limit_idx, (∀ β, β ≺ α → P β) → P α) := {
index_rec_lim_ext_proofs α H1 H2 f: lim α f = lim (mklimitidx α H2 H1) f;
index_rec_lim_ext_function α f g: (∀ β Hβ, f β Hβ = g β Hβ) → lim α f = lim α g
}.
@@ -409,7 +408,7 @@ Section ordinal_recursor.
- exfalso. eapply index_lt_irrefl, Hlim, index_succ_greater.
Qed.
- Lemma index_rec_lim P s f lim `{index_rec_lim_ext P lim} (α: limit_idx SI):
+ Lemma index_rec_lim P s f lim `{index_rec_lim_ext P lim} (α: limit_idx):
index_rec P s f lim α = lim α (λ β _, index_rec P s f lim β).
Proof.
rewrite index_rec_unfold; eauto.
@@ -424,14 +423,14 @@ End ordinal_recursor.
Section ordinal_cumulative_recursor.
Context {SI: indexT}.
- Variable (P: SI → Type) (Q: ∀ α, (∀ β, β ≺ α → P β) → Type).
+ Variable (P: index → Type) (Q: ∀ α, (∀ β, β ≺ α → P β) → Type).
Let R α := {f: ∀ β, β ≺ α → P β & Q α f}.
Lemma index_cumulative_rec (F: ∀ α, R α → P α):
(∀ α G, Q α (λ β Hβ, F β (G β Hβ))) → (∀ α, R α).
Proof.
- intros IH. apply (Fix (index_lt_wf SI)).
+ intros IH. apply (Fix (index_lt_wf)).
intros α G. unfold R. unshelve econstructor.
- intros β Hβ. by eapply F, G.
- by apply IH.
@@ -457,7 +456,7 @@ Section ordinal_cumulative_recursor.
→ ∀ β, M β (index_cumulative_rec F step β).
Proof.
intros H β. unfold index_cumulative_rec, Fix.
- pattern β, (index_lt_wf SI β). eapply Acc_inv_dep. clear β.
+ pattern β, (index_lt_wf β). eapply Acc_inv_dep. clear β.
intros β succs Hβ.
unfold index_cumulative_rec_dep in H.
eapply H. apply Hβ.
@@ -469,7 +468,7 @@ End ordinal_cumulative_recursor.
(* finite indicies are exactly the natural numbers *)
Class FiniteIndex (SI: indexT) :=
- finite_index (α: SI): α = zero ∨ ∃ β, α = succ β.
+ finite_index (α: index): α = zero ∨ ∃ β, α = succ β.
(* Canonical instances: natural numbers, pairs *)
Section nat_index.
@@ -494,14 +493,17 @@ Section nat_index.
+ left; by (exists n).
Qed.
- Canonical Structure natI : indexT := IndexT nat lt 0 S nat_index_mixin.
+ Definition natI : indexT := IndexT nat lt 0 S nat_index_mixin.
Global Instance nat_finite_index: FiniteIndex natI.
Proof. intros [|n]; eauto. Qed.
End nat_index.
Section pair_index.
- Variable (I J: indexT).
+ Variable (SI SJ: indexT).
+
+ Notation I := (@index SI).
+ Notation J := (@index SJ).
Definition pair_zero : I * J := (zero, zero).
@@ -519,8 +521,8 @@ Section pair_index.
Lemma pair_lt_wf: wf pair_lt.
Proof.
- intros [m n]. revert n; induction m using (well_founded_ind (index_lt_wf I)).
- intros n; induction n using (well_founded_ind (index_lt_wf J)).
+ intros [m n]. revert n; induction m using (well_founded_ind (index_lt_wf)).
+ intros n; induction n using (well_founded_ind (index_lt_wf)).
constructor. intros [m' n'] [|[->]]; eauto.
Qed.
@@ -533,7 +535,9 @@ Section pair_index.
destruct (index_lt_eq_lt_dec m1 m2) as [[]|];
destruct (index_lt_eq_lt_dec n1 n2) as [[]|].
all: subst; firstorder.
- - intros [[m n] [H1 | [_ H1]]]; eapply index_zero_least; eauto.
+ - intros [[m n] [H1 | [_ H1]]].
+ + eapply (@index_zero_least SI); eauto.
+ + eapply (@index_zero_least SJ); eauto.
- intros [m n]; simpl. right; split; eauto.
- intros [m1 n1] [m2 n2]; simpl; intros [|[]]; subst.
+ right. by left.
@@ -545,7 +549,7 @@ Section pair_index.
+ right; intros [m' n']; simpl; intros []; firstorder.
Qed.
- Canonical Structure pairI : indexT := IndexT (I * J) pair_lt pair_zero pair_succ pair_index_mixin.
+ Local Instance pairI : indexT := IndexT (I * J) pair_lt pair_zero pair_succ pair_index_mixin.
Lemma pair_rc_right n m m': (n, m) ⪯ (n, m') ↔ m ⪯ m'.
Proof.
--
GitLab