[Merged by Bors] - feat: tactic `compute_degree` #6221

adomani · 2023-07-28T16:49:43Z

This PR ports the whole compute_degree tactic from mathlib3.

The tactic makes progress on goals of the form

natDegree f ≤ d,
degree f ≤ d,
natDegree f = d,
degree f = d,
coeff f n = r.

The variant compute_degree! applies norm_num and assumption to all left-over goals.

For instance, here is a valid computation of the degree of the 105-th cyclotomic polynomial:

example : natDegree
    (1 + X + X ^ 2 - X ^ 5 - X ^ 6 - 2 * X ^ 7 - X ^ 8 - X ^ 9 + X ^ 12 + X ^ 13 + X ^ 14 +
        X ^ 15 + X ^ 16 + X ^ 17 - X ^ 20 - X ^ 22 - X ^ 24 - X ^ 26 - X ^ 28 + X ^ 31 + X ^ 32 +
        X ^ 33 + X ^ 34 + X ^ 35 + X ^ 36 - X ^ 39 - X ^ 40 - 2 * X ^ 41 - X ^ 42 - X ^ 43 +
        X ^ 46 + X ^ 47 + X ^ 48 : ℤ[X]) = 48 := by
  compute_degree!

(Lean takes approximately 3s on my computer to prove the computation above.)

Affected files:

Mathlib/Lean/Expr/Basic.lean
Mathlib/Tactic/ComputeDegree.lean
test/ComputeDegree.lean

depends on: [Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220 for some basic lemmas

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221). The signature of a theorem changed: ```lean theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (n * m) = p.coeff n ^ m -- <-- the order of the product was `n * m` (p ^ m).coeff (m * n) = p.coeff n ^ m -- <-- and it became `m * n` ``` Modified files: ``` Data/Polynomial/Basic.lean Data/Polynomial/Degree/Lemmas.lean Data/Polynomial/Degree/Definitions.lean Data/Polynomial/Coeff.lean -- for a "`simp` can prove this" golf ```

leanprover-community-mathlib4-bot · 2023-08-10T13:47:04Z

This PR/issue depends on:

~~[Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220~~
By Dependent Issues (🤖). Happy coding!

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221). The signature of a theorem changed: ```lean theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (n * m) = p.coeff n ^ m -- <-- the order of the product was `n * m` (p ^ m).coeff (m * n) = p.coeff n ^ m -- <-- and it became `m * n` ``` Modified files: ``` Data/Polynomial/Basic.lean Data/Polynomial/Degree/Lemmas.lean Data/Polynomial/Degree/Definitions.lean Data/Polynomial/Coeff.lean -- for a "`simp` can prove this" golf ```

kmill

Thanks for writing this tactic. There are some things I'd like to see changed before it is merged, and I've tested all these suggestions locally.

Mathlib/Tactic/ComputeDegree.lean

test/ComputeDegree.lean

adomani · 2023-09-02T04:46:31Z

Kyle, thank you so much for taking the time to review the PR!

I've looked through your suggestions and I find them all great! I hope to have time later today to sit at a computer and implement them.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

…ity/mathlib4 into adomani_compute_degree

kmill · 2023-09-02T11:47:34Z

I think this is in a good state now, and the user interface seems well-specified enough (with internals solid enough) that I'm happy to merge it. One thing we might want in the future is to have compute_degree be changed into a collection of norm_num extensions, with compute_degree in particular applying to the goals laid out in the docstring. One might even have compute_degree be a version of norm_num specialized to just degree/natDegree/coeff expressions and inequality goals involving them, letting it automatically compute degrees.

Anyway, the perfect is the enemy of the good, so

bors r+

This PR ports the whole `compute_degree` tactic from mathlib3. The tactic makes progress on goals of the form * `natDegree f ≤ d`, * `degree f ≤ d`, * `natDegree f = d`, * `degree f = d`, * `coeff f n = r`. The variant `compute_degree!` applies `norm_num` and `assumption` to all left-over goals. For instance, here is a valid computation of the degree of the 105-th cyclotomic polynomial: ```lean example : natDegree (1 + X + X ^ 2 - X ^ 5 - X ^ 6 - 2 * X ^ 7 - X ^ 8 - X ^ 9 + X ^ 12 + X ^ 13 + X ^ 14 + X ^ 15 + X ^ 16 + X ^ 17 - X ^ 20 - X ^ 22 - X ^ 24 - X ^ 26 - X ^ 28 + X ^ 31 + X ^ 32 + X ^ 33 + X ^ 34 + X ^ 35 + X ^ 36 - X ^ 39 - X ^ 40 - 2 * X ^ 41 - X ^ 42 - X ^ 43 + X ^ 46 + X ^ 47 + X ^ 48 : ℤ[X]) = 48 := by compute_degree! ``` (Lean takes approximately 3s on my computer to prove the computation above.) Affected files: ``` Mathlib/Lean/Expr/Basic.lean Mathlib/Tactic/ComputeDegree.lean test/ComputeDegree.lean ```

bors · 2023-09-02T13:20:21Z

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.

This PR is a companion to #6221. It uses the tactic `compute_degree` to golf two proofs and restore a proof closer to its mathlib3 version.

This was referenced Jul 28, 2023

[Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220

Closed

tactic porting tracking issue #430

Open

feat: Add tactic compute_degree_le #5882

Closed

feat: a minimalistic port of compute_degree_le #6007

Closed

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 28, 2023

adomani mentioned this pull request Jul 28, 2023

[Merged by Bors] - chore: golf using compute_degree #6222

Closed

1 task

adomani added awaiting-review modifies-tactic-syntax This PR adds a new interactive tactic or modifies the syntax of an existing tactic. t-meta Tactics, attributes or user commands labels Jul 28, 2023

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Aug 10, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 10, 2023

adomani added 17 commits August 10, 2023 16:19

Rework tactic compute_degree

93eca5d

Remove duplicate tests

affded0

Shorten a line

5fc9871

Remove a space before a semicolon.

27528e6

Use Command instead of eval

b52bfd7

Reassess conditions

bd24777

Use renamed tactic compute_degree

7fa4c0d

Whitespace

c3d44f5

twoHeadsArgs docstring

6abeb5f

dispatchLemma docstring

01d7d88

Better error reporting and more docs

72d950d

More tests

8470949

Rearrange lemmas

9432f66

Restore "congruence" lemma

051da37

Tests also for natDegree/degree _ = _.

90836bc

Add lemmas of separate PR

6e67c7a

Add lemmas of separate PR

ab9e72e

adomani force-pushed the adomani_compute_degree branch from 811c325 to a66f2ca Compare August 10, 2023 14:35

adomani added 5 commits August 10, 2023 21:52

Merge branch 'master' into adomani_compute_degree

0795ff0

Merge branch 'master' into adomani_compute_degree

88ef77e

Merge branch 'master' into adomani_compute_degree

e15a63c

Reduce imports

b88e9e8

Remove dir?

152f18a

adomani added 2 commits August 15, 2023 07:52

Merge branch 'master' into adomani_compute_degree

b885049

Add no longer autoimplicit vars

2db2210

adomani added 2 commits August 31, 2023 12:06

Merge branch 'master' into adomani_compute_degree

c687172

Merge branch 'master' into adomani_compute_degree

578f0b9

kmill reviewed Sep 1, 2023

View reviewed changes

adomani and others added 5 commits September 2, 2023 11:14

Merge branch 'master' into adomani_compute_degree

9fce113

Kyle's improvements

c3fbc10

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Kyle's improvements, locally

9d662a4

Merge branch 'adomani_compute_degree' of github.com:leanprover-commun…

8066f3b

…ity/mathlib4 into adomani_compute_degree

Move recognizer Lean.Expr.le? to M.Lean.Expr.Basic

4d8cfc9

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 2, 2023

bors bot changed the title ~~feat: tactic compute_degree~~ [Merged by Bors] - feat: tactic compute_degree Sep 2, 2023

bors bot closed this Sep 2, 2023

bors bot deleted the adomani_compute_degree branch September 2, 2023 13:20

bors bot pushed a commit that referenced this pull request Sep 6, 2023

chore: golf using compute_degree (#6222)

48eb1fb

This PR is a companion to #6221. It uses the tactic `compute_degree` to golf two proofs and restore a proof closer to its mathlib3 version.

ebab pushed a commit that referenced this pull request Sep 11, 2023

chore: golf using compute_degree (#6222)

463cef2

This PR is a companion to #6221. It uses the tactic `compute_degree` to golf two proofs and restore a proof closer to its mathlib3 version.

kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023

chore: golf using compute_degree (#6222)

4bb5638

This PR is a companion to #6221. It uses the tactic `compute_degree` to golf two proofs and restore a proof closer to its mathlib3 version.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: tactic `compute_degree` #6221

[Merged by Bors] - feat: tactic `compute_degree` #6221

adomani commented Jul 28, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Aug 10, 2023

kmill left a comment

adomani commented Sep 2, 2023

kmill commented Sep 2, 2023

bors bot commented Sep 2, 2023

[Merged by Bors] - feat: tactic compute_degree #6221

[Merged by Bors] - feat: tactic compute_degree #6221

Conversation

adomani commented Jul 28, 2023 • edited Loading

leanprover-community-mathlib4-bot commented Aug 10, 2023

kmill left a comment

Choose a reason for hiding this comment

adomani commented Sep 2, 2023

kmill commented Sep 2, 2023

bors bot commented Sep 2, 2023

[Merged by Bors] - feat: tactic `compute_degree` #6221

[Merged by Bors] - feat: tactic `compute_degree` #6221

adomani commented Jul 28, 2023 •

edited

Loading