[Merged by Bors] - feat(data/matrix/hadamard): add the Hadamard product

[l534zhan]

---

[l534zhan]

This is a PR as a part of a large project mentioned in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Contribute.20a.20project.

[l534zhan]

I got the reported error:
/- The decidable_classical linter reports: -/
/- USES OF decidable SHOULD BE REPLACED WITH classical IN THE PROOF. -/
-- data/matrix/hadamard.lean
#print matrix.sum_Hadamard_eq /- The following decidable hypotheses should be replaced with
classical in the proof. argument 12: [_inst_12 : decidable_eq I], argument 13: [_inst_13 : decidable_eq J] -/

Why should I do this change?

[ericrbg]

get rid of those parameters and start the proof with classical or something like that

[l534zhan]

get rid of those parameters and start the proof with classical or something like that

I just don't understand, why I have to do this?

Do you have any idea? @ericrbg @eric-wieser

[ericrbg]

it's unneeded, basically. the decidable_eq in that lemma is just used in an intermediate step (have h:= trace_identity A B (λ i, 1 : I → α) (λ i, 1 : J → α)) and not in the type of the lemma, so why require that parameter when it's irrelevant?

[ericrbg]

i'm sort of finding it hard to say exactly what I mean, but the main essential difference is that trace_identity needs decidable_eq for diagonal, but sum_Hadamard_eq only uses diagonal in the middle and gets out of it fast anyways.

[l534zhan]

i'm sort of finding it hard to say exactly what I mean, but the main essential difference is that trace_identity needs decidable_eq for diagonal, but sum_Hadamard_eq only uses diagonal in the middle and gets out of it fast anyways.

So that still means [decidable_eq I] [decidable_eq J] are necessary conditions for all the lemmas there. Why does linter complain? Should I only use [decidable_eq I] [decidable_eq J] as conditions when the formulation needs this and use classical for the others?
@ericrbg

[ericrbg]

so mathlib as a library overall accepts Choice (⇒ LEM). therefore, in some ways, decidable_eq is kind of meaningless as we can always create some decidable equality (using choice). However, if we just blindly do this, we end up with many issues; there's a lot of decidable_eq instances floating around, and although they're all obviously propositionally equal, they're not defeq. this leads to weird rewriting errors that look something like this:

rewrite tactic failed, did not find instance of the pattern in the target expression
  α
state:
...
...
...
⊢ α = β

because in the first α has an implicit classical.decidable_eq whilst the second has an implicit my_fancy_instance.decidable_eq or whatever. these are always a pain to flag down, and so we give some leeway; whenever, in the output type, there's a decidable_eq argument hidden in somewhere, we pass decidable_eq arguments to the lemma itself so you don't have to deal with these issues. (this happens often with fintype too).

now, in your proof, you don't actually write down diagonal in the output type, so there's no such issues; you use it internally; this means that there's no issues with these "diamonds" for the rest. furthermore, even if you were trying to avoid choice, you also already use classical.choice anyways (try #print axioms ...) so you're not avoiding anything at all.

[l534zhan]

Any further improvement or suggestions? @eric-wieser
Thanks for all your suggestions, which enable me to write better codework in the future!

[eric-wieser]

LGTM, but I think @Vierkantor should take a quick look at the trace statements to check we're not missing a simpler result.

[Vierkantor]

I believe dot_product_vec_mul_hadamard is AFAIK the standard formulation of that statement, and the complexity of the proof is not so bad. So I don't really know a simpler result.

[Vierkantor]

Thanks 🎉

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[l534zhan]

What's the problem here? @Vierkantor

[bors]

Build failed (retrying...):

• Build mathlib

[bryangingechen]

What's the problem here? @Vierkantor

There aren't any problems here as far as I can tell. We merge our PRs in batches using bors, so a build failure could be due to any of the PRs in a batch or an interaction between any subset of them. Generally, if the bot posts a message that says "retrying...", you can just keep waiting; oftentimes the issue is elsewhere and your PR will get merged in a later batch. If it posts a "Build failed" message without "retrying" though, then that means the problem is with your PR and you should click the link to see what exactly failed.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests