struggling with proving span of linear combinations

Stream: new members

[David Chanin]

I'm trying to prove that if {v1, v2, v3, v4} spans V, then {v1 - v2, v2 - v3, v3 - v4, v4} also spans V. On pen and paper, this is easy to prove because you can form {v1, v2, v3, v4} from a simple linear combination of {v1 - v2, v2 - v3, v3 - v4, v4} and vice-versa. I see there's a theorem submodule.span_eq_span which seems like it should be able to prove this if I can prove that each set of vectors is in the span of the other set of vectors. I can't figure out how to express the idea of a linear combination in Lean, or even where to look to figure out how to express this, or what a theorem that deals with this would be called, or really where to begin. I know this is probably really trivial, but any help is greatly appreciated!

[Eric Wieser]

(docs#submodule.span_eq_span for reference)

[David Chanin]

So far I just have the following in Lean:

import tactic
open submodule


example
  (k : Type)
  (V : Type)
  [field k] [add_comm_group V] [module k V]
  (v1 v2 v3 v4: V)
  (b1 : set V)
  (b2 : set V)
  (hb1: b1 = {v1, v2, v3, v4})
  (hb2: b2 = {v1 - v2, v2 - v3, v3 - v4, v4})
:
  span k b1 = span k b2
:= begin
  sorry
end

[Eric Wieser]

I would guess that docs#submodule.span_insert is useful here

[David Chanin]

That's saying that the span of adding a vector to a set of vectors is equal to the span of the vector union the span of the set of vectors?

[David Chanin]

I'm trying to go through a linear algebra textbook to see if I can do some of the proofs in the book in Lean, and the book has the following definition of span, which I assume must be in mathlib somewhere if I were less incompetent at understanding how this stuff works :sweat_smile: Screen-Shot-2022-07-22-at-21.39.41.png

[David Chanin]

I think if I could find something like this it would be trivial to do this proof

[Alex J. Best]

I feel like @Vasily Ilin asked a very similar question a couple of months ago, which book are you looking at?

[Junyan Xu]

A full proof:

import tactic
open submodule

lemma span_insert_sub {R M} [ring R] [add_comm_group M] [module R M] (s : set M)
  (v w : M) (hw : w ∈ s) : span R (insert v s) = span R (insert (v - w) s) :=
begin
  rw span_eq_span,
  { rintro _ (rfl|h),
    { rw [span_insert, set_like.mem_coe, mem_sup],
      exact ⟨x - w, subset_span rfl, w, subset_span hw, sub_add_cancel x w⟩ },
    { exact subset_span (or.inr h) } },
  { rintro _ (rfl|h),
    { rw [span_insert, set_like.mem_coe, mem_sup],
      refine ⟨v, subset_span rfl, -w, neg_mem (subset_span hw), (sub_eq_add_neg _ _).symm⟩ },
    { exact subset_span (or.inr h) } },
end

example
  (k : Type)
  (V : Type)
  [ring k] [add_comm_group V] [module k V]
  (v1 v2 v3 v4 : V) :
  span k {v1, v2, v3, v4} = span k ({v1 - v2, v2 - v3, v3 - v4, v4} : set V) :=
begin
  rw span_insert_sub _ v1 v2, swap, exact or.inl rfl,
  conv_lhs { rw span_insert }, conv_rhs { rw span_insert }, congr' 1,
  rw span_insert_sub _ v2 v3, swap, exact or.inl rfl,
  conv_lhs { rw span_insert }, conv_rhs { rw span_insert }, congr' 1,
  rw span_insert_sub _ v3 v4, swap, exact rfl,
end

[Eric Wieser]

That looks like it hits the lemmas I had in mind and is probably shorter than what I would have come up with; but it still feels very clumsy

[David Chanin]

I'm going through Linear Algebra Done Right. I see his solutions here as well, which is super helpful too! https://github.com/Vilin97/linear-algebra-done-right/blob/master/src/chapter2.lean. It looks like he broke down everything into constituent base definitions and tried to prove things from there, but only did a 2-d version due to how complex that is. But I feel like there must be a way to use the theorems in Mathlib to prove this without

[Eric Wieser]

Does docs#finsupp.mem_span_iff_total help at all?

[Eric Wieser]

Yes, I think ext x, simp_rw [finsupp.mem_span_iff_total] gets it in an almost familiar form

[Eric Wieser]

Or maybe using that lemma after apply span_eq_span; intros x hx

[David Chanin]

Junyan Xu said:

A full proof:

import tactic
open submodule

lemma span_insert_sub {R M} [ring R] [add_comm_group M] [module R M] (s : set M)
  (v w : M) (hw : w ∈ s) : span R (insert v s) = span R (insert (v - w) s) :=
begin
  rw span_eq_span,
  { rintro _ (rfl|h),
    { rw [span_insert, set_like.mem_coe, mem_sup],
      exact ⟨x - w, subset_span rfl, w, subset_span hw, sub_add_cancel x w⟩ },
    { exact subset_span (or.inr h) } },
  { rintro _ (rfl|h),
    { rw [span_insert, set_like.mem_coe, mem_sup],
      refine ⟨v, subset_span rfl, -w, neg_mem (subset_span hw), (sub_eq_add_neg _ _).symm⟩ },
    { exact subset_span (or.inr h) } },
end

example
  (k : Type)
  (V : Type)
  [ring k] [add_comm_group V] [module k V]
  (v1 v2 v3 v4 : V) :
  span k {v1, v2, v3, v4} = span k ({v1 - v2, v2 - v3, v3 - v4, v4} : set V) :=
begin
  rw span_insert_sub _ v1 v2, swap, exact or.inl rfl,
  conv_lhs { rw span_insert }, conv_rhs { rw span_insert }, congr' 1,
  rw span_insert_sub _ v2 v3, swap, exact or.inl rfl,
  conv_lhs { rw span_insert }, conv_rhs { rw span_insert }, congr' 1,
  rw span_insert_sub _ v3 v4, swap, exact rfl,
end

Wow this is amazing, thank you for writing this out @Junyan Xu ! This will take me a bit to study to understand fully

[Junyan Xu]

There's a certain amount of defeq (ab)use, but it's mainly that docs#set.has_insert is a disjunction, and {v1, v2, v3, v4} := insert v1 {v2, v3, v4}, and A ⊆ B is definitionally ∀ {x}, x ∈ A → x ∈ B in docs#submodule.subset_span.

[David Chanin]

Eric Wieser said:

Does docs#finsupp.mem_span_iff_total help at all?

This looks like it might be close to what's in the book. So this is saying something about linear combinations spanning things it looks like? There's a bunch of terms in here I'm not familiar with, but I'll see if I can find examples of how to use this theorem on Github projects

[Eric Wieser]

I can make some progress with that approach, but I don't know offhand how to clean up the goals:

example
  (k : Type)
  (V : Type)
  [ring k] [add_comm_group V] [module k V]
  (v1 v2 v3 v4 : V) :
  span k {v1, v2, v3, v4} = span k ({v1 - v2, v2 - v3, v3 - v4, v4} : set V) :=
begin
  apply span_eq_span _ _; intros x hx;
    simp_rw [set_like.mem_coe, finsupp.mem_span_iff_total,
      finsupp.total_apply, finsupp.sum];
    change _ ∨ _ ∨ _ ∨ _ = _ at hx;
    rcases hx with rfl|rfl|rfl|rfl,
  sorry,
end

[Eric Wieser]

This gives you 8 goals, one for each vector in each direction

[Eric Wieser]

I was hoping something like

  let U := ![v1, v2, v3, v4],
  let U' := ![v1 - v2, v2 - v3, v3 - v4, v4],
  let M : (fin 4 → V) ≃ₗ[k] (fin 4 → V) :=
  { to_fun := λ v, ![v 0 - v 1, v 1 - v 2, v 2 - v 3, v 3],
    inv_fun := λ v, ![v 0 + v 1 + v 2 + v 3, v 1 + v 2 + v 3, v 2 + v 3, v 3],
    map_add' := λ v₁ v₂, funext $ λ i, by fin_cases i; simp [pi.add_apply, add_sub_add_comm],
    map_smul' := λ v₁ v₂, funext $ λ i, by fin_cases i; simp [pi.smul_apply, smul_sub],
    left_inv := λ v, funext $ λ i, by fin_cases i; simp,
    right_inv := λ v, funext $ λ i, by fin_cases i; simp },
  have hU : {v1, v2, v3, v4} = set.range U,
  { ext i, simp [set.mem_range]; tauto },
  have hU' : {v1 - v2, v2 - v3, v3 - v4, v4} = set.range U',
  { ext i, simp [set.mem_range]; tauto },
  have hUU' : M U = U' := rfl,

would lead to a clear solution, but either some machinery is missing or I need to sleep

[Vasily Ilin]

Can you post a link to your repo so far if you do use GitHub? I would be curious to compare

[David Chanin]

This has depressingly been the first problem I've tried, thinking it should be really easy, and had to ask for help on here immediately :sweat_smile:. I'll see if I can solve some other problems too, but given I couldn't even get this simple proof to work in Lean I'm not too hopeful I'll have any luck with any others. I did the natural number game, but proving anything beyond that in Lean might be too hard for me it seems

[Alex J. Best]

I think problems like this that are example like are generally harder than more abstract / less specific questions. In informal math we are pretty good at seeing what happens when only 4 objects are involved, and they are permuted or something like that intuitively. But actually spelling out the details results in a lot more work. So I'd say don't be discouraged by this problem, it could just be something that we need better tooling to match human intuition.

[David Chanin]

I mean, for all the lean experts on here you're able to figure this stuff out pretty easily, so that gives me confidence that it's at least possible. I guess I just hit walls and don't really have any idea how to proceed at a pretty immediate level. Even looking at the mathlib docs just makes my head spin. Maybe I need to go through more tutorials or something before this starts to make sense.

[Alex J. Best]

That's true to some extent of course, but I remember trying this problem last time it came up in the chat and finding it really annoying, and way longer in lean than in my head, which naturally means it takes a long time to find the right incantations if you don't know them

[Alex J. Best]

But yes the tutorials and other materials on the leanprover-community site are definitely a good idea I think

[David Chanin]

I tried proving a simpler version of this, just the simple v1 ∈ span k ({v1 - v2, v2 - v3, v3 - v4, v4}: set V), but even this I can't get to work :disappointed:. My idea is to use the matrix ![![1,1,1,1]], and turn it into a linear map with matrix.to_lin, so then I can apply finsupp.mem_span_iff_total with this linear map to show that the result is v1. However, I can't get the matrix.to_lin stuff to work. The code below gives the error invalid field notation, type is not of the form (C ...) where C is a constant

example
    (k : Type)
    (V : Type)
    [field k] [add_comm_group V] [module k V]
    (v1 v2 v3 v4: V)
  :
    v1 ∈ span k ({v1 - v2, v2 - v3, v3 - v4, v4}: set V)
  := begin
    let matrix_map := ![![1, 1, 1, 1]],
    let linear_map := matrix_map.to_lin,
  end

I tried changing to the following syntax to explicitly state what the matrix type is and it doesn't work either, giving the error invalid field notation, 'to_lin' is not a valid "field" because environment does not contain 'matrix.to_lin':

example
    (k : Type)
    (V : Type)
    [field k] [add_comm_group V] [module k V]
    (v1 v2 v3 v4: V)
  :
    v1 ∈ span k ({v1 - v2, v2 - v3, v3 - v4, v4}: set V)
  := begin
    let matrix_map : matrix (fin 1) (fin 4) k := ![![1, 1, 1, 1]],
    let linear_map := matrix_map.to_lin,
    rw finsupp.mem_span_iff_total,
  end

What am I overlooking?

[Eric Wieser]

That's essentially the approach I was trying to do above, but I couldn't work out how to use the fact that I had a map between the vectors

[Eric Wieser]

I'll second Alex's point that this is a surprisingly hard problem in lean; suggesting that we're missing either some lemmas, or documentation to create awareness of them

[Violeta Hernández]

Here's some general advice: it's sometimes easier to prove things in general than it is to prove specific cases

[Violeta Hernández]

So maybe we could prove that span {v1, v2, ..., vn} = span {v1 - v2, v2 - v3, ..., v(n-1) - vn, vn} for all n? Seems like induction might help.

[Violeta Hernández]

The Lean spelling of this result probably involves finsets and finset.image.

[Violeta Hernández]

Or maybe even lists

[Violeta Hernández]

Do we have any API for turning [a, b, c] into [op a b, op b c] and such?

[Junyan Xu]

My proof is sort of proof by induction; it uses the same lemma three times.

But it seems what people want is a proof by providing explicit coefficients + calculation. Maybe this proof will satisfy them?

example
  (k : Type)
  (V : Type)
  [field k] [add_comm_group V] [module k V]
  (v1 v2 v3 v4: V) :
  v1 ∈ span k ({v1 - v2, v2 - v3, v3 - v4, v4} : set V) :=
begin
  simp only [mem_span_insert, mem_sup],
  use [1, v2, 1, v3, 1, v4, subset_span rfl]; simp,
end

[Junyan Xu]

I think the following approach is maybe close to what people had in mind:

import tactic
import data.fin.vec_notation
import algebra.big_operators.fin
open submodule

lemma mem_span_iff_eq_sum_smul {M} (R)
  [semiring R] [add_comm_monoid M] [module R M] (s : set M) (x : M) :
  x ∈ submodule.span R s ↔
  ∃ n (r : fin n → R) (m : fin n → M), (∀ i, m i ∈ s) ∧ finset.univ.sum (λ i, r i • m i) = x :=
sorry

example
  (k : Type)
  (V : Type)
  [field k] [add_comm_group V] [module k V]
  (v1 v2 v3 v4 : V) :
  v1 ∈ span k ({v1 - v2, v2 - v3, v3 - v4, v4} : set V) :=
begin
  rw mem_span_iff_eq_sum_smul,
  use [4, ![1,1,1,1], ![v1-v2,v2-v3,v3-v4,v4]],
  split,
  { intro i, fin_cases i; simp },
  { simp [fin.sum_univ_succ] },
end

The lemma might follow relatively easily from docs#finsupp.mem_span_image_iff_total and docs#finsupp.equiv_fun_on_fintype. docs#finsupp.mem_span_iff_total isn't very applicable because {v1 - v2, v2 - v3, v3 - v4, v4} isn't necessarily pairwise distinct.

[David Chanin]

Junyan Xu said:

My proof is sort of proof by induction; it uses the same lemma three times.

But it seems what people want is a proof by providing explicit coefficients + calculation. Maybe this proof will satisfy them?

example
  (k : Type)
  (V : Type)
  [field k] [add_comm_group V] [module k V]
  (v1 v2 v3 v4: V) :
  v1 ∈ span k ({v1 - v2, v2 - v3, v3 - v4, v4} : set V) :=
begin
  simp only [mem_span_insert, mem_sup],
  use [1, v2, 1, v3, 1, v4, subset_span rfl]; simp,
end

This is brilliant! I was able to understand this even with my poor understanding of math and lean, and was able to write a version in dumbed-down syntax too:

example
    (k : Type)
    (V : Type)
    [field k] [add_comm_group V] [module k V]
    (v1 v2 v3 v4: V) :
    v1 ∈ span k ({v1 - v2, v2 - v3, v3 - v4, v4} : set V) :=
  begin
    rw mem_span_insert,
    use [1, v2],
    simp,
    rw mem_span_insert,
    use [1, v3],
    simp,
    rw mem_span_insert,
    use [1, v4],
    simp,
    exact mem_span_singleton_self v4,
  end

This makes me feel like it's maybe possible for me to use Lean to prove things in beginner textbooks. Although there's still no way I would have come up with this on my own

[Vasily Ilin]

This is a great discussion! I felt and still feel the same way as you, David! Lean is hard, often in unexpected ways

[Kevin Buzzard]

We have all gone through this. First there's the "I know exactly what to do in math but have no idea how to do it in Lean" phase, then there's the "I know exactly what to do in math and I can do it in Lean but it takes 20 lines to do a trivial thing" phase, and then there's the "I know exactly what to do in math and I just explain it to Lean and most of the time it understands me" phase. In my experience one way of moving through the phases is to keep formalising mathematics you understand and then ask here if you're stuck or if you know that your code is far too long. Beyond some point, when there's stuff that you still can't do easily, it might turn out that this is an interesting question, maybe an interesting area of research, because you might be trying to do something which the theorem prover community still hasn't manage to make smooth yet.

[Vasily Ilin]

A similar question: how can I prove this?

import tactic
import linear_algebra.basis

open_locale big_operators

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (n : ℕ) (w : V) (v : fin n → V) (coeff : fin n → k) (w = ∑ i : fin n, (coeff i • v i)) : w ∈ submodule.span k (set.range v) :=
begin
  sorry,
end

[Eric Wieser]

rw H, then docs#sum_mem, then docs#submodule.subset_span

[Junyan Xu]

import tactic
import linear_algebra.basis

open_locale big_operators

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (n : ℕ) (w : V) (v : fin n → V) (coeff : fin n → k) (w = ∑ i : fin n, coeff i • v i) :
  w ∈ submodule.span k (set.range v) :=
begin
  rw H,
  refine submodule.sum_mem _ _,
  rintro i -,
  refine submodule.smul_mem _ _ _,
  apply submodule.subset_span,
  exact set.mem_range_self i,
end

[Alex J. Best]

Its an iff too

import tactic
import linear_algebra.basis

open_locale big_operators

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]


example (n : ℕ) (w : V) (v : fin n → V) : (∃ coeff : fin n → k, w = ∑ i : fin n, (coeff i • v i)) ↔
  w ∈ submodule.span k (set.range v) :=
begin
  rw [← set.image_univ, finsupp.mem_span_image_iff_total],
  simp only [finsupp.supported_univ, submodule.mem_top, exists_true_left],
  symmetry,
  convert finsupp.equiv_fun_on_fintype.exists_congr_left,
  ext v,
  rw [finsupp.total_apply, finsupp.sum_fintype],
  simp only [finsupp.equiv_fun_on_fintype_symm_apply_to_fun, eq_comm],
  simp only [zero_smul, eq_self_iff_true, implies_true_iff],
  apply_instance,
end

[Kevin Buzzard]

I needed a version of this for the span of a set yesterday. Do we have it? Anything of the form "you're in the submodule.span of a set/indexed family iff you're a finite linear combination of the elements" would be lovely.

[Alex J. Best]

docs#finsupp.mem_span_iff_total is hopefully the right thing