Zulip Chat Archive

Stream: new members

Topic: misunderstanding coe?


view this post on Zulip Alex Mathers (Mar 30 2020 at 18:04):

I currently have the following two lines of code

instance (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] : has_coe (subalgebra R A) (set A) := λ S, S.carrier
instance (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] (S : subalgebra R A) : is_subring S := S.subring

returning the error message

type mismatch at application
  is_subring S
term
  S
has type
  subalgebra R A : Type ?
but is expected to have type
  set ?m_1 : Type ?

am I misunderstanding how the coercion should be working?

view this post on Zulip Reid Barton (Mar 30 2020 at 18:20):

It doesn't know yet what S is supposed to be a subring of

view this post on Zulip Alex Mathers (Mar 30 2020 at 18:24):

How can I make it explicit? In the definition of is_subring the ambient ring is not explicit, i.e. it looks like

class is_subring {R : Type*} [ring R] (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.

view this post on Zulip Reid Barton (Mar 30 2020 at 18:24):

I guess you could claim it should be able to infer it from the definition S.subring, but I think the coercion will not fire soon enough for that to work.

view this post on Zulip Reid Barton (Mar 30 2020 at 18:24):

Maybe is_subring (S : set A) for example.

view this post on Zulip Alex Mathers (Mar 30 2020 at 18:25):

I see. That fixes it!

view this post on Zulip Reid Barton (Mar 30 2020 at 18:25):

Just because you have written this first has_coe instance doesn't mean Lean has to use it.

view this post on Zulip Alex Mathers (Mar 30 2020 at 18:25):

is there a simple explanation of what Lean is doing for why it doesn't "use" it?

view this post on Zulip Reid Barton (Mar 30 2020 at 18:26):

It isn't doing anything because it has no way to know what the ?m_1 is in the error message.

view this post on Zulip Reid Barton (Mar 30 2020 at 18:28):

For example, someone else could add an instance : has_coe (subalgebra R A) (set R) (never mind that it would be nonsense) and then what do you expect to happen?

view this post on Zulip Alex Mathers (Mar 30 2020 at 18:29):

Ah, I see

view this post on Zulip Alex Mathers (Mar 30 2020 at 19:46):

I guess this is related to my previous question: my code

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] :
integral_domain (integral_closure R A) := subring.domain ((integral_closure R A) : set A)

is giving the error message

failed to synthesize type class instance for
R : Type ?,
_inst_1 : comm_ring R,
A : Type ?,
_inst_2 : integral_domain A,
_inst_3 : algebra R A
⊢ is_subring (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)))

while the code from the previous question is supposed to be giving the instance of (integral_closure R A) : subalgebra R A as a subring of A. How can I "remind" Lean that this does have an instance of is_subring?

view this post on Zulip Alex Mathers (Mar 30 2020 at 19:50):

also it seems from the error message that Lean isn't actually using the coercion I set up, rather I guess it's using the sequence of coercions subalgebra R A → submodule R A → set A. Is there a possibility that this is related to my issue?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:01):

What happens if you remove your coercion and then attempt to coerce anyway?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:02):

If it still works then you should trust that the people who set it up knew what they were doing and don't add the coercion

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:02):

It has the same error message

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:02):

Sure

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:02):

But I'm asking just about whether the coercion succeeds

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:03):

From subalgebra to set

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:03):

My guess is that you shouldn't be creating that instance but this is not the answer to your problem

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:05):

You should also see if the second instance is solved by by apply_instance

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:05):

It would surprise me if there were important coercions which were not there already

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:06):

The inbuilt coercions might have subtle priorities set, for example

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:08):

And what happens if you just remove the explicit coercion to set A in your error? Mathlib might have solved all your problems already

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:08):

I'll get to a computer and stop guessing in a sec

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:21):

I'm still working out the imports :-(

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:22):

I think we should have a bot which just flags all posted code which doesn't actually compile and either kicks the poster or suggests imports and opens which will fix it.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:24):

Right. This succeeds

import ring_theory.algebra ring_theory.subring

instance (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] :
has_coe (subalgebra R A) (set A) := by apply_instance

so don't add a new one.

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:24):

sorry for the delay. These imports should be the necessary ones:

import ring_theory.integral_closure
import ring_theory.localization
import ring_theory.algebra
import ring_theory.subring

view this post on Zulip Patrick Massot (Mar 30 2020 at 20:24):

A more realistic idea would be to try someone who could write a web page explaining what is a MWE, so that we can paste a link to that web page each it's needed.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:25):

So do we not have bundled subrings?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:25):

Where are my undergraduates?

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:27):

This is the only definition I see on the subring document:

class is_subring (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:27):

Yeah, I think we don't have bundled subrings. Shame. I bet it would be easier with those.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:27):

And this doesn't work:

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] :
integral_domain (integral_closure R A) := by apply_instance

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:30):

Unfortunate :/

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:32):

Did you see the Artin-Tate thread?

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:32):

No I didn't

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:32):

This whole algebra, subring thing drives me nuts

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:33):

I saw a conversation about difficulties with "triangles" of rings in commutative algebra, not sure if that's the thread you mean but yeah it seems to be an annoying issue

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:34):

import ring_theory.integral_closure
import ring_theory.localization
import ring_theory.algebra
import ring_theory.subring

instance foo (R : Type*) [comm_ring R] {A : Type*} [comm_ring A] [algebra R A] (S : subalgebra R A) :
  is_subring (S : set A) := S.subring

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] :
integral_domain (integral_closure R A) := @subring.domain A _ _ (foo _ _)

works

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:35):

i.e. I just feed it the things it can't find

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:36):

Nice! what purpose does the @ character serve?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:36):

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] :
integral_domain (integral_closure R A) := @subring.domain A _ (integral_closure R A) _

@ means "forget {} and [] and just tell me every input"

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:37):

Ohh that makes sense

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:37):

It's exactly the same problem as before. You want to prove integral_domain (integral_closure R A) and you want to use subring.domain.

#check @subring.domain
/-
subring.domain :
  Π {D : Type u_1} [_inst_3 : integral_domain D] (S : set D) [_inst_4 : is_subring S], integral_domain ↥S
-/

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:39):

Lean asks you for S which is in your case some kind of coercion of integral_closure R A to a set, i.e. to a term of type set D for some D, but Lean doesn't have a clue what D is.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:39):

If it knew it had to find a coercion to set A it could do it (indeed, my second solution is doing just that).

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:41):

But until you tell it it's looking for a coercion to set ?m_1 and it can't find one for some reason.

view this post on Zulip Alex Mathers (Mar 30 2020 at 20:42):

I see. so by using @ you are allowed to enter the first implicit argument A which I guess basically tells Lean that we are meant to consider integral_closure R A as an element of set A, then it finds the previously defined coercion to do this on its own

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:45):

Exactly. And using my new toy

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

instance (R : Type*) [comm_ring R] {A : Type*} [integral_domain A] [algebra R A] :
integral_domain (integral_closure R A) := subring.domain (integral_closure R A) -- fails

we can see from the debugging output that indeed the unifier is failing to find the coercion when the metavariable is in place:

[type_context.is_def_eq_detail] [1]: subalgebra R A =?= set ?m_1
[type_context.is_def_eq_detail] unfold right: set
[type_context.is_def_eq_detail] [2]: subalgebra R A =?= ?m_1 → Prop
[type_context.is_def_eq_detail] on failure: subalgebra R A =?= ?m_1 → Prop
[type_context.is_def_eq] subalgebra R A =?= set ?m_1 ... failed  (approximate mode)

view this post on Zulip Reid Barton (Mar 30 2020 at 20:47):

Is that failing to find a coercion or simply checking that the two sides are not defeq (without a coercion)?

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:48):

Oh man, looking at this debugging output it even seems to get so close!

[type_context.is_def_eq_detail] [7]: has_coe_to_sort.coe (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] [8]: (λ (s : set A), {x // x ∈ s}) (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] after whnf_core: {x // x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))} =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] process_assignment ?m_1 := A
[type_context.is_def_eq_detail] assign: ?m_1 := A
[type_context.is_def_eq_detail] [9]: x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= x ∈ ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] [10]: set ?m_1 =?= set A
[type_context.is_def_eq_detail] assign: ?m_1 := has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq] integral_domain ↥(integral_closure R A) =?= integral_domain ↥?m_2 ... success  (approximate mode)

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:49):

I don't know how to read these logs, I only started looking at them today.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 20:51):

https://gist.github.com/kbuzzard/b8c86cfd46b5253c4888979078ba1f00


Last updated: May 11 2021 at 12:15 UTC