Contribute a project on Hadamard matrices

Stream: maths

[Alex Zhang]

I am going to PR the definition of Hadamard matrices (and basic results) in my project: https://github.com/l534zhan/my_project.
This is the definition currently used there.

class Hadamard_matrix (H : matrix I I ℚ) : Prop :=
(one_or_neg_one []: ∀ i j, (H i j) = 1 ∨ (H i j) = -1)
(orthogonal_rows []: H.has_orthogonal_rows)

Does anyone suggest changing the definition?

[Yaël Dillies]

I would advise putting that in #maths so that more people see it.

[Filippo A. E. Nuccio]

Why do you want to restrict the coefficients to $\mathbb{Q}$?

[Alex Zhang]

Because Q is easy to work with. I can use Z, but Z will make some following lemmas more complicated as coercions are then needed. Using R will make some lemmas noncomputalbe.

[Alex Zhang]

Should I use Z?

[Yaël Dillies]

Hmm... That sounds wrong.

[Yaël Dillies]

You shouldn't have to use concrete structures. Is there a PR I can look at?

[Alex Zhang]

I have done several closed PRs for this project. The next PR will be the definition.

[Filippo A. E. Nuccio]

Indeed, I would be interested in having a look as well (although @Yaël Dillies will certainly beat me :racecar: )

[Alex Zhang]

The closed PRs are not about Hadamard matrices though.

[Yaël Dillies]

Then please @ me when your PR is out!

[Alex Zhang]

What are the things you want to have a look at?

[Filippo A. E. Nuccio]

Well, in general it is strange that to define a matrix with $1$ and $-1$ you need to work over $\mathbb{Q}$; I would suggest working over a very general type with an instance of 1 and -1 and only restrict to rings/fields when needed.

[Yaël Dillies]

What are you using about ℚ? Its ring,field, linear_ordered_field structure?

[Alex Zhang]

The file contains the definition and the lemmas is main2.lean. Maybe you can have a look at that file.

[Yaël Dillies]

Oh yeah, if you really just need the presence of 1 and -1, you should simply assume has_one and has_neg.

[Alex Zhang]

That is indeed more general.

[Alex Zhang]

For lemmas about the determinants, I guess I need to use a ring or a field.

[Yaël Dillies]

Because 1 is by default assumed to be a natural, you'll probably need a lot of type annotations. But these are harmless and you shouldn't take that as a sign that not using ℚ will make you need casts.

[Filippo A. E. Nuccio]

A ring would probably be enough, although some things are already true over semi-rings. The good thing is that you can try to put basically no structure and let Lean complain whenever something is needed: it will say that it can't find the correct type instance (for example, if you set your coefficients to $\mathbb{N}$ it won't like your $-1$), and then you can improve things little by little.

[Eric Wieser]

Note also that instead of class Hadamard_matrix you likely want structure matrix.is_hadamard.

Using Hadamard_matrix as a typeclass is unlikely to be helpful to you here

[Yaël Dillies]

Filippo, that's all I'm doing :rofl: Don't sell my secrets like that!

[Filippo A. E. Nuccio]

OOOPS, sorry :angel: :lol:

[Alex Zhang]

So, we will be happier with the more general condition has_one has_neg in the definition?

[Alex Zhang]

Cool. I will generalise it!

[Eric Wieser]

docs#matrix.has_orthogonal_rows needs a semiring, right?

[Filippo A. E. Nuccio]

Eric Wieser said:

Note also that instead of class Hadamard_matrix you likely want structure matrix.is_hadamard.

Using Hadamard_matrix as a typeclass is unlikely to be helpful to you here

This is certainly a valid point, but may be you can speculate a bit more to help @Alex Zhang with the difference between the two approaches?

[Alex Zhang]

Eric Wieser said:

docs#matrix.has_orthogonal_rows needs a semiring, right?

Yeah. I think so.

[Eric Wieser]

I think perhaps it would be best for Alex to PR what they have right now, so that we can point out where our suggestions make things easier

[Eric Wieser]

Alex Zhang said:

Eric Wieser said:

docs#matrix.has_orthogonal_rows needs a semiring, right?

Yeah. I think so.

Actually it just needs [has_mul α] [add_comm_monoid α].

In principle you could use [has_mul α] [add_comm_monoid α] [has_neg α] [has_one α], but I think that's probably ridiculous and you should just assume ring α.

[Yaël Dillies]

If you do that, please put a TODO next to the variables, in case we later change the hierarchy and a more appropriate typeclass appears.

[Alex Zhang]

Yeah. [has_mul α] [add_comm_monoid α] [has_neg α] [has_one α] is the condition, which usually yields at least a semiring a think.

[Alex Zhang]

I will relax the conditions the make things more general in the PR (no need to keep Q).

[Johan Commelin]

The has_neg suggests that you even want a ring

[Alex Zhang]

right right

[Eric Wieser]

At best I could see you wanting to relax to a non_assoc_ring in future (if that ever existed)

[Alex Zhang]

That is exactly the thing I was thinking about

[Alex Zhang]

Eric Wieser said:

I think perhaps it would be best for Alex to PR what they have right now, so that we can point out where our suggestions make things easier

Should I keep it as a class or change it to a structure. I don't fully know the effects of doing this.

[Eric Wieser]

Leave it as class for the initial PR and I'll add a comment to show you where things get simpler if its a structure

[Yaël Dillies]

A class is a structure that typeclass inference can use.

[Eric Wieser]

But you may as well rename it to is_hadamard now

[Alex Zhang]

Yaël Dillies said:

A class is a structure that typeclass inference can use.

Not just that I think. If so, there is no need to remove the tag.

[Yaël Dillies]

Well, Eric is not only proposing to change from class to structure. That's my point.

[Alex Zhang]

OK, nice. I will do this PR after having my dinner. (I have been caught up with something else.)

[Alex Zhang]

Thanks a lot for your suggestions!

[Filippo A. E. Nuccio]

Alex Zhang said:

Yaël Dillies said:

A class is a structure that typeclass inference can use.

Not just that I think. If so, there is no need to remove the tag.

Well, one question you might ask yourself is: would you plan to start a lemma about Hadamard matrices writing

lemma foo (M : hadamard_matrix n n R) : bla :=

or

lemma foo (M : matrix n n R) [hadamard_matrix M] : bla :=

You will go for structure in the former case and for class in the latter.

[Yaël Dillies]

Yes exactly. To emphasize, this is the difference being bundling and not bundling a Hadamard matrix.

[Yaël Dillies]

in the first case, this info is part of the object. In the second case, it is a distinct proof.

[Yaël Dillies]

No way is better than the other in general, but in that particular case I think it makes sense to leave it unbundled.

[Filippo A. E. Nuccio]

At any rate, from my own experience, this is quite puzzling at the beginning. The best way (for me) was to develop a feeling using mathlib rather than dwelling in precise definitions -- but that's just a personal point.

[Filippo A. E. Nuccio]

@Alex Zhang I can certainly recommend the reading of the beautiful paper https://dl.acm.org/doi/10.1145/3372885.3373824 by the whole mathlib community, if you haven't read that already: it is very useful about this structure vs class debate.

[Alex Zhang]

I personally prefer the second one. I would like to just make is_hadamard a "bundled proposition" rather than a bundled structure containing the carrier.

[Eric Wieser]

Filippo A. E. Nuccio said:

Alex Zhang said:
e question you might ask yourself is: would you plan to start a lemma about Hadamard matrices writing

lemma foo (M : hadamard_matrix n n R) : bla :=

or

lemma foo (M : matrix n n R) [hadamard_matrix M] : bla :=

You will go for structure in the former case and for class in the latter.

This is not the remark I was making

[Eric Wieser]

I think is_hadarmard should remain unbundled like docs#matrix.is_diag, unless we come up with a convincing use case

[Eric Wieser]

And since is_diag isn't a typeclass, is_hadamard probably shouldn't be either

[Filippo A. E. Nuccio]

You mean that it will probably never happen that Lean will need to infer that a certain matrix is a Hadamard one?

[Anne Baanen]

I agree with Eric, it should be an unbundled structure, not class.

The rule of thumb I use for typeclasses is that they are typeclasses: they basically only work well when their parameters are types. (My intuition suggests this is basically because the logic used to find instances only contains ∧ and →, not =, so once you get (non-definitional) equalities, you enter a world of suffering.)

[Anne Baanen]

For example, if you have somethingl ike is_hadamard (diagonal (a * b)) then you can't actually rewrite a * b to b * a because the typeclass system can't guess that is_hadamard (diagonal (a * b)) also works for is_hadamard (diagonal (b * a)).

[Anne Baanen]

If you need an equality between two Types, then you are already screwed for other reasons, so typeclasses don't create extra pain :P

[Notification Bot]

This topic was moved here from #new members > Contribute a project on Hadamard matrices by Scott Morrison

[Scott Morrison]

An alternative take on Anne's rule of thumb is that if you're using typeclass search as a prover, then you're probably doing it wrong. You don't want to be telling typeclass search "please go prove this matrix is a Hadamard matrix".

[David Wärn]

This looks very cool, great work!

I think it's fine to define the property "H is a Hadamard matrix" for H a matrix over any ring, but when you actually develop the theory there's no reason to consider general rings. You get exactly the same Hadamard matrices over any ring of characteristic zero. Also, why can't you work directly with $\Z$? Do you need division somewhere?

I think you should also consider bundling the matrix and the proof, and work with the bundled version when doing things like the Sylvester construction. It should lead to more concise code and you can write some coercions to e.g. view a bundled Hadamard matrix as a function. Fundamentally, a Hadamard matrix is a combinatorial gadget. It's great that you can represent a Hadamard matrix as, well, a matrix, because it lets you do algebraic manipulations. But morally this is just a representation. Bundling is more in line with this view.

Some more practical advice: you can use docs#fin_prod_fin_equiv to define fin_Kronecker. You might also like to define something like exists_Hadamard_of_order (n : ℕ) : nonempty (Hadamard_matrix (fin n)). Then you can write Hadamard's conjecture as def Hadamard_conjecture : Prop := ∀ k, exists_Hadamard_of_order (4 * k). And your results can be neatly summarized as saying something about exists_Hadamard_of_order n for different n, which helps the reader understand exactly what has been proved.

[Eric Wieser]

Do you need division somewhere?

You need division to state results about the inverse of a hadamard matrix, although perhaps those aren't that interesting.

[David Wärn]

Ok, that makes sense. I think the inverse itself isn't very interesting, but you want some way to go from $AB = nI$ to $BA = nI$ when $n$ isn't a zero-divisor. There's an argument for this that works in a general comm_ring (using docs#matrix.mul_adjugate), but maybe it's more comfortable to work in $\mathbb Q$.

[Yaël Dillies]

I'm afraid you're rowing in the wrong direction, David. In an ideal world, we would never refer to concrete structures but merely to their properties (possibly even when these properties identify the concrete structure up to isomorphism, like being an canonically ordered bottom commutative monoid with successors for ℕ). I personally changed a few results about ℚ that were in mathlib to apply to any field, because coercing was a pain.

[Yaël Dillies]

Explicit your assumptions by instances instead of using concrete structures. If your proof requires more structure than the optimal proof, fine, because this will be noticeable by the instances.

[Yaël Dillies]

The current pain is ℝ. It has many properties that we didn't bother yet to reflect in the typeclass system, like being a complete_linear_ordered_field (I guess?), for example.

[Yaël Dillies]

And I mean, the entire convexity refactor I'm undertaking now is precisely to eradicate concrete structures from analysis.convex.*

[Yaël Dillies]

Even when the structure is unique up to isomorphism, it's nice to abstract it away. For example, we don't have Jensen's inequality for concave functions even though it's just the dual of the convex one because ℝ is hardcoded in it, so we can't replace with it order_dual ℝ.

[David Wärn]

I'm all in favour of generalisation and abstraction. It's great that you generalise convexity for example, since it makes sense to talk about it over different fields. But this situation is more like docs#nat.choose. Should nat.choose take values in an arbitrary semiring instead of $\N$? Certainly the definition makes sense, and you can still prove properties about it. But once you have the nat-version you can map it to any semiring, so what is really the benefit?

[Yaël Dillies]

Well, the reason here is that you know n.choose k is a natural, and this definition reflects that without needing further arguments. But reducing the number of arguments as such comes at the cost of having to work with nat.cast all over the place as soon as you leave ℕ. In that particular case, I think it's a fine cost to pay. For Hadamard matrices, I'm very circonspect.

[Reid Barton]

If anything, it makes a lot more sense to consider n.choose k mod 2 than to consider a Hadamard matrix over $\mathbb{Z}/2\mathbb{Z}$

[Alex Zhang]

I left away for travelling, and I am back now and can continue the PRs!