chore: fix tests

This modification improves the performance of the example in issue #4861.
It no longer times out but is still expensive.

Here is the analysis of the performance issue: Given `(x : Int)`, to elaborate `x ^ 1`, a few default instances have to be tried.

First, the homogeneous instance is tried and fails since `Int` does
not implement `Pow Int`. Then, the `NatPow` instance is tried, and it
also fails. The same process is performed for each term of the form `p
^ 1`. There are seveal of them at #4861. After all of these fail,
the lower priority default instance for numerals is tried, and
`x ^ 1` becomes `x ^ (1 : Nat)`. Then, `HPow Int Nat Int` can be
applied, and the elaboration succeeds. However, this process has
to be repeated for every single term of the form `p ^ 1`.
The elaborator tries all homogeneous `HPow` and `NatPow` instances
for all `p ^ 1` terms before trying the lower priority default instance `OfNat`.

This commit ensures `Int` has a `NatPow` instance instead of `HPow Int
Nat Int`. This change shortcuts the process, but it still first
tries the homogeneous `HPow` instance, fails, and then tries
`NatPow`. The elaboration can be made much more efficient by writing `p ^ (1 : Nat)`.

src/Init/Data/Int/Basic.lean

@@ -322,8 +322,8 @@ protected def pow (m : Int) : Nat → Int
   | 0      => 1
   | succ n => Int.pow m n * m
 
-instance : HPow Int Nat Int where
-  hPow := Int.pow
+instance : NatPow Int where
+  pow := Int.pow
 
 instance : LawfulBEq Int where
   eq_of_beq h := by simp [BEq.beq] at h; assumption

tests/lean/2040.lean

@@ -1,41 +0,0 @@
-/-! Unification across `calc` steps -/
-
--- Tests were written when `^` was still using `binop%`
-macro_rules | `($x ^ $y) => `(binop% HPow.hPow $x $y)
-
-example (n : Nat) (a : Int) : a = 22 :=
-  calc
-    a = 2 ^ n := sorry -- error
-    _ = (22 : Int) := sorry
-
-example (n : Nat) (a : Int) : a = 22 :=
-  calc
-    a = (37 : Int) := sorry
-    _ = 2 ^ n := sorry -- should be same error as above
-    _ = (22 : Int) := sorry
-
-example (n : Nat) (a : Int) : a = (2 : Int) ^ n :=
-  calc
-    a = (37 : Int) := sorry
-    _ = 2 ^ n := sorry -- should be same error as above
-
-example (n : Nat) (h : n = 42) : 42 = (n : Int) :=
-  calc
-    (42 : Int) = 42 := rfl
-    _ = n := h ▸ rfl
-      --^ coe needs to be inserted here
-
-example (n : Nat) (h : n = 42) : 42 = (n : Int) :=
-  calc
-    (42 : Int) = 42 := rfl -- TODO: type of 42 should match goal (i.e., `Int`)
-    _ = n := h ▸ rfl
-      --^ coe needs to be inserted here
-
-example (n : Nat) (h : n = 42) : 42 = (n : Int) :=
-  calc
-    (_ : Int) = 42 := rfl -- TODO: type of 42 should match goal (i.e., `Int`)
-    _ = n := h ▸ rfl
-      --^ coe needs to be inserted here
-
-example := calc 1 = 1 := rfl
-example := by calc 1 = 1 := rfl

tests/lean/2040.lean.expected.out

@@ -1,15 +0,0 @@
-2040.lean:8:8-8:13: error: failed to synthesize
-  HPow Nat Nat Int
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
-2040.lean:14:8-14:13: error: failed to synthesize
-  HPow Nat Nat Int
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
-2040.lean:20:8-20:13: error: failed to synthesize
-  HPow Nat Nat Int
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
-2040.lean:18:2-20:22: error: type mismatch
-  trans (sorryAx (a = 37)) (sorryAx (37 = 2 ^ n))
-has type
-  a = @OfNat.ofNat Nat 2 (instOfNatNat 2) ^ n : Prop
-but is expected to have type
-  a = @OfNat.ofNat Int 2 instOfNat ^ n : Prop

tests/lean/2220.lean

@@ -1,26 +0,0 @@
-/-! Coercions should ignore the RHS of `^` -/
-
-set_option pp.coercions false
-set_option pp.explicit true
-
-#check (3 : Int) ^ 2
--- 3 is Int
--- 2 is Nat
-
-#check (1 : Int) + 3 ^ 2
--- 1 is Int
--- 3 is Int
--- 2 is Nat
-
-#check (1 + 3 ^ 2 : Int)
--- 1 is Int
--- 3 is Int
--- 2 is Nat
-
-/-! With the binop behavior instead: -/
-
-macro_rules | `($x ^ $y)   => `(binop% HPow.hPow $x $y)
-
-#check (3 : Int) ^ 2  -- same
-#check (1 : Int) + 3 ^ 2  -- breaks
-#check (1 + 3 ^ 2 : Int)  -- breaks

tests/lean/2220.lean.expected.out

@@ -1,18 +0,0 @@
-@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
-  (@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3))
-    (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
-  (@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3))
-    (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
-2220.lean:25:19-25:24: error: failed to synthesize
-  HPow Nat Nat Int
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
-  (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-2220.lean:26:12-26:17: error: failed to synthesize
-  HPow Nat Nat Int
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
-@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
-  (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int

tests/lean/run/2220.lean

@@ -0,0 +1,35 @@
+/-! Coercions should ignore the RHS of `^` -/
+
+set_option pp.coercions false
+set_option pp.explicit true
+
+/--
+info: @HPow.hPow Int Nat Int (@instHPow Int Nat (@instPowNat Int Int.instNatPow)) (@OfNat.ofNat Int 3 (@instOfNat 3))
+  (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
+-/
+#guard_msgs in
+#check (3 : Int) ^ 2
+-- 3 is Int
+-- 2 is Nat
+
+/--
+info: @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
+  (@HPow.hPow Int Nat Int (@instHPow Int Nat (@instPowNat Int Int.instNatPow)) (@OfNat.ofNat Int 3 (@instOfNat 3))
+    (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
+-/
+#guard_msgs in
+#check (1 : Int) + 3 ^ 2
+-- 1 is Int
+-- 3 is Int
+-- 2 is Nat
+
+/--
+info: @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
+  (@HPow.hPow Int Nat Int (@instHPow Int Nat (@instPowNat Int Int.instNatPow)) (@OfNat.ofNat Int 3 (@instOfNat 3))
+    (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
+-/
+#guard_msgs in
+#check (1 + 3 ^ 2 : Int)
+-- 1 is Int
+-- 3 is Int
+-- 2 is Nat

tests/lean/run/4861.lean

@@ -0,0 +1,55 @@
+set_option maxHeartbeats 210000 in
+theorem foo (x y z p q : Int) : False :=
+  have : (1 * x ^ 1 + z ^ 1 * p) *
+        (1 / 1 * p ^ 1 * x ^ 1 + 1 * q * p ^ 1 * x * z + 1 * q ^ 1 * p ^ 1 * x ^ 1 +
+                            1 * q ^ 1 * p ^ 1 * x * z -
+                          1 * q * p ^ 1 * y ^ 1 +
+                        1 * q ^ 1 * p ^ 1 * x ^ 1 +
+                      1 * q ^ 1 * p ^ 1 * x * z -
+                    1 * q ^ 1 * p ^ 1 * y ^ 1 +
+                  1 * q ^ 1 * p ^ 1 * x ^ 1 +
+                1 * q ^ 1 * p ^ 1 * x * z -
+              1 * q ^ 1 * p ^ 1 * y ^ 1 +
+            1 * q ^ 1 * x ^ 1 -
+          1 * q ^ 1 * p * y ^ 1) +
+      z * (1 * y) *
+        (-(1 / 1 * p ^ 1 * x * y) + 1 * q * p ^ 1 * z * y - 1 * q ^ 1 * p ^ 1 * x * y +
+                  1 * q ^ 1 * p ^ 1 * z * y -
+                1 * q ^ 1 * p ^ 1 * x * y +
+              1 * q ^ 1 * p ^ 1 * z * y -
+            1 * q ^ 1 * p ^ 1 * x * y +
+          1 / 1 * q ^ 1 * p ^ 1 * z * y) +
+    (-y ^ 1 + p * x * (1 * z) + q * (1 * z ^ 1)) *
+      (-(1 / 1 * p ^ 1 * x * z) - 1 * q * p ^ 1 * x ^ 1 - 1 * q ^ 1 * p ^ 1 * x * z -
+                1 * q ^ 1 * p ^ 1 * x ^ 1 -
+              1 * q ^ 1 * p ^ 1 * x * z -
+            1 * q ^ 1 * p ^ 1 * x ^ 1 -
+          1 * q ^ 1 * p ^ 1 * x * z -
+        1 * q ^ 1 * p * x ^ 1) =
+  1 *
+        (1 / 1 * p ^ 1 * x ^ 1 + 1 * q * p ^ 1 * x * z + 1 * q ^ 1 * p ^ 1 * x ^ 1 +
+                            1 * q ^ 1 * p ^ 1 * x * z -
+                          1 * q * p ^ 1 * y ^ 1 +
+                        1 * q ^ 1 * p ^ 1 * x ^ 1 +
+                      1 * q ^ 1 * p ^ 1 * x * z -
+                    1 * q ^ 1 * p ^ 1 * y ^ 1 +
+                  1 * q ^ 1 * p ^ 1 * x ^ 1 +
+                1 * q ^ 1 * p ^ 1 * x * z -
+              1 * q ^ 1 * p ^ 1 * y ^ 1 +
+            1 * q ^ 1 * x ^ 1 -
+          1 * q ^ 1 * p * y ^ 1) +
+      1 *
+        (-(1 / 1 * p ^ 1 * x * y) + 1 * q * p ^ 1 * z * y - 1 * q ^ 1 * p ^ 1 * x * y +
+                  1 * q ^ 1 * p ^ 1 * z * y -
+                1 * q ^ 1 * p ^ 1 * x * y +
+              1 * q ^ 1 * p ^ 1 * z * y -
+            1 * q ^ 1 * p ^ 1 * x * y +
+          1 / 1 * q ^ 1 * p ^ 1 * z * y) +
+    1 *
+      (-(1 / 1 * p ^ 1 * x * z) - 1 * q * p ^ 1 * x ^ 1 - 1 * q ^ 1 * p ^ 1 * x * z -
+                1 * q ^ 1 * p ^ 1 * x ^ 1 -
+              1 * q ^ 1 * p ^ 1 * x * z -
+            1 * q ^ 1 * p ^ 1 * x ^ 1 -
+          1 * q ^ 1 * p ^ 1 * x * z -
+        1 * q ^ 1 * p * x ^ 1) := sorry
+  sorry