Zulip Chat Archive

Stream: maths

Topic: Span of finite set is sequentially closed


view this post on Zulip Lambert A'Campo (Dec 03 2019 at 15:47):

I am trying to prove the following lemma

open metric set

variables
{V : Type*} [normed_group V] [normed_space  V]

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed (submodule.span  A).carrier :=
begin
  sorry,
end

Is this somewhere in mathlib? If not, how can you induct on the cardinality of A?

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 15:59):

It might be in there -- @Sebastien Gouezel ? Oh, I just remembered he's giving a talk in Orsay right now ;-)

If it's not then maybe this is a useful induction procedure for you:

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed (submodule.span  A).carrier :=
begin
  intro h,
  apply finite.induction_on h,
  sorry, sorry
end

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 16:57):

So it turns out it is actually in mathlib!

variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
{E : Type u} [normed_group E] [normed_space 𝕜 E]
[complete_space 𝕜]

lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
  is_closed (s : set E)

but I'm not quite sure how to make lean transform this into what I need.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 16:59):

I guess you want to find the following facts:
(1) Closed implies sequentially closed [this will be proved near the definition of sequentially closed]
(2) the reals are a nondiscrete normed field [type class inference will handle this]
(3) the vector space spanned by a finite set is finite-dimensional [that will surely be there somewhere]

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:00):

(2) is indeed there:

noncomputable example : nondiscrete_normed_field  := by apply_instance

so you don't have to do anything -- type class inference will do it for you.

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 17:00):

So we are this far

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed (submodule.span  A).carrier :=
begin
  intro h_fin,
  let S := (submodule.span  A).carrier,
  apply is_seq_closed_of_is_closed S,

  apply submodule.closed_of_finite_dimensional,
end

but we get an error:
invalid apply tactic, failed to unify
is_closed S
with
is_closed ↑?m_6

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 17:01):

I thought that this should reduce it to showing that submodule.span \R A is finite dimensional

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:01):

Is there any possibility that you can post some fully working code?

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:02):

I'm getting a bit sick of having to guess all the imports ;-)

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 17:03):

Yes of course, sorry.

import analysis.normed_space.banach
import analysis.normed_space.basic
import linear_algebra.basic
import linear_algebra.basis
import linear_algebra.dimension
import linear_algebra.finite_dimensional
import topology.subset_properties
import set_theory.cardinal
import data.real.basic
import topology.sequences
import order.bounded_lattice
import analysis.specific_limits
import analysis.normed_space.finite_dimension

noncomputable theory
open_locale classical

open metric set

variables
{V : Type*} [normed_group V] [normed_space  V]

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed (submodule.span  A).carrier :=
begin
  intro h_fin,
  let S := (submodule.span  A).carrier,
  apply is_seq_closed_of_is_closed S,

  apply submodule.closed_of_finite_dimensional,
end

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:09):

Yeah. There might be a universe issue and also a typeclass issue.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:11):

#check @submodule.closed_of_finite_dimensional
/-
submodule.closed_of_finite_dimensional :
  ∀ {𝕜 : Type u_2} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u_2} [_inst_2 : normed_group E]
  [_inst_3 : normed_space 𝕜 E] [_inst_6 : complete_space 𝕜] (s : submodule 𝕜 E)
  [_inst_7 : finite_dimensional 𝕜 ↥s], is_closed ↑s
-/

For some reason 𝕜 and E are supposed to be in the same universe in this lemma. This might be some subtlety that I don't know about, or it might be an error in mathlib.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:12):

-- we use linear equivs, which require all the types to live in the same universe
variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
{E : Type u} [normed_group E] [normed_space 𝕜 E]
{F : Type v} [normed_group F] [normed_space 𝕜 F]

This is explicit design decision. I don't know what's going on here. This has consequences for you -- the reals have type Type so Lean expects your vector space also to have type Type.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:13):

But changing the variable to {V : Type} unmasks a new problem.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:15):

which is that type class inference cannot figure out why s is finite-dimensional.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:15):

