instance priorities

Stream: general

[Kenny Lau]

import algebra.ring

universe u

local attribute [priority 1] ring.to_monoid
local attribute [priority 2000] group.to_monoid

variables {G : Type u} [group G]

set_option trace.class_instances true
#check (by apply_instance : monoid G)

[Kenny Lau]

one would expect group.to_monoid to have higher priority than ring.to_monoid right

[Kenny Lau]

but the trace looks like this:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : monoid G := @ring.to_monoid ?x_1 ?x_2
[class_instances] (1) ?x_2 : ring G := @domain.to_ring ?x_3 ?x_4
[class_instances] (2) ?x_4 : domain G := @integral_domain.to_domain ?x_5 ?x_6
[class_instances] (1) ?x_2 : ring G := @comm_ring.to_ring ?x_3 ?x_4
[class_instances] (2) ?x_4 : comm_ring G := @integral_domain.to_comm_ring ?x_5 ?x_6
[class_instances] (2) ?x_4 : comm_ring G := @nonzero_comm_ring.to_comm_ring ?x_5 ?x_6
[class_instances] (3) ?x_6 : nonzero_comm_ring G := @integral_domain.to_nonzero_comm_ring ?x_7 ?x_8
[class_instances] (0) ?x_0 : monoid G := @ring_hom.monoid ?x_1 ?x_2
failed is_def_eq
[class_instances] (0) ?x_0 : monoid G := @semiring.to_monoid ?x_3 ?x_4
[class_instances] (1) ?x_4 : semiring G := @nonzero_semiring.to_semiring ?x_5 ?x_6
[class_instances] (2) ?x_6 : nonzero_semiring G := @nonzero_comm_semiring.to_nonzero_semiring ?x_7 ?x_8
[class_instances] (3) ?x_8 : nonzero_comm_semiring G := @nonzero_comm_ring.to_nonzero_comm_semiring ?x_9 ?x_10
[class_instances] (4) ?x_10 : nonzero_comm_ring G := @integral_domain.to_nonzero_comm_ring ?x_11 ?x_12
[class_instances] (1) ?x_4 : semiring G := @ring.to_semiring ?x_5 ?x_6
[class_instances] (2) ?x_6 : ring G := @domain.to_ring ?x_7 ?x_8
[class_instances] (3) ?x_8 : domain G := @integral_domain.to_domain ?x_9 ?x_10
[class_instances] (2) ?x_6 : ring G := @comm_ring.to_ring ?x_7 ?x_8
[class_instances] (3) ?x_8 : comm_ring G := @integral_domain.to_comm_ring ?x_9 ?x_10
[class_instances] (3) ?x_8 : comm_ring G := @nonzero_comm_ring.to_comm_ring ?x_9 ?x_10
[class_instances] (4) ?x_10 : nonzero_comm_ring G := @integral_domain.to_nonzero_comm_ring ?x_11 ?x_12
[class_instances] (1) ?x_4 : semiring G := @comm_semiring.to_semiring ?x_5 ?x_6
[class_instances] (2) ?x_6 : comm_semiring G := @nonzero_comm_semiring.to_comm_semiring ?x_7 ?x_8
[class_instances] (3) ?x_8 : nonzero_comm_semiring G := @nonzero_comm_ring.to_nonzero_comm_semiring ?x_9 ?x_10
[class_instances] (4) ?x_10 : nonzero_comm_ring G := @integral_domain.to_nonzero_comm_ring ?x_11 ?x_12
[class_instances] (2) ?x_6 : comm_semiring G := @comm_ring.to_comm_semiring ?x_7 ?x_8
[class_instances] (3) ?x_8 : comm_ring G := @integral_domain.to_comm_ring ?x_9 ?x_10
[class_instances] (3) ?x_8 : comm_ring G := @nonzero_comm_ring.to_comm_ring ?x_9 ?x_10
[class_instances] (4) ?x_10 : nonzero_comm_ring G := @integral_domain.to_nonzero_comm_ring ?x_11 ?x_12
[class_instances] (0) ?x_0 : monoid G := @group.to_monoid ?x_1 ?x_2
[class_instances] (1) ?x_2 : group G := _inst_1

[Kenny Lau]

so what exactly does setting priorities do?

[Chris Hughes]

Try local attribute [instance, priority 1]

[Chris Hughes]

All of the attributes have a priority setting, I don't think Lean knows you mean the instance priority.

[Kenny Lau]

aha

[Kenny Lau]

thanks

[Kevin Buzzard]

Can I change simp priority to change the behaviour of the simplifier?

[Chris Hughes]

I think you can, but I'm not sure how useful this is. It's still going to apply every lemma it can, but in a different order, and if that makes a difference to what you end up with, then you have a non normalising simp.

[Chris Hughes]

Also, I think it still simplifies the deepest sub expressions it can first, this ordering takes priority over the ordering given by setting the priority. I vaguely remember a conversation about this.

[Kevin Buzzard]

Oh I see, because simp is supposed to be a confluent rewriting system it shouldn't matter what order things get done in

[Johan Commelin]

Chris Hughes said:

I think you can, but I'm not sure how useful this is. It's still going to apply every lemma it can, but in a different order, and if that makes a difference to what you end up with, then you have a non normalising simp.

It can matter... if you greedily simplify ring_hom.of bla then later on you have to do typeclass resolution to apply is_ring_hom.map_add, whereas ring_hom.map_add is a no-brainer for simp. So I would like to simplify ring_hom.of f x = f x as late as possible.

[Chris Hughes]

Even with priorities, because it simplifies the deepest subexpression first it will still greedily simplify ring_hom.of bla before applying ring_hom.map_add