Zulip Chat Archive

Stream: new members

Topic: Quadratic forms don't work on ℤ


view this post on Zulip 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?

view this post on Zulip Reid Barton (Jul 18 2020 at 17:41):

What is the error?

view this post on Zulip Markus Himmel (Jul 18 2020 at 17:43):

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.

view this post on Zulip Johan Commelin (Jul 18 2020 at 17:48):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 18 2020 at 17:53):

It works with by convert for some reason

view this post on Zulip Reid Barton (Jul 18 2020 at 17:54):

I thought the problem would be with the module structure.

view this post on Zulip Reid Barton (Jul 18 2020 at 17:54):

Does Lean know Z-module structures are unique?

view this post on Zulip Johan Commelin (Jul 18 2020 at 17:54):

Hmmm, I don't recall seeing that

view this post on Zulip Markus Himmel (Jul 18 2020 at 17:55):

Reid Barton said:

Does Lean know Z-module structures are unique?

Yes!

view this post on Zulip Reid Barton (Jul 18 2020 at 17:56):

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

view this post on Zulip 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