variables
{V : Type} [normed_group V] [normed_space  V]

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed (submodule.span  A).carrier :=
begin
  intro h_fin,
  let S : set V := (submodule.span  A),
  apply is_seq_closed_of_is_closed S,
  exact @submodule.closed_of_finite_dimensional  _ V _ _ _ _ sorry,
end

works, but there's a sorry

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:17):

So what is left is the proof that S is finite-dimensional. Oh -- by the way -- in Lean there is a "canonical" way of doing many things, and your definition of S as (...).carrier is non-canonical: I changed it to the canonical way of writing this, with the little up-arrow.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:23):

variables {V : Type} [normed_group V] [normed_space  V]

instance moo {V : Type} [normed_group V] [normed_space  V] (A : set V) (hA : finite A) :
  finite_dimensional  (submodule.span  A) :=
begin
  sorry
end


lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed (submodule.span  A).carrier :=
begin
  intro h_fin,
  let S : set V := (submodule.span  A),
  apply is_seq_closed_of_is_closed S,
  exact @submodule.closed_of_finite_dimensional  _ V _ _ _ _ (moo A h_fin),
end

There is this thing called type class inference, which mathematicians tend to push in all sorts of directions which it turns out that Lean 3 was not quite expecting, because computer scientists did not really know what mathematicians wanted to do with it. I can't actually get it to work in this situation (hence all the ridiculous _s and the moo in the lemma) but probably some fiddling around with priorities could fix this.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:25):

You should really change the statement to use the coercion.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:25):

Actually I see now that perhaps moo is a bad instance, because finite is not a typeclass which might mean that typeclass inference will not be able to find the hypothesis that A is finite. I am a bit out of my depth here.

However this is eventually resolved, the missing part of the argument is still the sorry above.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:26):

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V)

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:26):

Needing this up-arrow in the statement is really painful, but we don't know how to avoid this. We explain a tiny variation on this issue in our perfectoid paper.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:27):

Exactly in the paragraph where we complain about Lean elaboration being not yet good enough for maths.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:28):

Then you can write:

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed ((submodule.span  A) : set V) :=
begin
  intro h_fin,
  apply is_seq_closed_of_is_closed,
  haveI : finite_dimensional  (submodule.span  A) := sorry,
  exact submodule.closed_of_finite_dimensional _,
end

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:28):

Where the sorry is still the same one, but there is no more Morse code @... _ _ _ _ _

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:29):

Patrick do you understand why V has to have type Type?

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:30):

It might be in there -- Sebastien Gouezel ? Oh, I just remembered he's giving a talk in Orsay right now ;-)

Yes, he was finishing his talk at that moment. It was very nice talk. He explained maths for 15 minutes, then propaganda for Sledgehammer for 30 minutes then 15 minutes about how simple type theory is unfortunately unbearable.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:31):

theorem finite_dimensional_of_finite_span {V : Type} [normed_group V] [normed_space  V] {A : set V} (hA : finite A) :
  finite_dimensional  (submodule.span  A) :=
begin
  sorry
end

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed ((submodule.span  A) : set V) :=
begin
  intro h_fin,
  apply is_seq_closed_of_is_closed,
  haveI : finite_dimensional  (submodule.span  A) := finite_dimensional_of_finite_span h_fin,
  exact submodule.closed_of_finite_dimensional _,
end

I moved the sorry to a more respectable place.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:32):

He was a bit unfair to Lean though. He explained how Lean is harder to read than Isabelle by comparing tactic scripts on a white background with proof terms on a black background (using a video beamer making it impossible to read VScode's default dark theme).

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:32):

I would rename that as finite_dimensional_span_of_finite.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:32):

And no, I don't know anything about universe issues.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:33):

but then did someone ask him the question about which system is more likely to be able to define the tangent space of a manifold, a trivial undergraduate thing?

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:33):

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space  V] {A : set V} (hA : finite A) :
  finite_dimensional  (submodule.span  A) :=
