fix: overeager Nat.sub constant folding (#11043)

This PR fixes a case of overeager constant folding on Nat where the
compiler would mistakenly assume `0 - x = x` (see also #11042 for the
same bug on UInts).

Author: Rob23oba

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -355,7 +355,7 @@ def arithmeticFolders : List (Name × Folder) := [
   (``UInt16.add,  Folder.first #[Folder.mkBinary UInt16.add, Folder.leftRightNeutral (0 : UInt16)]),
   (``UInt32.add,  Folder.first #[Folder.mkBinary UInt32.add, Folder.leftRightNeutral (0 : UInt32)]),
   (``UInt64.add,  Folder.first #[Folder.mkBinary UInt64.add, Folder.leftRightNeutral (0 : UInt64)]),
-  (``Nat.sub,    Folder.first #[Folder.mkBinary Nat.sub, Folder.leftRightNeutral 0]),
+  (``Nat.sub,    Folder.first #[Folder.mkBinary Nat.sub, Folder.leftAnnihilator 0 0, Folder.rightNeutral 0]),
   (``UInt8.sub,  Folder.first #[Folder.mkBinary UInt8.sub, Folder.rightNeutral (0 : UInt8)]),
   (``UInt16.sub,  Folder.first #[Folder.mkBinary UInt16.sub, Folder.rightNeutral (0 : UInt16)]),
   (``UInt32.sub,  Folder.first #[Folder.mkBinary UInt32.sub, Folder.rightNeutral (0 : UInt32)]),

tests/lean/run/compiler_bug_neutral.lean

@@ -0,0 +1,26 @@
+/-!
+This test guards against a constant folding bug
+-/
+
+
+def danger : UInt64 := UInt64.ofNat UInt64.size - 1
+theorem danger_eq_large : danger = 18446744073709551615 := by decide +kernel
+/--
+error: Tactic `native_decide` evaluated that the proposition
+  danger = 1
+is false
+-/
+#guard_msgs in
+theorem danger_eq_one : danger = 1 := by native_decide
+theorem bad : False := by simpa using danger_eq_large.symm.trans danger_eq_one
+
+def danger2 (x : Nat) : Nat := 0 - x
+theorem danger2_eq_zero : danger2 1 = 0 := by decide +kernel
+/--
+error: Tactic `native_decide` evaluated that the proposition
+  danger2 1 = 1
+is false
+-/
+#guard_msgs in
+theorem danger2_eq_one : danger2 1 = 1 := by native_decide
+theorem bad2 : False := by simpa using danger2_eq_zero.symm.trans danger2_eq_one