feat(LinearAlgebra): add a variable_alias for VectorSpace#19212
feat(LinearAlgebra): add a variable_alias for VectorSpace#19212
Conversation
PR summary dd812d8c50Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 No changes to technical debt.You can run this locally as
|
Taken directly from the variable_alias docs.
| "Mathlib.Logic.Function.Defs": ["Mathlib.Tactic.AdaptationNote"], | ||
| "Mathlib.Logic.Function.Basic": ["Batteries.Tactic.Init"], | ||
| "Mathlib.Logic.Equiv.Defs": ["Mathlib.Data.Bool.Basic"], | ||
| "Mathlib.LinearAlgebra.VectorSpace": ["Mathlib.Algebra.Module.Pi"], |
There was a problem hiding this comment.
(I'm aware this is needed because I used Mathlib.Algebra.Module.Pi -- my rationale was that someone looking for the alias was likely to be newer, and that this other import seems reasonably cheap anyways. Let me know if that doesn't seem like a good enough reason to ignore this.)
There was a problem hiding this comment.
Please add a test file with variable? [VectorSpace K V] and guard_msgs instead.
There was a problem hiding this comment.
(newbie:) Is there a standard format for adding a test file? What to name it, where to place it? Just asking so I can mimick the moves in my own PR.
|
I just started to use an alias in my own PR on Quantales as well (branch#PieterCuijpers_Quantales / #17289) and basically follow the same route. I just defined the alias in the 'main file' where, I think, it belongs. The planned use, after all to me, is writing [VectorSpace a] is more natural (in a file that proofs something about vector spaces) than writing the unfolding of it. In my case, my reviewers asked me to define a mixin IsQuantale instead of having a proper class Quantale. But then again... this is my first PR ever... so I don't really now anything ;-) |
|
Aha! Thanks for the cross-link and info, I'll have a look at yours as well! |
| /-- A vector space is a module over a field. -/ | ||
| @[variable_alias] | ||
| structure VectorSpace (k V : Type*) | ||
| [Field k] [AddCommGroup V] [Module k V] |
There was a problem hiding this comment.
The docstring should underline the fact that this is not a class and it's here to be used with a variable? command, not as a [VectorSpace K V] assumption in a theorem.
There was a problem hiding this comment.
(I agree with this) but it will apply to every use of variable_alias, correct? In which case it seems like perhaps variable_alias should automatically append that sort of message to the docstring of the declaration you use it on, presuming that should be possible, no?
@Julian That would be great. However, I'm a bit weighing off two choices. I'd like the quantale PR to go through quickly, and having the |
|
The original PR for Quantale has been merged, now it's time to add the variable_alias. I've added a dependency to this PR, so that we can focus the discussion. |
similar to #19212, but for Quantales, taken from the variable_alias docs. Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/why.20.5Bvariable_alias.5D.20attribute.20is.20not.20used.20in.20Mathlib.3F
Taken directly from the variable_alias docs.
Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/why.20.5Bvariable_alias.5D.20attribute.20is.20not.20used.20in.20Mathlib.3F
This is the first actual variable alias added to mathlib. I haven't reviewed variable_alias fully, but it seems like there's at least 3 ways they could be distributed in Mathlib:
Aliasessomewhere near the thing they alias (which seems less discoverable to me)Mathlib.TrainingWheels(with some less playful name) which is meant to define a bunch of more "friendly" aliases all in one place.I kind of like the idea of the third thing as a future module but perhaps it can be synthesized if/when there are more aliases? For now as I say I've done the first one, but please let me know if someone prefers something else.