[Merged by Bors] - feat: porting norm_num extensions for Nat.gcd, Nat.lcm, Int.gcd, Int.lcm, and IsCoprime

[kmill]

This completes the porting of these norm_num extensions while adding a new extension for IsCoprime over Int. It also adds the norm_num extension testing file from mathlib3. Closes #3246.

---

[kmill]

@digama0 I figure I'll ping you about these ported norm_num extensions (and feel free to take over if I've done it all wrong).

Notes:

• I simplified the Nat.coprime extension. It used to be a recap of the Nat.gcd implementation, and it seemed easier to instead just calculate whether the GCD was 1 or not, which I think only increases the proof term size by a constant amount.
• The extensions are generally split into three, for example proveNatCoprime', proveNatCoprime, and evalNatCoprime. I found that match generalization worked better and led to better-checked Qq types when there were actual natural number arguments, hence the split with the primed version.
• I deleted helper lemmas that were no longer needed and gave them #noalign. If any of them are wanted, see the "delete unused helper lemmas" commit.

[Ruben-VandeVelde]

Can you check if this can replace nat_gcd_helper_1 in Mathlib/GroupTheory/Perm/Cycle/Type.lean?

[kmill]

@Ruben-VandeVelde Thanks, I cleaned that up.

[fpvandoorn]

was this intentional?

[kmill]

Yes, it's the source of Int.natAbs_pow and isUnit_ofPowEqOne, and these used to be transitively provided by NormNum.

[digama0]

I removed the #aligns since we do not align tactic files (and the theorems in these files are not stable for direct use in mathlib in the first place).

bors r+

[kmill]

@digama0 Those Nat.beq's were intentional to keep intermediate calculations out of proof terms -- I thought it was kind of neat how passing Eq.refl true was enough to get the kernel to compute everything. If you don't think that's important then I suppose that's fine with me.

[digama0]

The intermediate calculations are not in the proof term, I'm not sure what you mean. The proof term contains an occurrence of e.g. 13 * 42, but not the result of that evaluation. This approach still requires the kernel to prove the equality, but it does so as a defeq between two nats which have normalized to the same thing instead of an extra beq computation. (Put another way, what is being optimized is not the term size so much as the amount of typechecking computation that has to happen. If we wanted to minimize term size we could write a reflective checker like they do in Coq.)

It would be nice to find a way to do microbenchmarks on this kind of thing though. It's just a bit hard to measure in most workloads.

BTW there is actually a way to remove even the Eq.refl terms from the proof term, which is to have the return type of the lemma be if cond then IsNat ... else True, and use the lemma in a place where IsNat ... is expected. You need one extra type ascription at the outermost level though, and I'm not sure how good it is to have the kernel working with a more complex defeq problem like this; using subgoals gives us a bit more control over the defeq problem.

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style

[kmill]

@digama0 Really, I just thought it was neat having the proof terms look like

Tactic.NormNum.nat_lcm_helper 2 3 1 6
  (Tactic.NormNum.nat_gcd_helper_1' 2 3 1 1 (Eq.refl true))
  (Eq.refl false) (Eq.refl true)

without needing to feed in the LHS or RHS in the Eq.refl constructor -- it also avoids some code duplication. I liked how it makes it obvious what the kernel is going to compute, and I figured having the kernel do an extra Nat.beq is negligible.

I think my main objection is the commit message classifying changing Nat.beq x y = true to x = y to be "cleanup." They're different designs optimizing for different sets of things, but to be clear I'm fine with the change.

Thanks for mentioning the if ... pattern -- I was wondering about whether there was a way to avoid passing in these proof terms. (And also thanks for reviewing!)