From fa9a32b5c8f5d3b8ca0db221709d3da77c9222ea Mon Sep 17 00:00:00 2001
From: Jesse Alama <jessealama@users.noreply.github.com>
Date: Mon, 16 Mar 2026 11:52:06 +0100
Subject: [PATCH] fix: correct swapped operands in Std.Time subtraction
 instances (#12919)

This PR fixes the `HSub PlainTime Duration` instance, which had its
operands reversed: it computed `duration - time` instead of `time -
duration`. For example, subtracting 2 minutes from `time("13:02:01")`
would give `time("10:57:59")` rather than the expected
`time("13:00:01")`. We also noticed that `HSub PlainDateTime
Millisecond.Offset` is similarly affected.

Closes #12918
---
 src/Std/Time/DateTime/PlainDateTime.lean |  2 +-
 src/Std/Time/Duration.lean               |  2 +-
 tests/elab/timeSub.lean                  | 55 ++++++++++++++++++++++++
 3 files changed, 57 insertions(+), 2 deletions(-)
 create mode 100644 tests/elab/timeSub.lean

diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean
index d1c3eb9474..4f14a41981 100644
--- a/src/Std/Time/DateTime/PlainDateTime.lean
+++ b/src/Std/Time/DateTime/PlainDateTime.lean
@@ -566,7 +566,7 @@ instance : HAdd PlainDateTime Millisecond.Offset PlainDateTime where
   hAdd := addMilliseconds
 
 instance : HSub PlainDateTime Millisecond.Offset PlainDateTime where
-  hSub := addMilliseconds
+  hSub := subMilliseconds
 
 instance : HAdd PlainDateTime Second.Offset PlainDateTime where
   hAdd := addSeconds
diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean
index c89495f8eb..35ff4ca3d8 100644
--- a/src/Std/Time/Duration.lean
+++ b/src/Std/Time/Duration.lean
@@ -384,7 +384,7 @@ instance : HAdd PlainTime Duration PlainTime where
    hAdd pt d := PlainTime.ofNanoseconds (d.toNanoseconds + pt.toNanoseconds)
 
 instance : HSub PlainTime Duration PlainTime where
-   hSub pt d := PlainTime.ofNanoseconds (d.toNanoseconds - pt.toNanoseconds)
+   hSub pt d := PlainTime.ofNanoseconds (pt.toNanoseconds - d.toNanoseconds)
 
 end Duration
 end Time
diff --git a/tests/elab/timeSub.lean b/tests/elab/timeSub.lean
new file mode 100644
index 0000000000..ba9aac9ae2
--- /dev/null
+++ b/tests/elab/timeSub.lean
@@ -0,0 +1,55 @@
+import Std.Time
+open Std.Time
+
+def dt := datetime("2000-01-20T03:02:01")
+
+/--
+info: datetime("2000-01-20T03:02:01.500000000")
+-/
+#guard_msgs in
+#eval dt + (500 : Millisecond.Offset)
+
+/--
+info: datetime("2000-01-20T03:02:00.500000000")
+-/
+#guard_msgs in
+#eval dt - (500 : Millisecond.Offset)
+
+/--
+info: datetime("2000-01-20T03:02:04.000000000")
+-/
+#guard_msgs in
+#eval dt + (3000 : Millisecond.Offset)
+
+/--
+info: datetime("2000-01-20T03:01:58.000000000")
+-/
+#guard_msgs in
+#eval dt - (3000 : Millisecond.Offset)
+
+/--
+info: true
+-/
+#guard_msgs in
+#eval (dt + (1234 : Millisecond.Offset) - (1234 : Millisecond.Offset)) == dt
+
+def t := time("13:02:01")
+def dur := Duration.ofSeconds (120 : Second.Offset)
+
+/--
+info: time("13:04:01.000000000")
+-/
+#guard_msgs in
+#eval t + dur
+
+/--
+info: time("13:00:01.000000000")
+-/
+#guard_msgs in
+#eval t - dur
+
+/--
+info: true
+-/
+#guard_msgs in
+#eval (t + dur - dur) == t