Skip to content
Snippets Groups Projects
Commit 320b9511 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

WIP.

parent 676a5302
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 171 additions and 137 deletions
theories/algebra/ofe.v
+ 171
− 137
View file @ 320b9511
......@@ -107,42 +107,34 @@ Instance: Params (@Discrete) 1 := {}.
Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
(** OFEs with a completion *)
Record chain (A : ofeT) := {
chain_car :> nat → A;
chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n
}.
Arguments chain_car {_} _ _.
Arguments chain_cauchy {_} _ _ _ _.
Definition chain A := nat → A.
Class Cauchy {A : ofeT} (c : chain A) :=
cauchy n i : n ≤ i → c i ≡{n}≡ c n.
Arguments cauchy {_} _ {_} _ _ _.
Instance chain_fmap : FMap chain := λ A B f c n, f (c n).
Instance chain_fmap_cauchy {A B : ofeT} (f : A → B) c :
NonExpansive f → Cauchy c → Cauchy (f <$> c).
Proof. intros Hf Hc n i ?. by apply Hf, Hc. Qed.
Program Definition chain_map {A B : ofeT} (f : A → B)
`{!NonExpansive f} (c : chain A) : chain B :=
{| chain_car n := f (c n) |}.
Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Instance const_cauchy {A : ofeT} (x : A) : Cauchy (const x).
Proof. by intros n i _. Qed.
Notation Compl A := (chain A%type → A).
Notation Compl A := (chain A → A).
Class Cofe (A : ofeT) := {
compl : Compl A;
conv_compl n c : compl c ≡{n}≡ c n;
compl_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) compl;
conv_compl n c : Cauchy c → compl c ≡{n}≡ c n;
}.
Existing Instance compl_ne.
Arguments compl : simpl never.
Hint Mode Cofe ! : typeclass_instances.
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
compl (chain_map f c) ≡ f (compl c).
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
Program Definition chain_const {A : ofeT} (a : A) : chain A :=
{| chain_car n := a |}.
Next Obligation. by intros A a n i _. Qed.
Lemma compl_chain_const {A : ofeT} `{!Cofe A} (a : A) :
compl (chain_const a) ≡ a.
Proof. apply equiv_dist=>n. by rewrite conv_compl. Qed.
(** General properties *)
Section ofe.
Context {A : ofeT}.
Implicit Types x y : A.
Global Instance ofe_equivalence : Equivalence ((≡) : relation A).
Proof.
split.
......@@ -179,10 +171,17 @@ Section ofe.
by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed.
Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
Global Instance conv_proper `{Cofe A} :
Proper (pointwise_relation _ (≡) ==> (≡)) (compl (A:=A)).
Proof.
transitivity (c n); first by apply conv_compl. symmetry.
apply chain_cauchy. lia.
intros c1 c2 Hc. apply equiv_dist=> n. apply compl_ne=> x. by apply equiv_dist.
Qed.
Lemma conv_compl' `{Cofe A} n (c : chain A) :
Cauchy c → compl c ≡{n}≡ c (S n).
Proof.
intros Hc. transitivity (c n); first by apply conv_compl.
symmetry. apply Hc. lia.
Qed.
Lemma discrete_iff n (x : A) `{!Discrete x} y : x ≡ y ↔ x ≡{n}≡ y.
......@@ -263,57 +262,82 @@ Section limit_preserving.
Lemma limit_preserving_ext (P Q : A → Prop) :
(∀ x, P x ↔ Q x) → LimitPreserving P → LimitPreserving Q.
Proof. intros HP Hlimit c ?. apply HP, Hlimit=> n; by apply HP. Qed.
Proof. intros HP Hlimit c ?. apply HP, Hlimit=> // n. by apply HP. Qed.
Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _ : A, P).
Proof. intros c HP. apply (HP 0). Qed.
Lemma limit_preserving_discrete (P : A → Prop) :
Proper (dist 0 ==> impl) P → LimitPreserving P.
Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed.
Proof. intros PH c Hc. rewrite (conv_compl 0). Qed.
*)
Lemma limit_preserving_and (P1 P2 : A → Prop) :
LimitPreserving P1 → LimitPreserving P2 →
LimitPreserving (λ x, P1 x ∧ P2 x).
Proof. intros Hlim1 Hlim2 c Hc. split. apply Hlim1, Hc. apply Hlim2, Hc. Qed.
Proof. intros Hlim1 Hlim2 c HP. split. by apply Hlim1, HP. by apply Hlim2, HP. Qed.
(*
Lemma limit_preserving_impl (P1 P2 : A → Prop) :
Proper (dist 0 ==> impl) P1 → LimitPreserving P2 →
LimitPreserving (λ x, P1 x → P2 x).
Proof.
intros Hlim1 Hlim2 c Hc HP1. apply Hlim2=> n; apply Hc.
eapply Hlim1, HP1. apply dist_le with n; last lia. apply (conv_compl n).
intros Hlim1 Hlim2 c HP HPc. apply Hlim2=> // n. apply HP.
eapply Hlim1, HPc. apply dist_le with n; last lia. apply (conv_compl n).
Qed.
*)
Lemma limit_preserving_forall {B} (P : B → A → Prop) :
(∀ y, LimitPreserving (P y)) →
LimitPreserving (λ x, ∀ y, P y x).
Proof. intros Hlim c Hc y. by apply Hlim. Qed.
Proof. intros Hlim c HPc y. by apply Hlim. Qed.
End limit_preserving.
(** Fixpoint *)
Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Next Obligation.
intros A ? f ? n.
induction n as [|n IH]=> -[|i] //= ?; try lia.
Definition fixpoint_chain `{Inhabited A} (f : A → A) : chain A :=
λ i, Nat.iter (S i) f inhabitant.
Instance fixpoint_chain_cauchy `{Cofe A, Inhabited A} (f : A → A) :
Contractive f → Cauchy (fixpoint_chain f).
Proof.
intros ? n. induction n as [|n IH]=> -[|i] //= ?; try lia.
- apply (contractive_0 f).
- apply (contractive_S f), IH; auto with lia.
Qed.
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A) : A :=
compl (fixpoint_chain f).
Definition fixpoint_aux : seal (@fixpoint_def). by eexists. Qed.
Definition fixpoint {A AC AiH} f {Hf} := fixpoint_aux.(unseal) A AC AiH f Hf.
Definition fixpoint := fixpoint_aux.(unseal).
Arguments fixpoint {_ _ _} f : assert.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
Instance fixpoint_ne `{Cofe A, Inhabited A} :
Proper ((dist n ==> dist n) ==> dist n) (fixpoint (A:=A)).
Proof.
intros n f1 f2 Hf. rewrite fixpoint_eq. apply compl_ne=> i.
rewrite /fixpoint_chain. induction (S i) as [|j IH]=> //=. by apply Hf.
Qed.
Instance fixpoint_proper `{Cofe A, Inhabited A} :
Proper (((≡) ==> (≡)) ==> (≡)) (fixpoint (A:=A)).
Proof.
intros f1 f2 Hf. rewrite fixpoint_eq.
apply equiv_dist=> n. apply compl_ne=> i. apply equiv_dist.
rewrite /fixpoint_chain. induction (S i) as [|j IH]=> //=. by apply Hf.
Qed.
Section fixpoint.
Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
Context `{Cofe A, Inhabited A} (f : A → A) `{Hf : !Contractive f}.
Local Unset Default Proof Using.
Local Hint Extern 0 (cauchy _) => by apply fixpoint_chain_cauchy : core.
Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
Proof.
apply equiv_dist=>n.
rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
rewrite /fixpoint_chain.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Qed.
......@@ -324,34 +348,21 @@ Section fixpoint.
- rewrite Hx fixpoint_unfold. apply (contractive_S _), IH.
Qed.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
(∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
Proof.
intros Hfg. rewrite fixpoint_eq /fixpoint_def
(conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
rewrite Hfg; apply contractive_S, IH; auto using dist_S.
Qed.
Lemma fixpoint_proper (g : A → A) `{!Contractive g} :
(∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
Lemma fixpoint_ind (P : A → Prop) :
Proper ((≡) ==> impl) P →
(∃ x, P x) → (∀ x, P x → P (f x)) →
LimitPreserving P →
P (fixpoint f).
Proof.
intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x).
assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n).
{ intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=;
intros ? [x Hx] Hincr Hlim. set (ch i := Nat.iter (S i) f x).
assert (Cauchy ch) as Hcauch.
{ intros n. rewrite /ch. induction n as [|n IH]=> -[|i] //=;
eauto using contractive_0, contractive_S with lia. }
set (fp2 := compl {| chain_cauchy := Hcauch |}).
set (fp2 := compl ch).
assert (f fp2 ≡ fp2).
{ apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
{ apply equiv_dist=>n. rewrite /fp2 (conv_compl n) //= /ch.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. }
rewrite -(fixpoint_unique fp2) //.
apply Hlim=> n /=. by apply Nat_iter_ind.
rewrite -(fixpoint_unique fp2) //. apply Hlim=> // n. by apply Nat_iter_ind.
Qed.
End fixpoint.
......@@ -361,9 +372,9 @@ Definition fixpointK `{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 `{Cofe A, Inhabited A} (f : A → A) (k : nat).
Context {f_contractive : Contractive (Nat.iter k f)} {f_ne : NonExpansive f}.
Local Unset Default Proof Using.
(* Note than f_ne is crucial here: there are functions f such that f^2 is contractive,
but f is not non-expansive.
Consider for example f: SPred → SPred (where SPred is "downclosed sets of natural numbers").
......@@ -392,13 +403,13 @@ Section fixpointK.
Lemma fixpointK_unfold : fixpointK k f ≡ f (fixpointK k f).
Proof.
symmetry. rewrite /fixpointK. apply fixpoint_unique.
symmetry. rewrite /fixpointK. apply (fixpoint_unique _).
by rewrite -Nat_iter_S_r Nat_iter_S -fixpoint_unfold.
Qed.
Lemma fixpointK_unique (x : A) : x ≡ f x → x ≡ fixpointK k f.
Proof.
intros Hf. apply fixpoint_unique. clear f_contractive.
intros Hf. apply (fixpoint_unique _). clear f_contractive.
induction k as [|k' IH]=> //=. by rewrite -IH.
Qed.
......@@ -408,7 +419,7 @@ Section fixpointK.
Lemma fixpointK_ne n : (∀ z, f z ≡{n}≡ g z) → fixpointK k f ≡{n}≡ fixpointK k g.
Proof.
rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z.
rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z1 z2 Hz.
clear f_contractive g_contractive.
induction k as [|k' IH]=> //=. by rewrite IH Hfg.
Qed.
......@@ -430,23 +441,22 @@ End fixpointK.
(** Mutual fixpoints *)
Section fixpointAB.
Local Unset Default Proof Using.
Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
Context (fA : A → B → A).
Context (fB : A → B → B).
Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
Local Unset Default Proof Using.
Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x).
Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
Global Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
Proof.
intros n x x' Hx; rewrite /fixpoint_AB.
apply fixpoint_ne=> y. by f_contractive.
intros n x1 x2 Hx; rewrite /fixpoint_AB.
apply fixpoint_ne=> y1 y2 Hy. f_contractive. done. by apply dist_S.
Qed.
Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x).
Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
Global Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
Proof. solve_contractive. Qed.
Definition fixpoint_A : A := fixpoint fixpoint_AA.
......@@ -468,11 +478,11 @@ Section fixpointAB.
Lemma fixpoint_A_unique p q : fA p q ≡ p → fB p q ≡ q → p ≡ fixpoint_A.
Proof.
intros HfA HfB. rewrite -HfA. apply fixpoint_unique. rewrite /fixpoint_AA.
f_equiv=> //. apply fixpoint_unique. by rewrite HfA HfB.
intros HfA HfB. rewrite -HfA. apply (fixpoint_unique _). rewrite /fixpoint_AA.
f_equiv=> //. apply (fixpoint_unique _). by rewrite HfA HfB.
Qed.
Lemma fixpoint_B_unique p q : fA p q ≡ p → fB p q ≡ q → q ≡ fixpoint_B.
Proof. intros. apply fixpoint_unique. by rewrite -fixpoint_A_unique. Qed.
Proof. intros. apply (fixpoint_unique _). by rewrite -fixpoint_A_unique. Qed.
End fixpointAB.
Section fixpointAB_ne.
......@@ -483,20 +493,22 @@ Section fixpointAB_ne.
Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA'}.
Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB'}.
Local Unset Default Proof Using.
Lemma fixpoint_A_ne n :
(∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
fixpoint_A fA fB ≡{n}≡ fixpoint_A fA' fB'.
Proof.
intros HfA HfB. apply fixpoint_ne=> z.
rewrite /fixpoint_AA /fixpoint_AB HfA. f_equiv. by apply fixpoint_ne.
intros HfA HfB. apply fixpoint_ne=> z1 z2 Hz.
rewrite /fixpoint_AA /fixpoint_AB HfA. f_equiv; [by apply dist_dist_later|].
apply fixpoint_ne=> y1 y2 Hy. rewrite HfB. f_equiv; by apply dist_dist_later.
Qed.
Lemma fixpoint_B_ne n :
(∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
fixpoint_B fA fB ≡{n}≡ fixpoint_B fA' fB'.
Proof.
intros HfA HfB. apply fixpoint_ne=> z. rewrite HfB. f_contractive.
apply fixpoint_A_ne; auto using dist_S.
intros HfA HfB. apply fixpoint_ne=> y1 y2 Hy. rewrite HfB.
f_equiv; auto using dist_dist_later, fixpoint_A_ne.
Qed.
Lemma fixpoint_A_proper :
......@@ -541,24 +553,25 @@ Section ofe_mor.
Qed.
Canonical Structure ofe_morO := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
Program Definition ofe_mor_chain (c : chain ofe_morO)
(x : A) : chain B := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morO := λ c,
{| ofe_mor_car x := compl (ofe_mor_chain c x) |}.
λne x, compl (flip c x).
Next Obligation.
intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
(conv_compl n (ofe_mor_chain c y)) /= Hx.
intros ? c n x1 x2 Hx. apply compl_ne=> i /=. by rewrite Hx.
Qed.
Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morO :=
{| compl := ofe_mor_compl |}.
Next Obligation.
intros ? n c x; simpl.
by rewrite (conv_compl n (ofe_mor_chain c x)) /=.
intros ? n c1 c2 Hc x. rewrite /ofe_mor_compl /=.
apply compl_ne=> i. apply Hc.
Qed.
Next Obligation.
intros ? n c Hc x. assert (Cauchy (flip c x)).
{ intros n' i ?. by apply Hc. }
by rewrite /ofe_mor_compl /= conv_compl.
Qed.
Global Instance ofe_mor_car_ne :
NonExpansive2 (@ofe_mor_car A B).
Global Instance ofe_mor_car_ne : NonExpansive2 (@ofe_mor_car A B).
Proof. intros n f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
Global Instance ofe_mor_car_proper :
Proper ((≡) ==> (≡) ==> (≡)) (@ofe_mor_car A B) := ne_proper_2 _.
......@@ -582,8 +595,7 @@ Definition ccompose {A B C}
(f : B -n> C) (g : A -n> B) : A -n> C := OfeMor (f ∘ g).
Instance: Params (@ccompose) 3 := {}.
Infix "◎" := ccompose (at level 40, left associativity).
Global Instance ccompose_ne {A B C} :
NonExpansive2 (@ccompose A B C).
Global Instance ccompose_ne {A B C} : NonExpansive2 (@ccompose A B C).
Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
(* Function space maps *)
......@@ -595,8 +607,7 @@ Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
Definition ofe_morO_map {A A' B B'} (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 {A A' B B'} :
NonExpansive2 (@ofe_morO_map A A' B B').
Instance ofe_morO_map_ne {A A' B B'} : NonExpansive2 (@ofe_morO_map A A' B B').
Proof.
intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
by repeat apply ccompose_ne.
......@@ -625,6 +636,7 @@ Section empty.
Global Program Instance Empty_set_cofe : Cofe Empty_setO := { compl x := x 0 }.
Next Obligation. by repeat split; try exists 0. Qed.
Next Obligation. done. Qed.
Global Instance Empty_set_ofe_discrete : OfeDiscrete Empty_setO.
Proof. done. Qed.
......@@ -635,8 +647,7 @@ Section product.
Context {A B : ofeT}.
Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
Global Instance pair_ne :
NonExpansive2 (@pair A B) := _.
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 (A * B).
......@@ -650,11 +661,9 @@ Section product.
Canonical Structure prodO : ofeT := OfeT (A * B) prod_ofe_mixin.
Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodO :=
{ compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
Next Obligation.
intros ?? n c; split. apply (conv_compl n (chain_map fst c)).
apply (conv_compl n (chain_map snd c)).
Qed.
{ compl c := (compl (fst <$> c), compl (snd <$> c)) }.
Next Obligation. intros ?? n c1 c2 Hc. split; apply compl_ne=> i; apply Hc. Qed.
Next Obligation. intros ?? n c ?. by rewrite /= !conv_compl. Qed.
Global Instance prod_discrete (x : A * B) :
Discrete (x.1) → Discrete (x.2) → Discrete x.
......@@ -792,12 +801,14 @@ Section sum.
Qed.
Canonical Structure sumO : ofeT := OfeT (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 |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Program Definition inr_chain (c : chain sumO) (b : B) : chain B :=
{| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Definition inl_chain (c : chain sumO) (a : A) : chain A :=
λ n, match c n with inl a' => a' | _ => a end.
Instance inl_chain_cauchy c a : Cauchy c → Cauchy (inl_chain c a).
Proof. intros ? n i ?. rewrite /inl_chain. by destruct (cauchy c n i). Qed.
Definition inr_chain (c : chain sumO) (b : B) : chain B :=
λ n, match c n with inr b' => b' | _ => b end.
Instance inr_chain_cauchy c a : Cauchy c → Cauchy (inr_chain c a).
Proof. intros ? n i ?. rewrite /inr_chain. by destruct (cauchy c n i). Qed.
Definition sum_compl `{Cofe A, Cofe B} : Compl sumO := λ c,
match c 0 with
......@@ -807,10 +818,15 @@ Section sum.
Global Program Instance sum_cofe `{Cofe A, Cofe B} : Cofe sumO :=
{ compl := sum_compl }.
Next Obligation.
intros ?? n c; rewrite /compl /sum_compl.
feed inversion (chain_cauchy c 0 n); first by auto with lia; constructor.
- rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
- rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
intros ?? n c1 c2 Hc. rewrite /sum_compl.
destruct (Hc 0); simpl; do 2 f_equiv; intros i;
rewrite /inl_chain /inr_chain; by destruct (Hc i).
Qed.
Next Obligation.
intros ?? n c ?; rewrite /compl /sum_compl.
feed inversion (cauchy c 0 n); first by auto with lia; constructor.
- rewrite (conv_compl n (inl_chain c _)) /inl_chain. destruct (c n); naive_solver.
- rewrite (conv_compl n (inr_chain c _)) /inr_chain. destruct (c n); naive_solver.
Qed.
Global Instance inl_discrete (x : A) : Discrete x → Discrete (inl x).
......@@ -878,10 +894,8 @@ Section discrete_ofe.
Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
{ compl c := c 0 }.
Next Obligation.
intros n c. rewrite /compl /=;
symmetry; apply (chain_cauchy c 0 n). lia.
Qed.
Next Obligation. solve_proper. Qed.
Next Obligation. intros n c ?; simpl. rewrite (cauchy c 0 n); auto with lia. Qed.
End discrete_ofe.
Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
......@@ -917,6 +931,9 @@ Section option.
Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
Proof. done. Qed.
Global Instance Some_ne : NonExpansive (@Some A).
Proof. by constructor. Qed.
Definition option_ofe_mixin : OfeMixin (option A).
Proof.
split.
......@@ -928,25 +945,29 @@ Section option.
Qed.
Canonical Structure optionO := OfeT (option A) option_ofe_mixin.
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_chain (c : chain optionO) (x : A) : chain A :=
λ n, default x (c n).
Instance option_chain_cauchy c x : Cauchy c → Cauchy (option_chain c x).
Proof. intros ? n i ?. rewrite /option_chain. by destruct (cauchy c n i). Qed.
Definition option_compl `{Cofe A} : Compl optionO := λ c,
match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
Global Program Instance option_cofe `{Cofe A} : Cofe optionO :=
{ compl := option_compl }.
Next Obligation.
intros ? n c; rewrite /compl /option_compl.
feed inversion (chain_cauchy c 0 n); auto with lia; [].
constructor. rewrite (conv_compl n (option_chain c _)) /=.
intros ? n c1 c2 Hc. rewrite /option_compl.
destruct (Hc 0) as [x1 x2 Hx|]; last done.
f_equiv; f_equiv=> i. rewrite /option_chain. f_equiv; [done|apply Hc].
Qed.
Next Obligation.
intros ? n c ?; rewrite /compl /option_compl.
feed inversion (cauchy c 0 n); auto with lia; [].
constructor. rewrite (conv_compl n (option_chain c _)) /option_chain.
destruct (c n); naive_solver.
Qed.
Global Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionO.
Proof. destruct 2; constructor; by apply (discrete _). Qed.
Global Instance Some_ne : NonExpansive (@Some A).
Proof. by constructor. Qed.
Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
Proof. destruct 1; split; eauto. Qed.
Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
......@@ -1030,6 +1051,10 @@ Section later.
Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
Instance later_dist : Dist (later A) := λ n x y,
dist_later n (later_car x) (later_car y).
Global Instance Next_contractive : Contractive (@Next A).
Proof. by intros [|n] x y. Qed.
Definition later_ofe_mixin : OfeMixin (later A).
Proof.
split.
......@@ -1043,17 +1068,17 @@ Section later.
Qed.
Canonical Structure laterO : ofeT := OfeT (later A) later_ofe_mixin.
Program Definition later_chain (c : chain laterO) : chain A :=
{| chain_car n := later_car (c (S n)) |}.
Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
Definition later_chain (c : chain laterO) : chain A :=
λ n, later_car (c (S n)).
Instance later_chain_cauchy c : Cauchy c → Cauchy (later_chain c).
Proof. intros ? n i ?; apply (cauchy c (S n)); lia. Qed.
Global Program Instance later_cofe `{Cofe A} : Cofe laterO :=
{ compl c := Next (compl (later_chain c)) }.
Next Obligation. intros ? n c1 c2 Hc. f_contractive; f_equiv=> i. apply Hc. Qed.
Next Obligation.
intros ? [|n] c; [done|by apply (conv_compl n (later_chain c))].
intros ? [|n] c ?; [done|]. apply (conv_compl n (later_chain c) _).
Qed.
Global Instance Next_contractive : Contractive (@Next A).
Proof. by intros [|n] x y. Qed.
Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
Proof. by intros x y. Qed.
......@@ -1157,12 +1182,14 @@ Section discrete_fun.
Qed.
Canonical Structure discrete_funO := OfeT (discrete_fun B) discrete_fun_ofe_mixin.
Program Definition discrete_fun_chain `(c : chain discrete_funO)
(x : A) : chain (B x) := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Definition discrete_fun_chain (c : chain discrete_funO) (x : A) : chain (B x) :=
λ n, c n x.
Instance discrete_fun_chain_cauchy c x : Cauchy c → Cauchy (discrete_fun_chain c x).
Proof. intros ? n i ?. by apply (cauchy c). Qed.
Global Program Instance discrete_fun_cofe `{∀ x, Cofe (B x)} : Cofe discrete_funO :=
{ compl c x := compl (discrete_fun_chain c x) }.
Next Obligation. intros ? n c x. apply (conv_compl n (discrete_fun_chain c x)). Qed.
Next Obligation. intros ? n c1 c2 Hc x. f_equiv=> i. apply Hc. Qed.
Next Obligation. intros ? n c ? x. apply (conv_compl n (discrete_fun_chain c x) _). Qed.
Global Instance discrete_fun_inhabited `{∀ x, Inhabited (B x)} : Inhabited discrete_funO :=
populate (λ _, inhabitant).
......@@ -1255,22 +1282,29 @@ Section iso_cofe_subtype.
Proof. intros n y1 y2. apply g_dist. Qed.
Existing Instance Hgne.
Context (gf : ∀ x Hx, g (f x Hx) ≡ x).
Context (Hlimit : ∀ c : chain B, P (compl (chain_map g c))).
Context (Hlimit : ∀ c : chain B, P (compl (g <$> c))).
Program Definition iso_cofe_subtype : Cofe B :=
{| compl c := f (compl (chain_map g c)) _ |}.
Next Obligation. apply Hlimit. Qed.
{| compl c := f (compl (g <$> c)) (Hlimit c) |}.
Next Obligation.
intros n c1 c2 Hc. apply g_dist. rewrite !gf. f_equiv=> i. apply g_dist, Hc.
Qed.
Next Obligation.
intros n c; simpl. apply g_dist. by rewrite gf conv_compl.
intros n c ?; simpl. apply g_dist. by rewrite gf conv_compl.
Qed.
End iso_cofe_subtype.
(*
Lemma iso_cofe_subtype' {A B : ofeT} `{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)
(gf : ∀ x Hx, g (f x Hx) ≡ x)
(Hlimit : LimitPreserving P) : Cofe B.
Proof. apply: (iso_cofe_subtype P f g)=> // c. apply Hlimit=> ?; apply Pg. Qed.
Proof. apply: (iso_cofe_subtype P f g)=> // c.
apply Hlimit. => ?. apply Pg. Qed.
*)
Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A → B) (g : B → A)
(g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
......@@ -1301,7 +1335,7 @@ Section sigma.
Canonical Structure sigO : ofeT := OfeT (sig P) sig_ofe_mixin.
Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigO.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig). => //. by intros []. Qed.
Global Instance sig_discrete (x : sig P) : Discrete (`x) → Discrete x.
Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (discrete _). Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment