defeq of `NormedAddCommGroup ℂ`

Stream: mathlib4

[Tomas Skrivan]

If you turn on set_option trace.Meta.Tactic.simp.discharge true you see an error

            [Meta.Tactic.fun_prop.discharge] @differentiable_const, failed to assign instance
                  NormedAddCommGroup ℂ
                sythesized value
                  Complex.instNormedAddCommGroupComplex
                is not definitionally equal to
                  NonUnitalNormedRing.toNormedAddCommGroup

It looks like that Complex.instNormedAddCommGroupComplex and NonUnitalNormedRing.toNormedAddCommGroup are not defeq under "reducible and instances" transparency.

I'm not exactly sure what to do about it. One way to fix this would be to remove this defeq check or loosen the transparency but I'm just doing the same thing Lean's simplifier is doing. Doing something different might not be a good idea.

Other option is that this is actually mathlib's problem how it sets up instances. But so far I do not really understand what is going wrong in the defeq check.

[Tomas Skrivan]

I have two instances of NormedAddCommGroup ℂ that are not defeq under "reducible and instances" transparency. The trace suggests that the check fails on norm =?= ⇑Complex.abs but when I try that alone it works. What is going on?

import Lean
import Qq
import Mathlib.Analysis.Complex.Basic

open Lean Meta Qq
-- set_option trace.Meta.isDefEq true

-- error: not defeq
#eval show MetaM Unit from do

  let a := q(NonUnitalNormedRing.toNormedAddCommGroup : NormedAddCommGroup ℂ)
  let b := q(Complex.instNormedAddCommGroupComplex : NormedAddCommGroup ℂ)

  if (← withReducibleAndInstances <| isDefEq a b) then
    IO.println "are defeq"
  else
    throwError "not defeq"


-- are defeq
#eval show MetaM Unit from do

  let a := q(norm : ℂ → ℝ)
  let b := q(Complex.abs : ℂ → ℝ)

  if (← withReducibleAndInstances <| isDefEq a b) then
    IO.println "are defeq"
  else
    throwError "not defeq"

[Jireh Loreaux]

I think @Matthew Ballard has been telling us we have a reducible transparency issue throughout our hierarchy, perhaps he knows that answer to this.

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/defeq.20of.20.60NormedAddCommGroup.20.E2.84.82.60 the correct topic, BTW

[Notification Bot]

3 messages were moved here from #mathlib4 > fun_prop issues by Jireh Loreaux.

[Matthew Ballard]

It’s already mathlib’s problem because simp isn’t changing.

[Tomas Skrivan]

I see so before mathlib fixes this I will just changes the defeq transparency level in fun_prop.

[Eric Rodriguez]

Is it a fixable problem Matthew?

[Eric Wieser]

I think the issue is src#AddGroupNorm.toNormedAddCommGroup which should be reducible

[Eric Wieser]

(but isn't)

[Eric Wieser]

I tested with:

example :
  (NonUnitalNormedRing.toNormedAddCommGroup : NormedAddCommGroup ℂ) =
    Complex.instNormedAddCommGroupComplex := by
  with_reducible_and_instances
    unfold Complex.instNormedAddCommGroupComplex
    -- unfold NonUnitalNormedRing.toNormedAddCommGroup
    unfold AddGroupNorm.toNormedAddCommGroup
    -- unfold Complex.abs Complex.normSq
    rfl

(adding unfolds until the rfl worked)

[Eric Wieser]

#10726

[Jireh Loreaux]

i think all of these were marked @[to_additive (attr := reducible)]. Why do we need abbrev?

[Eric Wieser]

Oh, I missed that.

[Eric Wieser]

I think the answer is that only some of them were marked reducible, but I didn't notice because it was hidden between docstrings

[Eric Wieser]

It's possible that abbrev is broken with to_additive? I didn't check

[Jireh Loreaux]

will abbrev get passed on to to_additive?

[Junyan Xu]

Apparently yes, e.g. docs#AddMonCat.AssocAddMonoidHom

[Eric Rodriguez]

doesn't seem to have @[inline, reducible]

[Eric Wieser]

How can you check?

[Eric Rodriguez]

it doesn't appear on docgen but I guess you're right

[Eric Rodriguez]

:(

[Eric Rodriguez]

guess it can be checked by doing a defeq check manually

[Eric Rodriguez]

this weird thing about attributes is annoyign

[Matthew Ballard]

Did we already figure out this is fixed by deleting the to_additive and adding a reducible AddGroupNorm.toNormedAddCommGroup by hand?

[Matthew Ballard]

Ah ok. to_additive and abbrev don’t get along which is probably why have to feed attributes to to_additive directly anyway!

[Matthew Ballard]

So if Eric changes from abbrev to to_additive (attr := reducible) we are good here

[Eric Wieser]

Feel free to push that change, I might not get around to it today

[Eric Wieser]

Matthew Ballard said:

Ah ok. to_additive and abbrev don’t get along which is probably why have to feed attributes to to_additive directly anyway!

Maybe we should have a linter for this, though maybe that's harder than fixing it

[Matthew Ballard]

I pushed changes. Two fixes required:

1. delete some stuff :octopus:
2. addresses a porting note (I think)

Currently benchmarking. It would good if someone(s) could carefully go over the changes in Analysis.Normed.Group.Basic to make sure nothing was missed, both in terms of def’s that should be reducible and with actually implementing the changes.

Also someone with familiarity with docs#Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable who can find a more elegant proof now that docs#ContinuousLinearMap.coe_restrictScalars’ fires simp would be a great help!

[Matthew Ballard]

Ok mathlib3 proof is what works for 2.