Prove conv_as_prob_1_rvmaxabs, proving a bunch of stuff about vectors…

… on the way Signed-off-by: Avi Shinnar <[email protected]>
IBM · Dec 22, 2023 · 075274b · 075274b
1 parent 040e4a3
commit 075274b
Show file tree

Hide file tree

Showing 3 changed files with 210 additions and 91 deletions.
diff --git a/coq/ProbTheory/VectorRandomVariable.v b/coq/ProbTheory/VectorRandomVariable.v
@@ -88,7 +88,21 @@ Section VectorRandomVariables.
     rewrite vector_nth_create.
     f_equal; apply le_uniqueness_proof.
   Qed.
-
+
+  Lemma vector_of_funs_to_fun_to_vector_add_to_end {n} (x:Ts -> Td) (v : vector (Ts -> Td) n) (ω: Ts) :
+    (vector_of_funs_to_fun_to_vector (vector_add_to_end x v)) ω =
+      vector_add_to_end (x ω) (vector_of_funs_to_fun_to_vector v ω).
+  Proof.
+    apply vector_nth_eq; intros.
+    rewrite vector_of_funs_vector_nth.
+    destruct (Nat.eq_dec i n).
+    - subst.
+      now repeat rewrite (vector_nth_add_to_end_suffix).
+    - assert (pf':(i < n)%nat) by lia.
+      repeat rewrite (vector_nth_add_to_end_prefix _ _ _ _ pf').
+      now rewrite vector_of_funs_vector_nth.
+  Qed.
+
 End VectorRandomVariables.
 
 Require Import Expectation.
@@ -1517,74 +1531,6 @@ Section real_pullback.
     destruct (classic (x0 vector0)); tauto.
   Qed.
 
-  Program Definition vector_removelast {n} {A} (v:vector A (S n)) : vector A n :=
-    exist _ (removelast (proj1_sig v)) _.
-  Next Obligation.
-    destruct v.
-    simpl.
-    rewrite removelast_length.
-    rewrite e.
-    lia.
-  Qed.
-
-  Lemma vector_removelast_eq {n} {A} (v:vector A (S n)) :
-    v = vector_add_to_end (vector_nth n (Nat.lt_succ_diag_r _) v) (vector_removelast v).
-  Proof.
-    apply vector_eq.
-    destruct v; simpl.
-    revert n e.
-    induction x; [simpl; lia |].
-    intros.
-    destruct n.
-    - destruct x; simpl in *; try lia.
-      f_equal.
-    - assert (e' : length x = S n) by (simpl in *; lia).
-      specialize (IHx _ e').
-      simpl; destruct x; [simpl in *; lia |].
-      rewrite <- app_comm_cons.
-      f_equal.
-      etransitivity; try apply IHx.
-      f_equal.
-      f_equal.
-      generalize (vector_nth_in (S n)
-                                (Nat.lt_succ_diag_r (S n))
-                                (exist (fun l : list A => length l = S (S n)) (a :: a0 :: x) e))
-      ; intros HH1.
-      generalize (vector_nth_in n
-                                (Nat.lt_succ_diag_r n) (exist (fun l : list A => length l = S n) (a0 :: x) e'))
-      ; intros HH2.
-      simpl in *.
-      rewrite <- HH2 in HH1.
-      now invcs HH1.
-  Qed.
-
-  Lemma vector_removelast_add_to_end {n} {A} x (v:vector A n) :
-    v = vector_removelast (vector_add_to_end x v).
-  Proof.
-    apply vector_eq.
-    destruct v; simpl; clear.
-    induction x0; simpl; trivial.
-    destruct x0; simpl; trivial.
-    f_equal.
-    apply IHx0.
-  Qed.
-
-  Program Lemma vector_nth_removelast  {n} {A} (v:vector A (S n)) i pf :
-    vector_nth i pf (vector_removelast v) = vector_nth i _ v.
-  Proof.
-    rewrite (vector_removelast_eq v) at 2.
-    now rewrite (vector_nth_add_to_end_prefix _ _ _ _ pf).
-  Qed.
-
-  Program Lemma vector_removelast_create {T : Type} n f :
-    vector_removelast (vector_create (T:=T) 0 (S n) f) =
-      vector_create 0 n (fun i pf1 pf2 => f i pf1 _).
-  Proof.
-    apply vector_nth_eq; intros.
-    rewrite vector_nth_removelast.
-    repeat rewrite vector_nth_create.
-    now apply vector_create_fun_ext.
-  Qed.
 
   Lemma make_vector_from_seq_removelast {Ts : Type} (X : nat -> Ts -> R) (n : nat):
     forall (a : Ts),

diff --git a/coq/QLearn/vecslln.v b/coq/QLearn/vecslln.v
@@ -17,7 +17,7 @@ Set Bullet Behavior "Strict Subproofs".
 Set Default Goal Selector "!".
 
 Import ListNotations.
-
+  
 Section conv_as.
     Context {Ts : Type}
             {dom: SigmaAlgebra Ts}.
@@ -131,6 +131,20 @@ Section conv_as.
         apply vector_nth_ext.
     Qed.
 
+    Lemma vector_map_add_to_end {n} {A B} (x:A) (v:vector A n) (f:A->B):
+      vector_map f (vector_add_to_end x v) = vector_add_to_end (f x) (vector_map f v).
+    Proof.
+      apply vector_nth_eq; intros.
+      rewrite vector_nth_map.
+      destruct (Nat.eq_dec i n).
+      - subst.
+        now repeat rewrite vector_nth_add_to_end_suffix.
+      - assert (pf':(i < n)%nat) by lia.
+        repeat rewrite vector_nth_add_to_end_prefix with (pf2:=pf').
+        now rewrite vector_nth_map.
+    Qed.
+
+
     Lemma conv_as_prob_1_rvmaxabs {prts: ProbSpace dom} {size} (f : nat -> Ts -> vector R size)
       {rv : forall n, RandomVariable dom (Rvector_borel_sa size) (f n)} :
       almost prts (fun x => forall i pf, is_lim_seq (fun n => vector_nth i pf (f n x)) 0) ->
@@ -144,30 +158,82 @@ Section conv_as.
         apply almost_impl.
         apply all_almost.
         intros ??.
-        unfold rvmaxabs.
-        admit.
-      }
+        unfold rvmaxabs, Rvector_max_abs, Rvector_abs.
+        revert H; clear; intros HH.
+        generalize (iso_b_f (Isomorphism:=(@vector_iso nat R size)) (fun n => f n x)); intros eqqf.
+        cut ( is_lim_seq (fun n : nat => vector_fold_left Rmax (vector_map Rabs (iso_b (Isomorphism:=(@vector_iso nat R size)) (iso_f (Isomorphism:=(@vector_iso nat R size)) (fun n : nat => f n x)) n)) 0) 0).
+        {
+          apply is_lim_seq_ext; intros.
+          now rewrite eqqf.
+        } 
+        assert (HH':forall (i : nat) (pf : (i < size)%nat), is_lim_seq (fun n : nat => vector_nth i pf (iso_b (Isomorphism:=(@vector_iso nat R size)) (iso_f (Isomorphism:=(@vector_iso nat R size)) (fun n : nat => f n x)) n)) 0).
+        {
+          intros.
+          generalize (HH i pf).
+          apply is_lim_seq_ext; intros.
+          now rewrite eqqf.
+        }
+        assert (HH'':
+                  forall (i : nat) (pf : (i < size)%nat),
+                    is_lim_seq (fun n : nat => vector_nth i pf (vector_map Rabs (iso_b (iso_f (fun n0 : nat => f n0 x)) n))) 0).
+        {
+          intros i pf.
+          specialize (HH' i pf).
+          apply is_lim_seq_abs in HH'.
+          revert HH'.
+          unfold Rbar_abs.
+          rewrite Rabs_R0.
+          apply is_lim_seq_ext; intros nn.
+          now rewrite vector_nth_map.
+        } 
+        revert HH''.
+        generalize (iso_f (Isomorphism:=(@vector_iso nat R size)) (fun n0 : nat => f n0 x)).
+        clear.
+        intros v.
+        induction size, v using vector_ind_end; intros.
+        - eapply is_lim_seq_ext; try eapply is_lim_seq_const; intros; reflexivity.
+        - simpl in *.
+          cut (is_lim_seq
+                 (fun nn : nat =>
+                    Rmax (vector_fold_left Rmax (vector_map Rabs (vector_of_funs_to_fun_to_vector v nn)) 0) (Rabs (x nn))) 0).
+          {
+            apply is_lim_seq_ext; intros nn.
+            rewrite vector_of_funs_to_fun_to_vector_add_to_end, vector_map_add_to_end.
+            now rewrite  (vector_fold_left_add_to_end Rmax (n:=n)).
+          } 
+          apply is_lim_seq_max.
+          + apply IHv.
+            intros i pf.
+            assert (pf': (i < S n)%nat) by lia.
+            generalize (HH'' i pf').
+            apply is_lim_seq_ext; intros nn.
+            repeat rewrite vector_nth_map.
+            repeat rewrite vector_of_funs_vector_nth.
+            now rewrite (vector_nth_add_to_end_prefix _ _ _ _ pf).
+          + generalize (HH'' n (Nat.lt_succ_diag_r n)).
+            apply is_lim_seq_ext; intros nn.
+            rewrite vector_nth_map.
+            now rewrite vector_of_funs_vector_nth, vector_nth_add_to_end_suffix.
+      } 
       destruct (conv_as_prob_1_eps (fun n => rvmaxabs (f n)) H0 eps eps).
       exists x.
       intros.
       specialize (H1 n H2).
-      eapply Rge_trans.
-      - shelve.
-      - apply H1.
-        Unshelve.
-        right.
-        apply ps_proper.
-        intros ?.
-        simpl.
-        assert (rvmaxabs (f n) x0 = rvabs (rvmaxabs (f n)) x0).
-        {
-          unfold rvabs.
-          rewrite Rabs_right; trivial.
-          apply Rle_ge.
-          apply rvmaxabs_pos.
-        }
-        now rewrite H3.
-    Admitted.
+
+      eapply Rge_trans; [| apply H1].
+      right.
+      apply ps_proper.
+      intros ?.
+      simpl.
+      assert (rvmaxabs (f n) x0 = rvabs (rvmaxabs (f n)) x0).
+      {
+        unfold rvabs.
+        rewrite Rabs_right; trivial.
+        apply Rle_ge.
+        apply rvmaxabs_pos.
+      }
+      now rewrite H3.
+    Qed.
 
 End conv_as.
 

diff --git a/coq/utils/DVector.v b/coq/utils/DVector.v
@@ -1025,7 +1025,29 @@ Proof.
     congruence.
   - rewrite vector_length; reflexivity.
 Qed.
-
+
+Lemma vector_map_add_to_end {n} {A B} (x:A) (v:vector A n) (f:A->B):
+  vector_map f (vector_add_to_end x v) = vector_add_to_end (f x) (vector_map f v).
+Proof.
+  apply vector_nth_eq; intros.
+  rewrite vector_nth_map.
+  destruct (Nat.eq_dec i n).
+  - subst.
+    now repeat rewrite vector_nth_add_to_end_suffix.
+  - assert (pf':(i < n)%nat) by lia.
+    repeat rewrite vector_nth_add_to_end_prefix with (pf2:=pf').
+    now rewrite vector_nth_map.
+Qed.
+
+Lemma vector_fold_left_add_to_end {A B} (f: A -> B -> A) {n} (x:B) (v: vector B n) (init : A) :
+  vector_fold_left f (vector_add_to_end x v) init =
+    f (vector_fold_left f v init) x.
+Proof.
+  destruct v; simpl.
+  unfold vector_fold_left; simpl; clear e.
+  now rewrite fold_left_app.
+Qed.
+
 Lemma vector_fold_left_map_commute {A} {n} f g (v: vector A n) init
   (factor : forall a b, f (g a) (g b) = g (f a b)) :
   vector_fold_left f (vector_map g v) (g init) =
@@ -1036,6 +1058,91 @@ Proof.
   now apply fold_left_map_factor.
 Qed.
 
+
+Program Definition vector_removelast {n} {A} (v:vector A (S n)) : vector A n :=
+  removelast (proj1_sig v).
+Next Obligation.
+  now rewrite removelast_length, vector_length; simpl.
+Qed.
+
+Definition vector_last  {A} {n} (v:vector A (S n)) : A
+  := vector_nth n (Nat.lt_succ_diag_r n) v.
+
+
+Lemma vector_removelast_eq {n} {A} (v:vector A (S n)) :
+  v = vector_add_to_end (vector_last v) (vector_removelast v).
+Proof.
+  apply vector_eq.
+  destruct v; simpl.
+  revert n e.
+  induction x; [simpl; lia |].
+  intros.
+  destruct n.
+  - destruct x; simpl in *; try lia.
+    f_equal.
+  - assert (e' : length x = S n) by (simpl in *; lia).
+    specialize (IHx _ e').
+    simpl; destruct x; [simpl in *; lia |].
+    rewrite <- app_comm_cons.
+    f_equal.
+    etransitivity; try apply IHx.
+    f_equal.
+    f_equal.
+    generalize (vector_nth_in (S n)
+                  (Nat.lt_succ_diag_r (S n))
+                  (exist (fun l : list A => length l = S (S n)) (a :: a0 :: x) e))
+    ; intros HH1.
+    generalize (vector_nth_in n
+                  (Nat.lt_succ_diag_r n) (exist (fun l : list A => length l = S n) (a0 :: x) e'))
+    ; intros HH2.
+    simpl in *.
+    rewrite <- HH2 in HH1.
+    now invcs HH1.
+Qed.
+
+Lemma vector_removelast_add_to_end {n} {A} x (v:vector A n) :
+  v = vector_removelast (vector_add_to_end x v).
+Proof.
+  apply vector_eq.
+  destruct v; simpl; clear.
+  induction x0; simpl; trivial.
+  destruct x0; simpl; trivial.
+  f_equal.
+  apply IHx0.
+Qed.
+
+Program Lemma vector_nth_removelast  {n} {A} (v:vector A (S n)) i pf :
+  vector_nth i pf (vector_removelast v) = vector_nth i _ v.
+Proof.
+  rewrite (vector_removelast_eq v) at 2.
+  now rewrite (vector_nth_add_to_end_prefix _ _ _ _ pf).
+Qed.
+
+Program Lemma vector_removelast_create {T : Type} n f :
+  vector_removelast (vector_create (T:=T) 0 (S n) f) =
+    vector_create 0 n (fun i pf1 pf2 => f i pf1 _).
+Proof.
+  apply vector_nth_eq; intros.
+  rewrite vector_nth_removelast.
+  repeat rewrite vector_nth_create.
+  now apply vector_create_fun_ext.
+Qed.
+
+Lemma vector_ind_end {A} (P:forall {n}, vector A n -> Prop)
+  (Pzero : P vector0)
+  (Psucc : forall {n} (v:vector A n) x,
+      P v -> P (vector_add_to_end x v))
+  : forall {n} (v:vector A n), P v.
+Proof.
+  induction n; simpl.
+  - intros.
+    rewrite vector0_0.
+    exact Pzero.
+  - intros.
+    rewrite vector_removelast_eq.
+    now apply Psucc.
+Qed.
+
 Section ivector.
 
   Fixpoint ivector (T:Type) (n:nat) : Type :=