progress

Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>

Author: shinnar

coq/QLearn/infprod.v

@@ -1,4 +1,4 @@
-Require Import Reals Sums Lra Lia.
+Require Import ZArith Reals Sums Lra Lia.
 (* Require Import Coquelicot.Hierarchy Coquelicot.Series Coquelicot.Lim_seq Coquelicot.Rbar.*)
 Require Import Coquelicot.Coquelicot.
 Require Import LibUtils.
@@ -493,7 +493,7 @@ Proof.
   replace (S n2 - n1)%nat with ((S m - n1) + (S n2 - S m))%nat by lia.
   rewrite seq_plus.
   rewrite List.fold_right_app.
-  rewrite fold_right_plus_acc.
+  rewrite (@fold_right_plus_acc G).
   now replace (n1 + (S m - n1))%nat with (S m) by lia.
 Qed.
 
@@ -534,7 +534,7 @@ Qed.
             now simpl.
         + intros.
           unfold sum_n.
-          rewrite sum_split with (m := (nk-1)%nat); try lia.
+          rewrite (@sum_split R_AbelianGroup) with (m := (nk-1)%nat); try lia.
           apply Rplus_eq_compat_l.
           replace (S (nk - 1)) with (nk) by lia.
           apply sum_n_m_shift.
@@ -562,7 +562,8 @@ Qed.
       cut (ex_lim_seq (fun n : nat => sum_n_m α 0 (nk + S n) - sum_n_m α 0 nk)).
       {
         apply ex_lim_seq_ext; intros.
-        rewrite (sum_split_plus α 0 nk (S n)); try lia.
+        change ((@sum_n_m R_AbelianGroup α 0 (nk + S n) - @sum_n_m R_AbelianGroup α 0 nk) = @sum_n_m R_AbelianGroup α (S nk) (n + S nk)).
+        rewrite (@sum_split_plus R_AbelianGroup α 0 nk (S n) ltac:(lia) ltac:(lia)).
         unfold plus; simpl.
         field_simplify.
         f_equal.
@@ -948,7 +949,7 @@ Proof.
     specialize (IHk H1).
     apply Rle_trans with (r2 := part_prod_n (pos_sq_fun F) (m + k) n); trivial.
     replace (m + S k)%nat with (S (m+k)%nat) by lia.
-    destruct (le_gt_dec (S (m+k)) n).
+    destruct (Compare_dec.le_gt_dec (S (m+k)) n).
     + apply max_bounded1_pre_le; trivial.
       intros; apply pos_sq_bounded1; trivial.
     + rewrite (part_prod_n_1 (pos_sq_fun F) (S (m + k)%nat)) ; [|lia].
@@ -1110,7 +1111,7 @@ Section Dvoretsky.
 Theorem Dvoretzky4_0 (F: nat -> posreal) (sigma V : nat -> R) :
   (forall (n:nat), V (S n) <= (F n) * (V n) + (sigma n)) ->
   (forall (n:nat), 
-      V (S n) <= sum_n (fun k => (sigma k)*(part_prod_n F (S k) n)) n + 
+      V (S n) <= @sum_n R_AbelianGroup (fun k => (sigma k)*(part_prod_n F (S k) n)) n + 
                  (V 0%nat)*(part_prod_n F 0 n)).
 Proof.
   intros.
@@ -1145,8 +1146,8 @@ Qed.
 
 Lemma sum_bound_prod_A (F : nat -> posreal) (sigma : nat -> R) (A : R) (n m:nat) :
   (forall r s, part_prod_n (pos_sq_fun F) r s <= A) ->
-  sum_n_m (fun k => (Rsqr (sigma k))*(part_prod_n (pos_sq_fun F) (S k) n)) (S m) n <=
-  (sum_n_m (fun k => Rsqr (sigma k)) (S m) n) * A.
+  @sum_n_m R_AbelianGroup (fun k => (Rsqr (sigma k))*(part_prod_n (pos_sq_fun F) (S k) n)) (S m) n <=
+  (@sum_n_m R_AbelianGroup (fun k => Rsqr (sigma k)) (S m) n) * A.
 Proof.
   intros.
   rewrite <- sum_n_m_mult_r with (a := A).
@@ -1160,8 +1161,8 @@ Qed.
 
 Lemma sum_bound3_max (F : nat -> posreal) (sigma : nat -> R) (n m:nat) :
   (S m <= n)%nat ->
-  sum_n (fun k => (Rsqr (sigma k))*(part_prod_n (pos_sq_fun F) (S k) n)) m <=
-  (sum_n (fun k => (Rsqr (sigma k))) m) * (max_prod_fun (pos_sq_fun F) (S m) n).
+  @sum_n R_AbelianGroup (fun k => (Rsqr (sigma k))*(part_prod_n (pos_sq_fun F) (S k) n)) m <=
+  (@sum_n R_AbelianGroup (fun k => (Rsqr (sigma k))) m) * (max_prod_fun (pos_sq_fun F) (S m) n).
 Proof.  
   intros.
   rewrite <- sum_n_mult_r with (a := (max_prod_fun (pos_sq_fun F) (S m) n)).
@@ -1176,15 +1177,16 @@ Theorem Dvoretzky4_8_5 (F : nat -> posreal) (sigma V: nat -> R) (n m:nat) (A:R):
   (forall (n:nat), Rsqr (V (S n)) <= (pos_sq_fun F) n * Rsqr (V n) + Rsqr (sigma n)) ->
   (m<n)%nat ->
    Rsqr (V (S n)) <= 
-     ( sum_n_m (fun k => Rsqr (sigma k)) (S m) n) * A +
-     (Rsqr (V 0%nat) + sum_n (fun k => (Rsqr (sigma k))) m) *
+     ( @sum_n_m R_AbelianGroup (fun k => Rsqr (sigma k)) (S m) n) * A +
+     (Rsqr (V 0%nat) + @sum_n R_AbelianGroup (fun k => (Rsqr (sigma k))) m) *
              (max_prod_fun (pos_sq_fun F) (S m) n).
 Proof.
   intros F1 Vsqle mn.
   generalize (Dvoretzky4_0 (pos_sq_fun F) (fun k => Rsqr(sigma k)) (fun k => Rsqr (V k))).
   intros.
   specialize (H Vsqle n).
   unfold sum_n in H.
+  
   rewrite (sum_split _ _ _ m) in H; trivial; [|lia].
   generalize (sum_bound_prod_A F sigma A n m F1); intros.
   generalize (max_prod_le (pos_sq_fun F) 0 (S m) n); intros.
@@ -1204,8 +1206,8 @@ Lemma sum_bound_prod_A_sigma1
       (F : nat -> posreal) (sigma : nat -> R) (A : R) (n m:nat) :
   (forall r s, part_prod_n (pos_sq_fun F) r s <= A) ->
   (forall n, 0 <= sigma n) ->
-  sum_n_m (fun k => (sigma k)*(part_prod_n (pos_sq_fun F) (S k) n)) (S m) n <=
-  (sum_n_m sigma (S m) n) * A.
+  @sum_n_m R_AbelianGroup (fun k => (sigma k)*(part_prod_n (pos_sq_fun F) (S k) n)) (S m) n <=
+  (@sum_n_m R_AbelianGroup sigma (S m) n) * A.
 Proof.
   intros.
   rewrite <- sum_n_m_mult_r with (a := A).
@@ -1218,8 +1220,8 @@ Qed.
 Lemma sum_bound3_max_sigma1 (F : nat -> posreal) (sigma : nat -> R) (n m:nat) :
   (S m <= n)%nat ->
   (forall n, 0 <= sigma n) ->
-  sum_n (fun k => (sigma k)*(part_prod_n (pos_sq_fun F) (S k) n)) m <=
-  (sum_n sigma m) * (max_prod_fun (pos_sq_fun F) (S m) n).
+  @sum_n R_AbelianGroup (fun k => (sigma k)*(part_prod_n (pos_sq_fun F) (S k) n)) m <=
+  (@sum_n R_AbelianGroup sigma m) * (max_prod_fun (pos_sq_fun F) (S m) n).
 Proof.  
   intros.
   rewrite <- sum_n_mult_r with (a := (max_prod_fun (pos_sq_fun F) (S m) n)).
@@ -1238,8 +1240,8 @@ Theorem Dvoretzky4_8_5_V1 (F : nat -> posreal) (sigma V: nat -> R) (n m:nat) (A:
   (forall (n:nat), 0 <= sigma n) ->
   (m<n)%nat ->
   V (S n) <= 
-  (sum_n_m sigma (S m) n) * A +
-  (V 0%nat + sum_n sigma m) *
+  (@sum_n_m R_AbelianGroup sigma (S m) n) * A +
+  (V 0%nat + @sum_n R_AbelianGroup sigma m) *
              (max_prod_fun (pos_sq_fun F) (S m) n).
 Proof.
   intros F1 Vle Vpos sigma_pos mn.
@@ -1269,12 +1271,12 @@ Theorem Dvoretzky4_8_5_1 (F : nat -> posreal) (sigma V: nat -> R) (n m:nat) (A s
   is_series (fun n => Rsqr (sigma n)) sigmasum ->   
   (m<n)%nat ->
    Rsqr (V (S n)) <= 
-      (sum_n_m (fun k => Rsqr (sigma k)) (S m) n) * A +
+      (@sum_n_m R_AbelianGroup (fun k => Rsqr (sigma k)) (S m) n) * A +
      (Rsqr (V 0%nat) + sigmasum) * (max_prod_fun (pos_sq_fun F) (S m) n).      
 Proof.
   intros.
   generalize (Dvoretzky4_8_5 F sigma V n m A H H0 H2); intros.
-  assert (sum_n (fun k : nat => (sigma k)²) m <= sigmasum).
+  assert (@sum_n R_AbelianGroup (fun k : nat => (sigma k)²) m <= sigmasum).
   - assert (H1' := H1).
     apply is_series_unique in H1.
     assert (ex_series (fun k : nat => (sigma k)²)).
@@ -1300,12 +1302,12 @@ Theorem Dvoretzky4_8_5_1_V1 (F : nat -> posreal) (sigma V: nat -> R) (n m:nat) (
   is_series sigma sigmasum ->   
   (m<n)%nat ->
    V (S n) <= 
-      (sum_n_m sigma (S m) n) * A +
+      (@sum_n_m R_AbelianGroup sigma (S m) n) * A +
       (V 0%nat + sigmasum) * (max_prod_fun (pos_sq_fun F) (S m) n).      
 Proof.
   intros.
   generalize (Dvoretzky4_8_5_V1 F sigma V n m A H H0 H2 H1 H4); intros.
-  assert (sum_n sigma m <= sigmasum).
+  assert (@sum_n R_AbelianGroup sigma m <= sigmasum).
   - assert (H3' := H3).
     apply is_series_unique in H3.
     assert (ex_series sigma).

coq/QLearn/slln.v

@@ -1,12 +1,10 @@
-Require Import Qreals.
 Require Import Lra Lia Reals RealAdd RandomVariableL2 Coquelicot.Coquelicot.
 Require Import Morphisms FiniteType List ListAdd Permutation infprod Almost NumberIso.
 Require Import Sums SimpleExpectation PushNeg.
 Require Import EquivDec.
 Require Import Classical.
 Require Import ClassicalChoice.
 Require Import IndefiniteDescription ClassicalDescription.
-Require QArith.
 Require Import BorelSigmaAlgebra.
 Require Import utils.Utils.
 Require Import ConditionalExpectation.
@@ -1693,7 +1691,7 @@ Qed.
       rv_unfold.
       rewrite  Rmax_list_app by now simpl.
       unfold Rmax.
-      rewrite plus_0_l.
+      rewrite Nat.add_0_l.
       destruct (Rle_dec (Rmax_list (map (fun n : nat => F n a) (seq 0 (S k)))) (F (S k) a)); trivial.
     } 
     apply IsFiniteExpectation_case.
@@ -2867,12 +2865,12 @@ Qed.
   Qed.
 
    Lemma sum_shift_diff (X : nat -> R) (m a : nat) :
-     sum_n X (a + S m) - sum_n X m =
-     sum_n (fun n0 : nat => X (n0 + S m)%nat) a.
+     @sum_n R_AbelianGroup X (a + S m) - @sum_n R_AbelianGroup X m =
+     @sum_n R_AbelianGroup (fun n0 : nat => X (n0 + S m)%nat) a.
    Proof.
      rewrite <- sum_n_m_shift.
      unfold sum_n.
-     rewrite (@sum_split _ _ _ _ m); try lia.
+     rewrite (@sum_split R_AbelianGroup _ _ _ m); try lia.
      unfold plus; simpl.
      lra.
    Qed.
@@ -3997,7 +3995,7 @@ Qed.
         match_destr.
       }
       unfold independent_event_collection in indep.
-      destruct (in_dec NPeano.Nat.eq_dec 0%nat l).
+      destruct (in_dec Nat.eq_dec 0%nat l).
       - pose (ll := 1%nat :: map (fun n => match n with
                                        | 0%nat => n
                                        | S n' => S n
@@ -4024,13 +4022,28 @@ Qed.
         etransitivity; [| etransitivity]; [| apply indep' |].
         + apply ps_proper.
           unfold ll.
-          rewrite perm.
-          simpl.
+          etransitivity.
+          { apply list_inter_equivlist_proper.
+            apply Permutation_equivlist.
+            apply Permutation_map.
+            apply perm.
+          }
+          etransitivity; cycle 1.
+          {
+            apply list_inter_equivlist_proper.
+            apply Permutation_equivlist.
+            apply Permutation_map.
+            apply Permutation_cons; [reflexivity |].
+            apply Permutation_map.
+            symmetry.
+            apply perm.
+          }
+          repeat rewrite map_cons.
           repeat rewrite list_inter_cons.
           rewrite event_inter_assoc.
           apply event_inter_proper.
-          * rewrite event_inter_comm.
-             apply H6.
+          * red; simpl.
+            now rewrite pre_event_inter_comm.
           * apply list_inter_proper.
              rewrite map_map.
              apply Forall2_map_f.
@@ -4924,7 +4937,7 @@ Qed.
     - apply collection_take_preserves_disjoint.
       intros ????[??][??]; simpl in *.
       apply H.
-      apply le_antisym.
+      apply Nat.le_antisymm.
       + assert (INR n1 < INR (S n2)) by (rewrite S_INR; lra).
         apply INR_lt in H4.
         lia.
@@ -5292,7 +5305,7 @@ Qed.
               apply Rbar_finite_eq.
               lra.
            -- intros.
-              rewrite sum_split with (m := n); try lia.
+              rewrite (@sum_split R_AbelianGroup) with (m := n); try lia.
               rewrite sum_n_m_ext_loc with (b := fun _ => zero).
               ++ rewrite sum_n_m_const_zero.
                  rewrite plus_zero_l.
@@ -5324,7 +5337,7 @@ Qed.
               apply ps_pos.
        + intros.
          unfold sum_n.
-         rewrite sum_split with (m := n); try lia.
+         rewrite (@sum_split R_AbelianGroup) with (m := n); try lia.
          reflexivity.
     Qed.
 
@@ -5387,7 +5400,7 @@ Qed.
           -- replace (n0 + S (S a))%nat with (S (n0 + S a)) by lia.
              rewrite sum_Rbar_n_finite_sum_n.
              unfold sum_n.
-             rewrite sum_split with (m := a); try lia.
+             rewrite (@sum_split R_AbelianGroup) with (m := a); try lia.
              rewrite plus_comm.
              rewrite sum_n_m_ext_loc with (b := (fun _ => @zero R_AbelianGroup)).
              ++ rewrite sum_n_m_const_zero.

coq/utils/Sums.v

@@ -1243,7 +1243,7 @@ Qed.
 
 
 Lemma sum_n_m_shift (α : nat -> R) (k n0 : nat) :
-  sum_n_m α k (n0 + k)%nat = sum_n (fun n1 : nat => α (n1 + k)%nat) n0.
+  @sum_n_m R_AbelianGroup α k (n0 + k)%nat = @sum_n R_AbelianGroup (fun n1 : nat => α (n1 + k)%nat) n0.
 Proof.
   unfold sum_n.
   induction n0.
@@ -1259,7 +1259,7 @@ Qed.
 
 Lemma sum_n_m_pos a n1 n2 :
   (forall n, (n1 <= n <= n2)%nat -> 0 <= a n) ->
-  0 <= (sum_n_m a n1 n2).
+  0 <= (@sum_n_m R_AbelianGroup a n1 n2).
 Proof.
   intros.
   rewrite sum_n_m_fold_right_seq.
@@ -1276,7 +1276,7 @@ Qed.
 
 
 Lemma sum_n_pos_incr a n1 n2 : (forall n, (n1 < n <= n2)%nat -> 0 <= a n) ->
-                               (n1 <= n2)%nat -> sum_n a n1 <= sum_n a n2.
+                               (n1 <= n2)%nat -> @sum_n R_AbelianGroup a n1 <= @sum_n R_AbelianGroup a n2.
 Proof.
   intros.
   destruct (Nat.eq_dec n1 n2); [rewrite e; lra|].