Type class trouble

Stream: general

[Michael Stoll]

I am having trouble with the following.

import tactic.basic
import field_theory.finite.basic
import ring_theory.trace

def finite_field.trace_to_zmod (F : Type*) [field F] [fintype F] : F →ₗ[zmod (ring_char F)] zmod (ring_char F) :=
begin
  haveI := ring_char.char_p F,
  haveI := zmod.algebra F (ring_char F),
  let tr := algebra.trace (zmod (ring_char F)) F,
  exact tr, -- invalid type ascription ...
end

Before exact tr, the state looks like this:

F: Type ?
_inst_1: field F
_inst_2: fintype F
_inst: char_p F (ring_char F)
_inst_3: algebra (zmod (ring_char F)) F
tr: F →ₗ[zmod (ring_char F)] zmod (ring_char F) := algebra.trace (zmod (ring_char F)) F
⊢ F →ₗ[zmod (ring_char F)] zmod (ring_char F)

Clicking on the type of tr in the infoview shows exactly the same information as clicking on the type of the goal:

linear_map
zmod (ring_char F)
zmod (ring_char F)
ring.to_semiring
ring.to_semiring
ring_hom.id (zmod (ring_char F))
F
zmod (ring_char F)
add_comm_group.to_add_comm_monoid F
add_comm_group.to_add_comm_monoid (zmod (ring_char F))
algebra.to_module
semiring.to_module

The mismatching types in the error message differ in the following places:

       (@ring.to_add_comm_group F
          (@comm_ring.to_ring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))))

vs.

       (@ring.to_add_comm_group F (@division_ring.to_ring F (@field.to_division_ring F _inst_1))))

and

       (@ring.to_semiring F
          (@comm_ring.to_ring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1))))
       _inst_3)

vs.

       (@ring.to_semiring F (@division_ring.to_ring F (@field.to_division_ring F _inst_1)))
       (@zmod.algebra F (@division_ring.to_ring F (@field.to_division_ring F _inst_1))
          (@ring_char F
             (@non_assoc_ring.to_non_assoc_semiring F
                (@ring.to_non_assoc_ring F (@division_ring.to_ring F (@field.to_division_ring F _inst_1)))))
          _))

It looks like part of the problem is that two differing paths are used to get from field to ring. I have no idea how to avoid this...

[Eric Wieser]

What doesconvert tr leave as a goal?

[Eric Wieser]

Does changing the second haveI to a letI help?

[Eric Wieser]

I think that's your problem; lean is saying "you told me to forget what _inst_3 is, so I can't unfold it any further to check it's equal to the other instance"

[Michael Stoll]

Thanks! I was forgetting that algebra ... is data.

[Michael Stoll]

A more helpful error message would go a long way...

[Eric Wieser]

We could make haveI detect this error

[Eric Wieser]

Do you even need the haveI there though?

[Michael Stoll]

Actually, no.

[Eric Wieser]

What made you think you did?

[Eric Wieser]

(that is, do we need to improve documentation somewhere?)

[Michael Stoll]

I think I thought I needed [char_p F (ring_char F)] for something. But it is possible that as the proof evolved, that changed.

[Eric Wieser]

Ah right, docs#ring_char.char_p is not an instance

[Eric Wieser]

So you have that automatically with no need for a haveI

[Michael Stoll]

Ah, I hadn't realized that. Good to know...

[Eric Wieser]

Having said that, the strategy of adding letI lines is a good one when lean can't find the instance through a long chain and you can't work out what condition you're missing

[Eric Wieser]

For instance, if it can't find addition on a product type, you add letI : has_add (X × Y) := prod.has_add and then your error message will tell you where the left or right half is missing addition

[Michael Stoll]

Thanks for the tip! I'll try to remember it.

[Michael Stoll]

Another question: I'm having trouble with something like the following.

import tactic.basic
import field_theory.finite.basic

structure test (A : Type) [comm_ring A] := (A' : Type) (B : comm_ring A') (C : A →+ A')

def test1 : test ℤ := { A' := ℤ, B := _, C := add_monoid_hom.id ℤ }

def test2 : test ℤ :=
{ A' := test1.A', B := test1.B,
  C := test1.C.comp (add_monoid_hom.id _) }
-- failed to synthesize type class instance for
-- ⊢ add_zero_class test1.A'

def test3 : test ℤ :=
{ A' := test1.A', B := test1.B,
  C := begin haveI := test1.B, exact test1.C.comp (add_monoid_hom.id _) end }
-- synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
--  add_monoid.to_add_zero_class test1.A'
-- inferred
--  add_monoid.to_add_zero_class test1.A'

How do I get the correct instance(s) into the context when filling the fields of the structure?

[Yaël Dillies]

What about

structure test (A : Type) [comm_ring A] := (A' : Type) [B : comm_ring A'] (C : A →+ A')

[Michael Stoll]

Still gives the same error for test2 (and test3).

[Michael Stoll]

In fact, test2 gives now the additional message

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  add_monoid.to_add_zero_class test1.A'

[Michael Stoll]

replacing comm_ring by add_zero_class to exclude possible problems from chaining of instances doesn't help. Instead of add_monoid.to_add_zero_class test1.A'the error messages now refer to test1.B, but they are still there:

import tactic.basic
import data.int.basic

structure test (A : Type) [add_zero_class A] := (A' : Type) [B : add_zero_class A'] (C : A →+ A')

def test1 : test ℤ := { A' := ℤ, B := _, C := add_monoid_hom.id ℤ }

def test2 : test ℤ :=
{ A' := test1.A', B := _,
  C := test1.C.comp (add_monoid_hom.id _) }
-- failed to synthesize type class instance for
-- ⊢ add_zero_class test1.A'
--
-- synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
--   ⁇
-- inferred
--   test1.B

def test3 : test ℤ :=
begin haveI := test1.B, exact
{ A' := test1.A', B := _,
  C := test1.C.comp (add_monoid_hom.id _) }
end
-- synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
--   _inst
-- inferred
--   test1.B

[Michael Stoll]

The red squiggly line is below C(in test1.C.comp) in test2, but below test1 in test3.

[Damiano Testa]

I do not know how to analyze this, but maybe this is useful:

import tactic.basic
import data.int.basic

--  B is now implicit, rather than typeclass
structure test (A : Type*) [add_zero_class A] := (A' : Type*) {B : add_zero_class A'} (C : A →+ A')

def test1 : test ℤ := { A' := ℤ, B := _, C := add_monoid_hom.id ℤ }

def test2 : test ℤ :=
{ A' := test1.A', B := _,
--  use @, ugh, and the ℤ is important!
  C :=  @add_monoid_hom.comp _ _ ℤ _ _ _ test1.C (add_monoid_hom.id _) }

[Reid Barton]

Add attribute [instance] test.B after the definition of test, and get rid of the haveI tactic stuff in test3 (it creates a variable instance with no local definition)

[Michael Stoll]

Thanks, Reid.
Can you also explain why this is necessary?

[Eric Wieser]

When you write:

structure test (A : Type) [add_zero_class A] := (A' : Type) [B : add_zero_class A'] (C : A →+ A')

this means "make B a typeclass argument to test.mk"

[Eric Wieser]

It does not mean "use B when performing instance search"

[Eric Wieser]

To say that, you need to add the [instance] attribute; it helps if you remember that instance is roughly @[instance] def

[Michael Stoll]

OK. And why did the haveI ... version not work? The error message was quite confusing, claiming that two things are not defeq that look exactly the same.

[Reid Barton]

It is the usual letI vs haveI issue

[Michael Stoll]

Again! :oh_no: