From 8c82615376f31cc8f24052def6d955c18fa43e0e Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Wed, 8 Jul 2026 18:17:38 +0000
Subject: [PATCH] Add Ltac2 Int.min and Int.max

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
---
 .../22242-ltac2-int-min-max-Added.rst              |  4 ++++
 test-suite/ltac2/int_min_max.v                     | 12 ++++++++++++
 theories/Ltac2/Int.v                               | 14 ++++++++++++++
 3 files changed, 30 insertions(+)
 create mode 100644 doc/changelog/06-Ltac2-language/22242-ltac2-int-min-max-Added.rst
 create mode 100644 test-suite/ltac2/int_min_max.v

diff --git a/doc/changelog/06-Ltac2-language/22242-ltac2-int-min-max-Added.rst b/doc/changelog/06-Ltac2-language/22242-ltac2-int-min-max-Added.rst
new file mode 100644
index 000000000000..776fc4776e72
--- /dev/null
+++ b/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).
diff --git a/test-suite/ltac2/int_min_max.v b/test-suite/ltac2/int_min_max.v
new file mode 100644
index 000000000000..7851c639aa9f
--- /dev/null
+++ b/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)).
diff --git a/theories/Ltac2/Int.v b/theories/Ltac2/Int.v
index 9ce87e01bba2..681abee63986 100644
--- a/theories/Ltac2/Int.v
+++ b/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.