## Stream: new members

### Topic: Quadratic forms don't work on ℤ

#### Eloi (Jul 18 2020 at 17:32):

Hi, I can't define a quadratic form over ℤ, but I can over ℚ...

Here is my code:

import linear_algebra.quadratic_form

-- this is the quadratic form x², and it works
example : quadratic_form ℚ (fin 1→ ℚ) :=
@quadratic_form.proj ℚ  _ (fin 1) 0 0

-- this does not work
example : quadratic_form ℤ (fin 1→ ℤ) :=
@quadratic_form.proj ℤ  _ (fin 1) 0 0


The definition of quadratic_form.proj has the following signature in mathlib:

def proj (i j : n) : quadratic_form R₁ (n → R₁)


with the assumtion [comm_ring R₁]. What is happening?

#### Reid Barton (Jul 18 2020 at 17:41):

What is the error?

#### Markus Himmel (Jul 18 2020 at 17:43):

The error is

type mismatch, term
has type
@quadratic_form ℤ (fin 1 → ℤ) (@comm_ring.to_ring ℤ int.comm_ring)
(@pi.add_comm_group (fin 1) (λ (a : fin 1), ℤ)
(λ (i : fin 1), @ring.to_add_comm_group ℤ (@comm_ring.to_ring ℤ int.comm_ring)))
(@pi.semimodule (fin 1) (λ (a : fin 1), ℤ) ℤ (@ring.to_semiring ℤ (@comm_ring.to_ring ℤ int.comm_ring))
(λ (i : fin 1),
(λ (i : fin 1), @semiring.to_semimodule ℤ (@ring.to_semiring ℤ (@comm_ring.to_ring ℤ int.comm_ring))))
but is expected to have type
@quadratic_form ℤ (fin 1 → ℤ) int.ring
(@pi.add_comm_group (fin 1) (λ (a : fin 1), ℤ)
(λ (i : fin 1),
(@pi.semimodule (fin 1) (λ (a : fin 1), ℤ) ℤ (@ring.to_semiring ℤ int.ring)
(λ (i : fin 1), int.add_comm_monoid)
(λ (i : fin 1),


There seem to be several typeclass diamonds here.

#### Johan Commelin (Jul 18 2020 at 17:48):

Hmmm... it's the olde decidable_* that strikes again :sad:

#### Johan Commelin (Jul 18 2020 at 17:49):

I wish we could fix all these problems in one go, but I guess it requires a complete rethinking of the way computation / decidability is handled :sad: Most likely a problem for which a solution is not yet known.

#### Alex J. Best (Jul 18 2020 at 17:50):

I'm not saying its the way to go, but if you just leave the type out lean looks happy

def a :=
@quadratic_form.proj ℤ  _ (fin 1) 0 0
#print a


#### Reid Barton (Jul 18 2020 at 17:53):

It works with by convert for some reason

#### Reid Barton (Jul 18 2020 at 17:54):

I thought the problem would be with the module structure.

#### Reid Barton (Jul 18 2020 at 17:54):

Does Lean know Z-module structures are unique?

#### Johan Commelin (Jul 18 2020 at 17:54):

Hmmm, I don't recall seeing that

#### Markus Himmel (Jul 18 2020 at 17:55):

Reid Barton said:

Does Lean know Z-module structures are unique?

Yes!

#### Reid Barton (Jul 18 2020 at 17:56):

Couldn't we just define * on int to be whatever action comes from add_comm_group?

#### Johan Commelin (Jul 18 2020 at 18:46):

You mean to make the two defeq? It would mean refactoring core...

Last updated: May 11 2021 at 22:14 UTC