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

Vierkantor · 2024-01-16T18:29:01Z

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

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 ```

Mathlib/Algebra/Category/MonCat/Basic.lean

Mathlib/Algebra/Module/LinearMap.lean

kbuzzard · 2024-01-17T13:58:30Z

Mathlib/Algebra/Ring/CentroidHom.lean

 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


Do you think editing this porting note is OK?

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

Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

Mathlib/Data/FunLike/Basic.lean

Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean

Mathlib/Algebra/Category/MonCat/Basic.lean

mattrobball

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

mattrobball · 2024-01-17T14:43:35Z

Mathlib/LinearAlgebra/Projection.lean

 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


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

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

Mathlib/Order/Category/BddOrd.lean

Mathlib/Order/Category/Semilat.lean

Mathlib/Probability/ProbabilityMassFunction/Basic.lean

Mathlib/Topology/ContinuousFunction/CocompactMap.lean

kbuzzard

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.

Mathlib/Combinatorics/Young/SemistandardTableau.lean

Mathlib/Data/DFinsupp/Basic.lean

kbuzzard · 2024-01-17T14:10:22Z

Mathlib/Data/FunLike/Basic.lean

@@ -13,7 +13,7 @@ import Mathlib.Util.CompileInductive

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

-## Basic usage of `FunLike`
+## Basic usage of `DFunLike`


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

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.

kbuzzard · 2024-01-17T14:12:50Z

Mathlib/Data/FunLike/Basic.lean


-namespace FunLike
+namespace DFunLike


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

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.

Mathlib/Data/FunLike/Fintype.lean

Mathlib/Order/Category/Semilat.lean

kbuzzard · 2024-01-17T14:45:40Z

Mathlib/Order/Hom/Bounded.lean

@@ -36,15 +36,15 @@ variable {F α β γ δ : Type*}

 /-- 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`. -/


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

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.

Mathlib/Topology/Connected/PathConnected.lean

Mathlib/Topology/Homotopy/HomotopyGroup.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Vierkantor · 2024-01-17T16:27:48Z

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 · 2024-01-17T17:38:18Z

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 · 2024-01-17T17:46:59Z

Human error.

bors delegate+

mathlib-bors · 2024-01-17T17:47:01Z

✌️ 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.

Vierkantor · 2024-01-17T18:24:49Z

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

Vierkantor · 2024-01-17T22:18:26Z

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

bors merge

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 · 2024-01-18T00:39:39Z

Pull request successfully merged into master.

Build succeeded:

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.

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.

Vierkantor added awaiting-review The author would like community review of the PR awaiting-CI labels Jan 16, 2024

Vierkantor mentioned this pull request Jan 16, 2024

[Merged by Bors] - refactor(Data/FunLike): use unbundled inheritance from FunLike #8386

Closed

2 tasks

github-actions bot removed the awaiting-CI label Jan 16, 2024

Vierkantor added 2 commits January 17, 2024 13:39

Wrap lines

4145626

Vierkantor force-pushed the FunLike-to-DFunLike branch from 871dbbd to 4145626 Compare January 17, 2024 13:40

kbuzzard reviewed Jan 17, 2024

View reviewed changes

Mathlib/Algebra/Category/MonCat/Basic.lean Outdated Show resolved Hide resolved

kbuzzard reviewed Jan 17, 2024

View reviewed changes

Mathlib/Algebra/Module/LinearMap.lean Outdated Show resolved Hide resolved

kbuzzard reviewed Jan 17, 2024

View reviewed changes

Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean Outdated Show resolved Hide resolved

kbuzzard reviewed Jan 17, 2024

View reviewed changes

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 17, 2024

View reviewed changes

Mathlib/Data/FunLike/Basic.lean Outdated Show resolved Hide resolved

mattrobball reviewed Jan 17, 2024

View reviewed changes

Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean Outdated Show resolved Hide resolved

riccardobrasca reviewed Jan 17, 2024

View reviewed changes

Mathlib/Algebra/Category/MonCat/Basic.lean Outdated Show resolved Hide resolved

mattrobball approved these changes Jan 17, 2024

View reviewed changes

kbuzzard reviewed Jan 17, 2024

View reviewed changes

Vierkantor and others added 7 commits January 17, 2024 16:06

Docstring improvements

e900597

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

This one will not be dependent, so we don't need to change the comment

b8428f8

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Replace Hom_FunLike with Hom_DFunLike

3ae01fa

Replace instFunLike with instDFunLike

51c5d09

Update references from fun_like to DFunLike

6d03bae

Rename instances called funLike to instDFunLike

e5798c5

Update comment

6393cd4

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Jan 17, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 17, 2024

mathlib-bors bot changed the title ~~chore(*): rename FunLike to DFunLike~~ [Merged by Bors] - chore(*): rename FunLike to DFunLike Jan 18, 2024

mathlib-bors bot closed this Jan 18, 2024

mathlib-bors bot deleted the FunLike-to-DFunLike branch January 18, 2024 00:39

Vierkantor mentioned this pull request Jan 18, 2024

[Merged by Bors] - refactor(*): abbreviation for non-dependent FunLike #9833

Closed

Seasawher mentioned this pull request Apr 2, 2024

Update lean to v4.6.0 yuma-mizuno/lean-math-workshop#33

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

Vierkantor commented Jan 16, 2024 •

edited

kbuzzard Jan 17, 2024

Vierkantor Jan 17, 2024

mattrobball left a comment

mattrobball Jan 17, 2024

Vierkantor Jan 17, 2024

kbuzzard left a comment •

edited

kbuzzard Jan 17, 2024

Vierkantor Jan 17, 2024

kbuzzard Jan 17, 2024

Vierkantor Jan 17, 2024

kbuzzard Jan 17, 2024

Vierkantor Jan 17, 2024

Vierkantor commented Jan 17, 2024

mattrobball commented Jan 17, 2024

mattrobball commented Jan 17, 2024

mathlib-bors bot commented Jan 17, 2024

Vierkantor commented Jan 17, 2024

Vierkantor commented Jan 17, 2024

mathlib-bors bot commented Jan 18, 2024

	/- 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

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

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

Conversation

Vierkantor commented Jan 16, 2024 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mattrobball left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kbuzzard left a comment • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Vierkantor commented Jan 17, 2024

mattrobball commented Jan 17, 2024

mattrobball commented Jan 17, 2024

mathlib-bors bot commented Jan 17, 2024

Vierkantor commented Jan 17, 2024

Vierkantor commented Jan 17, 2024

mathlib-bors bot commented Jan 18, 2024

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

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

Vierkantor commented Jan 16, 2024 •

edited

kbuzzard left a comment •

edited