universe hell in linear algebra

Stream: maths

[Patrick Massot]

Is there a user guide to universe hell fighting in linear algebra? For instance:

variables  {K : Type*}  [field K] {V : Type*} [add_comm_group V] [vector_space K V] [finite_dimensional K V]
           {n : ℕ} {v : fin n → V}


lemma le_of_linear_independent (h : linear_independent K v) : n ≤ findim K V :=

[Patrick Massot]

It looks like docs#finite_dimensional.fintype_card_le_findim_of_linear_independent would help but it assumes the indexing type is in the same universe as the vector space.

[Mario Carneiro]

what hell?

[Mario Carneiro]

I don't see anything troubling in this snippet

[Patrick Massot]

The trouble is in the proof.

[Patrick Massot]

Because fin n and V live in different universes, you cannot apply the lemma I linked to.

[Floris van Doorn]

The lemma has the note

-- Note here we've restricted the universe levels of `ι` and `V` to be the same, for convenience.

I think generalizing this lemma to arbitrary universe levels is a better use of time than writing a user guide to work around it.

[Mario Carneiro]

For whose convenience?

[Floris van Doorn]

The prover of the lemma, presumably.

[Patrick Massot]

My question is: how to prove a general version of such lemmas where it's convenient to assume universe equalities?

[Floris van Doorn]

after you have proven the lemma, apply it to ulift \i and ulift V, and then massage the statement along equivalences to get it for \i and V.

This assumes you have proven that every component of the (statement of the) lemma is invariant under equivalences.

[Patrick Massot]

Mario, what Floris wrote is what I called universe hell.

[Mario Carneiro]

Alternatively, just use the theorem that talks about lift (mk A) instead of mk A when using the cardinal library

[Mario Carneiro]

the proof is exactly as long, you just use different lemmas

[Patrick Massot]

This sounds promising.

[Patrick Massot]

Except I have no idea how to turn it into Lean code.

[Mario Carneiro]

I'm working on it

[Patrick Massot]

Thanks a lot!

[Floris van Doorn]

I think the fintype.card library is not as consistent as the cardinal library, but there is fintype.​card_ulift which requires one more step.

[Floris van Doorn]

import linear_algebra.finite_dimensional

variables  {K : Type*}  [field K] {V : Type*} [add_comm_group V] [vector_space K V] [finite_dimensional K V]
           {n : ℕ} {v : fin n → V}

open finite_dimensional

lemma ulift.down.injective {α} : function.injective (ulift.down : ulift α → α) :=
by { rintro ⟨x⟩ ⟨y⟩ h, dsimp at h, rw h }

lemma le_of_linear_independent (h : linear_independent K v) : n ≤ findim K V :=
begin
  have : linear_independent K (v ∘ ulift.down) :=
    linear_independent.comp h _ ulift.down.injective,
  convert finite_dimensional.fintype_card_le_findim_of_linear_independent this,
  simp,
end

[Mario Carneiro]

#3721

[Mario Carneiro]

Floris's suggestion is good for when you don't want to change the library, but it is better in this case to just already have the universe generalized versions of all the lemmas

[Patrick Massot]

Sure. Thank you very much to both of you anyway.

[Kevin Buzzard]

Patrick -- come back to Type! All your universe problems will melt away!

[Utensil Song]

I think in this topic I've learned something opposite to the other topic:

Even if we can put the universe issue aside at the beginning, one day we'll have to come back to give it a proper treatment.

This topic provides two methods to deal with the situation, both seem not costly, but both are hard to decipher, especially the changes in #3721 look totally random, I'm seeing the 's on u v w, Type*, lemma {m}, _s and maxs, and have no idea how the universes are arranged and by any chance u and u' (for example), m and others, * and others are related in the arrangement. There's so much magic in one page...

[Utensil Song]

Floris van Doorn said:

after you have proven the lemma, apply it to ulift \i and ulift V, and then massage the statement along equivalences to get it for \i and V.

This assumes you have proven that every component of the (statement of the) lemma is invariant under equivalences.

The massage seems to have a pattern, is turning this into a reusable tactic possible?

[Patrick Massot]

I have a variation on universe issues in linear algebras:

example {ι K V : Type*} [field K] [add_comm_group V] [vector_space K V]
  [finite_dimensional K V] {v : ι → V} (hv : is_basis K v) :  fintype ι

the universe issue is hidden a bit, but not much since there are cardinals involved.

[Patrick Massot]

@Mario Carneiro do you have a magic trick here?

[Mario Carneiro]

what's the context?

[Patrick Massot]

import linear_algebra.finite_dimensional

example {ι K V : Type*} [field K] [add_comm_group V] [vector_space K V]
  [finite_dimensional K V] {v : ι → V} (hv : is_basis K v) :  fintype ι :=
sorry

[Patrick Massot]

This is a combination of handling universes in cardinals and fighting fintype

[Mario Carneiro]

I didn't have any universe issues in the proof:

import linear_algebra.finite_dimensional

noncomputable example {ι K V : Type*} [field K] [add_comm_group V] [vector_space K V]
  [finite_dimensional K V] {v : ι → V} (hv : is_basis K v) : fintype ι :=
begin
  apply classical.choice,
  rw [← cardinal.lt_omega_iff_fintype, ← finite_dimensional.findim_eq_card_basis' hv],
  apply cardinal.nat_lt_omega,
end

[Mario Carneiro]

I'm not sure which finite_dimensional theorem you were intending to use

[Patrick Massot]

Thanks you very much Mario. I was stuck at:

  apply fintype.of_cardinal_lt,
  have c1 := finite_dimensional.dim_lt_omega K V,
  have c2 := hv.mk_eq_dim',

(with or without the last prime) which left me with a context having all I needed but all in wrong universes. Was it possible to salvage things from there? Is there any easy explanation of why this was the wrong road? Also I would have never guessed the first line would be this apply classical.choice but I guess this comes from the weirdness of fintype X not being in Prop.

[Patrick Massot]

Would you mind having

lemma fintype.of_cardinal_lt {α : Type*} (h : cardinal.mk α < cardinal.omega) : fintype α :=
classical.choice $ cardinal.lt_omega_iff_fintype.mp h

PRed?

[Patrick Massot]

I makes your proof a lot less puzzling.

[Patrick Massot]

I have yet another example of "fintype is data" fun:

import data.fintype.card

open_locale big_operators

example  (n : ℕ) (ι : Type*)
  [fintype ι]
--  [fintype (fin n ⊕ ι)]
  (f : fin n ⊕ ι → ℤ)
  : ∑ (i : fin n ⊕ ι), f i = 0 :=
begin
  rw fintype.sum_sum_type,
  admit,
end

Uncomment the commented line to see the rewrite failing. Something is really wrong in this whole fintype setup...

[Mario Carneiro]

why is that a reasonable thing to do? That's like having two group instances

[Mario Carneiro]

In this case the second fintype can clearly be inferred from the first

[Patrick Massot]

The sum does not depend on the fintype instance.

[Patrick Massot]

In my real example, the commented instance was used to build the uncommented one, not the other way around.

[Patrick Massot]

I'm not saying that fintype is useless, I can totally believe it can be useful for programming or constructive mathematics, but it's not the right class for defining sums.

[Mario Carneiro]

how about a sum that takes no finiteness argument and returns 0 when the input function is not finitely supported

[Patrick Massot]

I sometimes dreams about that, but I fear this will be very confusing where you think about converging series.

[Mario Carneiro]

We already have tsum for infinite series

[Patrick Massot]

Because such series would have a vanishing sum.

[Mario Carneiro]

Whatever this new sum is it has to work without a topology

[Patrick Massot]

But maybe this would still be better than the current situation.

[Mario Carneiro]

(or equivalently, the discrete topology, where convergence of the infinite sum means that it is finitely supported)

[Mario Carneiro]

we can't really get rid of the existing theory of finset sums, those are still true and applicable for their domain, but we can take the notation and apply it to a different constant

[Mario Carneiro]

of course, it's already a localized notation so it doesn't even have to conflict with the existing development

[Mario Carneiro]

Proposal:

import data.finsupp

open_locale classical

noncomputable def finsum {ι α} [add_comm_group α] (f : ι → α) : α :=
if h : ∃ f' : ι →₀ α, f = f' then (classical.some h).sum (λ _ a, a) else 0

noncomputable def finsum_in {ι α} [add_comm_group α] (s : set ι) (f : ι → α) : α :=
finsum (λ i, if i ∈ s then f i else 0)

localized "notation `∑` binders `, ` r:(scoped:67 f, finsum f) := r" in finsum
localized "notation `∑` binders ` in ` s `, ` r:(scoped:67 f, finsum_in s f) := r" in finsum

[Patrick Massot]

Yes, we should probably have something like that. But the next question is: can we avoid duplicating the whole API?

[Mario Carneiro]

that's sort of the cost of doing business. The theorems aren't the same, so it's mostly a question of which finset sum theorems we want to forego

[Mario Carneiro]

I imagine that most theorems that aren't in the big_operators file can just change to the new sum without being duplicated, but the old API itself still has to stay mostly intact

[Mario Carneiro]

one obvious reason being that the definition I just gave uses finsupp, which uses finset sums to define it

[Mario Carneiro]

so it's more like another API on top of the existing one than a replacement

[Patrick Massot]

All theorem will be there, but some of them will have finiteness assumptions. But sure, this is business.

[Mario Carneiro]

As consolation, I think most of the proofs will be one liners

[Mario Carneiro]

but people generally can never have enough API theorems

[Kevin Buzzard]

@Patrick Massot your theorem about fintype (fin n + iota) is provable with the weaker hypothesis nonempty (fintype iota) which I think is a more useful typeclass for people like you and me

[Kevin Buzzard]

And nonempty (fintype (X + Y)) implies nonempty (fintype X)

[Kevin Buzzard]

@Mario Carneiro you have done a brilliant job of making computable finiteness in Lean but we are missing API for a good noncomputable finiteness concept. I think Reid's idea of making set.finite the fundamental Prop-valued finiteness class and then bundling it with finset2 will produce a type which is easier for reasoning and which will have a noncomputable card which cant be #eval'ed but about which you can prove theorems like Sylow's theorems

[Kevin Buzzard]

I think there should be a typeclass which is propositional and equivalent to nonempty (fintype X)

[Kevin Buzzard]

I don't know whether this should be literally nonempty (fintype X) or whether its actual definition should be finite univ

[Kevin Buzzard]

Maybe it doesn't matter as long as it's proved equivalent to nonempty fintype X

[Kevin Buzzard]

Because Patrick is reasoning not computing, he should be using this Prop-valued concept of finiteness. He is in trouble because he's trying to do reasoning using the wrong typeclass

[Patrick Massot]

Clearly we should do something. The current setup just doesn't work for our purposes (we should probably keep it, maybe with a more specialized name since it corresponds to very specialized purposes).

[Kevin Buzzard]

I'm making an API for a class fintype2 X := nonempty (fintype X). This will at least fix the problem where I was working with finite groups and had a complicated expression involving card (bot : subgroup G) but I couldn't rw (card_bot : card (bot) = 1) because type class inference had managed to find two non-defeq proofs of fintype bot (one coming from the fact that G was finite and one indpendent of this).

[Mario Carneiro]

Kevin Buzzard said:

I think there should be a typeclass which is propositional and equivalent to nonempty (fintype X)

Why don't we just call it is_finite X?

[Mario Carneiro]

We could even eliminate set.finite in favor of is_finite (\u s)

[Mario Carneiro]

it's always been a bit weird that set.finite combines these two operations (going from type to prop and then using sets instead of types) and there is no term for the intermediate operation

[Mario Carneiro]

But I also think that for all these examples of noncomputable versions of functions like card you would be better served getting rid of the typeclass argument entirely rather than making it propositional

[Kevin Buzzard]

So for the definition of card we should dump the typeclass, but then when we're actually proving something which does need finiteness...the idea is that we put the is_finite typeclass into the theorem statement but still use the nat-valued card?

[Kevin Buzzard]

I wondered if finprop X was good name for it, but I think the type in fintype refers to X rather than the type of the output!

[Scott Morrison]

We could do something like rename fintype to finenum or fin_bij, or something that more clearly indicates it is carrying data? Not sure.