begin
  sorry
end

lemma finite_span_seq_closed (A : set V) : finite A  is_seq_closed ((submodule.span  A) : set V) :=
begin
  intro h_fin,
  apply is_seq_closed_of_is_closed,
  haveI : finite_dimensional  (submodule.span  A) := finite_dimensional_span_of_finite h_fin,
  exact submodule.closed_of_finite_dimensional _,
end

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:35):

He was very clear Isabelle/HOL is unusable for maths. And also very clear that any system giving him dependant type (and the type Type -> X) + Sledgehammer would make him quit Lean without thinking twice (which looks like a very sensible thing to do).

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:35):

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space  V] {A : set V} (hA : finite A) :
  finite_dimensional  (submodule.span  A) :=
begin
  apply finite_dimensional.of_fg,
  sorry
end

Now we need a finset from a finite set

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:37):

He was very clear Isabelle/HOL is unusable for maths. And also very clear that any system giving him dependant type (and the type Type -> X) + Sledgehammer would make him quit Lean without thinking twice (which looks like a very sensible thing to do).

So we need to make a sledgehammer? Then he'll quit Lean for Lean.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:41):

Look at the discussion we are having. How could we say this software is usable if two non-beginners cannot prove finite_dimensional_span_of_finite within 10 seconds?

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:43):

Of course we don't know the linear algebra part of the library, but this was Sébastien main point: sledgehammer makes knowing the library much much less important.

view this post on Zulip Patrick Massot (Dec 03 2019 at 17:44):

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:44):

I see -- so this is the sort of thing which Sledgehammer does quickly?

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:47):

Of course this result is easily provable, we just have to look through the library and learn the relevant parts (except that I need to leave the office in 10 minutes and I'm trying to finish a grant proposal before that ;-) )

view this post on Zulip Wojciech Nawrocki (Dec 03 2019 at 17:49):

sledgehammer makes knowing the library much much less important

I found this to be the nicest thing about sledgehammer in Isabelle, even more so than the fact that it gives you a proof. The generated snippet is a proof of the goal at hand, but more importantly it contains a list of lemmas which can be used to prove it. Effectively, it's like library_search on steroids, because it automatically finds relevant facts - you can look at the lemmas it found and use them to write a nicer proof.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 17:53):

Then what is our long-term plan for getting a sledgehammer for Lean?

view this post on Zulip Gabriel Ebner (Dec 03 2019 at 17:55):

Then what is our long-term plan for getting a sledgehammer for Lean?

Me moving to Amsterdam. :smile: I'll talk about the current status in January.

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 17:58):

Yes, he was finishing his talk at that moment. It was very nice talk. He explained maths for 15 minutes, then propaganda for Sledgehammer for 30 minutes then 15 minutes about how simple type theory is unfortunately unbearable.

I think that's a fair summary. I also said that Sledgehammer makes the learning curve much smoother in Isabelle/HOL than in Lean or COQ.

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 18:00):

He was a bit unfair to Lean though. He explained how Lean is harder to read than Isabelle by comparing tactic scripts on a white background with proof terms on a black background (using a video beamer making it impossible to read VScode's default dark theme).

The point is that, proof terms don't exist in Isabelle, and this proof in Isabelle would just have been done by automation without needing to think at all. While a tactic proof in Lean would not have been nicer than the term proof. So, I don't think I have been really unfair :)

view this post on Zulip Rob Lewis (Dec 03 2019 at 18:00):

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

I don't think that's fair at all, the higher order proving work that they're doing is great progress.

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 18:29):

Thanks for the extensive discussion. So do I understand correctly that I cannot use this lemma unless R and V have the same type? I find this very strange.

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 18:39):

When I try to prove this theorem I need to transform A : set V to A set ↥(submodule.span ℝ A)... How does that work?

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space  V] {A : set V} (hA : finite A) :
  finite_dimensional  (submodule.span  A) :=
begin
  apply finite_dimensional.of_fg,
  rw submodule.fg_def,
  existsi (A : set (submodule.span  A)),
