Zulip Chat Archive

Stream: general

Topic: synthesized type class instance is not definitionally equal


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

view this post on Zulip Johan Commelin (Jan 30 2021 at 15:21):

Probably adding [decidable_pred p] will solve the issue

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

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

view this post on Zulip Kevin Buzzard (Jan 30 2021 at 15:58):

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

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

view this post on Zulip Kevin Buzzard (Jan 30 2021 at 16:05):

Aah, I also added it to the lemma.

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

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