Zulip Chat Archive

Stream: general

Topic: Diamond in multiplicative nat

Eric Wieser (Jan 04 2022 at 15:54):

What's going on with this diamond, and why is dunfold enough to solve it?

import algebra.group.type_tags
import data.nat.basic

example :
  @monoid.to_mul_one_class (multiplicative ℕ) (comm_monoid.to_monoid _) =
    multiplicative.mul_one_class :=
rfl -- fails

example :
  @monoid.to_mul_one_class (multiplicative ℕ) (comm_monoid.to_monoid _) =
    multiplicative.mul_one_class :=
begin
  dunfold has_one.one multiplicative.mul_one_class,
  refl,  -- ok
end

Anne Baanen (Jan 04 2022 at 15:55):

Could you post a trace.type_context.is_def_eq_detail trace? I assume it's either something irreducible blocking unification, or is_def_eq going down the wrong path and committing to it.

Eric Wieser (Jan 04 2022 at 15:56):

Sure:

[type_context.is_def_eq_detail] process_assignment ?m_1 := ℕ
[type_context.is_def_eq_detail] assign: ?m_1 := ℕ
[type_context.is_def_eq_detail] [1]: monoid (multiplicative ℕ) =?= monoid ?m_1
[type_context.is_def_eq_detail] [2]: monoid =?= monoid
[type_context.is_def_eq_detail] process_assignment ?m_1 := multiplicative ℕ
[type_context.is_def_eq_detail] assign: ?m_1 := multiplicative ℕ
[type_context.is_def_eq_detail] process_assignment ?m_1 := multiplicative ℕ
[type_context.is_def_eq_detail] assign: ?m_1 := multiplicative ℕ
[type_context.is_def_eq_detail] process_assignment ?m_1 := multiplicative.comm_monoid
[type_context.is_def_eq_detail] [1]: comm_monoid ?m_1 =?= comm_monoid (multiplicative ℕ)
[type_context.is_def_eq_detail] [2]: comm_monoid =?= comm_monoid
[type_context.is_def_eq_detail] assign: ?m_1 := multiplicative.comm_monoid
[type_context.is_def_eq_detail] [1]: monoid ?m_1 =?= monoid (multiplicative ℕ)
[type_context.is_def_eq_detail] [2]: monoid =?= monoid
[type_context.is_def_eq_detail] [2]: multiplicative ℕ =?= multiplicative ℕ
[type_context.is_def_eq_detail] process_assignment ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [1]: mul_one_class (multiplicative ℕ) =?= mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [2]: mul_one_class =?= mul_one_class
[type_context.is_def_eq_detail] [2]: multiplicative ℕ =?= multiplicative ℕ
[type_context.is_def_eq_detail] process_assignment ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [1]: mul_one_class (multiplicative ℕ) =?= mul_one_class (multiplicative ?m_1)
[type_context.is_def_eq_detail] [2]: mul_one_class =?= mul_one_class
[type_context.is_def_eq_detail] [2]: multiplicative ℕ =?= multiplicative ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := ℕ
[type_context.is_def_eq_detail] assign: ?m_1 := ℕ
[type_context.is_def_eq_detail] process_assignment ?m_1 := add_monoid.to_add_zero_class ℕ
[type_context.is_def_eq_detail] [1]: add_zero_class ?m_1 =?= add_zero_class ℕ
[type_context.is_def_eq_detail] [2]: add_zero_class =?= add_zero_class
[type_context.is_def_eq_detail] assign: ?m_1 := add_monoid.to_add_zero_class ℕ
[type_context.is_def_eq_detail] [1]: mul_one_class (multiplicative ?m_1) =?= mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [2]: mul_one_class =?= mul_one_class
[type_context.is_def_eq_detail] [2]: multiplicative ?m_1 =?= multiplicative ℕ
[type_context.is_def_eq_detail] process_assignment ?m_1 := multiplicative.mul_one_class
[type_context.is_def_eq_detail] assign: ?m_1 := multiplicative.mul_one_class
[type_context.is_def_eq_detail] [1]: monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class =?= ?m_7 = ?m_7
[type_context.is_def_eq_detail] [2]: eq =?= eq
[type_context.is_def_eq_detail] process_assignment ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] process_assignment ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [2]: multiplicative.mul_one_class =?= monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [3]: {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _} =?= {one := monoid.one (comm_monoid.to_monoid (multiplicative ℕ)),
 mul := monoid.mul (comm_monoid.to_monoid (multiplicative ℕ)),
 one_mul := _,
 mul_one := _}
[type_context.is_def_eq_detail] [4]: mul_one_class.mk =?= mul_one_class.mk
[type_context.is_def_eq_detail] [4]: 1 =?= monoid.one
[type_context.is_def_eq_detail] [5]: ⇑multiplicative.of_add 0 =?= comm_monoid.one
[type_context.is_def_eq_detail] unfold left: coe_fn
[type_context.is_def_eq_detail] [6]: has_coe_to_fun.coe multiplicative.of_add 0 =?= comm_monoid.one
[type_context.is_def_eq_detail] [7]: multiplicative.of_add.to_fun 0 =?= monoid.one
[type_context.is_def_eq_detail] [8]: (λ (x : ?m_1), x) 0 =?= 1
[type_context.is_def_eq_detail] after whnf_core: 0 =?= 1
[type_context.is_def_eq_detail] on failure: {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _} =?= {one := monoid.one (comm_monoid.to_monoid (multiplicative ℕ)),
 mul := monoid.mul (comm_monoid.to_monoid (multiplicative ℕ)),
 one_mul := _,
 mul_one := _}
[type_context.is_def_eq_detail] on failure: monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class =?= ?m_7 = ?m_7
[type_context.is_def_eq_detail] [1]: ?m_2 = ?m_2 =?= monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] [2]: eq =?= eq
[type_context.is_def_eq_detail] process_assignment ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] process_assignment ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [2]: monoid.to_mul_one_class (multiplicative ℕ) =?= multiplicative.mul_one_class
[type_context.is_def_eq_detail] [3]: {one := monoid.one (comm_monoid.to_monoid (multiplicative ℕ)),
 mul := monoid.mul (comm_monoid.to_monoid (multiplicative ℕ)),
 one_mul := _,
 mul_one := _} =?= {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _}
[type_context.is_def_eq_detail] [4]: mul_one_class.mk =?= mul_one_class.mk
[type_context.is_def_eq_detail] [4]: monoid.one =?= 1
[type_context.is_def_eq_detail] [5]: comm_monoid.one =?= ⇑multiplicative.of_add 0
[type_context.is_def_eq_detail] unfold right: coe_fn
[type_context.is_def_eq_detail] [6]: comm_monoid.one =?= has_coe_to_fun.coe multiplicative.of_add 0
[type_context.is_def_eq_detail] [7]: monoid.one =?= multiplicative.of_add.to_fun 0
[type_context.is_def_eq_detail] [8]: 1 =?= (λ (x : ?m_1), x) 0
[type_context.is_def_eq_detail] after whnf_core: 1 =?= 0
[type_context.is_def_eq_detail] on failure: {one := monoid.one (comm_monoid.to_monoid (multiplicative ℕ)),
 mul := monoid.mul (comm_monoid.to_monoid (multiplicative ℕ)),
 one_mul := _,
 mul_one := _} =?= {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _}
[type_context.is_def_eq_detail] on failure: ?m_2 = ?m_2 =?= monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] process_assignment ?x_1 := monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] assign: ?x_1 := monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] process_assignment ?x_0 := ?m_2 = ?m_2
[type_context.is_def_eq_detail] assign: ?x_0 := ?m_2 = ?m_2
[type_context.is_def_eq_detail] [1]: ?m_2 = ?m_2 =?= monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] [2]: eq =?= eq
[type_context.is_def_eq_detail] process_assignment ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] process_assignment ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] assign: ?m_1 := monoid.to_mul_one_class (multiplicative ℕ)
[type_context.is_def_eq_detail] [2]: monoid.to_mul_one_class (multiplicative ℕ) =?= multiplicative.mul_one_class
[type_context.is_def_eq_detail] [3]: {one := monoid.one (comm_monoid.to_monoid (multiplicative ℕ)),
 mul := monoid.mul (comm_monoid.to_monoid (multiplicative ℕ)),
 one_mul := _,
 mul_one := _} =?= {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _}
[type_context.is_def_eq_detail] [4]: mul_one_class.mk =?= mul_one_class.mk
[type_context.is_def_eq_detail] [4]: monoid.one =?= 1
[type_context.is_def_eq_detail] [5]: comm_monoid.one =?= ⇑multiplicative.of_add 0
[type_context.is_def_eq_detail] unfold right: coe_fn
[type_context.is_def_eq_detail] [6]: comm_monoid.one =?= has_coe_to_fun.coe multiplicative.of_add 0
[type_context.is_def_eq_detail] [7]: monoid.one =?= multiplicative.of_add.to_fun 0
[type_context.is_def_eq_detail] [8]: 1 =?= (λ (x : ?m_1), x) 0
[type_context.is_def_eq_detail] after whnf_core: 1 =?= 0
[type_context.is_def_eq_detail] on failure: {one := monoid.one (comm_monoid.to_monoid (multiplicative ℕ)),
 mul := monoid.mul (comm_monoid.to_monoid (multiplicative ℕ)),
 one_mul := _,
 mul_one := _} =?= {one := 1, mul := has_mul.mul multiplicative.has_mul, one_mul := _, mul_one := _}
[type_context.is_def_eq_detail] on failure: ?m_2 = ?m_2 =?= monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] process_assignment ?x_1 := monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] assign: ?x_1 := monoid.to_mul_one_class (multiplicative ℕ) = multiplicative.mul_one_class
[type_context.is_def_eq_detail] process_assignment ?x_0 := ?m_2 = ?m_2
[type_context.is_def_eq_detail] assign: ?x_0 := ?m_2 = ?m_2

Eric Wieser (Jan 04 2022 at 16:04):

Interestingly I can fix it by adding one := 1 in a few places, but then the dunfold version breaks instead!

Anne Baanen (Jan 04 2022 at 16:05):

docs#multiplicative docs#multiplicative.comm_monoid

Anne Baanen (Jan 04 2022 at 16:08):

It's a bit weird that it gives up on 1 =?= 0 without delta-reducing, since both sides should be projections out of a known structure.

Eric Wieser (Jan 04 2022 at 16:12):

Yeah, it's very weird

Eric Wieser (Jan 04 2022 at 16:12):

I made #11240 to try out a fix, but maybe it's worth fixing a deeper problem here

Reid Barton (Jan 04 2022 at 16:30):

More minimized version, using the expression where whnf got stuck:

import algebra.group.type_tags
import data.nat.basic

set_option trace.type_context.is_def_eq_detail true
set_option pp.all true

#check (rfl : @has_one.one.{0} (multiplicative.{0} nat)
  (@multiplicative.has_one.{0} nat
     (@add_zero_class.to_has_zero.{0} nat
        (@add_monoid.to_add_zero_class.{0} nat (@add_comm_monoid.to_add_monoid.{0} nat nat.add_comm_monoid))))
     = nat.zero)

I can't see any irreducibility setting which would interfere with reducing the left hand side, so it looks like an elaborator bug. The left hand side does #reduce to nat.zero.

Last updated: Dec 20 2023 at 11:08 UTC