end

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 19:36):

Things which mathematicians think of as equal are perhaps not equal in type theory. The submodule.span has type submodule ℝ V and probably A has type set V, but when you start talking about the span as an abstract vector space you want A to be a subset of the span, so the span needs to become a type (the ) rather than a term, and then A needs to be changed from set V to set <the finite-dimensional space>.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 19:39):

I don't think that's fair at all, the higher order proving work that they're doing is great progress

I don't know anything about what they're doing. I looked at the website and it didn't seem to mention Lean. So the plan is their work + Gabriel will result in a sledgehammer for Lean? This makes me happy, I am somehow convinced that Gabriel can do anything :D

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 19:57):

So do I understand correctly that I cannot use this lemma unless R and V have the same type? I find this very strange.

Not the same type, the same universe. This is an issue with the linear algebra library, that requires vector spaces to be in the same universe to define linear equivalences between them. But in practice one can do all mathematics in a single universe, so this is not a real issue.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:21):

But in practice one can do all mathematics in a single universe, so this is not a real issue.

That is not the message we get from the CS people. They assure us that it is important that we be maximally universe polymorphic. Is there an actual reason why this design decision was made or was it just for convenience?

Clark Barwick gave a talk at Imperial yesterday and when he was talking about pyknotic sets he had to fix a strongly inaccessible cardinal. This is a point where one really cannot do mathematics in a single universe. Scholze's condensed sets are a variant of this which does not need the inaccessible cardinal, however Scholze ends up with a slightly different class of objects (and he has to jump through a lot of set-theoretic hoops, choosing uncountable cardinals with properties whose existence can be proved in ZFC). We have to make a decision about whether to follow Scholze's point of view or Barwick's, and Barwick's would be much easier to do in Lean, although his pyknotic sets will end up having type Type 1, so pyknotic vector spaces are not going to work in Lean.

view this post on Zulip Mario Carneiro (Dec 03 2019 at 20:34):

But in practice one can do all mathematics in a single universe, so this is not a real issue.

I think that should read "in principle one can do all mathematics in a single universe". In practice you run into exactly the issues that Lambert is noting. Do we have a comprehensive set of instances on ulift? (Including a ulift_instance tactic for making more instances.) If so, it might be possible to work around this by using ulift R as the scalar ring, but it's not a particularly natural solution to work with.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:35):

And what about the solution of making mathlib properly polymorphic? Why is it not polymorphic here?

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 20:35):

What prevents you from adding a large cardinal axiom and doing exactly his construction in Type? (Note that I wouldn't mind using the additional flexibility of type theory to simplify things, but my point is that everything you do in usual mathematics with set theory should be doable in Type).

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:36):

What prevents you from adding a large cardinal axiom and doing exactly his construction in Type? (Note that I wouldn't mind using the additional flexibility of type theory to simplify things, but my point is that everything you do in usual mathematics with set theory should be doable in Type).

Nothing, I believe. Except then you'll have an extra axiom which somehow looks silly in Lean because it basically says "assume Type -1 exists".

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:36):

The obvious response is "why not renumber?"

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:39):

And to be honest if we're going to start using cardinal bounds then we may as well do it the Scholze way anyway, because proving the existence of an uncountable strong limit cardinal (a fun exercise for you Mario? ;-) ) will be possible in Lean without any extra axioms.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:39):

(what we need is an uncountable κ\kappa such that λ<κ    2λ<κ\lambda<\kappa\implies 2^{\lambda}<\kappa)

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:42):

(proof: define a sequence of cardinals κα\kappa_\alpha for α\alpha an ordinal by κ0=0\kappa_0=\aleph_0, κα+1=2κα\kappa_{\alpha+1}=2^{\kappa_\alpha}, and unions at limits; then κα\kappa_\alpha for any (positive) limit ordinal will do the trick)

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 20:45):

I don't know where the root of polymorphism loss is, but dimension.lean starts with the line

variables {K : Type u} {V V₂ V₃ V₄ : Type v}

