Skip to content

feat: Add tactic compute_degree_le#5882

Closed
adomani wants to merge 40 commits intomasterfrom
adomani_cdle
Closed

feat: Add tactic compute_degree_le#5882
adomani wants to merge 40 commits intomasterfrom
adomani_cdle

Conversation

@adomani
Copy link
Copy Markdown
Contributor

@adomani adomani commented Jul 14, 2023 •
edited
Loading

This PR is a port of the mathlib3 tactic compute_degree_le. Internally, the new tactic performs differently than the original tactic. It passes all the tests for mathlib3's compute_degree_le.

Analogous to this PR there is the shorter implementation #6007.

This PR supersedes #5276.

compute_degree_le was used only once in mathlib3: PR #5883 restores its use in mathlib4.

Open in Gitpod

This was referenced Jul 14, 2023
Closed
Open
@adomani 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 14, 2023
@adomani adomani changed the title Add tactic compute_degree_le feat: Add tactic compute_degree_le Jul 14, 2023
@adomani adomani mentioned this pull request Jul 14, 2023
Closed
1 task
@adomani adomani changed the title feat: Add tactic compute_degree_le feat: Add tactic compute_degree_le Jul 14, 2023
adomani

This comment was marked as resolved.

Sign in to view

adomani
adomani commented Jul 16, 2023
View reviewed changes
adomani

This comment was marked as resolved.

Sign in to view

adomani

This comment was marked as resolved.

Sign in to view

adomani
adomani commented Jul 16, 2023
View reviewed changes
@adomani adomani mentioned this pull request Jul 18, 2023
Closed
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 18, 2023
bors bot pushed a commit that referenced this pull request Jul 19, 2023
@adomani @urkud
feat(Tactic/ComputeDegree): add helper lemmas for compute_degree_le (…
801ae80 
…#5978)

This PR is a prequel to #5882: it simply adds the helper lemmas about polynomials that the tactic uses.

[Zulip discussion ](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235882.20.60compute_degree_le.60)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 19, 2023
@ghost
Copy link
Copy Markdown

ghost commented Jul 19, 2023

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 19, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 19, 2023
@adomani adomani mentioned this pull request Jul 19, 2023
Closed
@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented Jul 28, 2023

The implementation in #6221 achieves more than the one here and, in my opinion, better!

@adomani adomani closed this Jul 28, 2023
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@adomani @urkud @kim-em
feat(Tactic/ComputeDegree): add helper lemmas for compute_degree_le (…
b48d2bd 
…#5978)

This PR is a prequel to #5882: it simply adds the helper lemmas about polynomials that the tactic uses.

[Zulip discussion ](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235882.20.60compute_degree_le.60)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@adomani adomani deleted the adomani_cdle branch January 12, 2024 07:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

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

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@adomani