diff --git a/CHANGELOG.md b/CHANGELOG.md index 1b947097454d49273806161e056a20a5c184631b..43b69064de1d19557874ea5ca402bc04898c3e36 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -208,6 +208,8 @@ s/\bgnameC/gnameO/g; s/\bcoPset\_disjC/coPset\_disjO/g; ' \$(find theories -name "*.v") ``` +- Add a COFE construction (and functor) on dependent pairs `sigTO`, dual to + `discrete_funO`. ## Iris 3.1.0 (released 2017-12-19) diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 5250feeb42858e9a3022202a267e68ba111cd798..4c8422bbe1c81f75529e4d318f339ca1f4ce1750 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -1284,3 +1284,160 @@ Section sigma. End sigma. Arguments sigO {_} _. + +(** Ofe for [sigT]. The first component must be discrete + and use Leibniz equality, while the second component might be any OFE. *) +Section sigmaT. + Import EqNotations. + Local Set Default Proof Using "Type*". + (* For this construction we need UIP (Uniqueness of Identity Proofs) on [A] + (i.e. [∀ x y : A, ProofIrrel (x = y)]. UIP is most commonly obtained from + decidable equality (by Hedberg’s theorem, see [stdpp.proof_irrel.eq_pi]). *) + + Context {A : Type} `{!∀ a b : A, ProofIrrel (a = b)} {P : A → ofeT}. + Implicit Types x : sigT P. + + (** + The equality/distance for [{ a : A & P }] uses Leibniz equality on [A] to + transport the second components to the same type, + and then step-indexed equality/distance on the second component. + Unlike in the topos of trees, with (C)OFEs we cannot use step-indexed equality + on the first component. + *) + Instance sigT_equiv : Equiv (sigT P) := λ x1 x2, + ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡ projT2 x2. + Instance sigT_dist : Dist (sigT P) := λ n x1 x2, + ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡{n}≡ projT2 x2. + + (** Unfolding lemmas. + Written with [↔] not [=] to avoid https://github.com/coq/coq/issues/3814. *) + Definition sigT_equiv_eq x1 x2 : (x1 ≡ x2) ↔ + ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡ projT2 x2 := + reflexivity _. + + Definition sigT_dist_eq x1 x2 n : (x1 ≡{n}≡ x2) ↔ + ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡{n}≡ projT2 x2 := + reflexivity _. + + Definition sigT_equiv_proj1 x y : x ≡ y → projT1 x = projT1 y := proj1_ex. + Definition sigT_dist_proj1 n {x y} : x ≡{n}≡ y → projT1 x = projT1 y := proj1_ex. + + (** [existT] is "non-expansive". *) + Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} : + ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡{n}≡ v2) → + existT i1 v1 ≡{n}≡ existT i2 v2. + Proof. intros ->; simpl. exists eq_refl => /=. done. Qed. + + Definition sigT_ofe_mixin : OfeMixin (sigT P). + Proof. + split. + - move => [x Px] [y Py] /=. + setoid_rewrite sigT_dist_eq; rewrite sigT_equiv_eq /=; split. + + destruct 1 as [-> Heq]. exists eq_refl => /=. + by apply equiv_dist. + + intros Heq. destruct (Heq 0) as [-> _]. exists eq_refl => /=. + apply equiv_dist => n. case: (Heq n) => [Hrefl]. + have -> //=: Hrefl = eq_refl y. exact: proof_irrel. + - move => n; split; hnf; setoid_rewrite sigT_dist_eq. + + intros. by exists eq_refl. + + move => [xa x] [ya y] /=. destruct 1 as [-> Heq]. + by exists eq_refl. + + move => [xa x] [ya y] [za z] /=. + destruct 1 as [-> Heq1]. + destruct 1 as [-> Heq2]. exists eq_refl => /=. by trans y. + - setoid_rewrite sigT_dist_eq. + move => n [xa x] [ya y] /=. destruct 1 as [-> Heq]. + exists eq_refl. exact: dist_S. + Qed. + + Canonical Structure sigTO : ofeT := OfeT (sigT P) sigT_ofe_mixin. + + Implicit Types (c : chain sigTO). + + Global Instance sigT_discrete x : Discrete (projT2 x) → Discrete x. + Proof. + move: x => [xa x] ? [ya y]. + rewrite sigT_dist_eq sigT_equiv_eq /=. destruct 1 as [-> Hxy]. + exists eq_refl. move: Hxy => /=. exact: discrete _. + Qed. + + Global Instance sigT_ofe_discrete : (∀ a, OfeDiscrete (P a)) → OfeDiscrete sigTO. + Proof. intros ??. apply _. Qed. + + Lemma sigT_chain_const_proj1 c n : projT1 (c n) = projT1 (c 0). + Proof. refine (sigT_dist_proj1 _ (chain_cauchy c 0 n _)). lia. Qed. + + Program Definition chain_map_snd c : chain (P (projT1 (c 0))) := + {| chain_car n := rew (sigT_chain_const_proj1 c n) in projT2 (c n) |}. + Next Obligation. + move => c n i Hle /=. + (* [Hgoal] is our thesis, up to casts: *) + case: (chain_cauchy c n i Hle) => [Heqin Hgoal] /=. + (* Pretty delicate. We have two casts to [projT1 (c 0)]. + We replace those by one cast. *) + move: (sigT_chain_const_proj1 c i) (sigT_chain_const_proj1 c n) + => Heqi0 Heqn0. + (* Rewrite [projT1 (c 0)] to [projT1 (c n)] in goal and [Heqi0]: *) + destruct Heqn0; cbn. + have {Heqi0} -> /= : Heqi0 = Heqin; first exact: proof_irrel. + exact Hgoal. + Qed. + + Section cofe. + Context `{!∀ a, Cofe (P a)}. + Definition sigT_compl : Compl sigTO := + λ c, existT (projT1 (chain_car c 0)) (compl (chain_map_snd c)). + + Global Program Instance sigT_cofe : Cofe sigTO := { compl := sigT_compl }. + Next Obligation. + intros n c. rewrite /sigT_compl sigT_dist_eq /=. + exists (symmetry (sigT_chain_const_proj1 c n)). + (* Our thesis, up to casts: *) + pose proof (conv_compl n (chain_map_snd c)) as Hgoal. + move: (compl (chain_map_snd c)) Hgoal => pc0 /=. + destruct (sigT_chain_const_proj1 c n); simpl. done. + Qed. + End cofe. +End sigmaT. + +Arguments sigTO {_ _} _. + +Section sigTOF. + Context {A : Type} `{!∀ x y : A, ProofIrrel (x = y)} . + + Program Definition sigT_map {P1 P2 : A → ofeT} : + discrete_funO (λ a, P1 a -n> P2 a) -n> + sigTO P1 -n> sigTO P2 := + λne f xpx, existT _ (f _ (projT2 xpx)). + Next Obligation. + move => ?? f n [x px] [y py] [/= Heq]. destruct Heq; simpl. + exists eq_refl => /=. by f_equiv. + Qed. + Next Obligation. + move => ?? n f g Heq [x px] /=. exists eq_refl => /=. apply Heq. + Qed. + + Program Definition sigTOF (F : A → oFunctor) : oFunctor := {| + oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A _ B CB); + oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := sigT_map (λ a, oFunctor_map (F a) fg) + |}. + Next Obligation. + repeat intro. exists eq_refl => /=. solve_proper. + Qed. + Next Obligation. + intros; exists eq_refl => /=. apply oFunctor_id. + Qed. + Next Obligation. + intros; exists eq_refl => /=. apply oFunctor_compose. + Qed. + + Global Instance sigTOF_contractive {F} : + (∀ a, oFunctorContractive (F a)) → oFunctorContractive (sigTOF F). + Proof. + repeat intro. apply sigT_map => a. exact: oFunctor_contractive. + Qed. +End sigTOF. +Arguments sigTOF {_ _} _%OF. + +Notation "{ x & P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope. +Notation "{ x : A & P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.