And since this file was written by Mario and Johannes I am pretty sure there is a very good reason for this.

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 20:46):

Probably when you have maps between these modules you want to compare their dimensions, which are cardinals in some fixed universe.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:48):

Probably you sometimes want to compare their dimensions, but you often do not? That's like saying that equiv should only take two types from the same universe because sometimes you might want to compare their cardinalities. That is not what is done there. I am confused.

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 20:49):

For instance

theorem linear_equiv.dim_eq (f : V ≃ₗ[K] V₂) :
  dim K V = dim K V₂

does not make sense if V and V_2 are not in the same universe, as their dimensions don't live in the same place.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:50):

So that one theorem could be formalised under the assumption that the universes are the same.

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 20:50):

That's the first statement that breaks in this file if I change the universe constraints, but there are many more below. But I agree with you that it would make sense to only assume the same universe when it is really necessary.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:51):

or some ulift nonsense could be added. There are ways around this and all I am saying is that I am surprised that this design decision was taken by people who take universe polymorphism so seriously.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:53):

Of course the Barwick example is very much an extreme case. I absolutely agree with you that 99% of modern maths can be done within one universe. I'm sure Lambert doesn't want to assume the existence of an inaccessible cardinal in his proof so he could change V to have type Type and not lose too much sleep about it.

Can the finite-dimensionality proof be made into an instance?

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 20:53):

Sorry, which proof?

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:58):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Span.20of.20finite.20set.20is.20sequentially.20closed/near/182481084

finite_dimensional is a class but finite is not.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:59):

Oh -- this does not even compile for me! I thought Lambert had done it!

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 20:59):

sorry the proof for now :D

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 21:00):

It doesn't look like an instance. It could be one if you replaced your finite set by a finset, I guess.

view this post on Zulip Mario Carneiro (Dec 03 2019 at 21:01):

There are a few statements in there that require the universe restriction to typecheck, but I'm wary about having that be in the variables list because this is likely to carry the restriction through to other theorems that don't have the restriction

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 21:01):

I'm pretty sure that Lambert's result doesn't need V to be in Type.

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 21:03):

In the dimension file, most of the statements require it, as they talk about dimensions as cardinals. However, when one uses these results to prove things on findim, this imposes the universe restriction in situations where it shouldn't be needed any more.

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 21:07):

Oh -- this does not even compile for me! I thought Lambert had done it!

I have not haha. I just changed V : Type* to V:Type (I don't understand what this means anyways.) and I now I am just left with this nonsensical theorem that the span of a finite set is finite dimensional but I don't know how to prove it because I don't understand the coercion stuff.

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 21:10):

I tried this but now I don't know how to prove things about B...

theorem finite_dimensional_span_of_finite {V : Type} {A : set V} [normed_group V] [normed_space  V] (hA : finite A) :
  finite_dimensional  (submodule.span  A) :=
begin
  apply finite_dimensional.of_fg,
  rw submodule.fg_def,
  let B : set (submodule.span  A) := {b |  a : V, a  A  a = b},
  existsi B,
  sorry
end

view this post on Zulip Patrick Massot (Dec 03 2019 at 21:11):

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

I don't think that's fair at all, the higher order proving work that they're doing is great progress.

I'm very sorry I wrote that too quickly. I was trying to help Lambert, report on Sébastien's talk and cook dinner for my kids in a 10 minutes time slot (on top of the frustration boost I get each time I see sledgehammer). I should have written that end users don't see any progress so far. But I understand there is foundational work to be done, and I'm very excited to read it's progressing (and Gabriel is helping).

view this post on Zulip Sebastien Gouezel (Dec 03 2019 at 21:23):

Something along the lines of

theorem finite_dimensional_of_finite_span {A : set V} (hA : set.finite A):
  finite_dimensional K (submodule.span K A) :=
begin
  apply is_noetherian_of_fg_of_noetherian,
  exact submodule.fg_def.2 A, hA, rfl,
end

could help you.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 21:23):

