Skip to content

[Merged by Bors] - chore(*): rename FunLike to DFunLike#9785

Closed
Vierkantor wants to merge 9 commits intomasterfrom
FunLike-to-DFunLike
Closed

[Merged by Bors] - chore(*): rename FunLike to DFunLike#9785
Vierkantor wants to merge 9 commits intomasterfrom
FunLike-to-DFunLike

Conversation

@Vierkantor
Copy link
Copy Markdown
Contributor

@Vierkantor Vierkantor commented Jan 16, 2024

This prepares for the introduction of a non-dependent synonym of FunLike, which helps a lot with keeping #8386 readable.

This is entirely search-and-replace in 680197f combined with manual fixes in 4145626, e900597 and b8428f8. The commands that generated this change:

sed -i 's/\bFunLike\b/DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\btoFunLike\b/toDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/import Mathlib.Data.DFunLike/import Mathlib.Data.FunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\bHom_FunLike\b/Hom_DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean     
sed -i 's/\binstFunLike\b/instDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\bfunLike\b/instDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\btoo many metavariables to apply `fun_like.has_coe_to_fun`/too many metavariables to apply `DFunLike.hasCoeToFun`/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean

Open in Gitpod

@Vierkantor Vierkantor added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jan 16, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 16, 2024
This prepares for the introduction of a non-dependent synonym of FunLike, which helps a lot with keeping #8386 readable.

This is entirely search-and-replace. The commands that generated this change:
```bash
sed -i 's/\bFunLike\b/DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/import Mathlib.Data.DFunLike/import Mathlib.Data.FunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
```
/-- Helper instance for when there's too many metavariables to apply `DFunLike.CoeFun`
directly. -/
/- Porting note: Lean gave me `unknown constant 'FunLike.CoeFun'` and says `CoeFun` is a type
/- Porting note: Lean gave me `unknown constant 'DFunLike.CoeFun'` and says `CoeFun` is a type
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Do you think editing this porting note is OK?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Not sure: it would be false as written so probably revert this? Although I suppose the error would involve DFunLike if we ported now, so maybe it's okay. Probably we can delete this instance anyway (after #8386).

Suggested change
/- Porting note: Lean gave me `unknown constant 'DFunLike.CoeFun'` and says `CoeFun` is a type
/- Porting note: Lean gave me `unknown constant 'FunLike.CoeFun'` and says `CoeFun` is a type

Copy link
Copy Markdown
Contributor

@mattrobball mattrobball left a comment

Choose a reason for hiding this comment

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

Quick pass through visible changes in GH UI. Only some naming conventions.

used for example with `ContinuousLinearMap` or `Matrix`.
-/
structure IsProj {F : Type*} [FunLike F M fun _ => M] (f : F) : Prop where
structure IsProj {F : Type*} [DFunLike F M fun _ => M] (f : F) : Prop where
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Should this be dependent? Might be out of scope for this PR

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I'd like to postpone this cleanup after the heavy changes of #8386 have passed.

Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

I manually looked through the diff and didn't see any howlers. I guess the main thing I learnt is that we are very inconsistent with instFunLike v funLike for instance names. I guess the instance names might also all be changeable with sed.

This typeclass is primarily for use by homomorphisms like `MonoidHom` and `LinearMap`.

## Basic usage of `FunLike`
## Basic usage of `DFunLike`
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Should this entire directory be renamed Mathlib/Data/DFunLike?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

We're going to re-add FunLike in #8386 and pretend it's the main definition (or at least the one most users will care about), so I'd like to keep the current directory name.

variable {F α β : Sort*} [i : DFunLike F α fun _ ↦ β]

namespace FunLike
namespace DFunLike
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Is the idea right now to still leave this stuff in the DFunLike namespace?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

For now, yes. I would like to eventually have everything in the FunLike namespace (except perhaps anything specialized to the dependent case), but that would require something smarter than a find-and-replace everywhere.

/-- The type of `⊤`-preserving functions from `α` to `β`. -/
structure TopHom (α β : Type*) [Top α] [Top β] where
/-- The underlying function. The preferred spelling is `FunLike.coe`. -/
/-- The underlying function. The preferred spelling is `DFunLike.coe`. -/
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Do you think that the preferred spelling will be FunLike.coe again one day? (also the change a few lines later)

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I don't know: coe is a field of the DFunLike structure so it's not quite as easy to rename it as it would be for a plain definition.

@Vierkantor
Copy link
Copy Markdown
Contributor Author

I decided to rename all the instance funLike to instance instDFunLike to make the naming convention consistent all at once. If you disagree, it should be easy to revert and redo e5798c5.

@mattrobball
Copy link
Copy Markdown
Contributor

I think this has had a thorough look-over. I am going to delegate it.

If anyone has any more comments, please register them soon.

bors-delegate+

@mattrobball
Copy link
Copy Markdown
Contributor

Human error.

bors delegate+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 17, 2024

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

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jan 17, 2024
@Vierkantor
Copy link
Copy Markdown
Contributor Author

Build passed! I'll merge in a couple hours unless there are any further comments.

@Vierkantor
Copy link
Copy Markdown
Contributor Author

I see no objection and no changes relating to FunLike on the master branch, so let's try and get this merged!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 17, 2024
This prepares for the introduction of a non-dependent synonym of FunLike, which helps a lot with keeping #8386 readable.

This is entirely search-and-replace in [680197f](680197f) combined with manual fixes in [4145626](4145626), [e900597](e900597) and [b8428f8](b8428f8). The commands that generated this change:
```bash
sed -i 's/\bFunLike\b/DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\btoFunLike\b/toDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/import Mathlib.Data.DFunLike/import Mathlib.Data.FunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\bHom_FunLike\b/Hom_DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean     
sed -i 's/\binstFunLike\b/instDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\bfunLike\b/instDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
sed -i 's/\btoo many metavariables to apply `fun_like.has_coe_to_fun`/too many metavariables to apply `DFunLike.hasCoeToFun`/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean
```



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(*): rename FunLike to DFunLike [Merged by Bors] - chore(*): rename FunLike to DFunLike Jan 18, 2024
@mathlib-bors mathlib-bors bot closed this Jan 18, 2024
@mathlib-bors mathlib-bors bot deleted the FunLike-to-DFunLike branch January 18, 2024 00:39
Vierkantor added a commit that referenced this pull request Jan 18, 2024
This follows up from #9785, which renamed `FunLike` to `DFunLike`,
by introducing a new abbreviation `FunLike F α β := DFunLike F α (fun _ => β)`,
to make the non-dependent use of `FunLike` easier.
mathlib-bors bot pushed a commit that referenced this pull request Jan 19, 2024
This follows up from #9785, which renamed `FunLike` to `DFunLike`, by introducing a new abbreviation `FunLike F α β := DFunLike F α (fun _ => β)`, to make the non-dependent use of `FunLike` easier.

I searched for the pattern `DFunLike.*fun` and `DFunLike.*λ` in all files to replace expressions of the form `DFunLike F α (fun _ => β)` with `FunLike F α β`. I did this everywhere except for `extends` clauses for two reasons: it would conflict with #8386, and more importantly `extends` must directly refer to a structure with no unfolding of `def`s or `abbrev`s.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants