synthesized type class instance is not definitionally equal

Stream: general

[Paul van Wamelen]

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]

Probably adding [decidable_pred p] will solve the issue

[Kevin Buzzard]

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]

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]

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

[Paul van Wamelen]

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]

Aah, I also added it to the lemma.

[Bhavik Mehta]

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]

Thanks Bhavik, I'll keep that in mind.

[Johan Commelin]

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]

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]

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]

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]

Both of these variations work:

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

[Yury G. Kudryashov]

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

[Alex J. Best]

It doesn't seem to help no