# Zulip Chat Archive

## 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: Aug 03 2023 at 10:10 UTC