Quadratic forms don't work on ℤ

Stream: new members

[Eloi]

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]

What is the error?

[Markus Himmel]

The error is

type mismatch, term
  quadratic_form.proj 0 0
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),
          @add_comm_group.to_add_comm_monoid ℤ (@ring.to_add_comm_group ℤ (@comm_ring.to_ring ℤ int.comm_ring)))
       (λ (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),
          @decidable_linear_ordered_add_comm_group.to_add_comm_group ℤ int.decidable_linear_ordered_add_comm_group))
    (@pi.semimodule (fin 1) (λ (a : fin 1), ℤ) ℤ (@ring.to_semiring ℤ int.ring)
       (λ (i : fin 1), int.add_comm_monoid)
       (λ (i : fin 1),
          @add_comm_group.int_module ℤ (@ring.to_add_comm_group ℤ (@comm_ring.to_ring ℤ int.comm_ring))))

There seem to be several typeclass diamonds here.

[Johan Commelin]

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

[Johan Commelin]

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]

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]

It works with by convert for some reason

[Reid Barton]

I thought the problem would be with the module structure.

[Reid Barton]

Does Lean know Z-module structures are unique?

[Johan Commelin]

Hmmm, I don't recall seeing that

[Markus Himmel]

Reid Barton said:

Does Lean know Z-module structures are unique?

Yes!

[Reid Barton]

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

[Johan Commelin]

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