Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

perf: use NatPow Int instead of HPow Int Nat Int #4903

Merged
merged 2 commits into from
Aug 3, 2024
Merged

perf: use NatPow Int instead of HPow Int Nat Int #4903

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e6d83ba
perf: use `NatPow Int` instead of `HPow Int Nat Int`
leodemoura Aug 2, 2024
88fb29b
chore: fix tests
leodemoura Aug 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/Init/Data/Int/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
41 changes: 0 additions & 41 deletions tests/lean/2040.lean
View file
Open in desktop

This file was deleted.

15 changes: 0 additions & 15 deletions tests/lean/2040.lean.expected.out
View file
Open in desktop

This file was deleted.

26 changes: 0 additions & 26 deletions tests/lean/2220.lean
View file
Open in desktop

This file was deleted.

18 changes: 0 additions & 18 deletions tests/lean/2220.lean.expected.out
View file
Open in desktop

This file was deleted.

35 changes: 35 additions & 0 deletions tests/lean/run/2220.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
55 changes: 55 additions & 0 deletions tests/lean/run/4861.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading