[Merged by Bors] - feat: `tfae_have ... :=` syntax by thorimur · Pull Request #10653 · leanprover-community/mathlib4

thorimur · 2024-02-17T08:41:14Z

This PR refactors tfae_have in terms of have, thus supporting all the syntax that have supports. We can now also write:

example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry
  tfae_have 2 → 1
  | p => f p
  tfae_have ⟨mp, mpr⟩ : 2 ↔ 3 := sorry
  ...

Previously, tfae_have exclusively pushed a new goal to the top of the goal list, requiring that the result be proved via tactic.

This PR does not deprecate or remove the "old-style" syntax, but does de-document it. The removal of old-style syntax is done in #11000.

This tees us up for a tfae block tactic (#10991, #11003).

See Zulip.

Ref #2061

…nt them appearing on hover

This reverts commit fba28f5.

github-actions · 2024-06-15T16:10:20Z

PR summary aa408695b3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ elabTFAEType
+ mkTFAEId
- mkImplType
- mkTFAEHypName
- tfaeHaveCore

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

urkud · 2024-06-15T20:48:55Z

@thorimur I merged master, now it fails to compile.

thorimur · 2024-06-15T20:53:25Z

@urkud Ah, thanks; I had given up on keeping this PR fresh! I'll take a look soon.

thorimur · 2024-09-13T02:19:36Z

@urkud "Soon" has finally arrived. :) I've freshened this PR and its 3 dependents as well.

joneugster · 2024-09-17T09:15:00Z

+-- Mathlib `have`
+| `(tfaeHave'|tfae_have $d:tfaeHaveIdLhs) => withMainContext do
+  let goal ← getMainGoal
+  let (_, tfaeList) ← getTFAEList (← goal.getType)
+  match d with
+  | `(tfaeHaveIdLhs| $b:ident : $t:tfaeType) =>
+    let type ← elabTFAEType tfaeList t
+    evalTactic <|← `(tactic|have $b:ident : $(← exprToSyntax type))
+  | _ => throwUnsupportedSyntax


I think the current consensus is that the mathlib-have should not be used inside mathlib anymore, and therefore ideally also not imported (see docs):

As a style choice, this [mathlib's have] should not be used in mathlib; but is provided for downstream users who preferred the old style.

Maybe it's easiest to just drop the import together with this snippet?

Or is there a reasonable workaround which allows not to import the modified have here?

Ah, that's right. :) I eliminated the import and moved the entirety of the old-style version to its own section below.

In parallel to Mathlib have, I think we ought to move the old tfae_have syntax to its own non-imported file in the PR that migrates Mathlib to the new syntax (#11000); what do you think?

joneugster · 2024-09-18T13:43:48Z

+/- Convert `tfae_have i <arr> j ...` to `tfae_have tfae_i_arr_j : i <arr> j ...`. See
+`expandHave`, which is responsible for inserting `this` in `have : A := ...`. -/
+macro_rules
+| `(tfaeHave|tfae_have $hy:hygieneInfo $t:tfaeType := $val) => do
+  let id := HygieneInfo.mkIdent hy (← mkTFAEId t) (canonical := true)
+  `(tfaeHave|tfae_have $id : $t := $val)
+| `(tfaeHave|tfae_have $hy:hygieneInfo $t:tfaeType $alts:matchAlts) => do
+  let id := HygieneInfo.mkIdent hy (← mkTFAEId t) (canonical := true)
+  `(tfaeHave|tfae_have $id : $t $alts)


I think it would be better to do this inside the elab and use Lean.Meta.mkFreshBinderNameForTactic in order to make the tactic hygienic.

I.e. the binder name should probably only be accessible if set_option tactic.hygienic false

Hmm, I'm not sure—tfae_have is specifically meant to mimic have when the binder name is not provided, which means producing an accessible name like tfae_2_iff_3 in analogy to producing the accessible name this. (Note that this is the same mechanism used by have to accomplish that.)

(This is also how it currently behaves, so I'd be wary of breaking it!)

ok that's a fair point!

joneugster

Thanks for the PR. I think it looks very clean and will be a good base for the upcoming improvements for the tfae tactic. I suggest

maintainer merge

github-actions · 2024-09-18T20:24:33Z

🚀 Pull request has been placed on the maintainer queue by joneugster.

urkud · 2024-09-20T03:16:21Z

LGTM. We can fix issues (if any) in the PR migrating Mathlib to the new syntax. Thanks a lot!
bors merge

This PR refactors `tfae_have` in terms of `have`, thus supporting all the syntax that `have` supports. We can now also write: ```lean example : TFAE [P, Q, R] := by tfae_have 1 → 2 := sorry tfae_have 2 → 1 | p => f p tfae_have ⟨mp, mpr⟩ : 2 ↔ 3 := sorry ... ``` Previously, `tfae_have` exclusively pushed a new goal to the top of the goal list, requiring that the result be proved via tactic. This PR does not deprecate or remove the "old-style" syntax, but does de-document it. The removal of old-style syntax is done in #11000. This tees us up for a `tfae` block tactic (#10991, #11003). See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/tfae_have.201.20.E2.86.92.202.20.3A.3D.20syntax). Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

mathlib-bors · 2024-09-20T04:21:44Z

Pull request successfully merged into master.

Build succeeded:

thorimur added 2 commits February 17, 2024 03:34

feat: := syntax

7c0f799

docs: update to include := syntax

fb4846a

adomani reviewed Feb 17, 2024

View reviewed changes

Comment thread Mathlib/Tactic/TFAE.lean Outdated

thorimur added t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Feb 17, 2024

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 17, 2024

chore: style, test comments/refinement

5c0b6f7

thorimur added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. awaiting-review labels Feb 17, 2024

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 17, 2024

fix: mimic have behavior more faithfully

d684d17

eric-wieser reviewed Feb 17, 2024

View reviewed changes

Comment thread Mathlib/Tactic/TFAE.lean

eric-wieser reviewed Feb 17, 2024

View reviewed changes

Comment thread Mathlib/Tactic/TFAE.lean Outdated

adomani reviewed Feb 17, 2024

View reviewed changes

Comment thread Mathlib/Tactic/TFAE.lean Outdated

thorimur removed the awaiting-review label Feb 17, 2024

thorimur added 5 commits February 18, 2024 04:00

refactor, feat: use have directly for tfae_have

60abee2

feat: re-support Mathlib have

fbbad64

chore: clean up hover text

d37994f

test: new tests, update syntax

bc4fd75

syntax: change tfae_have i <arr> j to tfae_have : i <arr> j

fba28f5

thorimur force-pushed the tfae-have-stx-tweak branch from 8c3adb8 to fba28f5 Compare February 18, 2024 09:52

style: clean up types/parses, remove docstrings from parsers to preve…

5a97360

…nt them appearing on hover

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 Feb 21, 2024

thorimur added 4 commits February 26, 2024 14:06

chore: revert tfae_have : 1 → 2 syntax to tfae_have 1 → 2

32ba7da

Revert "syntax: change tfae_have i <arr> j to tfae_have : i <arr> j"

b128a07

This reverts commit fba28f5.

test: revert : syntax

bdf07b8

chore: revert : syntax in docstrings

547af66

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 Feb 26, 2024

thorimur mentioned this pull request Feb 26, 2024

feat: tfae block tactic #10991

Closed

2 tasks done

thorimur added the modifies-tactic-syntax This PR adds a new interactive tactic or modifies the syntax of an existing tactic. label Feb 26, 2024

Merge branch 'master' into tfae-have-stx-tweak

98065f5

urkud requested a review from eric-wieser June 15, 2024 16:10

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 Jun 15, 2024

urkud added awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. and removed awaiting-review labels Jun 15, 2024

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 1, 2024

Merge remote-tracking branch 'origin/master' into tfae-have-stx-tweak

833ac67

thorimur removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 12, 2024

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 12, 2024

thorimur added 2 commits September 12, 2024 19:35

Use exprToSyntax instead of its Batteries synonym Expr.toSyntax

74efaeb

update noshake

2eeb358

joneugster reviewed Sep 17, 2024

View reviewed changes

joneugster self-assigned this Sep 17, 2024

thorimur added 2 commits September 17, 2024 20:05

refactor: eliminate Mathlib have import; separate old-style syntax

2caf1ba

docs: update

aa40869

joneugster reviewed Sep 18, 2024

View reviewed changes

github-actions Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 18, 2024

github-actions Bot added the ready-to-merge This PR has been sent to bors. label Sep 20, 2024

mathlib-bors Bot changed the title ~~feat: tfae_have ... := syntax~~ [Merged by Bors] - feat: tfae_have ... := syntax Sep 20, 2024

mathlib-bors Bot closed this Sep 20, 2024

mathlib-bors Bot deleted the tfae-have-stx-tweak branch September 20, 2024 04:21

Conversation

thorimur commented Feb 17, 2024 • edited by Ruben-VandeVelde Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented Jun 15, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary aa408695b3

Import changes for modified files

Declarations diff

Uh oh!

urkud commented Jun 15, 2024

Uh oh!

thorimur commented Jun 15, 2024

Uh oh!

thorimur commented Sep 13, 2024

Uh oh!

joneugster Sep 17, 2024

Choose a reason for hiding this comment

Uh oh!

thorimur Sep 18, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joneugster Sep 18, 2024

Choose a reason for hiding this comment

Uh oh!

thorimur Sep 18, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joneugster Sep 18, 2024

Choose a reason for hiding this comment

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Sep 18, 2024

Uh oh!

urkud commented Sep 20, 2024

Uh oh!

mathlib-bors Bot commented Sep 20, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

thorimur commented Feb 17, 2024 •

edited by Ruben-VandeVelde

Loading

github-actions Bot commented Jun 15, 2024 •

edited

Loading

thorimur Sep 18, 2024 •

edited

Loading

thorimur Sep 18, 2024 •

edited

Loading