## 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.

Last updated: May 06 2021 at 21:09 UTC