From 075274b896cb1be08f258ffc8c703f23176ab2ba Mon Sep 17 00:00:00 2001 From: Avi Shinnar Date: Fri, 22 Dec 2023 14:15:52 -0500 Subject: [PATCH] Prove conv_as_prob_1_rvmaxabs, proving a bunch of stuff about vectors on the way Signed-off-by: Avi Shinnar --- coq/ProbTheory/VectorRandomVariable.v | 84 ++++---------------- coq/QLearn/vecslln.v | 108 ++++++++++++++++++++----- coq/utils/DVector.v | 109 +++++++++++++++++++++++++- 3 files changed, 210 insertions(+), 91 deletions(-) diff --git a/coq/ProbTheory/VectorRandomVariable.v b/coq/ProbTheory/VectorRandomVariable.v index 98f496a1..ddb3b4bd 100644 --- 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 index b5783e17..d9614e50 100644 --- 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 index 2e1d9ee3..ac99e4ee 100644 --- 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 :=