simplify cauchy condition on chains

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 [(?&?&?) ?].

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.

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.

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.

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.

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.

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.

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.