## Stream: general

### Topic: synthesized type class instance is not definitionally equal

#### Paul van Wamelen (Jan 30 2021 at 15:17):

I'd like to prove the lemma below, but lean doesn't like my statement. Is there a nice way around this problem?

import linear_algebra.determinant

noncomputable theory
open_locale classical

universes u v
variables {m : Type u} [fintype m] {R : Type v} [comm_ring R]

def to_square_block (M : matrix m m R) (p : m → Prop) :
matrix {a // p a} {a // p a} R := λ i j, M ↑i ↑j

lemma upper_two_block_triangular_det (M : matrix m m R) (p : m → Prop)
(h : ∀ i (h1 : ¬p i) j (h2 : p j), M i j = 0) :
M.det = (to_square_block M p).det * (to_square_block M (λ i, ¬(p i))).det :=
begin
sorry
end


The error I get is:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
subtype.fintype (λ (x : m), (λ (a : m), (λ (i : m), ¬p i) a) x)
inferred
subtype.fintype (λ (a : m), (λ (i : m), ¬p i) a)


I could do

lemma upper_two_block_triangular_det' (M : matrix m m R) (p : m → Prop) (q : m → Prop)
(h : q = (λ i, ¬(p i))) (h2 : ∀ i (h1 : ¬p i) j (h2 : p j), M i j = 0) :
M.det = (to_square_block M p).det * (to_square_block M q).det :=
begin
sorry
end


but that seems a bit sad. More generally is there a way of adding some abbreviation\notation like "let q := ..." into the conclusion of a theorem statement?

#### Johan Commelin (Jan 30 2021 at 15:21):

Probably adding [decidable_pred p] will solve the issue

#### Kevin Buzzard (Jan 30 2021 at 15:52):

I don't think it does. The issue is that mathematics is happening here, and fintype is the natural way to say "this type is finite" but it's not Prop-valued. I think we need a Prop-valued fintype to solve this nicely. Do we have one? I might be wrong about this. The issue seems to be that something is not being beta-reduced in time for type class inference to get unconfused.

#### Bhavik Mehta (Jan 30 2021 at 15:55):

import linear_algebra.determinant

noncomputable theory
open_locale classical

universes u v
variables {m : Type u} [fintype m] {R : Type v} [comm_ring R]

def to_square_block (M : matrix m m R) (p : m → Prop) [decidable_pred p] :
matrix {a // p a} {a // p a} R := λ i j, M ↑i ↑j

lemma upper_two_block_triangular_det (M : matrix m m R) (p : m → Prop)
(h : ∀ i (h1 : ¬p i) j (h2 : p j), M i j = 0) :
M.det = (to_square_block M p).det * (to_square_block M (λ i, ¬(p i))).det :=
begin
sorry
end


works for me

#### Kevin Buzzard (Jan 30 2021 at 15:58):

Yes you're right, I wonder what I managed to do (I thought I checked).

#### Paul van Wamelen (Jan 30 2021 at 16:00):

Oh! I tried adding it to the lemma. Adding it to the def works for me too!
Is this all just a trick to learn, or is there some reason I should have known to try this? In particular why does the decidable_pred allow the beta reduction?

#### Kevin Buzzard (Jan 30 2021 at 16:05):

Aah, I also added it to the lemma.

#### Bhavik Mehta (Jan 30 2021 at 16:06):

My rule of thumb is that defs are better off with decidability assumptions rather than going classical, but when you're stating or proving lemmas you can either give explicit decidability constraints or just go classical and it shouldn't make a difference

#### Paul van Wamelen (Jan 30 2021 at 16:09):

Thanks Bhavik, I'll keep that in mind.

#### Johan Commelin (Sep 09 2021 at 14:28):

How should I interpret this error?

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
construction.is_tensor_product R R M
inferred
?m_1


My gut reaction is: "Well, if you inferred some meta-variable, why don't you instantiate it to the thing you synthesized?"
Why can't that be done?

#### Adam Topaz (Sep 09 2021 at 14:48):

I seem to recall running into similar errors when playing with tensor products when lean couldn't figure out what to take a tensor product over. Do you have a #mwe ?

#### Johan Commelin (Sep 09 2021 at 16:43):

It happened on a branch that is doing a major refactor of tensor products. So I'm not sure if I can easily create a #mwe.

#### Alex J. Best (Oct 20 2021 at 14:04):

I'm hitting an issue I don't understand:
The following code:

import ring_theory.polynomial.cyclotomic

open polynomial
variable (n : ℕ)
set_option pp.all true
#check splitting_field (cyclotomic n ℚ)


produces

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
@normed_ring.to_ring.{0} rat
(@normed_comm_ring.to_normed_ring.{0} rat (@normed_field.to_normed_comm_ring.{0} rat rat.normed_field))
inferred
@division_ring.to_ring.{0} rat (@field.to_division_ring.{0} rat ?m_1)


I don't understand why there is a metavariable in the inferred class, or why this is causing issues at all, if I fill in the metavariable by hand and check that things are defeq using rfl it always seems to work, so I'm a bit confused

#### Alex J. Best (Oct 20 2021 at 14:11):

Both of these variations work:

#check (splitting_field (@cyclotomic n ℚ _))
#check (splitting_field (@cyclotomic n ℚ (by apply_instance)))


#### Yury G. Kudryashov (Oct 21 2021 at 02:08):

Does it help if you add an explicit instance for ring rat?

#### Alex J. Best (Oct 23 2021 at 22:23):

It doesn't seem to help no

Last updated: Dec 20 2023 at 11:08 UTC