Failure to identify two types

Stream: general

[Heather Macbeth]

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]

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

[Anne Baanen]

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]

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]

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]

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]

def a : ℕ := 37

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

def newnat := ℕ

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Rob Lewis]

(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]

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]

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]

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]

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]

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]

again looks ugly :-/

[Kevin Buzzard]

but also good to know!

[Rob Lewis]

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]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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.