Commit 035f0b29 by Robbert Krebbers

### Put step-indexes first.

parent 88679d3e
 ... ... @@ -16,7 +16,7 @@ Context {A : cofeT}. Instance agree_validN : ValidN (agree A) := λ n x, agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ≡{n'}≡ x n. Lemma agree_valid_le (x : agree A) n n' : Lemma agree_valid_le n n' (x : agree A) : agree_is_valid x n → n' ≤ n → agree_is_valid x n'. Proof. induction 2; eauto using agree_valid_S. Qed. Instance agree_equiv : Equiv (agree A) := λ x y, ... ... @@ -43,14 +43,14 @@ Proof. * transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz. * transitivity (y n'). by apply Hxy. by apply Hyz, Hxy. - intros n x y Hxy; split; intros; apply Hxy; auto. - intros c n; apply and_wlog_r; intros; - intros n c; apply and_wlog_r; intros; symmetry; apply (chain_cauchy c); naive_solver. Qed. Canonical Structure agreeC := CofeT agree_cofe_mixin. Lemma agree_car_ne (x y : agree A) n : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n. Lemma agree_car_ne n (x y : agree A) : ✓{n} x → x ≡{n}≡ y → x n ≡{n}≡ y n. Proof. by intros [??] Hxy; apply Hxy. Qed. Lemma agree_cauchy (x : agree A) n i : ✓{n} x → i ≤ n → x i ≡{i}≡ x n. Lemma agree_cauchy n (x : agree A) i : ✓{n} x → i ≤ n → x i ≡{i}≡ x n. Proof. by intros [? Hx]; apply Hx. Qed. Program Instance agree_op : Op (agree A) := λ x y, ... ... @@ -87,7 +87,7 @@ Proof. repeat match goal with H : agree_is_valid _ _ |- _ => clear H end; by cofe_subst; rewrite !agree_idemp. Qed. Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y. Lemma agree_includedN n (x y : agree A) : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y. Proof. split; [|by intros ?; exists y]. by intros [z Hz]; rewrite Hz assoc agree_idemp. ... ... @@ -100,12 +100,12 @@ Proof. rewrite (Hx n'); last auto. symmetry; apply dist_le with n; try apply Hx; auto. - intros x; apply agree_idemp. - by intros x y n [(?&?&?) ?]. - by intros x y n; rewrite agree_includedN. - by intros n x y [(?&?&?) ?]. - by intros n x y; rewrite agree_includedN. Qed. Lemma agree_op_inv (x1 x2 : agree A) n : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2. Lemma agree_op_inv n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2. Proof. intros Hxy; apply Hxy. Qed. Lemma agree_valid_includedN (x y : agree A) n : ✓{n} y → x ≼{n} y → x ≡{n}≡ y. Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y. Proof. move=> Hval [z Hy]; move: Hval; rewrite Hy. by move=> /agree_op_inv->; rewrite agree_idemp. ... ... @@ -161,7 +161,7 @@ Section agree_map. Global Instance agree_map_monotone : CMRAMonotone (agree_map f). Proof. split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]]. intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy. intros n x y; rewrite !agree_includedN; intros Hy; rewrite Hy. split; last done; split; simpl; last tauto. by intros (?&?&Hxy); repeat split; intros; try apply Hxy; try apply Hf; eauto using @agree_valid_le. ... ...
 ... ... @@ -46,8 +46,8 @@ Proof. + by intros ?? [??]; split; symmetry. + intros ??? [??] [??]; split; etransitivity; eauto. - by intros ? [??] [??] [??]; split; apply dist_S. - intros c n; split. apply (conv_compl (chain_map authoritative c) n). apply (conv_compl (chain_map own c) n). - intros n c; split. apply (conv_compl n (chain_map authoritative c)). apply (conv_compl n (chain_map own c)). Qed. Canonical Structure authC := CofeT auth_cofe_mixin. Global Instance auth_timeless (x : auth A) : ... ... @@ -163,7 +163,7 @@ Lemma auth_update a a' b b' : (∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) → ● a ⋅ ◯ a' ~~> ● b ⋅ ◯ b'. Proof. move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *. move=> Hab n [[?| |] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *. destruct (Hab n (bf1 ⋅ bf2)) as [Ha' ?]; auto. { by rewrite Ha left_id assoc. } split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done]. ... ...
 ... ... @@ -147,11 +147,11 @@ Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := { Arguments local_updateN {_ _} _ {_} _ _ _ _ _. (** * Frame preserving updates *) Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n, Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z). Instance: Params (@cmra_updateP) 1. Infix "~~>:" := cmra_updateP (at level 70). Definition cmra_update {A : cmraT} (x y : A) := ∀ z n, Definition cmra_update {A : cmraT} (x y : A) := ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z). Infix "~~>" := cmra_update (at level 70). Instance: Params (@cmra_update) 1. ... ... @@ -202,23 +202,23 @@ Qed. Global Instance cmra_update_proper : Proper ((≡) ==> (≡) ==> iff) (@cmra_update A). Proof. intros x1 x2 Hx y1 y2 Hy; split=>? z n; [rewrite -Hx -Hy|rewrite Hx Hy]; auto. intros x1 x2 Hx y1 y2 Hy; split=>? n z; [rewrite -Hx -Hy|rewrite Hx Hy]; auto. Qed. Global Instance cmra_updateP_proper : Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A). Proof. intros x1 x2 Hx P1 P2 HP; split=>Hup z n; intros x1 x2 Hx P1 P2 HP; split=>Hup n z; [rewrite -Hx; setoid_rewrite <-HP|rewrite Hx; setoid_rewrite HP]; auto. Qed. (** ** Validity *) Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x. Proof. done. Qed. Lemma cmra_validN_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x. Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x. Proof. induction 2; eauto using cmra_validN_S. Qed. Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x. Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed. Lemma cmra_validN_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y. Lemma cmra_validN_op_r n x y : ✓{n} (x ⋅ y) → ✓{n} y. Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed. Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y. Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed. ... ... @@ -228,7 +228,7 @@ Lemma cmra_unit_r x : x ⋅ unit x ≡ x. Proof. by rewrite (comm _ x) cmra_unit_l. Qed. Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x. Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed. Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} unit x. Lemma cmra_unit_validN n x : ✓{n} x → ✓{n} unit x. Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed. Lemma cmra_unit_valid x : ✓ x → ✓ unit x. Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed. ... ... @@ -237,7 +237,7 @@ Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed. Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y. Proof. split; [by intros [z Hz] n; exists z; rewrite Hz|]. intros Hxy; exists (y ⩪ x); apply equiv_dist; intros n. intros Hxy; exists (y ⩪ x); apply equiv_dist=> n. symmetry; apply cmra_op_minus, Hxy. Qed. Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n). ... ... @@ -252,14 +252,14 @@ Proof. split; red; intros until 0; rewrite !cmra_included_includedN; first done. intros; etransitivity; eauto. Qed. Lemma cmra_validN_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x. Lemma cmra_validN_includedN n x y : ✓{n} y → x ≼{n} y → ✓{n} x. Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed. Lemma cmra_validN_included x y n : ✓{n} y → x ≼ y → ✓{n} x. Lemma cmra_validN_included n x y : ✓{n} y → x ≼ y → ✓{n} x. Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed. Lemma cmra_includedN_S x y n : x ≼{S n} y → x ≼{n} y. Lemma cmra_includedN_S n x y : x ≼{S n} y → x ≼{n} y. Proof. by intros [z Hz]; exists z; apply dist_S. Qed. Lemma cmra_includedN_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y. Lemma cmra_includedN_le n n' x y : x ≼{n} y → n' ≤ n → x ≼{n'} y. Proof. induction 2; auto using cmra_includedN_S. Qed. Lemma cmra_includedN_l n x y : x ≼{n} x ⋅ y. ... ... @@ -284,7 +284,7 @@ Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed. Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z. Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed. Lemma cmra_included_dist_l x1 x2 x1' n : Lemma cmra_included_dist_l n x1 x2 x1' : x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. Proof. intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using cmra_included_l. ... ... @@ -318,7 +318,7 @@ Qed. (** ** RAs with an empty element *) Section identity. Context `{Empty A, !CMRAIdentity A}. Lemma cmra_empty_leastN n x : ∅ ≼{n} x. Lemma cmra_empty_leastN n x : ∅ ≼{n} x. Proof. by exists x; rewrite left_id. Qed. Lemma cmra_empty_least x : ∅ ≼ x. Proof. by exists x; rewrite left_id. Qed. ... ... @@ -350,14 +350,14 @@ Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =). Proof. split. - by intros Hx z ?; exists y; split; [done|apply (Hx z)]. - by intros Hx z n ?; destruct (Hx z n) as (?&<-&?). - by intros Hx n z ?; destruct (Hx n z) as (?&<-&?). Qed. Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P. Proof. by intros ? z n ?; exists x. Qed. Proof. by intros ? n z ?; exists x. Qed. Lemma cmra_updateP_compose (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q. Proof. intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y). intros Hx Hy n z ?. destruct (Hx n z) as (y&?&?); auto. by apply (Hy y). Qed. Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q. Proof. ... ... @@ -370,9 +370,9 @@ Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed. Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. Proof. intros Hx1 Hx2 Hy z n ?. destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite assoc. destruct (Hx2 (y1 ⋅ z) n) as (y2&?&?); intros Hx1 Hx2 Hy n z ?. destruct (Hx1 n (x2 ⋅ z)) as (y1&?&?); first by rewrite assoc. destruct (Hx2 n (y1 ⋅ z)) as (y2&?&?); first by rewrite assoc (comm _ x2) -assoc. exists (y1 ⋅ y2); split; last rewrite (comm _ y1) -assoc; auto. Qed. ... ... @@ -389,7 +389,7 @@ Proof. intro. auto. Qed. Section identity_updates. Context `{Empty A, !CMRAIdentity A}. Lemma cmra_update_empty x : x ~~> ∅. Proof. intros z n; rewrite left_id; apply cmra_validN_op_r. Qed. Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed. Lemma cmra_update_empty_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y. Proof. split; [intros; transitivity ∅|]; auto using cmra_update_empty. Qed. End identity_updates. ... ... @@ -472,7 +472,7 @@ Section discrete. Definition discrete_cmra_mixin : CMRAMixin A. Proof. by destruct ra; split; unfold Proper, respectful, includedN; try setoid_rewrite <-(timeless_iff _ _ _ _). try setoid_rewrite <-(timeless_iff _ _). Qed. Definition discrete_extend_mixin : CMRAExtendMixin A. Proof. ... ... @@ -483,10 +483,10 @@ Section discrete. CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin. Lemma discrete_updateP (x : discreteRA) (P : A → Prop) : (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P. Proof. intros Hvalid z n; apply Hvalid. Qed. Proof. intros Hvalid n z; apply Hvalid. Qed. Lemma discrete_update (x y : discreteRA) : (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y. Proof. intros Hvalid z n; apply Hvalid. Qed. Proof. intros Hvalid n z; apply Hvalid. Qed. Lemma discrete_valid (x : discreteRA) : v x → validN_valid x. Proof. move=>Hx n. exact Hx. Qed. End discrete. ... ... @@ -540,7 +540,7 @@ Section prod. - intros n x y; rewrite !prod_includedN. by intros [??]; split; apply cmra_unit_preservingN. - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l. - intros x y n; rewrite prod_includedN; intros [??]. - intros n x y; rewrite prod_includedN; intros [??]. by split; apply cmra_op_minus. Qed. Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B). ... ... @@ -561,12 +561,12 @@ Section prod. - by intros ? [??]; split; apply (timeless _). Qed. Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y. Proof. intros ?? z n [??]; split; simpl in *; auto. Qed. Proof. intros ?? n z [??]; split; simpl in *; auto. Qed. Lemma prod_updateP P1 P2 (Q : A * B → Prop) x : x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q. Proof. intros Hx1 Hx2 HP z n [??]; simpl in *. destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto. intros Hx1 Hx2 HP n z [??]; simpl in *. destruct (Hx1 n (z.1)) as (a&?&?), (Hx2 n (z.2)) as (b&?&?); auto. exists (a,b); repeat split; auto. Qed. Lemma prod_updateP' P1 P2 x : ... ...
 ... ... @@ -54,7 +54,7 @@ Record CofeMixin A `{Equiv A, Compl A} := { mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y; mixin_dist_equivalence n : Equivalence (dist n); mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y; mixin_conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n) mixin_conv_compl n c : compl c ≡{n}≡ c (S n) }. Class Contractive `{Dist A, Dist B} (f : A -> B) := contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y. ... ... @@ -86,7 +86,7 @@ Section cofe_mixin. Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed. Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y. Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed. Lemma conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n). Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c (S n). Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed. End cofe_mixin. ... ... @@ -113,7 +113,7 @@ Section cofe. Qed. Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x). Proof. by apply dist_proper. Qed. Lemma dist_le (x y : A) n n' : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. Proof. induction 2; eauto using dist_S. Qed. Instance ne_proper {B : cofeT} (f : A → B) `{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100. ... ... @@ -147,7 +147,7 @@ Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. (** Timeless elements *) Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y. Arguments timeless {_} _ {_} _ _. Lemma timeless_iff {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ≡{n}≡ y. Lemma timeless_iff {A : cofeT} n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y. Proof. split; intros; [by apply equiv_dist|]. apply (timeless _), dist_le with n; auto with lia. ... ... @@ -168,14 +168,14 @@ Section fixpoint. Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}. Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). Proof. apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //. apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //. induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. 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 (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n) /=. (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. ... ... @@ -206,21 +206,21 @@ Section cofe_mor. Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c, {| cofe_mor_car x := compl (fun_chain c x) |}. Next Obligation. intros c n x y Hx. by rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hx. intros c n x y Hx. by rewrite (conv_compl n (fun_chain c x)) (conv_compl n (fun_chain c y)) /= Hx. Qed. Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B). Proof. split. - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|]. intros Hfg k; apply equiv_dist; intros n; apply Hfg. intros Hfg k; apply equiv_dist=> n; apply Hfg. - intros n; split. + by intros f x. + by intros f g ? x. + by intros f g h ?? x; transitivity (g x). - by intros n f g ? x; apply dist_S. - intros c n x; simpl. by rewrite (conv_compl (fun_chain c x) n) /=. - intros n c x; simpl. by rewrite (conv_compl n (fun_chain c x)) /=. Qed. Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin. ... ... @@ -278,8 +278,8 @@ Section product. rewrite !equiv_dist; naive_solver. - apply _. - by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S. - intros c n; split. apply (conv_compl (chain_map fst c) n). apply (conv_compl (chain_map snd c) n). - intros n c; split. apply (conv_compl n (chain_map fst c)). apply (conv_compl n (chain_map snd c)). Qed. Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin. Global Instance pair_timeless (x : A) (y : B) : ... ... @@ -311,7 +311,7 @@ Section discrete_cofe. - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. - intros c n. rewrite /compl /discrete_compl /=. - intros n c. rewrite /compl /discrete_compl /=. symmetry; apply (chain_cauchy c 0 (S n)); omega. Qed. Definition discreteC : cofeT := CofeT discrete_cofe_mixin. ... ... @@ -354,7 +354,7 @@ Section later. + by intros [x] [y]. + by intros [x] [y] [z] ??; transitivity y. - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. - intros c [|n]; [done|by apply (conv_compl (later_chain c) n)]. - intros [|n] c; [done|by apply (conv_compl n (later_chain c))]. Qed. Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. Global Instance Next_contractive : Contractive (@Next A). ... ...
 ... ... @@ -60,8 +60,8 @@ Program Instance tower_compl : Compl tower := λ c, {| tower_car n := compl (tower_chain c n) |}. Next Obligation. intros c k; apply equiv_dist=> n. by rewrite (conv_compl (tower_chain c k) n) (conv_compl (tower_chain c (S k)) n) /= (g_tower (c (S n)) k). by rewrite (conv_compl n (tower_chain c k)) (conv_compl n (tower_chain c (S k))) /= (g_tower (c (S n)) k). Qed. Definition tower_cofe_mixin : CofeMixin tower. Proof. ... ... @@ -74,7 +74,7 @@ Proof. + by intros X Y Z ?? n; transitivity (Y n). - intros k X Y HXY n; apply dist_S. by rewrite -(g_tower X) (HXY (S n)) g_tower. - intros c n k; rewrite /= (conv_compl (tower_chain c k) n). - intros n c k; rewrite /= (conv_compl n (tower_chain c k)). apply (chain_cauchy c); lia. Qed. Definition T : cofeT := CofeT tower_cofe_mixin. ... ... @@ -189,8 +189,8 @@ Qed. Definition unfold (X : T) : F T T := compl (unfold_chain X). Instance unfold_ne : Proper (dist n ==> dist n) unfold. Proof. intros n X Y HXY. by rewrite /unfold (conv_compl (unfold_chain X) n) (conv_compl (unfold_chain Y) n) /= (HXY (S (S n))). intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X)) (conv_compl n (unfold_chain Y)) /= (HXY (S (S n))). Qed. Program Definition fold (X : F T T) : T := ... ... @@ -210,7 +210,7 @@ Proof. rewrite equiv_dist; intros n k; unfold unfold, fold; simpl. rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)). transitivity (map (ff n, gg n) (X (S (n + k)))). { rewrite /unfold (conv_compl (unfold_chain X) n). { rewrite /unfold (conv_compl n (unfold_chain X)). rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia. rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia. rewrite f_S -!map_comp; apply (contractive_ne map); split=> Y. ... ... @@ -229,7 +229,7 @@ Proof. rewrite (map_ff_gg _ _ _ H). apply (_ : Proper (_ ==> _) (gg _)); by destruct H. - intros X; rewrite equiv_dist=> n /=. rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=. rewrite /unfold /= (conv_compl n (unfold_chain (fold X))) /=. rewrite g_S -!map_comp -{2}(map_id _ _ X). apply (contractive_ne map); split => Y /=. + apply dist_le with n; last omega. ... ...
 ... ... @@ -27,7 +27,7 @@ Inductive excl_dist `{Dist A} : Dist (excl A) := | ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot. Existing Instance excl_dist. Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A). Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A). Proof. by constructor. Qed. Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A). Proof. by constructor. Qed. ... ... @@ -58,13 +58,13 @@ Proof. + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etransitivity; eauto. - by inversion_clear 1; constructor; apply dist_S. - intros c n; unfold compl, excl_compl. - intros n c; unfold compl, excl_compl. destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|]. { assert (c 1 = Excl x) by (by destruct (c 1); simplify_eq/=). assert (∃ y, c (S n) = Excl y) as [y Hy]. { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. } rewrite Hy; constructor. by rewrite (conv_compl (excl_chain c x Hx) n) /= Hy. } by rewrite (conv_compl n (excl_chain c x Hx)) /= Hy. } feed inversion (chain_cauchy c 0 (S n)); first lia; constructor; destruct (c 1); simplify_eq/=. Qed. ... ... @@ -161,9 +161,9 @@ Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed. (** Updates *) Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y. Proof. by destruct y; intros ? [?| |]. Qed. Proof. destruct y; by intros ?? [?| |]. Qed. Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ~~>: P. Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed. Proof. intros ?? n z ?; exists y. by destruct y, z as [?| |]. Qed. End excl. Arguments exclC : clear implicits. ... ...
 ... ... @@ -24,7 +24,7 @@ Proof. + by intros m1 m2 ? k. + by intros m1 m2 m3 ?? k; transitivity (m2 !! k). - by intros n m1 m2 ? k; apply dist_S. - intros c n k; rewrite /compl /map_compl lookup_imap. - intros n c k; rewrite /compl /map_compl lookup_imap. feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia. by rewrite conv_compl /=; apply reflexive_eq. Qed. ... ... @@ -61,7 +61,7 @@ Proof. [by constructor|by apply lookup_ne]. Qed. Global Instance map_timeless `{∀ a : A, Timeless a} (m : gmap K A) : Timeless m. Global Instance map_timeless `{∀ a : A, Timeless a} m : Timeless m. Proof. by intros m' ? i; apply (timeless _). Qed. Instance map_empty_timeless : Timeless (∅ : gmap K A). ... ... @@ -140,7 +140,7 @@ Proof. by rewrite !lookup_unit; apply cmra_unit_preservingN. - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i). by rewrite -lookup_op. - intros x y n; rewrite map_includedN_spec=> ? i. - intros n x y; rewrite map_includedN_spec=> ? i. by rewrite lookup_op lookup_minus cmra_op_minus. Qed. Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A). ... ... @@ -248,8 +248,8 @@ Qed. Lemma map_insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x : x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q. Proof. intros Hx%option_updateP' HP mf n Hm. destruct (Hx (mf !! i) n) as ([y|]&?&?); try done. intros Hx%option_updateP' HP n mf Hm. destruct (Hx n (mf !! i)) as ([y|]&?&?); try done. { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. } exists (<[i:=y]> m); split; first by auto. intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm. ... ... @@ -276,8 +276,8 @@ Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A} (P : A → Prop) (Q : gmap K A → Prop) i : ∅ ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q. Proof. intros Hx HQ gf n Hg. destruct (Hx (from_option ∅ (gf !! i)) n) as (y&?&Hy). intros Hx HQ n gf Hg. destruct (Hx n (from_option ∅ (gf !! i))) as (y&?&Hy). { move:(Hg i). rewrite !left_id. case _: (gf !! i); simpl; auto using cmra_empty_valid. } exists {[ i := y ]}; split; first by auto. ... ... @@ -296,7 +296,7 @@ Context `{Fresh K (gset K), !FreshSpec K (gset K)}. Lemma map_updateP_alloc_strong (Q : gmap K A → Prop) (I : gset K) m x : ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q. Proof. intros ? HQ mf n Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))). intros ? HQ n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))). assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]]. { rewrite -not_elem_of_union -map_dom_op -not_elem_of_union; apply is_fresh. } exists (<[i:=x]>m); split. ... ...
 ... ... @@ -37,8 +37,8 @@ Section iprod_cofe. + by intros f g ? x. + by intros f g h ?? x; transitivity (g x). - intros n f g Hfg x; apply dist_S, Hfg. - intros c n x. rewrite /compl /iprod_compl (conv_compl (iprod_chain c x) n). - intros n c x. rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)). apply (chain_cauchy c); lia. Qed. Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin. ... ... @@ -55,7 +55,7 @@ Section iprod_cofe. (** Properties of iprod_insert. *) Context `{∀ x x' : A, Decision (x = x')}. Global Instance iprod_insert_ne x n : Global Instance iprod_insert_ne n x : Proper (dist n ==> dist n ==> dist n) (iprod_insert x). Proof. intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert. ... ... @@ -94,7 +94,7 @@ Section iprod_cofe. (** Properties of iprod_singletom. *) Context `{∀ x : A, Empty (B x)}. Global Instance iprod_singleton_ne x n : Global Instance iprod_singleton_ne n x : Proper (dist n ==> dist n) (iprod_singleton x). Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed. Global Instance iprod_singleton_proper x : ... ... @@ -182,7 +182,7 @@ Section iprod_cmra. y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) → iprod_insert x y1 g ~~>: Q. Proof. intros Hy1 HP gf n Hg. destruct (Hy1 (gf x) n) as (y2&?&?). intros Hy1 HP n gf Hg. destruct (Hy1 n (gf x)) as (y2&?&?). { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. } exists (iprod_insert x y2 g); split; [auto|]. intros x'; destruct (decide (x' = x)) as [->|]; ... ... @@ -242,7 +242,7 @@ Section iprod_cmra. Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :