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 :=
  dunfold has_one.one multiplicative.mul_one_class,
  refl,  -- ok

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):


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