chore(*): redefine {nat,int} mul based on a left-smul

[pechersky]

---

[pechersky]

Some issues still need to be ironed out, like why the dec_trivial proof needed to change in sampleable and why does doing the type_check in the norm_num test comlpetely time out.

[gebner]

Why did this test change?

[pechersky]

Here was my commit message for that change:

remove try_for in norm_num test …
8b9b65a
Previously, there was a try_for to make sure the types check. But now
the type checking of the result times out, so to make the tests work,
the try_for is removed entirely. This should be investigated further.
But in any case, norm_num is able to discharge the goal, and the
kernel does not complain, so that must mean that the proof does
typecheck properly.

[gebner]

Hmm, this gives me a deep recursion error:

example : 2 ^ 17 - 1 = 131071 :=
by {norm_num, tactic.result >>= tactic.type_check}

I wonder if we're missing something subtle here. The PR introducing this test (#1387) doesn't really explain why type-checking performance is important. It works for 16 and 18, but 17 fails. @digama0 ?

[digama0]

The reason why typechecking performance is relevant here is because whenever norm_num is working over nat or int, everything is true by refl but this is absolutely not the proof norm_num is supposed to be producing. So if there are any bugs in the application of lemmas, norm_num will not fail, it will just take a long time to typecheck the result. If all lemmas are syntactic matches, nothing expensive should be unfolded and this is a way to ensure that this is happening.

[digama0]

The 2 ^ 17 - 1 = 131071 example is also not random, it was actually part of a bug report and the test was added to ensure it did not regress (and it sounds like it did regress in this version).

[digama0]

Here's a minimized version that eliminates norm_num:

example : 10000 * 1 = 10000 := (@mul_one ℕ nat.monoid 10000 : _)

This takes longer to typecheck depending on the size of 10000 here, which means it's not actually matching the goal like it should and is instead directly computing both sides to refl.

[pechersky]

Right -- I don't understand the regression or the reason it is occurring.

…

On Wed, Apr 7, 2021 at 4:34 PM Mario Carneiro ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In test/norm_num.lean <#6773 (comment)> : > @@ -33,8 +33,7 @@ example : (6:real) < 10 := by norm_num example : (7:real)/2 > 3 := by norm_num example : (4:real)⁻¹ < 1 := by norm_num example : ((1:real) / 2)⁻¹ = 2 := by norm_num -example : 2 ^ 17 - 1 = 131071 := -by {norm_num, tactic.try_for 200 (tactic.result >>= tactic.type_check)} +example : 2 ^ 17 - 1 = 131071 := by norm_num The 2 ^ 17 - 1 = 131071 example is also not random, it was actually part of a bug report and the test was added to ensure it did not regress (and it sounds like it did regress in this version). — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#6773 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABIYHBWA45MGQLAGYK3AYN3THS6XFANCNFSM4ZPLMTUA> .