Formalizing basic linear algebra

Stream: new members

[Mitchell Douglass]

Thanks all for your answers.

How do you perform induction on a term which is not part of the context? I am trying to prove this lemma, which says "finite sums of vectors can be done coordinate-by-coodinate" . I'm trying to employ induction on the size of the fintype α. This is my best try so far:

import data.real.basic data.real.sqrt data.nat.basic data.fin.basic

open_locale big_operators

def R (n: ℕ) : Type := fin n -> ℝ

-- I've show (add_comm_monoid (R n))

lemma vec_sum_by_coordinate {α: Type} [fintype α] (f: α -> R n) :
(∑ a, f a) i = ∑ a, f a i :=
begin
  let n := sizeof α,
  induction n,
end

I used let n := sizeof α when induction (sizeof α) failed to work on its own. But now I don't know how to work with the resulting target term:

(let s : ℕ := sizeof α in (∑ (a : α), f a) i = ∑ (a : α), f a i) 0

What's the standard way forward here? Btw, I am trying to prove this first without finset.sum_induction, just as an exercise.

[Kevin Buzzard]

You should use finset.sum_induction and then specialise to finset.univ to get your result.

[Eric Wieser]

I'm pretty sure you want docs#fintype.card not docs#sizeof

[Eric Wieser]

induction h : fintype.card α might be what you're asking for

[Kevin Buzzard]

I'm not sure that encouraging the use of induction on the type is a good idea here. It's much easier to prove the more general statement about a finset because then you don't need to move the underlying type.

[Kyle Miller]

Just to give a mathlib example of how to do induction on the cardinality of a type (which is like what Eric brought up), there's this part of the proof of Hall's marriage theorem: https://github.com/leanprover-community/mathlib/blob/f1a2caaf51ef593799107fe9a8d5e411599f3996/src/combinatorics/hall/finite.lean#L229

There's a Lean technicality where you have to use unfreezingI since the fintype instance is "frozen".

[Eric Wieser]

Kevin Buzzard said:

I'm not sure that encouraging the use of induction on the type is a good idea here.

Indeed; but it does directly answer the "How do you perform induction on a term which is not part of the context?". It just happens that in this particular case that's not actually a helpful thing to do!

[Mitchell Douglass]

Hello all,

Thank you again for your helpful answers.

I am still stuck on proving the below lemma. @Kevin Buzzard thank you for your suggestion to use finset.sum_induction. Upon further study of that theorem, I am struggling to apply it to my case (though I do not doubt it may apply). Specifically, I am struggling to formulate a predicate p: R n -> Prop to use in my case. I believe I want to show a property of summing in R n.

Having temporarily hit a wall with the recommended approach, I have decided to continue playing with the ill-advised induction on fintype.card α, in hopes to learn why it breaks down. It did break down, but in an unexpected way. Here is my current state (using the induction pointed out by @Eric Wieser):

import data.real.basic data.fin.basic

open_locale big_operators

variables {n : ℕ}

def R (n: ℕ) : Type := fin n -> ℝ

variables {i : fin n}

-- In my file, I have shown
instance vec_add_comm_monoid: add_comm_monoid (R n) :=  sorry

-- the lemma in question
lemma vec_sum_pointwise {α: Type*} [fintype α] (f: α -> R n) :
(∑ a, f a) i = ∑ a, f a i :=
begin
  induction h: fintype.card α with n',
  {
    -- constructing this instance as I don't know how to help Lean find/infer it
    have α_is_empty : is_empty α := fintype.card_eq_zero_iff.mp h,
    -- error on this line
    rw @fintype.sum_empty α (R n) vec_add_comm_monoid α_is_empty f,
  },
end

Giving the following state/error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ∑ (x : α), f x
state:
n : ℕ,
i : fin n,
α : Type u_1,
_inst_1 : fintype α,
f : α → R n,
h : fintype.card α = 0,
α_is_empty : is_empty α
⊢ (∑ (a : α), f a) i = ∑ (a : α), f a i

I am quite stumped, as I expect Lean to find the pattern in the target as ∑ (a : α), f a. I believe this pattern is finset.univ.sum f. Does it perhaps have to do with Type universes?

Any help on either of these fronts would be greatly appreciated.

[Alistair Tucker]

I think what's being suggested here is to begin with something like

lemma vec_sum_pointwise {α: Type*} (A : finset α) (f : α → R n) :
  (∑ a in A, f a) i = ∑ a in A, f a i :=
begin
  induction A using finset.cons_induction with b A hb ih,
...

and only then proceed to

lemma vec_sum_pointwise' {α: Type*} [fintype α] (f : α → R n) :
  (∑ a, f a) i = ∑ a, f a i :=
vec_sum_pointwise finset.univ f

[Eric Wieser]

FWIW, this more general lemma exists already as docs#finset.sum_apply

[Mitchell Douglass]

Thanks to those who have helped me thus far.

This time I'm not stuck, I just want to know the most idiomatic way of doing something. I have the following lemmas

lemma dot_prod_right_distrib (α β : ℝ) (x y z : fin n -> ℝ) : ⟪(α • x + β • y), z⟫_ℝ = α * ⟪x, z⟫_ℝ + β * ⟪y, z⟫_ℝ := sorry
lemma vec_smul_one : (1 : ℝ) • x = x := sorry

