Zulip Chat Archive

Stream: maths

Topic: universe hell in linear algebra


view this post on Zulip Patrick Massot (Aug 07 2020 at 15:15):

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 :=

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:16):

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.

view this post on Zulip Mario Carneiro (Aug 07 2020 at 15:33):

what hell?

view this post on Zulip Mario Carneiro (Aug 07 2020 at 15:33):

I don't see anything troubling in this snippet

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:33):

The trouble is in the proof.

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:34):

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

view this post on Zulip Floris van Doorn (Aug 07 2020 at 15:35):

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.

view this post on Zulip Mario Carneiro (Aug 07 2020 at 15:36):

For whose convenience?

view this post on Zulip Floris van Doorn (Aug 07 2020 at 15:36):

The prover of the lemma, presumably.

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:37):

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

view this post on Zulip Floris van Doorn (Aug 07 2020 at 15:38):

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.

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:39):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 15:39):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 15:39):

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

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:41):

This sounds promising.

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:44):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 15:45):

I'm working on it

view this post on Zulip Patrick Massot (Aug 07 2020 at 15:45):

Thanks a lot!

view this post on Zulip Floris van Doorn (Aug 07 2020 at 15:45):

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.

view this post on Zulip Floris van Doorn (Aug 07 2020 at 15:56):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 16:12):

#3721

view this post on Zulip Mario Carneiro (Aug 07 2020 at 16:13):

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

view this post on Zulip Patrick Massot (Aug 07 2020 at 16:13):

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

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 16:36):

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

view this post on Zulip Utensil Song (Aug 08 2020 at 08:06):

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

view this post on Zulip Utensil Song (Aug 08 2020 at 08:10):

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?

view this post on Zulip Patrick Massot (Aug 09 2020 at 15:00):

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.

view this post on Zulip Patrick Massot (Aug 09 2020 at 18:42):

@Mario Carneiro do you have a magic trick here?

view this post on Zulip Mario Carneiro (Aug 09 2020 at 18:43):

what's the context?

view this post on Zulip Patrick Massot (Aug 09 2020 at 18:46):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 18:47):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 19:16):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 19:17):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 21:40):

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.

view this post on Zulip Patrick Massot (Aug 09 2020 at 21:43):

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?

view this post on Zulip Patrick Massot (Aug 09 2020 at 21:44):

I makes your proof a lot less puzzling.

view this post on Zulip Patrick Massot (Aug 09 2020 at 22:50):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 22:52):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 22:52):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 22:53):

The sum does not depend on the fintype instance.

view this post on Zulip Patrick Massot (Aug 09 2020 at 22:53):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 22:54):

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.

view this post on Zulip Mario Carneiro (Aug 09 2020 at 22:56):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 22:57):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 22:57):

We already have tsum for infinite series

view this post on Zulip Patrick Massot (Aug 09 2020 at 22:57):

Because such series would have a vanishing sum.

view this post on Zulip Mario Carneiro (Aug 09 2020 at 22:57):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 22:57):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 22:58):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:00):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:01):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:08):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 23:11):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:15):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:16):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:16):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:17):

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

view this post on Zulip Patrick Massot (Aug 09 2020 at 23:19):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:20):

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

view this post on Zulip Mario Carneiro (Aug 09 2020 at 23:20):

but people generally can never have enough API theorems

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:24):

@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

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:25):

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

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:29):

@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

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:30):

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

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:31):

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

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:31):

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

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:32):

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

view this post on Zulip Patrick Massot (Aug 10 2020 at 18:30):

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).

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 18:44):

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).

view this post on Zulip Mario Carneiro (Aug 10 2020 at 19:25):

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?

view this post on Zulip Mario Carneiro (Aug 10 2020 at 19:29):

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

view this post on Zulip Mario Carneiro (Aug 10 2020 at 19:30):

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

view this post on Zulip Mario Carneiro (Aug 10 2020 at 19:31):

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

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 19:59):

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?

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 19:59):

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!

view this post on Zulip Scott Morrison (Aug 11 2020 at 00:36):

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


Last updated: May 06 2021 at 18:20 UTC