Zulip Chat Archive

Stream: general

Topic: Failure to identify two types


view this post on Zulip Heather Macbeth (Feb 08 2021 at 06:37):

I'm having a problem where Lean can figure out that an object is of type {A // A.det = 1}, but not recognize it as an object of type special_linear_group, even though that is precisely the definition (docs#special_linear_group).

Apologies for the long example. The problem seems to turn up only after I've defined a coercion

has_coe (special_linear_group n ) (special_linear_group n R)

(you'll see that a similar example phrased without this coercion typechecks). So maybe this is a bad coercion (... ambiguity between this coercion and the subtype coercion?).

import linear_algebra.special_linear_group
import data.matrix.notation

open matrix

variables {n : Type*} [decidable_eq n] [fintype n]
variables {R : Type*} [comm_ring R] {S : Type*} [comm_ring S]

/-- A ring homomorphism from `S` to `R` induces a group homomorphism from
`special_linear_group n S` to `special_linear_group n R`. -/
def ring_hom.map_special_linear_group (f : S →+* R) :
  (special_linear_group n S) →* (special_linear_group n R) :=
{ to_fun := λ g, f.map_matrix g, by rw  matrix.ring_hom.map_det; simp [g.2]⟩,
  map_one' := by simpa,
  map_mul' := λ x y, by simpa }

variables {a : } (M : matrix (fin a) (fin a.succ) ) (v : (fin a.succ)  )
  (hM : det (vec_cons v M) = 1)

/- This typechecks! -/
example : (int.cast_ring_hom R).map_special_linear_group vec_cons v M, hM = 1 :=
sorry

/-- The coercion homomorphism from `ℤ` to `R` induces a group homomorphism from
`special_linear_group n ℤ` to `special_linear_group n R`. -/
instance : has_coe (special_linear_group n ) (special_linear_group n R) :=
⟨(int.cast_ring_hom R).map_special_linear_group

/- This doesn't typecheck!
invalid type ascription, term has type
  {A // A.det = 1} : Type
but is expected to have type
  special_linear_group (fin a.succ) R : Type u_2
-/
example :
  ((⟨vec_cons v M, hM : special_linear_group (fin a.succ) ) : special_linear_group (fin a.succ) R)
  = 1 :=
sorry

view this post on Zulip Anne Baanen (Feb 08 2021 at 09:50):

I think the : Type versus : Type u_2 is causing the error. Let me see...

view this post on Zulip Anne Baanen (Feb 08 2021 at 09:51):

This works:

example :
  @coe (special_linear_group (fin a.succ) ) _ _ vec_cons v M, hM = (1 : special_linear_group (fin a.succ) R) :=
sorry

view this post on Zulip Anne Baanen (Feb 08 2021 at 09:56):

Another issue is the has_coe, which should be has_coe_t to avoid looping:

/-- The coercion homomorphism from `ℤ` to `R` induces a group homomorphism from
`special_linear_group n ℤ` to `special_linear_group n R`. -/
instance : has_coe_t (special_linear_group n ) (special_linear_group n R) :=
⟨(int.cast_ring_hom R).map_special_linear_group

view this post on Zulip Anne Baanen (Feb 08 2021 at 09:58):

Aha! Looks like special_linear_group _ ℤ is unfolded before the coercion is inserted, and then the system can't find a coercion {A // A.det = (1 : ℤ)} → special_linear_group (fin a.succ) R. If we use show instead of type ascription, the type doesn't get unfolded and it works:

import linear_algebra.special_linear_group
import data.matrix.notation

open matrix

variables {n : Type*} [decidable_eq n] [fintype n]
variables {R : Type*} [comm_ring R] {S : Type*} [comm_ring S]

/-- A ring homomorphism from `S` to `R` induces a group homomorphism from
`special_linear_group n S` to `special_linear_group n R`. -/
def ring_hom.map_special_linear_group (f : S →+* R) :
  (special_linear_group n S) →* (special_linear_group n R) :=
{ to_fun := λ g, f.map_matrix g, by rw  matrix.ring_hom.map_det; simp [g.2]⟩,
  map_one' := by simpa,
  map_mul' := λ x y, by simpa }

variables {a : } (M : matrix (fin a) (fin a.succ) ) (v : (fin a.succ)  )
  (hM : det (vec_cons v M) = 1)

/- This typechecks! -/
example : (int.cast_ring_hom R).map_special_linear_group vec_cons v M, hM = 1 :=
sorry

/-- The coercion homomorphism from `ℤ` to `R` induces a group homomorphism from
`special_linear_group n ℤ` to `special_linear_group n R`. -/
instance : has_coe_t (special_linear_group n ) (special_linear_group n R) :=
⟨(int.cast_ring_hom R).map_special_linear_group

example :
  ((show special_linear_group (fin a.succ) , from vec_cons v M, hM⟩) : special_linear_group (fin a.succ) R)
  = 1 :=
sorry

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:23):

I used to think that if X : A then (X : B) meant "please coerce X to type B and then continue", but it actually means "oh, while we're here, please check that it makes sense to consider X as having type B". If A and B are not defeq but there's a coercion from A to B then this coercion will happen, but if A and B are defeq then my impression is that it could well happen that Lean just checks that (X : B) makes sense but then keeps considering X as having type A.

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:24):

def a :  := 37

#check (a : ) -- ↑a : ℤ

def newnat := 

#check (a : newnat) -- a : ℕ

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:25):

Thanks Heather and Anne! I had never understood why "sometimes (X : B) works and sometimes it doesn't" -- maybe the issue is simply whether there is a non-trivial coercion or whether it's a defeq thing. I had seen it failing in the past. To be quite frank I wish it always meant "OK now X has type B", I think this show B, from X idiom is a workaround but it does look weird. Whyever would I want (X : B) to mean anything other than "yes I mean X has type B"?

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:28):

