PiTensorProduct basis Finite/Fintype switch up

Stream: mathlib4

[Paradoxy]

In the LinearAlgebra.PiTensorProduct.Basis file, a switch up between [Finite ι] and [Fintype ι] has happened. In particular, in the Basis.piTensorProduct and Basis.piTensorProduct_repr_tprod_apply.

This, in turn has made the proof of Basis.piTensorProduct_repr_tprod_apply very long, ending with rather unusual convert rfl. I can instead safely prove

theorem Basis.piTensorProduct_repr_tprod_apply [Finite ι] (b : Π i, Basis (κ i) R (M i))
    (x : Π i, M i) (p : Π i, κ i) :
    haveI := Fintype.ofFinite ι
    (Basis.piTensorProduct b).repr (tprod R x) p = ∏ i : ι, (b i).repr (x i) (p i) := by
  simp [piTensorProduct]

In fact, I can see the same pattern in Dual file: (dualDistrib vs dualDistrib_apply). Can you please let me know how is beneficial to assume different instances here?

[Aaron Liu]

I have a shorter proof of Basis.piTensorProduct_repr_tprod_apply:

@[simp]
theorem Basis.piTensorProduct_repr_tprod_apply [Fintype ι] (b : Π i, Basis (κ i) R (M i))
    (x : Π i, M i) (p : Π i, κ i) :
    (Basis.piTensorProduct b).repr (tprod R x) p = ∏ i : ι, (b i).repr (x i) (p i) := by
  rw [piTensorProduct, Subsingleton.elim (Fintype.ofFinite ι) ‹_›]
  simp

[Aaron Liu]

fits in the file

[Aaron Liu]

#33023

[Paradoxy]

@Aaron Liu , well my problem is not the long proof per se, but the switch up itself. What is its purpose? In particular, what problem does it address?

[Aaron Liu]

ask the author maybe?

[Aaron Liu]

@Daniel Morrison

[Aaron Liu]

the relevant PR is #32613

[Kevin Buzzard]

Yeah that theorem looks bad: probably [Fintype ι] is the right assumption if you need it to make the theorem statement compile. Of course a better fix would be to fix things so that you didn't need Fintype to make the statement compile, but still...

[Paradoxy]

Aaron Liu said:

ask the author maybe?

I thought I am missing something very obvious. As an end-user it either forces me two create two instances, or to construct one instance from another which is painful.

[Aaron Liu]

Paradoxy said:

In fact, I can see the same pattern in Dual file: (dualDistrib vs dualDistrib_apply).

Oh no, that sounds bad

[Daniel Morrison]

The switch was suggested in review to avoid propagating the Fintype instance and continuing to require decidability. I think the idea is that Finite is the better one to use long term and is capping off the decidability conditions there. So short term its harder to use but long term this way is better. It doesn't really matter to me and I had initially just used Fintype since that was what was there. I was also reviving old work that never got merged so tbh I mainly used what other people had used or recommended.

[Aaron Liu]

Aaron Liu said:

Paradoxy said:

In fact, I can see the same pattern in Dual file: (dualDistrib vs dualDistrib_apply).

Oh no, that sounds bad

Wait no I misunderstood what you were saying, dualDistrib_apply is fine.

[Paradoxy]

Aaron Liu said:

Aaron Liu said:

Paradoxy said:

In fact, I can see the same pattern in Dual file: (dualDistrib vs dualDistrib_apply).

Oh no, that sounds bad

Wait no I misunderstood what you were saying, dualDistrib_apply is fine.

How is it fine? dualDistrib uses Finite instance, dualDistrib_apply uses Fintype instance. Also in the proof of dualDistrib_apply we again have convert rfl. I mean sure, one can fix it by rewriting instances, but the design decision itself is something that I cannot understand.

[Aaron Liu]

the idea is that we want to use the lemma to rewrite into whatever Fintype instance we have lying around, not just Fintype.ofFinite.

[Paradoxy]

@Aaron Liu then why can't we define dualDistrib with Fintype instance in the first place?

[Aaron Liu]

we can definitely do that

[Aaron Liu]

this is where I ask the author why didn't you do that

[Paradoxy]

Daniel Morrison said:

The switch was suggested in review to avoid propagating the Fintype instance and continuing to require decidability. I think the idea is that Finite is the better one to use long term and is capping off the decidability conditions there. So short term its harder to use but long term this way is better. It doesn't really matter to me and I had initially just used Fintype since that was what was there. I was also reviving old work that never got merged so tbh I mainly used what other people had used or recommended.

Hmm, I see classical instances are being used in both definitions and theorems with either open Classical in or classical tactic. So decidableEq instances are provided for free. What other decidability instance exists here?

[Daniel Morrison]

My understanding is that right now some basic parts of the API for these kinds of things, like finite sums, is written in terms of Fintype and using DecidableEq when they technically shouldn't require anything more than Finite. So at the moment Fintype and DecidableEq is an implicit requirement in lots of these structures when it probably shouldn't be long term. These are written in an awkward way to try to cut off that propagation of instances so future stuff can be build on top of it only using Finite. My understanding is the long term plan is to move everything over to Finite, and making the switch here can hopefully cut down the amount of stuff that needs to be rewritten in the future.

Like I said, this was suggested in review and I'm not really an expert on these kinds of issues and had initially written the PR using Fintype and DecidableEq for exactly the reason you are saying. Perhaps @Oliver Nash can explain more. But the short answer is that I guess there are long-term design goals at play that make some short-term additions a bit strange.

[Paradoxy]

@Daniel Morrison, @Oliver Nash
I think with haveI := Fintype.ofFinite ι instance (as already used in dualDistrib), we can change all theorems to require only Finite and not a Fintype. This also simplifies some proofs, like the one I wrote in my first post. In future, when other parts of library are re-written with Finite, we can just remove haveI := Fintype.ofFinite ι line from all theorems.

[Aaron Liu]

I really hope we don't get rid of Fintype

[Daniel Morrison]

There are probably ways to clean up some of the instance switching and if you do feel free to make changes. I added these as a part of reviving older work moving toward exterior powers so if you want to spend more time on the Multilinear stuff feel free!

[Oliver Nash]

@Paradoxy Here's an example of why we don't want to author lemmas using haveI := Fintype.ofFinite ι:

import Mathlib

variable {ι : Type*} (f : ι → ℕ)

noncomputable def myMax [Finite ι] : ℕ := ⨆ i, f i

-- Good
lemma myMax_eq [Fintype ι] :
    myMax f = Finset.sup Finset.univ f :=
  (Finset.sup_univ_eq_ciSup f).symm

-- Bad
lemma myMax_eq' [Finite ι] :
    haveI := Fintype.ofFinite ι
    myMax f = Finset.sup Finset.univ f := by
  convert (Finset.sup_univ_eq_ciSup f).symm

