fix: fix module Collections.Seq functions using a binary predicate (#6412)

Hi Robin(@robin-aws), the MaxBy() and MinBy() functionalties are using a
comparator previously. To ensure precision, @huanerw0608 changed it to
using a bianry predicate to replace the comparator functions.

---------

Co-authored-by: huanerw0608 <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>

Author: 3 people

Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs

@@ -191,49 +191,47 @@ public static Dafny.ISequence<__T> Repeat<__T>(__T v, BigInteger length)
         goto TAIL_CALL_START;
       }
     }
-    public static __T MaxBy<__T>(Dafny.ISequence<__T> s, Func<__T, __T, BigInteger> comparator)
+    public static __T MaxBy<__T>(Dafny.ISequence<__T> s, Func<__T, __T, bool> lessThan)
     {
-      return Std.Collections.Seq.__default.MaxByHelper<__T>(s, BigInteger.One, (s).Select(BigInteger.Zero), comparator);
+      return Std.Collections.Seq.__default.MaxByHelper<__T>(s, BigInteger.One, (s).Select(BigInteger.Zero), lessThan);
     }
-    public static __T MaxByHelper<__T>(Dafny.ISequence<__T> s, BigInteger idx, __T current, Func<__T, __T, BigInteger> comparator)
+    public static __T MaxByHelper<__T>(Dafny.ISequence<__T> s, BigInteger idx, __T current, Func<__T, __T, bool> lessThan)
     {
     TAIL_CALL_START: ;
       if ((idx) == (new BigInteger((s).Count))) {
         return current;
       } else {
-        BigInteger _0_cmp = Dafny.Helpers.Id<Func<__T, __T, BigInteger>>(comparator)(current, (s).Select(idx));
-        __T _1_next = (((_0_cmp).Sign == -1) ? ((s).Select(idx)) : (current));
+        __T _0_next = ((Dafny.Helpers.Id<Func<__T, __T, bool>>(lessThan)(current, (s).Select(idx))) ? ((s).Select(idx)) : (current));
         Dafny.ISequence<__T> _in0 = s;
         BigInteger _in1 = (idx) + (BigInteger.One);
-        __T _in2 = _1_next;
-        Func<__T, __T, BigInteger> _in3 = comparator;
+        __T _in2 = _0_next;
+        Func<__T, __T, bool> _in3 = lessThan;
         s = _in0;
         idx = _in1;
         current = _in2;
-        comparator = _in3;
+        lessThan = _in3;
         goto TAIL_CALL_START;
       }
     }
-    public static __T MinBy<__T>(Dafny.ISequence<__T> s, Func<__T, __T, BigInteger> comparator)
+    public static __T MinBy<__T>(Dafny.ISequence<__T> s, Func<__T, __T, bool> lessThan)
     {
-      return Std.Collections.Seq.__default.MinByHelper<__T>(s, BigInteger.One, (s).Select(BigInteger.Zero), comparator);
+      return Std.Collections.Seq.__default.MinByHelper<__T>(s, BigInteger.One, (s).Select(BigInteger.Zero), lessThan);
     }
-    public static __T MinByHelper<__T>(Dafny.ISequence<__T> s, BigInteger idx, __T current, Func<__T, __T, BigInteger> comparator)
+    public static __T MinByHelper<__T>(Dafny.ISequence<__T> s, BigInteger idx, __T current, Func<__T, __T, bool> lessThan)
     {
     TAIL_CALL_START: ;
       if ((idx) == (new BigInteger((s).Count))) {
         return current;
       } else {
-        BigInteger _0_cmp = Dafny.Helpers.Id<Func<__T, __T, BigInteger>>(comparator)(current, (s).Select(idx));
-        __T _1_next = (((_0_cmp).Sign == 1) ? ((s).Select(idx)) : (current));
+        __T _0_next = ((Dafny.Helpers.Id<Func<__T, __T, bool>>(lessThan)((s).Select(idx), current)) ? ((s).Select(idx)) : (current));
         Dafny.ISequence<__T> _in0 = s;
         BigInteger _in1 = (idx) + (BigInteger.One);
-        __T _in2 = _1_next;
-        Func<__T, __T, BigInteger> _in3 = comparator;
+        __T _in2 = _0_next;
+        Func<__T, __T, bool> _in3 = lessThan;
         s = _in0;
         idx = _in1;
         current = _in2;
-        comparator = _in3;
+        lessThan = _in3;
         goto TAIL_CALL_START;
       }
     }

Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo

@@ -10,6 +10,7 @@ operation using Dafny's {:test} annotation.
 These tests serve as verification examples that work with Dafny's formal proofs.
 */
 
+
 module TestDuration {
   import Std.Duration
   import opened Std.BoundedInts
@@ -123,26 +124,16 @@ module TestDuration {
     AssertAndExpect(str[1] == 'T');
   }
 
-  function CompareHelper(d1: Duration.Duration, d2: Duration.Duration): int
-    ensures -1 <= CompareHelper(d1, d2) <= 1
-  {
-    if d1.seconds < d2.seconds then -1
-    else if d1.seconds > d2.seconds then 1
-    else if d1.millis < d2.millis then -1
-    else if d1.millis > d2.millis then 1
-    else 0
-  }
-
   method {:test} TestMaxByWithCompareHelper() {
     var d1 := Duration.Duration(1, 100);
     var d2 := Duration.Duration(2, 50);
     var d3 := Duration.Duration(0, 999);
     var durations := [d1, d2, d3];
 
-    var maxD := MaxBy(durations, CompareHelper);
-    var minD := MinBy(durations, CompareHelper);
+    var maxD := MaxBy(durations, Duration.Less);
+    var minD := MinBy(durations, Duration.Less);
 
-    expect CompareHelper(maxD, d2) == 0;
-    expect CompareHelper(minD, d3) == 0;
+    expect maxD == d2;
+    expect minD == d3;
   }
-}
+}

Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo

@@ -442,57 +442,42 @@ module Std.Collections.Seq {
   }
 
 
-  function MaxBy<T>(s: seq<T>, comparator: (T, T) -> int): T
+  function MaxBy<T>(s: seq<T>, lessThan: (T, T) -> bool): T
     requires |s| > 0
     decreases |s|
   {
-    MaxByHelper(s, 1, s[0], comparator)
+    MaxByHelper(s, 1, s[0], lessThan)
   }
 
-/// Helper function for MaxBy - iterates through sequence tracking the maximum
-  function MaxByHelper<T>(s: seq<T>, idx: nat, current: T, comparator: (T, T) -> int): T
+  function MaxByHelper<T>(s: seq<T>, idx: nat, current: T, lessThan: (T, T) -> bool): T
     requires idx <= |s|
     decreases |s| - idx
   {
     if idx == |s| then
       current
     else
-      var cmp := comparator(current, s[idx]);
-      var next := if cmp < 0 then s[idx] else current;
-      MaxByHelper(s, idx + 1, next, comparator)
-  }
-
-/// Find the minimum element in a sequence using a comparator function
-///
-/// The comparator function should return:
-///   -1 if a < b (first argument is less than second)
-///    0 if a == b (equal)
-///    1 if a > b (first argument is greater than second)
-///
-/// Example usage with Duration:
-///   var minDuration := MinBy(durations, Duration.Compare)
-  function MinBy<T>(s: seq<T>, comparator: (T, T) -> int): T
+      var next := if lessThan(current, s[idx]) then s[idx] else current;
+      MaxByHelper(s, idx + 1, next, lessThan)
+  }
+
+  function MinBy<T>(s: seq<T>, lessThan: (T, T) -> bool): T
     requires |s| > 0
     decreases |s|
   {
-    MinByHelper(s, 1, s[0], comparator)
+    MinByHelper(s, 1, s[0], lessThan)
   }
 
-/// Helper function for MinBy - iterates through sequence tracking the minimum
-  function MinByHelper<T>(s: seq<T>, idx: nat, current: T, comparator: (T, T) -> int): T
+  function MinByHelper<T>(s: seq<T>, idx: nat, current: T, lessThan: (T, T) -> bool): T
     requires idx <= |s|
     decreases |s| - idx
   {
     if idx == |s| then
       current
     else
-      var cmp := comparator(current, s[idx]);
-      var next := if cmp > 0 then s[idx] else current;
-      MinByHelper(s, idx + 1, next, comparator)
+      var next := if lessThan(s[idx], current) then s[idx] else current;
+      MinByHelper(s, idx + 1, next, lessThan)
   }
 
-
-
   /* Unzipping and zipping a sequence results in the original sequence */
   lemma LemmaZipOfUnzip<A, B>(xs: seq<(A, B)>)
     ensures Zip(Unzip(xs).0, Unzip(xs).1) == xs