Zulip Chat Archive

Stream: general

Topic: has_inv.to_has_abs

Yury G. Kudryashov (Jun 01 2022 at 02:54):

I've just noticed that we have docs#has_inv.to_has_abs. Why Lean doesn't try to use this instance when I write |(1 : real)|?

Yury G. Kudryashov (Jun 01 2022 at 02:55):

More precisely, I have two questions.

  1. Why do we need the multiplicative version?
  2. Why it doesn't create issues?

Yaël Dillies (Jun 01 2022 at 07:28):

cc @Christopher Hoskin

Yaël Dillies (Jun 01 2022 at 07:31):

I know of the situation but I don't really understand what Christopher is doing. In my limited understanding, a new typeclass notation ∣ ∣ₘ would solve the problem without impeding Christopher's progress. It would also make it clearer that mabs refers to the multiplicative absolute value in the naming convention.

Eric Wieser (Jun 01 2022 at 09:08):

It's possible the multiplicative version was added as autopilot; maybe Christopher can comment whether it also appears in the literature

Floris van Doorn (Jun 01 2022 at 09:18):

It feels a little sketchy that the correctness of abs is purely a consequence of our instance priorities...

import data.rat.order
attribute [priority 1001, instance] has_inv.to_has_abs
#eval abs ((1 : ℚ) / 2) -- 2

Floris van Doorn (Jun 01 2022 at 09:23):

It was introduced in #9172

Johan Commelin (Jun 01 2022 at 10:17):

My apologies for merging it like that.

Johan Commelin (Jun 01 2022 at 10:18):

I think @Yaël Dillies has a good suggestion for a fix. I can try to implement it later this week, but I don't have much time.

Floris van Doorn (Jun 01 2022 at 10:42):

Johan Commelin said:

My apologies for merging it like that.

No worries! It's hard to recognize all potential problems in a PR. And as far as I know the instance never actually caused a problem.

Gabriel Ebner (Jun 01 2022 at 10:43):

I believe @Alex J. Best has a linter lying around in a branch that would have caught this diamond.

Alex J. Best (Jun 01 2022 at 10:51):

Right, I'm not sure if the most recent version works well enough to catch this or not, but I made some experiments a few months ago at branch#alexjbest/diamond-linter. I would like to come back to it at some point :smile:

Christopher Hoskin (Jun 01 2022 at 20:46):

Eric Wieser said:

It's possible the multiplicative version was added as autopilot; maybe Christopher can comment whether it also appears in the literature

This has come up a few times now. I have no interest in the multiplicative case - I only added it because someone requested it in the review of the original PR. I'll see if I can find the time to put in a PR to remove it in the next few days (but if someone wants to jump in before me and do it, that's fine with me.)

Eric Wieser (Jun 01 2022 at 20:59):

It looks like #9172 introduced the offending instance, which was previously a more harmless mabs definition introduced in #8673

Christopher Hoskin (Jun 24 2022 at 07:10):

@Alex J. Best How would I invoke your linter? Naively I tried:

import tactic.lint.diamond_linter_experiments

run_cmd find_diamonds `algebra_nat` prod.algebra

But that errors with:

(algebra_nat, prod.algebra)
algebra_nat
prod.algebra ℕ ?m_1 ?m_2

What do algebra_nat and prod.algebra represent?

Christopher Hoskin (Jun 24 2022 at 08:07):

Here is one of the previous conversations about this: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Positive.20parts

Alex J. Best (Jun 24 2022 at 21:58):

That is the correct syntax, but the output there isn't an error, its just not finding any issues. I guess there is an issue with those two instances but the linter isn't smart enough to find it yet?

Last updated: Dec 20 2023 at 11:08 UTC