Linear algebra in MIL

Stream: general

[Patrick Massot]

I just published a new chapter in Mathematics in Lean: Linear algebra. As usual comments are very welcome, both from beginners and from more advanced users. And PRs fixing typos are very welcome (I have a new baby cat at home who loves keyboard walking).

[Eric Wieser]

Regarding "(this is somehow an implementation accident).", perhaps a comment about how this is satisfied automatically in the common case of indexing by Nat is worthwhile?

[Eric Wieser]

I think

example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
    ∃ s ∈ S, ∃ t ∈ T, x = s + t  := by
  rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
  apply Submodule.span_induction h (p := fun x ↦ ∃ s ∈ S, ∃ t ∈ T, x = s + t)
  sorry

would be better-written as

example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
    ∃ s ∈ S, ∃ t ∈ T, x = s + t  := by
  rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
  induction h using Submodule.span_induction'

or

example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
    ∃ s ∈ S, ∃ t ∈ T, x = s + t  := by
  rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
  induction h using Submodule.span_induction' with
  | mem x hx => sorry
  | add hx hy => sorry
  | zero => sorry
  | smul x hx ih => sorry

and the

As usual with such lemmas, Lean sometimes needs help to figure out the predicate we are interested in.

is really "as usual when using apply instead of induction with such lemmas"

[Eric Wieser]

but we still have that, for any two bases of the same vector space, there is a bijection between the types indexing those bases

Is it worth mentioning this result by (lean) name?

[Eric Wieser]

(But I should say generally this looks excellent, thanks!)

[Patrick Massot]

Thanks for your suggestions Eric! I am puzzled by the span induction thing. Of course I tried using the induction tactic. But this is not enough. You need to switch from docs#Submodule.span_induction to docs#Submodule.span_induction' as you did. And this makes no sense to me. Do you understand what happens?

[Patrick Massot]

In particular it is not really “as usual when using apply instead of induction with such lemmas”.

[Eric Wieser]

Patrick Massot said:

I am puzzled by the span induction thing. Of course I tried using the induction tactic. But this is not enough. You need to switch from docs#Submodule.span_induction to docs#Submodule.span_induction' as you did. And this makes no sense to me. Do you understand what happens?

Yes, the problem is that docs#Submodule.span_induction is not an induction principle as it does not index the result with the thing that you are inducting on. Arguably we should just replace all these unprimed principles with the primed ones

[Eric Wieser]

That is, it's crucial that the conclusion of the induction principle is p x hx and not p x, else you are not actually inducting on hx.

[Patrick Massot]

Ok, that makes sense. So the issue is indeed not with apply vs induction, it is with calling whatever_induction something that does not have the correct shape.

[Patrick Massot]

It would be nice to try to replace docs#Submodule.span_induction with docs#Submodule.span_induction' everywhere. But I really don’t have time for this now.

[Eric Wieser]

Once again, you're running into something I also didn't have time for; I got as far as adding a lot of the primed versions, but never made it to replacing the unprimed ones.

[Eric Wieser]

Patrick Massot said:

Ok, that makes sense. So the issue is indeed not with apply vs induction, it is with calling whatever_induction something that does not have the correct shape.

If you start with the one that has the right shape, I believe apply will still fail. apply pretty much always fails on anything tagged @[elab_as_elim], I think.

[Patrick Massot]

Sure. But there is no point saying apply is bad and induction should be used if induction fails just as much. That’s why I stuck to apply which is simpler.

[Yaël Dillies]

Sorry Patrick, I swear I didn't carefully plan to make your new chapter immediately outdated, but today is the day I finally had the energy to rename docs#FiniteDimensional.finrank (a long unclear name in a soon-to-be-obsolete namespace) to Module.finrank (a short snappy name close to its sibling docs#Module.rank). See #17192.

[Patrick Massot]

There is no problem at all, this is normal MIL maintenance.

[Eric Wieser]

Patrick Massot said:

Sure. But there is no point saying apply is bad and induction should be used if induction fails just as much. That’s why I stuck to apply which is simpler.

refine is the compromise between the two; I believe it can correctly guess the motive for either lemma, if provided enough ?_s

[Patrick Massot]

Indeed it can in this case.

[Patrick Massot]

But explaining this isn’t super appealing…

[Jireh Loreaux]

Maybe I can just entice @Pietro Monticone to replace the unprimed induction lemmas with the primed ones in Mathlib or MIL? :stuck_out_tongue_wink: He seems to have a penchant for this kind of thing.

[Patrick Massot]

Please don’t tempt Pietro, it’s already embarrassing how much work he does for us.

[Siddhartha Gadgil]

A quick related question: are algorithms like Gaussian elimination to calculate ranks, solve equations etc implemented? I did not see them mentioned here.

[Patrick Massot]

Not in Mathlib. There is always the same issue with such algorithms. Do you want them to be implemented in a way that makes them nice to prove properties about or do you want them to be actually usable? I think having both with the same code is (at least currently) impossible. So if you want both you need to implement both and then prove they compute the same thing. This is a lot of work.

[Patrick Massot]

That being said, I would already be happy to have a version that is provably correct but not efficient.

[Henrik Böving]

Patrick Massot said:

Not in Mathlib. There is always the same issue with such algorithms. Do you want them to be implemented in a way that makes them nice to prove properties about or do you want them to be actually usable? I think having both with the same code is (at least currently) impossible. So if you want both you need to implement both and then prove they compute the same thing. This is a lot of work.

Verifying high perf code in Lean is totally possible but it definitely requires someone rather capable with both programming and proving in Lean. For example bv_decide has an efficiently implemented graph data structure and a couple of caches based on our Std.HashMap etc. that are all verified and yet never show up for more than a couple dozen ms at worst in our profiles.

[Patrick Massot]

I should be more explicit. This is in the context of docs#Matrix which a type synonym for a function type. When you write !![1, 2; 3, 4] : Matrix (Fin 2) (Fin 2) ℕ, you could think you built something like a size 4 Array of natural number. But this is really in Fin 2 → Fin 2 → ℕ. Of course I am completely incompetent in numerical analysis and high performance programming. But my understanding is there is no way to do anything efficient with this data structure. So, I think the current status is you would need an efficient Array-based implementation and then some glue with docs#Matrix (and this is not even considering the important case of sparse matrices where Array is not the best choice).

[Patrick Massot]

And then my “(at least currently)” is a vague allusion to a future where Lean would automatically translate between the Fin n → Fin m → α implementation and an Array-based implementation without user input.

[Siddhartha Gadgil]

Thanks. I will target these as possible projects and/or examples in my course beginning in January. Not an array based implementation but hopefully correct and proved correct.

[Kim Morrison]

The problem is that it's not really clear what having a provably correct but unusably slow algorithm actually buys you. :-)

The thing that it might buy you is a cheap way to prove a fast algorithm correct: now you just need to compare the extensional behaviour of the fast algorithm with the slow algorithm, rather than directly checking the spec on the fast algorithm. However achieving this payoff nearly always requires designing the fast (for execution) and slow (for verification) algorithms in tandem.

[Patrick Massot]

Yes, this is what I tried to explain.

[Patrick Massot]

But we can still argue that coding the naive version and proving it correct is math formalization since it gives Lean the same explanation we give to students in math courses.

[Patrick Massot]

There are even linear algebra courses which try to use these algorithm to prove as many things as possible, replacing abstract arguments about abstract vector spaces.

[Siddhartha Gadgil]

I would guess that for modest sized matrices slow algorithms are fast enough in practice. So linear equations coming from human mathematics say may be solvable.