Skip to content

[Merged by Bors] - feat: quick version of mono tactic#1740

Closed
hrmacbeth wants to merge 11 commits intomasterfrom
hrmacbeth-mono
Closed

[Merged by Bors] - feat: quick version of mono tactic#1740
hrmacbeth wants to merge 11 commits intomasterfrom
hrmacbeth-mono

Conversation

@hrmacbeth
Copy link
Copy Markdown
Member

@hrmacbeth hrmacbeth commented Jan 21, 2023 •
edited by thorimur
Loading

This is an extremely partial port of the mono* tactic from Lean 3, implemented as a macro on top of solve_by_elim. The original mono had many configuration options and no documentation, so quite a bit is missing (and almost all the Lean 3 tests fail). Nonetheless I think it's worth merging this, because

  • it will get rid of errors in mathport output which come from lemmas being tagged with a nonexistent attribute @[mono]
  • in most mathlib3 uses of mono, only the basic version was used, not the various configuration options; thus I would guess that this version of mono will succeed fairly often in the port even though it fails nearly all the tests

Note: the solve_by_elim behavior is closer to mono* than mono, so both mono and mono* are accepted here and, for now, mean the same thing.

The full port of mono will eventually work in every place that mathlib3 had mono, so as long as no mono* is changed to mono between now and the full port of mono, this conflation of mono* and mono shouldn't introduce many wrinkles. Any wrinkles it does introduce will be able to be easily corrected by changing mono to mono*.

@[mono], @[mono left], @[mono right], and @[mono both] all just mean @[mono] for now.

The full port of mono will be PR'd as #2323.

Open in Gitpod

@hrmacbeth hrmacbeth added awaiting-review t-meta Tactics, attributes or user commands labels Jan 21, 2023
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Jan 23, 2023 •
edited
Loading

This looks good to me, it's good to be able to tag lemmas with @[mono] already.
However, I'm a bit worried about the syntax being different (and duplicating) the syntax in Mathport/Syntax. Is it possible that this trips up mathport? Maybe it's safer to implement exactly the syntax from Mathport/Syntax (removing it there), but ignoring all the other options.

@digama0
Copy link
Copy Markdown
Member

digama0 commented Jan 23, 2023 •
edited
Loading

There should not be any duplicate syntaxes. When partially implementing a tactic, you should move the syntax line from Mathport.Syntax into the file, and then throwUnsupportedSyntax or ignore any flags you aren't planning on supporting yet.

@fpvandoorn fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 25, 2023
@thorimur thorimur added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 17, 2023
gebner
gebner reviewed Feb 17, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@gebner gebner left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Feb 17, 2023

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@kim-em kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 17, 2023
@gebner
Copy link
Copy Markdown
Member

gebner commented Feb 17, 2023

bors d=thorimur

@bors
Copy link
Copy Markdown

bors bot commented Feb 17, 2023

✌️ thorimur can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

thorimur and others added 2 commits February 18, 2023 15:13
@thorimur @gebner
Update Mathlib/Tactic/Monotonicity/Attr.lean
5f46d5c 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
@thorimur @gebner
Update Mathlib/Tactic/Monotonicity/Basic.lean
2fe717c 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
@thorimur
Copy link
Copy Markdown
Contributor

thorimur commented Feb 18, 2023

bors r+

bors bot pushed a commit that referenced this pull request Feb 18, 2023
@hrmacbeth @thorimur
feat: quick version of mono tactic (#1740)
cdd6d9c 
This is an extremely partial port of the `mono*` tactic from Lean 3, implemented as a macro on top of `solve_by_elim`.  The original `mono` had many configuration options and no documentation, so quite a bit is missing (and almost all the Lean 3 tests fail).  Nonetheless I think it's worth merging this, because
- it will get rid of errors in mathport output which come from lemmas being tagged with a nonexistent attribute `@[mono]`
- in most mathlib3 uses of mono, only the basic version was used, not the various configuration options; thus I would guess that this version of `mono` will succeed fairly often in the port even though it fails nearly all the tests



Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
@bors
Copy link
Copy Markdown

bors bot commented Feb 19, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: quick version of mono tactic [Merged by Bors] - feat: quick version of mono tactic Feb 19, 2023
@bors bors bot closed this Feb 19, 2023
@bors bors bot deleted the hrmacbeth-mono branch February 19, 2023 00:43
@thorimur thorimur mentioned this pull request Feb 19, 2023
Open
@casavaca casavaca mentioned this pull request Feb 25, 2023
Closed
bors bot pushed a commit that referenced this pull request Mar 1, 2023
@casavaca
chore: Restore most of the mono attribute (#2491)
ffb5ddd 
Restore most of the `mono` attribute now that #1740 is merged.

I think I got all of the `mono`s.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gebner gebner gebner left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@hrmacbeth @fpvandoorn @digama0 @gebner @thorimur @kim-em