Do we have to wait until January to hear the progress about Lean's sledgehammer?

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 21:24):

Lambert -- you should come along to Xena and get educated by Imperial's undergraduates ;-)

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 21:27):

Something along the lines of

theorem finite_dimensional_of_finite_span {A : set V} (hA : set.finite A):
  finite_dimensional K (submodule.span K A) :=
begin
  apply is_noetherian_of_fg_of_noetherian,
  exact submodule.fg_def.2 A, hA, rfl,
end

could help you.

Thank you! That did it.

view this post on Zulip Lambert A'Campo (Dec 03 2019 at 21:28):

Lambert -- you should come along to Xena and get educated by Imperial's undergraduates ;-)

Yeah I want to come, I just didn't have time on Thursdays so far. But the unit ball compact -> finite dimensional proof is now complete !

view this post on Zulip Floris van Doorn (Dec 03 2019 at 21:32):

And to be honest if we're going to start using cardinal bounds then we may as well do it the Scholze way anyway, because proving the existence of an uncountable strong limit cardinal (a fun exercise for you Mario? ;-) ) will be possible in Lean without any extra axioms.

Mario already did this fun exercise:
https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/cofinality.lean#L488

view this post on Zulip Floris van Doorn (Dec 03 2019 at 21:33):

Unless I misunderstand, and you want a strong limit ordinal in Type 0.

view this post on Zulip Patrick Massot (Dec 03 2019 at 21:38):

This certainly looks like a hole in mathlib (whose finite dimensional stuff is very sketchy). Shoud it be PRed? Probably something like:

variables (R : Type*) [comm_ring R] [is_noetherian_ring R]

theorem is_noetherian_span_of_finite {V : Type*} {A : set V} [add_comm_group V] [module R V] (hA : finite A) :
  is_noetherian R (submodule.span R A) :=
is_noetherian_of_fg_of_noetherian _ (submodule.fg_def.mpr A, hA, rfl)


variables (K : Type*) [discrete_field K]

theorem finite_dimensional_span_of_finite {V : Type*} {A : set V} [add_comm_group V] [vector_space K V] (hA : finite A) :
  finite_dimensional K (submodule.span K A) :=
is_noetherian_span_of_finite K hA

PRed in noetherian.lean and finite_dimensional.lean

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 21:46):

Oh that's totally the correct way to do it :-) Finitely-generated modules over a Noetherian ring are Noetherian, and hence finitely-generated vector spaces are finite-dimensional :D That's absolutely great :D My mind was muddied by the fact that they teach finite-dimensional vector spaces several years before Noetherian modules!

view this post on Zulip Patrick Massot (Dec 03 2019 at 21:48):

Seriously, that linear algebra library is really really hard to use. What Lambert was trying to do was completely natural, but ended up with had_coe_to_sort hell.

view this post on Zulip Kevin Buzzard (Dec 03 2019 at 21:51):

I think that if a part of the library is new to someone then they often find it hard to use.

view this post on Zulip Patrick Massot (Dec 03 2019 at 21:53):

In the topology part there is nothing that would get you stuck like Lambert was.

view this post on Zulip Johan Commelin (Dec 04 2019 at 08:11):

@Sebastien Gouezel Is there a recording of your talk? (With subtitles :grimacing:)

view this post on Zulip Patrick Massot (Dec 04 2019 at 08:49):

I think there will be video available soon (without subtitles).

view this post on Zulip Patrick Massot (Dec 04 2019 at 08:53):

I asked and immediately got a temporary url: https://webdiff.math.u-psud.fr/5de68f39862d2a0419e311ed

view this post on Zulip Patrick Massot (Dec 04 2019 at 08:56):

I have no idea why they kept the streams from cameras looking at the audience, especially since they were zooming on mostly empty areas of the lecture room.

view this post on Zulip Johan Commelin (Dec 04 2019 at 08:59):

Thanks for the link. I'll see if I can get anything out of it (-;


Last updated: May 09 2021 at 09:11 UTC