## Stream: general

### Topic: Failure to identify two types

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


#### Anne Baanen (Feb 08 2021 at 09:50):

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

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


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


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


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

#### Kevin Buzzard (Feb 08 2021 at 10:24):

def a : ℕ := 37

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

def newnat := ℕ

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


#### 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"?

#### Kevin Buzzard (Feb 08 2021 at 10:28):

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

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


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

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


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

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

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

#### 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 :=


#### Kevin Buzzard (Feb 08 2021 at 10:40):

again looks ugly :-/

#### Kevin Buzzard (Feb 08 2021 at 10:40):

but also good to know!

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

#### 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 :-)

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

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

#### Rob Lewis (Feb 08 2021 at 10:43):

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

#### Kevin Buzzard (Feb 08 2021 at 10:43):

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

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