Later on, I want to show that

⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + ⟪y, y⟫_ℝ + 2 * ⟪x, y⟫_ℝ

However, I find that I cannot rw or apply dot_prod_right_distrib directly. The problem is that the lemma does not know that α and β can be taken to be 1. Thus, my proof of the latter statements starts like:

example (x y : fin n -> ℝ) : ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + ⟪y, y⟫_ℝ + 2 * ⟪x, y⟫_ℝ  :=
begin
      -- insert "1 •" on every vector
      rw ← vec_smul_one x,
      rw ← vec_smul_one y,
      -- apply the lemma with α = β = 1
      rw dot_prod_distrib 1 1 x y ((1:ℝ) • x + (1:ℝ) • y),
      -- remove the "1 •"
      repeat { rw vec_smul_one },
end

My question is, is there a better way to do this? I suspect many theorems/lemmas will appear in these generalized forms. Can I tell LEAN how to guess α = β = 1 automatically? Alternatively, I could just write multiple versions of the same lemma, e.g.

lemma dot_prod_right_distrib (α β : ℝ) (x y z : fin n -> ℝ) : ⟪(α • x + β • y), z⟫_ℝ = α * ⟪x, z⟫_ℝ + β * ⟪y, z⟫_ℝ := sorry
lemma dot_prod_right_distrib' (α : ℝ) (x y z : fin n -> ℝ) : ⟪(α • x + y), z⟫_ℝ = α * ⟪x, z⟫_ℝ + ⟪y, z⟫_ℝ := sorry
lemma dot_prod_right_distrib'' (β : ℝ) (x y z : fin n -> ℝ) : ⟪(x + β • y), z⟫_ℝ = ⟪x, z⟫_ℝ + β * ⟪y, z⟫_ℝ := sorry
lemma dot_prod_right_distrib''' (x y z : fin n -> ℝ) : ⟪(x + y), z⟫_ℝ = ⟪x, z⟫_ℝ + ⟪y, z⟫_ℝ := sorry

but this seems rather tedious.

Thanks for the help!

[Kevin Buzzard]

1 bub x is neither syntactically nor definitely equal to x. The problem is not that lean isn't guessing alpha = 1, it's that even if you set alpha = 1 the lemma doesn't match. It might be what you see in the textbooks but the lemma isn't a good one for rewriting because it's doing too many jobs at once, and rw works up to syntactic equality. Why not prove additivity and linearity as two separate lemmas? (x+y,z) and (c \bub x,z), and also have lemmas for (x,y+z) etc.

[Kevin Buzzard]

You don't want the more complex lemmas, you should tell the simplifier about the basic lemmas and then it will prove the more complex ones by itself.

[Mitchell Douglass]

@Kevin Buzzard Thanks for the insight. I see what you mean about this lemma being overloaded. I'll prove the two lemmas separately and show the textbook's lemma as an example.

[Kevin Buzzard]

The proof of the textbook lemma should be simp

[Eric Wieser]

Isn't your vec_smul_one just docs#one_smul?

[Mitchell Douglass]

@Eric Wieser. Thanks for the pointer. I had not seen this theorem. I have since removed my vec_smul_one lemma as I don't need it.

What I'm trying to do is formalize a basic linalg book, replicating any definitions/theorems from the book, while using mathlib as much as possible to help with any definitions/theorems that the book assumes or uses without proof.

[Mitchell Douglass]

I had a followup question about the simplifier.

I am working on a theorem:

lemma vec_norm_sum :  ∥x + y∥ ^ 2 = ∥x∥ ^ 2 + ∥y∥ ^ 2 + 2 * ⟪x, y⟫_ℝ :=
begin
  simp,
  rw dot_prod_comm,
  rw dot_prod_comm y,
  simp,
  ring,

After the first simp, the tactic state becomes:

1 goal
n: ℕ
xy: R n
⊢ inner x (x + y) + inner y (x + y) = inner x x + inner y y + 2 * inner x y

However, I have a theorem dot_prod_comm marked with @[simp] with the following type:

-- #check dot_prod_comm
dot_prod_comm : ∀ (x y : R ?M_1), inner x y = inner y x

My question is, why doesn't the simplifier use this lemma to further simplify the state? As shown above, I can manually apply dot_prod_comm twice with another simp and ring to complete the proof.

[Yaël Dillies]

simp detects commutativity (such as your dot_prod_comm and only uses them if the rewrite results in smaller variable indices when taken lexicographically, or something along those lines. The details don't matter, but the point is that you don't want to rewrite a + b into b + a into a + b into... so simp has some secret preferred ordering of the variables, and in your case it just happens that the variables are in its preferred order.

[Yaël Dillies]

Here I would suggest adding dot_prod_comm x (or dot_prod_comm x, dot_prod_comm y) to your simp call because it suddenly isn't a commutativity lemma either (it won't rewrite back).

[Reid Barton]

In this case I think a better approach would be: you seem to have a simp lemma that says that inner is linear in the first argument, but not one for the second argument; you should add it.

[Reid Barton]

That's more sensible than relying on dot_prod_comm in this proof (which isn't "simplification" at all, it just happens to allow further simplification).

[Eric Wieser]

Are you aware of the lemmas docs#inner_add_right and docs#inner_add_left?