First Time Contributing

Stream: new members

[ccn]

Hey there, I'd like to add the definition of rank of a set of vectors (https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets) to mathlib,

The definition of the rank of a set of vectors is the number of linearly independent vectors, so given the set { [1 0], [0 1], [a b], ... } it's rank is always going to be 2, whereas the rank of { [1 0 ] } is just 1. Another way to figure it out is to take the span of those vectors and then take the rank of it as a vector space/module.

so far I've followed this guide: https://leanprover-community.github.io/install/linux.html and I made my own branch with the changes

So far my definition looks like this :

image.png

You can see on online 1151 I replaced it with the new defn and it seems to work just fine. Should I replace all instances?

Let me know if it looks good to do a pull request, and then I can try and push it to mathlib (after I get access).

[Kevin Buzzard]

I guess you might want to look at the statements below where you are and see if there's any more finrank span stuff which you can rephrase in this new way. You t also make a little API for the definition, eg. prove that if s ⊆ t then hiv ≤ t.finrank (probably this is. called set.finrank

[Kevin Buzzard]

You should also edit the undergraduate.yaml file to add your definition to it. Once you feel you're ready, ask for push access to non-master branches of mathlib and post your GitHub userid

[ccn]

Kevin Buzzard said:

I guess you might want to look at the statements below where you are and see if there's any more finrank span stuff which you can rephrase in this new way. You should also make a little API for the definition, eg. prove that if s ⊆ t then s.finrank ≤ t.finrank (probably this is called set.finrank_mono)

Ok, I'll try to do it! What does mono stand for? And this would just be a lemma right?

[Yaël Dillies]

"monotone", aka "increasing"

[Yaël Dillies]

You can also spell it monotone finrank by using docs#monotone

[ccn]

So I'm starting to work on the proof that s.finrank K <= t.finrank K So far I
have this sketch

lemma set.finrank_mono (s t: set V) : s ⊆ t → s.finrank K ≤ t.finrank K :=
begin
  intro h,
  -- We can prove that span s is a subset of span t using span_mono
  have x := span_mono h,
  -- Now I need to somehow use that with finrank
  have y := finrank_mono x,
  exact y,
end

span_mono:

lemma span_mono (h : s ⊆ t) : span R s ≤ span R t :=
span_le.2 $ subset.trans h subset_span

finrank_mono

lemma finrank_mono [finite_dimensional K V] :
  monotone (λ (s : submodule K V), finrank K s) :=
λ s t hst,
calc finrank K s = finrank K (comap t.subtype s)
  : linear_equiv.finrank_eq (comap_subtype_equiv_of_le hst).symm
... ≤ finrank K t : submodule.finrank_le _

Thing is, that proof doesn't work too well:

image.png

Any tips to fix it?

[Yaël Dillies]

Golf it down to one line. Then Lean will be able to figure all the types out.

[Kevin Buzzard]

Right now Lean can't guess that V is a vector space over K in have x := span_mono h because h can make it guess s and t and V, but not K. That's why you get all the extra goals. As Yael says, if you write the proof in term mode (\lam h, finrank_mono (span_mono h), like span_mono) then it should work.

[Adam Topaz]

Also, this lemma is false, because finrank gives zero for infinite dim vector spaces. Are you assuming V is f.d. ahead of time?

[Yaël Dillies]

If span_mono was

lemma span_mono : monotone (span R) :=

you could even use span_mono.comp finrank_mono

[ccn]

Adam Topaz said:

Also, this lemma is false, because finrank gives zero for infinite dim vector spaces. Are you assuming V is f.d. ahead of time?

The file I'm working in is called finite_dimensional so I think it's good

[Adam Topaz]

The instances listed in your goal window don't show me anything about finite dimensionality

[ccn]

Yaël Dillies said:

Golf it down to one line. Then Lean will be able to figure all the types out.

I made it into one line, it is still doesn't work out: image.png

[Yaël Dillies]

Yup, because as Adam said you're missing the finite dimensionality assumption on the statement of your lemma.

[ccn]

Adam Topaz said:

The instances listed in your goal window don't show me anything about finite dimensionality

I'm pretty new to this too, but I think it was defined at the top of the file like this: image.png

[Yaël Dillies]

This is a definition, not a variable declaration

[Yaël Dillies]

You need variables [finite_dimensional K V]

[Adam Topaz]

Or add [finite_dimensional V] to the lemma itself

[Adam Topaz]

How are you making these nice screenshots with rectangles by the way?

[ccn]

https://github.com/flameshot-org/flameshot

[ccn]

Thanks to both of you it works out now!

[Adam Topaz]

Be careful if you're using variable ... to obtain this instance, because the assumption might not be necessary in the rest of the file.

[Adam Topaz]

If you work in a section, and put the variable inside, that should be okay

[Adam Topaz]

E.g. finrank_span_le_card doesn't need this assumption

[ccn]

I utilized the solution which adds it to the lemma itself, so I think it'll stay in the scope of the lemma.

Also I am now trying to add a "link" to it via the undergrad.yaml file:

image.png

Since my definition looks like this:

noncomputable def set.finrank (s: set V) : ℕ := finrank K (span K s)

would I have to write finite_dimensional.set.finrank ?

[ccn]

Ok, so I think most things are in order

my github account is this: https://github.com/cuppajoeman

could I have access to push to the repo?

[Kevin Buzzard]

@maintainers (BTW please let me know if pinging you all whenever someone I'm "mentoring" asks for push access is not something you guys want me to be doing)

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

(Pings are appreciated, on my part, at least.)

[Eric Wieser]

I was hoping there would be some way to grant Kevin special "add permissions for new users" power without going through a ping, but github doesn't seem to support it

[Henrik Böving]

We could write a zulip bots that checks whether kevin pinged maintainers and mentioned push access and a github user in the message :p

[ccn]

Looks like my pull request failed: image.png

[Kevin Buzzard]

What has failed is that you broke mathlib. If you changed a definition which was used elsewhere then I guess this would not be surprising, but if you didn't do this then that's bad luck. You can see which proof you broke. Can you fix it?

[ccn]

I found the cause of the error:

geometry/euclidean/monge_point.lean @ line 391

/-- An altitude is one-dimensional (i.e., a line). -/
@[simp] lemma finrank_direction_altitude {n : ℕ} (s : simplex ℝ P (n + 1)) (i : fin (n + 2)) :
  finrank ℝ ((s.altitude i).direction) = 1 :=
begin
  rw direction_altitude,
  have h := submodule.finrank_add_inf_finrank_orthogonal
    (vector_span_mono ℝ (set.image_subset_range s.points ↑(univ.erase i))),
  have hc : card (univ.erase i) = n + 1, { rw card_erase_of_mem (mem_univ _), simp },
  refine add_left_cancel (trans h _),
  rw [s.independent.finrank_vector_span (fintype.card_fin _),
      ← finset.coe_image, s.independent.finrank_vector_span_image_finset hc]
end

with error

rewrite tactic failed, did not find instance of the pattern in the target expression
  set.finrank ?m_1 ?m_6
state:
V : Type u_1,
P : Type u_2,
_inst_1 : inner_product_space ℝ V,
_inst_2 : metric_space P,
_inst_3 : normed_add_torsor V P,
n : ℕ,
s : simplex ℝ P (n + 1),
i : fin (n + 2),
p : P,
hne : p ≠ s.points i,
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ finrank ℝ ↥(submodule.span ℝ {p -ᵥ s.points i}) = 1

So what I think is happening is that instead of using the standard finrank that
operates on a module:

noncomputable def finrank (R V : Type*) [semiring R]
  [add_comm_group V] [module R V] : ℕ :=
(module.rank R V).to_nat

it's somehow using my new definition:

noncomputable def set.finrank (s: set V) : ℕ := finrank K (span K s)

Even though in that proof they didn't use the set.finrank syntax

[Kevin Buzzard]

If the original finrank is in the root namespace then you can try _root_.finrank and see if it fixes the problem.

[Floris van Doorn]

You can also do protected noncomputable def (or is it noncomputable protected def?) for set.finrank. This means that finrank without anything else never means set.finrank, even if you open namespace set (you'd have to write set.finrank or s.finrank when s : set _).

[ccn]

Trying out Floris's solution, I just ran leanproject build how long does that usually take?

[Kevin Buzzard]

4 hours.

[Kevin Buzzard]

Better to push and go to bed :-)

[ccn]

o | o

[ccn]

Ok, I'll do the push

[Kevin Buzzard]

You can subscribe to #CI and see how long it took

[Kevin Buzzard]

We hit 4 hours for the first time a couple of weeks ago

[ccn]

So I've just been fixing up some of the other lemmas that depended on finrank K (span K s) and there's one that isn't working 100%

finite_dimensional @ 1177:

lemma finrank_span_set_eq_card (s : set V) [fin : fintype s]
  (hs : linear_independent K (coe : s → V)) :
  s.finrank K = s.to_finset.card :=
begin
  haveI := span_of_finite K ⟨fin⟩,
  have : module.rank K (span K s) = #s := dim_span_set hs,
  rw [←finrank_eq_dim, cardinal.mk_fintype, ←set.to_finset_card] a t this,
  exact_mod_cast this
end

It seems like since I changed line 1179 to use s.finrank K that what it's trying to prove becomes a little different and causes the proof that they had to not solve it anymore:

Peek-2022-01-07-14-02.gif

I think I would need to modify this line in some way:

  have : module.rank K (span K s) = #s := dim_span_set hs,

[ccn]

I tried this out to try to fix it, but it didn't work: image.png

[Eric Wieser]

You might find you want to define s.rank K to match s.finrank K

[ccn]

Ah I see what you're hinting at

[ccn]

Would section rank be a good place to store this? Peek-2022-01-07-15-11.gif

[ccn]

My definition of s.finrank K was in section span of finite_dimensional.lean maybe, I should make a similar section in dimension.lean (that's where rank is stored) but there is no section about span there. What do you think

[Arthur Paulino]

Just an idea, I think it's easier for people to provide more precise feedback once you actually open the PR :+1:

[Eric Wieser]

It's already open I think?

[Eric Wieser]

I'm starting to think though that the right thing to do might be to not change any other lemmas at all, and add set.finrank solely for the purpose of the undergrad yaml

[Eric Wieser]

Because otherwise you can't apply lemmas like submodule.span_image to (e '' s).finrank, which you could apply to finrank (span R (e '' s))

[ccn]

Eric Wieser said:

It's already open I think?

It is already open: https://github.com/leanprover-community/mathlib/pull/11290

[Eric Wieser]

You can write #11290 in Zulip and it will link it for you :)

[ccn]

Oh neat

[ccn]

Eric Wieser said:

I'm starting to think though that the right thing to do might be to not change any other lemmas at all, and add set.finrank solely for the purpose of the undergrad yaml

Yeah, it looks like it might need some design work to make it fit in with all the other existing proofs, It should still be useful though right? For future proof writers?

[ccn]

For the rollback would you want me to remove it from all of the proofs or just the ones it isn't compatible with right now?

[Eric Wieser]

I'm suggesting remove it from everywhere, but I'd encourage getting more opinions first

[ccn]

I'm getting this issue: image.png

Here's the definition I have right now:

finite_dimensional.lean

/-- The rank of a set of vectors as a natural number. -/
protected noncomputable def set.finrank (s : set V) : ℕ := finrank K (span K s)

[Alex J. Best]

Is your declaration in the finite_dimensional namespace? If it isn't contained within the lines

namespace finite_dimensional
...
end finite_dimensional

it's name will just be set.finrank no matter which file it is in

[ccn]

Alex J. Best said:

Is your declaration in the finite_dimensional namespace? If it isn't contained within the lines

namespace finite_dimensional
...
end finite_dimensional

it's name will just be set.finrank no matter which file it is in

Ah you're correct it is outside of that scope, I've made the modifications so hopefully it will pass the CI tests now, thanks