Determinant for low rank

Stream: maths

[Alex Kontorovich]

Dear @Anne Baanen @Eric Wieser @Yakov Pechersky,

We've been using the determinant a bit (see #8377 and branch#modular3), and we keep getting time out errors from proving things like det ((ab),(cd))=ad-bc. We noticed that in PR #6897, there seemed to be a conscious choice not to include a lemma such as:

example {α : Type*} [comm_ring α] {a b c d : α} :
  matrix.det ![![a, b], ![c, d]] = a * d - b * c :=
begin
  simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
  ring
end

But when this is needed inside a longer lemma, it very often gives deterministic timeout errors. What would you think of making, say, this and the 3x3 formulae proper lemmas?

Best,
Alex and @Heather Macbeth

[Eric Wieser]

I think adding them as lemmas is probably harmless, but it would also be worthwhile to work out how to make the simp approach faster

[Mario Carneiro]

I'm not sure what you mean by a conscious choice to avoid them, but I think that the 2x2 and 3x3 versions should definitely be stated as lemmas, proved by simp if possible

[Mario Carneiro]

if nothing else, the lemmas are a lot more approachable for readers than some simp-based metaprogram using lots of weird looking lemmas

[Alex Kontorovich]

Ok great, so no objections to adding these to src/linear_algebra/determinant.lean...

[Yakov Pechersky]

Thanks to @Anne Baanen , simp is able to do this via the Laplace expansion.

[Yakov Pechersky]

Your example is taken from test/matrix.lean, correct?

[Yakov Pechersky]

Ah I see that you mentioned Anne =)

[Anne Baanen]

Eric Wieser said:

I think adding them as lemmas is probably harmless, but it would also be worthwhile to work out how to make the simp approach faster

This was exactly what I was going to write, except I'd add that "how to make the simp approach faster" will probably turn out to be to switch to Lean 4 :)

[Mario Carneiro]

isn't cofactor expansion O(n!)? Seems obvious that the natural simp lemmas here are not going to yield efficient results for large examples

[Mario Carneiro]

It's perfectly fine for proving the 2x2 and 3x3 cases though

[Yakov Pechersky]

Wouldn't having the 2x2 as a simp lemma make the 3x3 simp proof faster? If going through the minors

[Mario Carneiro]

I would expect so, and similarly the 3x3 can help the 4x4

[Kevin Buzzard]

@Deniz Aydin was talking on the Discord today about formalising Gaussian elimination (it's on the undergrad Todo list). Would this make things quicker?

[Mario Carneiro]

proving all of the intermediate lemmas up to NxN is a lot less than O(n!)

[Eric Wieser]

I think my original hesitancy in adding these was mainly not being bothered to choose what order to put the terms in on the RHS

[Mario Carneiro]

but I'm not sure about tossing all that into simp

[Mario Carneiro]

at a certain point you should probably just get a proper metaprogram

[Eric Rodriguez]

is the metaprogram really worth it before lean4 though?

[Mario Carneiro]

I don't know, depends on how much people need to take the determinant of large matrices

[Eric Rodriguez]

regardless I stronly support 2x2 and 3x3 lemmata, but the rest not; 4x4 matrices are when I start loading up mathematica or numpy

[Mario Carneiro]

I don't think lean 3 / 4 matters much here, it's just as much work either way

[Eric Rodriguez]

I'm not sure how different things will be in Lean4; tactics will have to be compiled, right? so we'll want the metaprogram there to use the minimal possible number of lemmas

[Eric Rodriguez]

whilst in lean3 doesn't matter as much

[Anne Baanen]

Let's add 2x2 and 3x3 shortcut lemmas now, and whoever needs to deal with the 4x4 case gets to make their own PR for that case

[Eric Rodriguez]

(or do I not understand how tactic compilation will work)

[Mario Carneiro]

no it's the other way around - in lean 3 tactics are more expensive so you have to be more careful not to do unnecessary things

[Mario Carneiro]

lean 4 will make brute force a more viable strategy than it is currently, which will open up more CAS-like possibilities. For now having explicit lemmas is better

[Eric Rodriguez]

let me try and rephrase my misunderstanding; for some eval_det tactic, you'd need some lemma saying, e.g., a row switch matrix has det -1. however, this lemma would have to be available to the code writing eval_det before it can make it?

[Eric Rodriguez]

or is there some Expr hackyness that we use in that case instead?

[Mario Carneiro]

I'm not sure I understand. If the tactic is creating a proof then it needs that lemma to be available because it will be referenced

[Eric Rodriguez]

yes, so then we'd need all of mathlib up to determinants to be precompiled for this metaprogram to work

[Eric Rodriguez]

or am I missing something

[Anne Baanen]

I believe that is correct, except obviously we'll be using some build system that ensures the user doesn't have to care about this separate compilation

[Mario Carneiro]

it doesn't need the lemma, strictly speaking, it can do all the work to create the proof without the lemma actually in the environment, but the proof won't check. But this is fine if the tactic is written in the prelude and is being applied in an environment that contains the lemma in question

[Anne Baanen]

("obviously we'll be" is defined as "this is a hard requirement for me personally, at least")

[Alex Kontorovich]

Ok, I added it to PR #8377.

[Mario Carneiro]

That is, matrix.det_succ_row_zero requires mathlib to typecheck, but `matrix.det_succ_row_zero doesn't

[Eric Rodriguez]

oh, so there's no issue then! I didn't know that at all

[Mario Carneiro]

It's usually error prone to write tactics that reference nonexisting things though, but there are a number of techniques to ensure that the references make sense and "activate" the tactic after the fact

[Mario Carneiro]

norm_num handles this by having "plugins" that exist in separate files from the main tactic