non-defeq instances

Stream: general

[Yury G. Kudryashov]

In #18082 I'm trying to use docs#option.map₂ here and there. The build fails claiming that 2 instances are not defeq. How can I test this? For some reason, all data fields are defeq (refl proves the equalities) but the whole instances aren't.

[Junyan Xu]

#18081

[Yaël Dillies]

Possible idea: option.map_2 has the matches swapped compared to what was before.
That doesn't really explain the data fields being defeq, though...

[Yury G. Kudryashov]

No, option.map₂ unfolds to exactly the same bind+map.

[Yury G. Kudryashov]

The only definition that changes defeq is with_top.mul_zero_class but it is not used here.

[Eric Wieser]

attribute [semireducible] with_zero makes them defeq:

import data.int.order.basic
import algebra.order.group.type_tags
import algebra.order.with_zero

local notation `ℤₘ₀` := with_zero (multiplicative ℤ)

attribute [semireducible] with_zero -- fails without this

example : @with_zero.mul_zero_one_class (multiplicative ℤ)
    (@multiplicative.mul_one_class ℤ (@add_monoid.to_add_zero_class ℤ int.add_monoid))
=
  @monoid_with_zero.to_mul_zero_one_class ℤₘ₀
    (@group_with_zero.to_monoid_with_zero ℤₘ₀
       (@comm_group_with_zero.to_group_with_zero ℤₘ₀
          (@linear_ordered_comm_group_with_zero.to_comm_group_with_zero ℤₘ₀
             (@with_zero.linear_ordered_comm_group_with_zero (multiplicative ℤ)
                (@multiplicative.linear_ordered_comm_group ℤ int.linear_ordered_add_comm_group)))))
 :=
begin
  refl,
end

[Yury G. Kudryashov]

Is with_zero irreducible?

[Eric Wieser]

Yes

[Yaël Dillies]

docs#with_zero says so

[Yury G. Kudryashov]

I see this now.

[Eric Wieser]

Does the test above fail on master?

[Eric Wieser]

I.e., has the instance path somehow changed, or is there something weird about one of our instances?

[Yury G. Kudryashov]

What are our plans for with_one/with_zero reducibility in Lean 4?

[Yaël Dillies]

They will probably get turned into one-field structures.

[Eric Wieser]

Or maybe opaque?

[Yaël Dillies]

Isn't that overkill?

[Yaël Dillies]

Currently, docs4#WithZero is still a regular def.

[Eric Wieser]

There's something pretty weird going on with my example above; try using

begin
  change _ = mul_zero_one_class.mk _ _ _ _ _ _ _,
  change mul_zero_one_class.mk _ _ _ _ _ _ _ = _, -- fails
end

The LHS doesn't reduce to a constructor application

[Eric Wieser]

dunfold with_zero.mul_zero_one_class, makes progress, but then congr doesn't work to equat the arguments!

[Eric Wieser]

This is how far I can get:

import data.int.order.basic
import algebra.order.group.type_tags
import algebra.order.with_zero

local notation `ℤₘ₀` := with_zero (multiplicative ℤ)

example : @with_zero.mul_zero_one_class (multiplicative ℤ)
    (@multiplicative.mul_one_class ℤ (@add_monoid.to_add_zero_class ℤ int.add_monoid))
=
  @monoid_with_zero.to_mul_zero_one_class ℤₘ₀
    (@group_with_zero.to_monoid_with_zero ℤₘ₀
       (@comm_group_with_zero.to_group_with_zero ℤₘ₀
          (@linear_ordered_comm_group_with_zero.to_comm_group_with_zero ℤₘ₀
             (@with_zero.linear_ordered_comm_group_with_zero (multiplicative ℤ)
                (@multiplicative.linear_ordered_comm_group ℤ int.linear_ordered_add_comm_group)))))
 :=
begin
  change _ = mul_zero_one_class.mk _ _ _ _ _ _ _,
  dunfold with_zero.mul_zero_one_class with_zero.linear_ordered_comm_group_with_zero,
  refine congr_fun _ _,
  refine congr_fun _ _,
  refine congr_fun _ _,
  dunfold
    with_zero.linear_ordered_comm_monoid_with_zero
    with_zero.comm_monoid_with_zero
    with_zero.mul_zero_class
    linear_ordered_comm_group_with_zero.to_comm_group_with_zero
    comm_group_with_zero.to_group_with_zero
    group_with_zero.to_monoid_with_zero
    monoid_with_zero.mul
    group_with_zero.mul
    comm_group_with_zero.mul
    linear_ordered_comm_monoid_with_zero.mul
    linear_ordered_comm_group_with_zero.mul
    comm_monoid_with_zero.mul
    mul_zero_one_class.mul
    mul_zero_class.mul
    monoid_with_zero.one
    group_with_zero.one
    comm_group_with_zero.one
    linear_ordered_comm_monoid_with_zero.one
    linear_ordered_comm_group_with_zero.one
    mul_zero_one_class.one,
  dsimp,
  sorry
end

[Eric Wieser]

I think with_zero.mul_zero_one_class is to blame

[Eric Wieser]

I pushed a fix

[Eric Wieser]

Perhaps we should turn on linter.check_type for generated lemmas

[Eric Wieser]

For instance, this fails:

run_cmd do
  d ← tactic.get_decl `with_zero.semigroup_with_zero._proof_1,
  none ← check_type d,
  tactic.skip

[Eric Wieser]

cc @Floris van Doorn, since you wrote that linter

[Floris van Doorn]

There was some discussion about this in the PR that added the linter #7694. There were some issues (false positives) with turning linter.check_type on for automatically generated lemmas. But it might be fine, so feel free to try if you think that is better.

[Eric Wieser]

It would be great if there wwere some way to adjust "run on automated lemmas" on a local basis