I've never understood has_coe_t either, but that's another story :-)

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:32):

#check (⟨vec_cons v M, hM : special_linear_group (fin a.succ) ) -- ⟨vec_cons v M, hM⟩ : {A // A.det = 1}

view this post on Zulip Rob Lewis (Feb 08 2021 at 10:36):

(X : B) is just a hint for the elaborator. The : B doesn't show up in the resulting term at all. The type of this term will be whatever Lean infers as the type of the elaborated X. On the other hand, the show ... annotation does appear in the elaborated term.

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:36):

def constructor_with_right_type (A : matrix n n R) (hA : A.det = 1) : special_linear_group n R :=
A, hA

#check constructor_with_right_type (vec_cons v M) hM -- special_linear_group (fin a.succ) ℤ

example :
  ((constructor_with_right_type (vec_cons v M) hM : special_linear_group (fin a.succ) ) : special_linear_group (fin a.succ) R)
  = 1 :=
sorry

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:37):

But if B is not defeq to what the actual type of X is, then a coercion is inserted, so the notation really does change the term in that case.

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:39):

All these little tricks which one picks up over the years -- and with Lean 4 some will be wrong, some will still work, and we'll need to pick up a bunch of new ones.

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:40):

Presumably in Lean 4 I'll be able to write a macro to get (X : B) to mean (show B, from X), which is the thing which I think I've always wanted it to mean (and which Heather wanted it to mean above).

view this post on Zulip Sebastien Gouezel (Feb 08 2021 at 10:40):

Another trick that works is to insert an id, as in:

example :
  (((id vec_cons v M, hM⟩) : special_linear_group (fin a.succ) ) : special_linear_group (fin a.succ) R)
  = 1 :=

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:40):

again looks ugly :-/

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:40):

but also good to know!

view this post on Zulip Rob Lewis (Feb 08 2021 at 10:41):

Kevin Buzzard said:

But if B is not defeq to what the actual type of X is, then a coercion is inserted, so the notation really does change the term in that case.

Well, kind of. (X : B) is a preterm (unelaborated term). Elaboration "changes" the preterm into a term, regardless of whether there's a coercion or not. Elaborated X is never the same as unelaborated X.

view this post on Zulip Sebastien Gouezel (Feb 08 2021 at 10:41):

Don't ask me why it works, by the way. You don't understand Lean3, you just get used to it :-)

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:41):

I guess the id trick works because id is id {alpha} and the elaboration hint tells Lean what alpha to use.

view this post on Zulip Sebastien Gouezel (Feb 08 2021 at 10:42):

Yes, it builds stuff from the outside, so it chooses the type of id before it chooses the type of ⟨vec_cons v M, hM⟩.

view this post on Zulip Rob Lewis (Feb 08 2021 at 10:43):

I think the show B, from X macro expands to something like @id B X, right?

view this post on Zulip Kevin Buzzard (Feb 08 2021 at 10:43):

I love it when someone asks just the right question :-)

view this post on Zulip Heather Macbeth (Feb 08 2021 at 18:54):

Thank you very much, @Anne Baanen and all! You never understand something until it's bit you ... I'd seen people use these show ... from ... and id ... : ... idioms before but without quite internalizing the use case. The whole discussion was very instructive, for example this:

Kevin Buzzard said:

I used to think that if X : A then (X : B) meant "please coerce X to type B and then continue", but it actually means "oh, while we're here, please check that it makes sense to consider X as having type B". If A and B are not defeq but there's a coercion from A to B then this coercion will happen, but if A and B are defeq then my impression is that it could well happen that Lean just checks that (X : B) makes sense but then keeps considering X as having type A.


Last updated: May 13 2021 at 23:16 UTC