attributes

Stream: new members

[Alex Zhang]

simp * with parity_simpsuses attribute parity_simps. Is there any list documented of such attributes such that if I want to usesimp with, I can look for an attribute that I want to use?

[Eric Rodriguez]

they're not that commonly used, people just tend to jam many things into simp. i mentioned a couple more of them here

[Bryan Gin-ge Chen]

I think it might be something someone could get our documentation generator to collect, so I've opened an issue: doc-gen#133

[Alex Zhang]

What is the function of attitude reducibility

[Kevin Buzzard]

Attributes like reducible are a message to the elaborator

[Alex Zhang]

Right! I noticed reducible. There is also one called reducibility, between which I don't fully understand the difference.

[Kevin Buzzard]

I can't find reducibility in mathlib. Can you give me an example of what you're talking about?

[Eric Wieser]

I think docs#tactic.decl_reducibility is the underlying representation that @[reducible] etc use

[Floris van Doorn]

Most low-level tactics use docs#tactic.transparency to determine how definitions to unfold, for example in docs#tactic.is_def_eq or docs#tactic.whnf. It has two more options than docs#tactic.decl_reducibility (which is new to me): instances (this is used by type-class inference, and includes all reducible definitions and semireducible instances), and none (unfold nothing).

[Alex Zhang]

Could anyone please explain the tag @[nolint unused_arguments] before the definition of matices?

@[nolint unused_arguments]
def matrix (m : Type u) (n : Type u') [fintype m] [fintype n] (α : Type v) : Type (max u u' v) :=
m → n → α

[Alex J. Best]

Mathlib has several linters which check code added to the library doesn't contain certain mistakes or inefficiencies. One of these is the unused arguments linter, which complains when you try and a declaration with assumptions that aren't used. Most of the time this is useful but occasionally we want to have some assumptions on a definition that aren't required to make the definition itself. In this case mathlib assumes matrices are indexed by finite types even though this isnt necessary to define matrices as functions from m and n to alpha. So we ask the unused arguments linter to ignore this declaration using the nolint attribute.

[Patrick Massot]

That doesn't explain why this particular instance is allowed to be an exception.

[Scott Morrison]

Maybe one can just remove the [fintype] arguments in the actual definition. (Certainly they'll be needed later.)

[Scott Morrison]

Ideally every @[nolint] would also come with a comment explaining what goes wrong without it.

[Scott Morrison]

It's possible that in this case someone just felt the [fintype] arguments should be there from the beginning to "signal intent".

[Scott Morrison]

(Usually that's a bad idea, however. Infinite matrices are actually a reasonable thing sometimes!)

[Alex J. Best]

Yes I don't personally understand why the assumption is here in this case. Just explaining the general principle. If you know the reason Patrick please tell us

[Alex Zhang]

Many thanks for your explanations!

[Eric Rodriguez]

Alex J. Best said:

Yes I don't personally understand why the assumption is here in this case. Just explaining the general principle. If you know the reason Patrick please tell us

seems it's just always been like that: #334, and then no-one bothered removing the assumption

[Patrick Massot]

I vote for removing it

[Eric Wieser]

Removing it would stop fintype diamonds coming up in the type itself, which is probably a good thing!

[Eric Rodriguez]

I was starting on this, and matrix.mul is based on a finite definition. We could switch to composition, right? My brain is currently in "adding [fintype X] when Lean shouts" mode...

[Johan Commelin]

multiplying infinite matrices is tricky

[Eric Rodriguez]

so should I just leave it as is for now with fintypes sprinkled?

[Johan Commelin]

Yeah, that's what I would do.

[Johan Commelin]

Someone can add a matrix.sparse_mul later (or some other variant).

[Scott Morrison]

Don't you just introduce the fintype hypothesis at the moment you define mul?

[Eric Rodriguez]

yes, that's what I'm doing now but I was thinking if there was some way to have infinite matrix mul

[Alex J. Best]

Could there be a useful version using docs#finsum of the support of the set of products of entries to be added? Then the mul of any strictly upper triangular (i.e. nilpotent) matrices would be defined

[Johan Commelin]

I guess that works, but changing to finsum will be a refactor that requires quite a bit more work than simply removing these fintype assumptions.

[Johan Commelin]

If someone volunteers to do that, great!

[Eric Rodriguez]

i started doing this in branch#matrix_not_fintype; all I've done so far is busy-work (removing fintypes), but I'll start looking at some proofs soon... I think minor could have less fintypes

[Eric Rodriguez]

one that I'm specifically interested in is induction_on; that definitely doesn't seem fintype dependent, but the proof currently uses a blunt fintype argument. however, I don't think I know the areas of mathlib that deal with these sorts of sums yet; can anyone take a look at that?

[Alex J. Best]

I don't think this is true without fintype (I'm not at lean so I could be wrong but): the proposition "M has only finitely many nonzero entries" is true for the standard basis and is preserved by addition but isn't true for arbitrary (infinite) matrices

[Eric Rodriguez]

ahh, that's a nice counterexample - thanks :)

[Kevin Buzzard]

In the theory of p-adic modular forms there are infinite-dimensional spaces of forms, and Hecke operators can be represented as explicit matrices over a topological ring which don't have finite support in any sense, however there is a tmul or whatever it's called, and we only apply it when everything is absolutely convergent so there is no issue with order of summation.

[Kevin Buzzard]

If someone wants to knock up a tmul which works for the p-adic numbers then we could be proving theorems about p-adic modular forms before we've proved anything about classical modular forms, because p-adic modular forms have several combinatorial definitions

[Johan Commelin]

@Kevin Buzzard What do you mean with tmul? In mathlib tmul is the name for elementary tensors...
Do you mean the multiplicative variant of tsum?

[Kevin Buzzard]

Yeah I just got the name wrong, I have a bad memory and lousy internet. To compute the product of the infinite matrices you use tsum to compute the coefficients.

[Johan Commelin]

But tsum already exists. So everything is there in principal, right?

[Kevin Buzzard]

Right --- and then one has to prove things like mul_assoc etc

[Kevin Buzzard]

There's also a theory of characteristic power series if things converge enough

[Kevin Buzzard]

There's also a finite rank theory, where there is a finite support condition on columns but not rows -- then products are always well-defined

[Eric Rodriguez]

#8810

[Eric Rodriguez]

It'd be nice if it was merged soon, but honestly I had to change far less files than I thought so it's not like going to keep breaking

[Eric Rodriguez]

Most things like multiplying matrices it turns out ;b

[Eric Rodriguez]

Now compiles with no linter unused warnings :)

[Eric Rodriguez]

just wanna bump this — I feel like it's worth merging soon so people can start thinking about infinite matrix stuff