Add Ltac2 Int.min and Int.max

doc/changelog/06-Ltac2-language/22242-ltac2-int-min-max-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 functions ``Int.min`` and ``Int.max``
+  (`#22242 <https://github.com/rocq-prover/rocq/pull/22242>`_,
+  by Jason Gross).

test-suite/ltac2/int_min_max.v

@@ -0,0 +1,12 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Type exn ::= [ Regression_Test_Failure ].
+Ltac2 check (b : bool) := if b then () else Control.throw Regression_Test_Failure.
+
+Ltac2 Eval check (Int.equal (Int.min 1 2) 1).
+Ltac2 Eval check (Int.equal (Int.min 2 1) 1).
+Ltac2 Eval check (Int.equal (Int.min 1 1) 1).
+Ltac2 Eval check (Int.equal (Int.min (Int.neg 1) 1) (Int.neg 1)).
+Ltac2 Eval check (Int.equal (Int.max 1 2) 2).
+Ltac2 Eval check (Int.equal (Int.max 2 1) 2).
+Ltac2 Eval check (Int.equal (Int.max (Int.neg 3) (Int.neg 5)) (Int.neg 3)).

theories/Ltac2/Int.v

@@ -47,3 +47,17 @@ Ltac2 ge (x : int) (y : int) :=
   | true => true
   | false => gt x y
   end.
+
+(** [min x y] returns the smaller of [x] and [y]. *)
+Ltac2 min (x : int) (y : int) : int :=
+  match le x y with
+  | true => x
+  | false => y
+  end.
+
+(** [max x y] returns the larger of [x] and [y]. *)
+Ltac2 max (x : int) (y : int) : int :=
+  match le x y with
+  | true => y
+  | false => x
+  end.