## Stream: new members

### Topic: Contribute a project on Hadamard matrices

#### Alex Zhang (Sep 05 2021 at 19:31):

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 (Sep 05 2021 at 19:32):

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

#### Alex Zhang (Sep 15 2021 at 15:50):

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 (Sep 15 2021 at 15:51):

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

#### Filippo A. E. Nuccio (Sep 15 2021 at 15:52):

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

#### Alex Zhang (Sep 15 2021 at 15:55):

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 (Sep 15 2021 at 15:55):

Should I use Z?

#### Yaël Dillies (Sep 15 2021 at 15:55):

Hmm... That sounds wrong.

#### Yaël Dillies (Sep 15 2021 at 15:55):

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

#### Alex Zhang (Sep 15 2021 at 15:56):

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

#### Filippo A. E. Nuccio (Sep 15 2021 at 15:56):

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

#### Alex Zhang (Sep 15 2021 at 15:57):

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

#### Filippo A. E. Nuccio (Sep 15 2021 at 15:57):

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 (Sep 15 2021 at 15:58):

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

#### Alex Zhang (Sep 15 2021 at 15:59):

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

#### Yaël Dillies (Sep 15 2021 at 15:59):

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

#### Alex Zhang (Sep 15 2021 at 15:59):

That is indeed more general.

#### Alex Zhang (Sep 15 2021 at 16:01):

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

#### Yaël Dillies (Sep 15 2021 at 16:01):

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 (Sep 15 2021 at 16:02):

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 (Sep 15 2021 at 16:02):

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 (Sep 15 2021 at 16:02):

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

#### Filippo A. E. Nuccio (Sep 15 2021 at 16:03):

OOOPS, sorry :angel: :lol:

#### Alex Zhang (Sep 15 2021 at 16:04):

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

#### Alex Zhang (Sep 15 2021 at 16:05):

Cool. I will generalise it!

#### Eric Wieser (Sep 15 2021 at 16:05):

docs#matrix.has_orthogonal_rows needs a semiring, right?

#### Filippo A. E. Nuccio (Sep 15 2021 at 16:05):

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 (Sep 15 2021 at 16:06):

Eric Wieser said:

docs#matrix.has_orthogonal_rows needs a semiring, right?

Yeah. I think so.

#### Eric Wieser (Sep 15 2021 at 16:06):

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 (Sep 15 2021 at 16:07):

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 (Sep 15 2021 at 16:08):

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 (Sep 15 2021 at 16:08):

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

#### Alex Zhang (Sep 15 2021 at 16:10):

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

#### Johan Commelin (Sep 15 2021 at 16:10):

The has_neg suggests that you even want a ring

right right

#### Eric Wieser (Sep 15 2021 at 16:11):

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

#### Alex Zhang (Sep 15 2021 at 16:12):

That is exactly the thing I was thinking about

#### Alex Zhang (Sep 15 2021 at 16:13):

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 (Sep 15 2021 at 16:14):

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 (Sep 15 2021 at 16:14):

A class is a structure that typeclass inference can use.

#### Eric Wieser (Sep 15 2021 at 16:14):

But you may as well rename it to is_hadamard now

#### Alex Zhang (Sep 15 2021 at 16:15):

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 (Sep 15 2021 at 16:15):

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

#### Alex Zhang (Sep 15 2021 at 16:17):

OK, nice. I will do this PR after having my dinner. :upside_down:

#### Alex Zhang (Sep 15 2021 at 16:19):

Thanks a lot for your suggestions!

#### Filippo A. E. Nuccio (Sep 15 2021 at 16:22):

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 (Sep 15 2021 at 16:23):

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

#### Yaël Dillies (Sep 15 2021 at 16:23):

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

#### Yaël Dillies (Sep 15 2021 at 16:24):

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 (Sep 15 2021 at 16:25):

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 (Sep 15 2021 at 16:27):

@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 (Sep 15 2021 at 16:27):

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 (Sep 15 2021 at 16:27):

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 (Sep 15 2021 at 16:27):

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

#### Eric Wieser (Sep 15 2021 at 16:28):

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

#### Filippo A. E. Nuccio (Sep 15 2021 at 16:28):

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

#### Anne Baanen (Sep 15 2021 at 16:28):

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 (Sep 15 2021 at 16:30):

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 (Sep 15 2021 at 16:31):

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 (Sep 16 2021 at 02:51):

This topic was moved by Scott Morrison to #maths > Contribute a project on Hadamard matrices

Last updated: Dec 20 2023 at 11:08 UTC