cleanup

IBM · Jan 27, 2025 · 166087d · 166087d
1 parent 7acc3f0
commit 166087d
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 13 deletions.
diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
@@ -10535,19 +10535,6 @@ End FixedPoint_contract.
 
   Existing Instance Rbar_le_pre.
 
-  Lemma fold_left_Rmax_abs l : List.Forall (Rle 0) l -> fold_left Rmax l 0 = Rmax_list l.
-  Proof.
-    intros.
-    rewrite fold_symmetric.
-    - induction l; simpl; trivial.
-      invcs H.
-      rewrite IHl; trivial.
-      destruct l; simpl; trivial.
-      rewrite Rmax_left; trivial.
-    - apply Rmax_assoc.
-    - apply Rmax_comm.
-  Qed.
-
   Instance finfun_sa : SigmaAlgebra (Rfct (sigT M.(act))) :=
     iso_sa (iso := Isomorphism_symm (finite_fun_vec_encoder finA EqDecsigT (B := R)))
       (Rvector_borel_sa _).

diff --git a/coq/utils/RealAdd.v b/coq/utils/RealAdd.v
@@ -3321,6 +3321,20 @@ Section Rmax_list.
     - assumption.
   Qed.
 
+  Lemma fold_left_Rmax_abs l : List.Forall (Rle 0) l -> fold_left Rmax l 0 = Rmax_list l.
+  Proof.
+    intros.
+    rewrite fold_symmetric.
+    - induction l; simpl; trivial.
+      invcs H.
+      rewrite IHl; trivial.
+      destruct l; simpl; trivial.
+      rewrite Rmax_left; trivial.
+    - apply Rmax_assoc.
+    - apply Rmax_comm.
+  Qed.
+
+
   Definition Rmax_list_map {A} (l : list A) (f : A -> R) := Rmax_list (List.map f l).
   Definition Rmin_list_map {A} (l : list A) (f : A -> R) := Rmin_list (List.map f l).