example (g : Fin 10 → ℕ) :
    myMax g = Finset.sup Finset.univ g := by
  rw [← myMax_eq'] -- Fails 😱

example (g : Fin 10 → ℕ) :
    myMax g = Finset.sup Finset.univ g := by
  rw [← myMax_eq] -- Succeeds

[Oliver Nash]

The point is that if you use haveI := Fintype.ofFinite ι to make your lemma statement, then your lemma is a lemma about this instance but Fintype contains data and so your lemma may fail to apply in situations where a different Fintype instance has been provided.

[Oliver Nash]

The issue is that Fintype tells us how a type is finite (analogous to a chosen numbering of its elements) whereas Finite merely tells us that a type is finite and there is a choice of $n!$ ways for describing how something is finite.

[Oliver Nash]

The advantage of Fintype is that it is computable. The disadvantage is the diamond issue. In many circumstances in Mathlib, computability is irrelevant and so we are slowly changing things so that statements can be built using only Finite rather than Fintype.

For example if Finset.sup demanded [Finite ι] rather than [Fintype ι] then the issue would not arise.

[Oliver Nash]

This question comes up again and again (as does its DecidableEq variant) we should probably write a blog post about this, which starts with a cheat sheet for newcomers.

[Kevin Buzzard]

Or we could just fix it by making a nonconstructive finsupp and then ripping finsupp out of tensor products and group cohomology (where constructivity has found 0 uses so far)

[Paradoxy]

@Oliver Nash

So is this preferred?

variable {ι : Type*} [Finite ι] {R : Type*} {M : ι → Type*} [CommSemiring R]
  [Π i, AddCommMonoid (M i)] [Π i, Module R (M i)] (f : Π i, Dual R (M i)) (m : Π i, M i)

noncomputable def test := dualDistrib (⨂ₜ[R] i, f i) (⨂ₜ[R] i, m i)

-- Error: because Finset.prod univ requires Fintype
example : test f m = ∏ i, (f i) (m i) := sorry

example : -- Super ugly
  haveI := Fintype.ofFinite ι
  test f m = ∏ i, (f i) (m i) := by
  haveI := Fintype.ofFinite ι
  rw [test, dualDistrib_apply]
  convert rfl

example [Fintype ι] : -- Works, but now ι is assumed to be both Finite and Fintype!
  test f m = ∏ i, (f i) (m i) := by
  rw [test, dualDistrib_apply]

The situation above is avoidable by assuming [Fintype ι] from the beginning. But if we are going to use [Fintype ι] anyways, then we might as well define dualDistrib with Fintype. Not only does it make all relevant proofs much easier, but also if the computability is concerned, it should be formalized with the Fintype in the first place as you said (same logic / example can be applied to basis file).

[Oliver Nash]

I can only write a very brief message because I’m at a Christmas lunch but Finite for definitions and Fintype for lemmas whose statement requires it is approximately the rule.

[Johan Commelin]

@Paradoxy you can omit [Finite \iota] in before that example.

[Paradoxy]

Johan Commelin said:

Paradoxy you can omit [Finite \iota] in before that example.

As an end user, I cannot fix \iota to be a specific type, I have to keep it generic. With this restriction, what makes sense to me is to either assume Finite \iota or Fintype \iota and develop the rest of library based on that. What I would not like to do is to assume Finite \iota at the beginning and then use Fintype \iota whenever I get stuck, like in that example.

Just like @Oliver Nash said, the purpose of Fintype is to make things computable. To begin with, dualDistrib is made noncomputable by opening classical. Would it not better to make all corresponding lemmas require Finite as well? In my original post, I have provided this lemma as an example. If the end user has a Fintype, then it is their responsibility to make a Finite instance for it to use this part of library. Alternatively, if everything is Fintype based no issue would arise as well. It is this mixture that makes things hard.

[Johan Commelin]

Paradoxy said:

As an end user, I cannot fix \iota to be a specific type, I have to keep it generic. With this restriction, what makes sense to me is to either assume Finite \iota or Fintype \iota and develop the rest of library based on that.

I don't follow this claim. Fintype implies Finite. So just like with other theorems, you try to weaken your hyps and strengthen your conclusions where possible. So for the definition of test you only need Finite. But then you relate it to a Finset.prod univ which require Fintype, so for that result you assume Fintype.

You might argue that Finset.prod univ should only require Finite. But that is a separate discussion.

[David Gross]

Interesting conversation. Thanks everybody.

Let me try my hand at a lurker's summary.

There's competing visions about the long-term role of constructivism in the library, though "less of that" seems to command a majority. But however things might be in the future, for now, there's plenty of code that requires [Fintype] instances. The recommendation is to "contain further spread" of Fintype, by having new definitions depend on [Finite]. Necessarily this will lead to some boilerplate code when crossing the boundary from Finite to Fintype (see Daniel's code post-review). This isn't perfect, but generally seen as an acceptable way of handling the present situation. Finally, lemmas that expose the existing Fintype API should take the instance as an argument, rather than creating it locally, to avoid diamonds, as demonstrated by Oliver.

If I got this very wrong, then @Oliver Nash , I'd be very much looking forward to that blog post. :slight_smile:

[Oliver Nash]

Thanks David, this captures my thoughts on this matter extremely well!

[Johan Commelin]

I think for new definitions, it should be considered on a case-by-case basis, whether the computational aspects of Fintype over Finite are useful.
But certainly, one lesson that we didn't appreciate N years ago, but that we are well aware of now, is: if only a proof needs Fintype, but the statement doesn't, then the assumption should be Finite, and it should upgrade to Fintype in the proof.

[Bhavik Mehta]

Kevin Buzzard said:

Or we could just fix it by making a nonconstructive finsupp and then ripping finsupp out of tensor products and group cohomology (where constructivity has found 0 uses so far)

Note that Finsupp is already nonconstructive, and this is explicitly mentioned here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finsupp/Defs.html#Implementation-notes

[Paradoxy]

Johan Commelin said:

I think for new definitions, it should be considered on a case-by-case basis, whether the computational aspects of Fintype over Finite are useful.
But certainly, one lesson that we didn't appreciate N years ago, but that we are well aware of now, is: if only a proof needs Fintype, but the statement doesn't, then the assumption should be Finite, and it should upgrade to Fintype in the proof.

Neither of Basis.piTensorProduct, ofFinsuppEquiv, or ofDFinsuppEquiv require Fintype in the statement. However, only Basis.piTensorProduct requires Finite in the signature and upgrade it to Fintype in its proof. Both ofFinsuppEquiv and ofDFinsuppEquiv require Fintype in their signature as opposed to Finite. (The only use of ofFinsuppEquiv / ofDFinsuppEquiv is in Basis.piTensorProduct currently). Can you please tell me what makes ofFinsuppEquiv and ofDFinsuppEquiv exceptional?

On the other hand, the reason the current lemmas require Fintype in the statement itself is the use of BigOperators like Finset.prod. \Prod i is understood as product over Finset.univ iand Finset.univ i requires Fintype. However, one can define

variable {α : Type*} [Finite α]
noncomputable def Finset.univ' : Finset α :=
  haveI := Fintype.ofFinite α
  Finset.univ

and take product over Finset.univ' . This way, one would not need Fintype in the statement of the lemmas anymore. Sorry if I am misunderstanding. But still I cannot see why everything is not Finite based when computability is of no concern.

[Andrew Yang]

You will have to replace Finset.univ with Finset.univ' everywhere or this discrepancy will just show up somewhere else.

[Paradoxy]

Andrew Yang said:

You will have to replace Finset.univ with Finset.univ' everywhere or this discrepancy will just show up somewhere else.

Why do we need to change it everywhere? Some places may actually want computable definitions. I imagine both univ and univ' can coexists, they are also propositionally equal.

[Andrew Yang]

Then you will need to switch between them in proofs if you want to use theorems stated about both of them? And this will still amount to the same yoga that you are asking about here.

[Paradoxy]

Andrew Yang said:

Then you will need to switch between them in proofs if you want to use theorems stated about both of them? And this will still amount to the same yoga that you are asking about here.

I am not sure if I am following. I can prove

@[simp]
lemma univ'_eq_univ {α : Type*} [Fintype α] : Finset.univ' (α := α) = Finset.univ := by
  rw [Finset.univ', Subsingleton.elim (Fintype.ofFinite α) ‹_›]

Now, if I state all relevant lemmas of PiTensorProduct files with Finset.univ' and only Finite in the signature, I can simply do a simp inside the proof to get the usual univ lemmas. What is the extra work here?

[Andrew Yang]

The extra work is the use of univ'_eq_univ.

[Andrew Yang]

By containing the "univ'_eq_univ" problem locally in the proof of these lemmas, you avoid asking users to do this in downstream applications.

[Paradoxy]

Andrew Yang said:

The extra work is the use of univ'_eq_univ.

Is it not marginally better to have a unified Finite based lemmas/defs at the cost of this single extra lemma?

[Andrew Yang]

The cost is not "having this lemma", but requiring users to rewrite back and forth with this lemma when you can just avoid this problem by stating your lemmas more generally.

[Paradoxy]

Andrew Yang said:

The cost is not "having this lemma", but requiring users to rewrite back and forth with this lemma when you can just avoid this problem by stating your lemmas more generally.

I believe a lemma based on Finite is more general than the current lemmas based on Fintype. Fintype imlplies Finite, but not the otherway around. So a user who uses a Finite type cannot apply the current Fintype based lemmas. But a user that uses Fintype, may use the lemmas I am suggesting. But yes, it will come at the cost of using univ'_eq_univ.

[Aaron Liu]

the argument is that it's not as expensive to just write have := Fintype.ofFinite E when you need it than to have another definition

[Andrew Yang]

The point is that a user who uses a Finite type cannot possibly even write down the statement so this is not a concern. If it is possible for a user with only a Finite assumption to write down a hypothesis then yes you should use Finite in the theorem.

[Paradoxy]

Aaron Liu said:

the argument is that it's not as expensive to just write have := Fintype.ofFinite E when you need it than to have another definition

Well I wish it was just have := Fintype.ofFinite E. But in practice one needs to deal with diamonds, like the PR you commented at the beginning of the current thread. univ'_eq_univ on the other hand, takes care of diamonds by itself.

Andrew Yang
The point is that a user who uses a Finite type cannot possibly even write down the statement so this is not a concern. If it is possible for a user with only a Finite assumption to write down a hypothesis then yes you should use Finite in the theorem.

Well, I can write the statements of relevant lemmas with univ', since it only requires Finite.

[Aaron Liu]

Paradoxy said:

Aaron Liu said:

the argument is that it's not as expensive to just write have := Fintype.ofFinite E when you need it than to have another definition

Well I wish it was just have := Fintype.ofFinite E. But in practice one needs to deal with diamonds, like the PR you commented at the beginning of the current thread.

The argument is that if you have := Fintype.ofFinite E, then that implies there is no diamonds, since you have no Fintype instance in scope

[Andrew Yang]

Fintype imlplies Finite, but not the otherway around.

The correct picture is that there is a surjection (up-to-defeq) Fintype I -> Finite I and a section Fintype.ofFinite : Finite I -> Fintype I. Rather than stating theorems about the range of Fintype.ofFinite, you should state theorems about an arbitrary Fintype I. In this sense, theorems about Fintype.ofFinite are less general than theorems about arbitrary fintypes.

[Andrew Yang]

But in practice one needs to deal with diamonds, like the PR you commented at the beginning of the current thread.

A key point is that this messyness is self-contained. You don't need to worry about these when you are just using the API. On the contrary your univ' trick requires users of the API to also be aware of these nastiness and need to work around it.

[Paradoxy]

Andrew Yang said:

Fintype imlplies Finite, but not the otherway around.

The correct picture is that there is a surjection (up-to-defeq) f : Fintype I -> Finite I and a section Fintype.ofFinite : Finite I -> Fintype I. Rather than stating theorems about the range of Fintype.ofFinite, you should state theorems about an arbitrary Fintype I. In this sense, theorems about Fintype.ofFinite are less general than theorems about arbitrary fintypes.

Yes, this much I understood from yesterday's conversation. So I tried to use univ' to avoid the need of have := Fintype.ofFinite E in the statement of the lemma, which makes it less general and limited to a particular Fintype instance.

Now, I have a purely Finite based lemma, that never uses have := Fintype.ofFinite Ein the statement but has a univ' in its statement will be used as follows:

If the end user have Finite type, when they apply my lemma, in their proof they get a univ'. If they like, they can make have := Fintype.ofFinite E first, and then apply the lemma, automatically univ'_eq_univ will be also applied, so they get a normal product.

For the end user who have Fintype, once they apply the lemma, `univ'_eq_univ will be also applied, so they also get a normal product. No diamonds, defeq abuse, etc would happen.

[Andrew Yang]

There are also no diamonds, defeq abuse, etc happening for downstream users in this current setup.

[Andrew Yang]

Okay I maybe get some of your point now. In the titular lemma, only the RHS requires Fintype, but when using it as a simp lemma you might want it to fire even if you haven't upgraded your Finite to a Fintype yet.

(Basis.piTensorProduct b).repr (tprod R x) p = ∏ i : ι, (b i).repr (x i) (p i)

[Paradoxy]

Andrew Yang said:

There are also no diamonds, defeq abuse, etc happening for downstream users in this current setup.

Diamonds do not happen for the end-users in either of two setups. But it does happen for API developers. For example in this PR 33023 relevant to Basis file, a diamond is addressed by rw [Subsingleton.elim (Fintype.ofFinite ι) ‹_›]. Now, following the current rule of keeping definitions Finite and theorems Fintype when needed means, constantly doing rw [Subsingleton.elim (Fintype.ofFinite ι) ‹_›]. Whereas the existence of univ' somehow addresses the problem. Even though, it is very ugly indeed.

[Aaron Liu]

If you have univ' you now have to duplicate all the lemmas about univ

[Andrew Yang]

I don't think it "addresses the problem". It is still the same problem but you add Finset.univ'_eq_univ instead of Subsingleton.elim (Fintype.ofFinite ι) ‹_› to the simp lemmas, which is basically the same thing to me.

[Andrew Yang]

Andrew Yang said:

Okay I maybe get some of your point now. In the titular lemma, only the RHS requires Fintype, but when using it as a simp lemma you might want it to fire even if you haven't upgraded your Finite to a Fintype yet.

(Basis.piTensorProduct b).repr (tprod R x) p = ∏ i : ι, (b i).repr (x i) (p i)

But back to this point which I am now sympathetic to, I guess the point is that if you state it in terms of Finite, then this is a "weaker lemma", but a "stronger simp lemma". So then the question becomes: do we care about this extra strength? If so maybe we could have a Finite form as a simp lemma, i.e.

theorem Basis.piTensorProduct_repr_tprod_apply [Finite ι] (b : Π i, Basis (κ i) R (M i))
    (x : Π i, M i) (p : Π i, κ i) :
    (Basis.piTensorProduct b).repr (tprod R x) p =
      (haveI := Fintype.ofFinite ι; ∏ i : ι, (b i).repr (x i) (p i)) := by
  simp [piTensorProduct]

and keep the old one without a simp tag.

[Aaron Liu]

does this do anything though?

[Aaron Liu]

I feel like for this to be really useful you have to have that product on the rhs simplify further

[Paradoxy]

Aaron Liu said:

If you have univ' you now have to duplicate all the lemmas about univ

Andrew Yang said:

I don't think it "addresses the problem". It is still the same problem but you add Finset.univ'_eq_univ instead of Subsingleton.elim (Fintype.ofFinite ι) ‹_› to the simp lemmas, which is basically the same thing to me.

Fair enough. But if the plan is to migrating to Finite, and avoiding Fintype whenever possible, is it not the starting point anyways? For every definition with Finite we have several Fintype lemmas. At least the evil I am suggesting makes all lemmas Finite based too, less lemmas will be polluted by Fintype. But the current plan of mixing Finite with Fintype, well, I cannot see how it is helpful in this migration.

[Aaron Liu]

and the fintype prod lemmas have [Fintype α] as assumption so they won't fire

[Paradoxy]

Andrew Yang said:

>

But back to this point which I am now sympathetic to, I guess the point is that if you state it in terms of Finite, then this is a "weaker lemma", but a "stronger simp lemma". So then the question becomes: do we care about this extra strength? If so maybe we could have a Finite form as a simp lemma, i.e.

theorem Basis.piTensorProduct_repr_tprod_apply [Finite ι] (b : Π i, Basis (κ i) R (M i))
    (x : Π i, M i) (p : Π i, κ i) :
    (Basis.piTensorProduct b).repr (tprod R x) p =
      (haveI := Fintype.ofFinite ι; ∏ i : ι, (b i).repr (x i) (p i)) := by
  simp [piTensorProduct]

and keep the old one without a simp tag.

Well this one is not good, as you said, it won't fire for arbitrary Fintypes. univ' solution though does fire, and will be simplified further by univ'_eq_univ

[Andrew Yang]

But if the plan is to migrating to Finite, and avoiding Fintype whenever possible, is it not the starting point anyways?

I'm not sure if there is such a plan. We are avoiding Fintype whenever unnecessary, but I think the current consensus is to deem Fintype appearing in Finset.prod as necessary.

[Andrew Yang]

Well this one is not good, as you said, it won't fire for arbitrary Fintypes. univ' solution though does fire, and will be simplified further by univ'_eq_univ

No it does fire because the LHS does not contain Fintype.ofFinite ι. But I'm also not saying it is good. I'm just saying it might not be totally out of the picture.

[Andrew Yang]

Also Subsingleton.elim (Fintype.ofFinite ι) ‹_› probably is a good idea as a simproc.

[Johan Commelin]

@Paradoxy You might hear people say "Mathlib does not care about computability" as some sort of slogan. But with these short slogans, there are usually footnotes. For something like Finset.prod we do care about computability. At least until there is a tactic that takes over all the finite computations that the kernel currently does for us.
We just care much much less about computability than other formalization efforts.