Contribute a project on Hadamard matrices

Stream: new members

[Alex Zhang]

I would appreciate it if we can use this thread only for discussing the project here!
https://github.com/l534zhan/my_project

[Bryan Gin-ge Chen]

You may want to edit the Zulip thread title to make it more specific to your project.

[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. :upside_down:

[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 by Scott Morrison to #maths > Contribute a project on Hadamard matrices