From 9ac5d31acb59f4043c85ad9d76c165880f1ec7e3 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 29 Feb 2016 19:29:58 +0100 Subject: [PATCH] simplify cauchy condition on chains --- algebra/agree.v | 14 +++++++------- algebra/cofe.v | 22 +++++++++++++++------- algebra/cofe_solver.v | 13 +++++-------- algebra/excl.v | 24 ++++++++++++------------ algebra/fin_maps.v | 4 ++-- algebra/frac.v | 24 ++++++++++++------------ algebra/option.v | 18 +++++++++--------- algebra/upred.v | 6 +++--- 8 files changed, 65 insertions(+), 60 deletions(-) diff --git a/algebra/agree.v b/algebra/agree.v index 6494453f7..4a77956df 100644 --- a/algebra/agree.v +++ b/algebra/agree.v @@ -15,7 +15,7 @@ Section agree. Context {A : cofeT}. Instance agree_validN : ValidN (agree A) := λ n x, - agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ≡{n'}≡ x n. + agree_is_valid x n ∧ ∀ n', n' ≤ n → x n ≡{n'}≡ x n'. Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x. Lemma agree_valid_le n n' (x : agree A) : @@ -29,9 +29,9 @@ Instance agree_dist : Dist (agree A) := λ n x y, (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧ (∀ n', n' ≤ n → agree_is_valid x n' → x n' ≡{n'}≡ y n'). Program Instance agree_compl : Compl (agree A) := λ c, - {| agree_car n := c (S n) n; agree_is_valid n := agree_is_valid (c (S n)) n |}. + {| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}. Next Obligation. - intros c n ?. apply (chain_cauchy c n (S (S n))), agree_valid_S; auto. + intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto. Qed. Definition agree_cofe_mixin : CofeMixin (agree A). Proof. @@ -53,7 +53,7 @@ Canonical Structure agreeC := CofeT agree_cofe_mixin. 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 n (x : agree A) i : ✓{n} x → i ≤ n → x i ≡{i}≡ x n. +Lemma agree_cauchy n (x : agree A) i : ✓{n} x → i ≤ n → x n ≡{i}≡ x i. Proof. by intros [? Hx]; apply Hx. Qed. Program Instance agree_op : Op (agree A) := λ x y, @@ -70,8 +70,8 @@ Proof. split; naive_solver. Qed. Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n). Proof. intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?]. - rewrite -(proj2 Hxy n') 1?(Hx n'); eauto using agree_valid_le. - by apply dist_le with n; try apply Hxy. + rewrite -(proj2 Hxy n') -1?(Hx n'); eauto using agree_valid_le. + symmetry. by apply dist_le with n; try apply Hxy. Qed. Instance: ∀ x : agree A, Proper (dist n ==> dist n) (op x). Proof. @@ -110,7 +110,7 @@ Proof. split; try (apply _ || done). - by intros n x1 x2 Hx y1 y2 Hy. - intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?]. - rewrite (Hx n'); last auto. + rewrite -(Hx n'); last auto. symmetry; apply dist_le with n; try apply Hx; auto. - intros x; apply agree_idemp. - by intros n x y [(?&?&?) ?]. diff --git a/algebra/cofe.v b/algebra/cofe.v index f3f680d11..d8c5c3391 100644 --- a/algebra/cofe.v +++ b/algebra/cofe.v @@ -42,7 +42,7 @@ Tactic Notation "cofe_subst" := Record chain (A : Type) `{Dist A} := { chain_car :> nat → A; - chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n) + chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n }. Arguments chain_car {_ _} _ _. Arguments chain_cauchy {_ _} _ _ _ _. @@ -52,7 +52,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 n c : compl c ≡{n}≡ c (S n) + mixin_conv_compl n c : compl c ≡{n}≡ c 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. @@ -84,7 +84,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 n (c : chain A) : compl c ≡{n}≡ c (S n). + Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c n. Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed. End cofe_mixin. @@ -118,6 +118,8 @@ Section cofe. Proof. by apply dist_proper. Qed. Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y. Proof. induction 2; eauto using dist_S. Qed. + Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y. + Proof. intros; eauto using dist_le. Qed. Instance ne_proper {B : cofeT} (f : A → B) `{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100. Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed. @@ -140,6 +142,11 @@ Section cofe. Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} : Proper ((≡) ==> (≡)) f | 100 := _. + Lemma conv_compl' n (c : chain A) : compl c ≡{n}≡ c (S n). + Proof. + transitivity (c n); first by apply conv_compl. symmetry. + apply chain_cauchy. omega. + Qed. Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y. Proof. split; intros; [by apply equiv_dist|]. @@ -157,7 +164,8 @@ Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed. Program Definition fixpoint_chain {A : cofeT} `{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]; intros [|i] ?; simpl; try omega. + intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; + try reflexivity || omega; [|]. - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. Qed. @@ -306,15 +314,15 @@ Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed. Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. Instance discrete_dist : Dist A := λ n x y, x ≡ y. - Instance discrete_compl : Compl A := λ c, c 1. + Instance discrete_compl : Compl A := λ c, c 0. Definition discrete_cofe_mixin : CofeMixin A. Proof. split. - intros x y; split; [done|intros Hn; apply (Hn 0)]. - done. - done. - - intros n c. rewrite /compl /discrete_compl /=. - symmetry; apply (chain_cauchy c 0 (S n)); omega. + - intros n c. rewrite /compl /discrete_compl /=; + symmetry; apply (chain_cauchy c 0 n). omega. Qed. Definition discreteC : cofeT := CofeT discrete_cofe_mixin. Global Instance discrete_discrete_cofe : Discrete discreteC. diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v index 793f2c312..8012d3287 100644 --- a/algebra/cofe_solver.v +++ b/algebra/cofe_solver.v @@ -61,7 +61,7 @@ Program Instance tower_compl : Compl tower := λ c, Next Obligation. intros c k; apply equiv_dist=> n. by rewrite (conv_compl n (tower_chain c k)) - (conv_compl n (tower_chain c (S k))) /= (g_tower (c (S n)) k). + (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k). Qed. Definition tower_cofe_mixin : CofeMixin tower. Proof. @@ -179,9 +179,7 @@ Program Definition unfold_chain (X : T) : chain (F T T) := Next Obligation. intros X n i Hi. assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi. - induction k as [|k IH]; simpl. - { rewrite -f_tower f_S -map_comp. - by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f. } + induction k as [|k IH]; simpl; first done. rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia. rewrite f_S -map_comp. by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f. @@ -190,7 +188,7 @@ 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 n (unfold_chain X)) - (conv_compl n (unfold_chain Y)) /= (HXY (S (S n))). + (conv_compl n (unfold_chain Y)) /= (HXY (S n)). Qed. Program Definition fold (X : F T T) : T := @@ -229,11 +227,10 @@ Proof. rewrite (map_ff_gg _ _ _ H). apply (_ : Proper (_ ==> _) (gg _)); by destruct H. - intros X; rewrite equiv_dist=> n /=. - rewrite /unfold /= (conv_compl n (unfold_chain (fold X))) /=. + 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. - rewrite f_tower. apply dist_S. by rewrite embed_tower. + + rewrite f_tower. apply dist_S. by rewrite embed_tower. + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower]. Qed. End solver. End solver. diff --git a/algebra/excl.v b/algebra/excl.v index c1483d05d..c802cf0f0 100644 --- a/algebra/excl.v +++ b/algebra/excl.v @@ -40,16 +40,16 @@ Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A). Proof. by inversion_clear 1. Qed. Program Definition excl_chain - (c : chain (excl A)) (a : A) (H : maybe Excl (c 1) = Some a) : chain A := + (c : chain (excl A)) (a : A) (H : maybe Excl (c 0) = Some a) : chain A := {| chain_car n := match c n return _ with Excl y => y | _ => a end |}. Next Obligation. - intros c a ? n [|i] ?; [omega|]; simpl. - destruct (c 1) eqn:?; simplify_eq/=. - by feed inversion (chain_cauchy c n (S i)). + intros c a ? n i ?; simpl. + destruct (c 0) eqn:?; simplify_eq/=. + by feed inversion (chain_cauchy c n i). Qed. Instance excl_compl : Compl (excl A) := λ c, - match Some_dec (maybe Excl (c 1)) with - | inleft (exist a H) => Excl (compl (excl_chain c a H)) | inright _ => c 1 + match Some_dec (maybe Excl (c 0)) with + | inleft (exist a H) => Excl (compl (excl_chain c a H)) | inright _ => c 0 end. Definition excl_cofe_mixin : CofeMixin (excl A). Proof. @@ -63,14 +63,14 @@ Proof. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; apply dist_S. - intros n c; unfold compl, excl_compl. - destruct (Some_dec (maybe Excl (c 1))) as [[a Ha]|]. - { assert (c 1 = Excl a) by (by destruct (c 1); simplify_eq/=). - assert (∃ b, c (S n) = Excl b) as [b Hb]. - { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. } + destruct (Some_dec (maybe Excl (c 0))) as [[a Ha]|]. + { assert (c 0 = Excl a) by (by destruct (c 0); simplify_eq/=). + assert (∃ b, c n = Excl b) as [b Hb]. + { feed inversion (chain_cauchy c 0 n); eauto with lia congruence. } rewrite Hb; constructor. by rewrite (conv_compl n (excl_chain c a Ha)) /= Hb. } - feed inversion (chain_cauchy c 0 (S n)); first lia; - constructor; destruct (c 1); simplify_eq/=. + feed inversion (chain_cauchy c 0 n); first lia; + constructor; destruct (c 0); simplify_eq/=. Qed. Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin. Global Instance excl_discrete : Discrete A → Discrete exclC. diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index 625f20969..174fa190c 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -12,7 +12,7 @@ Program Definition map_chain (c : chain (gmap K A)) (k : K) : chain (option A) := {| chain_car n := c n !! k |}. Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed. Instance map_compl : Compl (gmap K A) := λ c, - map_imap (λ i _, compl (map_chain c i)) (c 1). + map_imap (λ i _, compl (map_chain c i)) (c 0). Definition map_cofe_mixin : CofeMixin (gmap K A). Proof. split. @@ -25,7 +25,7 @@ Proof. + by intros m1 m2 m3 ?? k; trans (m2 !! k). - by intros n m1 m2 ? k; apply dist_S. - 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. + feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia. by rewrite conv_compl /=; apply reflexive_eq. Qed. Canonical Structure mapC : cofeT := CofeT map_cofe_mixin. diff --git a/algebra/frac.v b/algebra/frac.v index aeb1dfd92..0f49b8e3d 100644 --- a/algebra/frac.v +++ b/algebra/frac.v @@ -39,17 +39,17 @@ Global Instance Frac_dist_inj n : Inj2 (=) (dist n) (dist n) (@Frac A). Proof. by inversion_clear 1. Qed. Program Definition frac_chain (c : chain (frac A)) (q : Qp) (a : A) - (H : maybe2 Frac (c 1) = Some (q,a)) : chain A := + (H : maybe2 Frac (c 0) = Some (q,a)) : chain A := {| chain_car n := match c n return _ with Frac _ b => b | _ => a end |}. Next Obligation. - intros c q a ? n [|i] ?; [omega|]; simpl. - destruct (c 1) eqn:?; simplify_eq/=. - by feed inversion (chain_cauchy c n (S i)). + intros c q a ? n i ?; simpl. + destruct (c 0) eqn:?; simplify_eq/=. + by feed inversion (chain_cauchy c n i). Qed. Instance frac_compl : Compl (frac A) := λ c, - match Some_dec (maybe2 Frac (c 1)) with + match Some_dec (maybe2 Frac (c 0)) with | inleft (exist (q,a) H) => Frac q (compl (frac_chain c q a H)) - | inright _ => c 1 + | inright _ => c 0 end. Definition frac_cofe_mixin : CofeMixin (frac A). Proof. @@ -64,15 +64,15 @@ Proof. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; done || apply dist_S. - intros n c; unfold compl, frac_compl. - destruct (Some_dec (maybe2 Frac (c 1))) as [[[q a] Hx]|]. - { assert (c 1 = Frac q a) by (by destruct (c 1); simplify_eq/=). - assert (∃ b, c (S n) = Frac q b) as [y Hy]. - { feed inversion (chain_cauchy c 0 (S n)); + destruct (Some_dec (maybe2 Frac (c 0))) as [[[q a] Hx]|]. + { assert (c 0 = Frac q a) by (by destruct (c 0); simplify_eq/=). + assert (∃ b, c n = Frac q b) as [y Hy]. + { feed inversion (chain_cauchy c 0 n); eauto with lia congruence f_equal. } rewrite Hy; constructor; auto. by rewrite (conv_compl n (frac_chain c q a Hx)) /= Hy. } - feed inversion (chain_cauchy c 0 (S n)); first lia; - constructor; destruct (c 1); simplify_eq/=. + feed inversion (chain_cauchy c 0 n); first lia; + constructor; destruct (c 0); simplify_eq/=. Qed. Canonical Structure fracC : cofeT := CofeT frac_cofe_mixin. Global Instance frac_discrete : Discrete A → Discrete fracC. diff --git a/algebra/option.v b/algebra/option.v index 96e53f851..1bcf8ea22 100644 --- a/algebra/option.v +++ b/algebra/option.v @@ -9,15 +9,15 @@ Inductive option_dist : Dist (option A) := | None_dist n : None ≡{n}≡ None. Existing Instance option_dist. Program Definition option_chain - (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A := + (c : chain (option A)) (x : A) (H : c 0 = Some x) : chain A := {| chain_car n := from_option x (c n) |}. Next Obligation. - intros c x ? n [|i] ?; [omega|]; simpl. - destruct (c 1) eqn:?; simplify_eq/=. - by feed inversion (chain_cauchy c n (S i)). + intros c x ? n i ?; simpl. + destruct (c 0) eqn:?; simplify_eq/=. + by feed inversion (chain_cauchy c n i). Qed. Instance option_compl : Compl (option A) := λ c, - match Some_dec (c 1) with + match Some_dec (c 0) with | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None end. Definition option_cofe_mixin : CofeMixin (option A). @@ -32,12 +32,12 @@ Proof. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; apply dist_S. - intros n c; unfold compl, option_compl. - destruct (Some_dec (c 1)) as [[x Hx]|]. - { assert (is_Some (c (S n))) as [y Hy]. - { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. } + destruct (Some_dec (c 0)) as [[x Hx]|]. + { assert (is_Some (c n)) as [y Hy]. + { feed inversion (chain_cauchy c 0 n); eauto with lia congruence. } rewrite Hy; constructor. by rewrite (conv_compl n (option_chain c x Hx)) /= Hy. } - feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. + feed inversion (chain_cauchy c 0 n); eauto with lia congruence. constructor. Qed. Canonical Structure optionC := CofeT option_cofe_mixin. diff --git a/algebra/upred.v b/algebra/upred.v index e462a32a9..5e0cf611a 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -27,11 +27,11 @@ Section cofe. { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }. Instance uPred_dist : Dist (uPred M) := uPred_dist'. Program Instance uPred_compl : Compl (uPred M) := λ c, - {| uPred_holds n x := c (S n) n x |}. + {| uPred_holds n x := c n n x |}. Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed. Next Obligation. intros c n1 n2 x1 x2 ????; simpl in *. - apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken. + apply (chain_cauchy c n2 n1); eauto using uPred_weaken. Qed. Definition uPred_cofe_mixin : CofeMixin (uPred M). Proof. @@ -45,7 +45,7 @@ Section cofe. + intros P Q Q' HP HQ; split=> i x ??. by trans (Q i x);[apply HP|apply HQ]. - intros n P Q HPQ; split=> i x ??; apply HPQ; auto. - - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i (S n)); auto. + - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto. Qed. Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin. End cofe. -- GitLab