No more `Abs`?

Stream: mathlib4

[Geoffrey Irving]

Did the Abs class go away entirely in cc7c881ae6e0d65a366d58016d7b253d43996c99? I have a computational type that implemented Abs, and I'm not sure if I get to keep clean |x| notation.

[Geoffrey Irving]

Cc @Yaël Dillies

[Geoffrey Irving]

Ah, it's called PosPart now? :upside_down:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Group/PosPart.html#PosPart

[Geoffrey Irving]

As a general docs ergonomics note, I'm finding it very difficult to work out where abs is defined. So far I'm about 10 minutes into the search.

[Ruben Van de Velde]

Loogle says

abs Mathlib.Algebra.Order.Group.Abs
{α : Type u_1} → [inst : Lattice α] → [inst : AddGroup α] → α → α

[Geoffrey Irving]

Ah, excellent. Which does mean I don't get to use nice notation anymore, since I want to do a custom computational implementation. :/

[Geoffrey Irving]

It's quite nice for computational types when Mathlib has a per-operation type class, since it means one can do custom stuff and prove the necessary lemmas for interfacing with standard theorems.

[Eric Wieser]

I think a good feature request in that direction would be specialized csimp lemmas

[Eric Wieser]

Right now you can only provide a computational alternative for foo, not foo Nat

[Geoffrey Irving]

Fair, but Abs was working just fine before the mentioned commit. Usually the lemmas I need to prove are trivial, so the thing that makes things nice is just having those per-operation type classes.

[Geoffrey Irving]

+, -, *, /, etc. are already nice.

[Geoffrey Irving]

Indeed, I don't think the csimp thing could ever work in my case, as the computational type is not nice enough for AddGroup (it has nan values). And this is a quite generic problem: a computational type with error conditions that make it approximate but not exactly match a mathematical structure.

[Eric Wieser]

Oh, i see; your problem was not wanting an "efficient" abs, but that you can't satisfy the requirements of docs#abs anymore because it assumes lawfulness?

[Geoffrey Irving]

Yes.

[Eric Wieser]

In that case I agree that we should probably restore the old Abs typeclass

[Eric Wieser]

(though perhaps docs#Norm is fine for you)

[Geoffrey Irving]

The result of norm is ℝ, and thus noncomputable.

[Eric Wieser]

Whoops, I was falsely imagining we'd generalized that.

[Geoffrey Irving]

It's probably getting off-topic, but I'm curious: if we generalize appropriately, why should abs and norm be different?

[Eric Wieser]

I think the difficulty in generalizing is the main reason; as soon as you make norm : α → β, then the elaborator has to solve for β in far more places

[Kevin Buzzard]

Isn't abs : X -> X and norm : X -> \R so they represent slightly different ideas.

[Yaël Dillies]

Geoffrey Irving said:

As a general docs ergonomics note, I'm finding it very difficult to work out where abs is defined. So far I'm about 10 minutes into the search.

What were you trying? I'm 10sec in and I get this.

[Yaël Dillies]

It's true that you used to be able to click on notation. We lost that we going to Lean 4.

[Yaël Dillies]

Sorry about removing the Abs typeclass. I looked everywhere around and I could only find one instance of it (well actually two and they were creating a non-propeq diamond!) so I removed the typeclass. This has the advantage of giving you a meaningful jump-to-definition and a meaningful hover. It also reduces typeclass search (although the reduction should be fringe here).

[Yaël Dillies]

If you just want it for one type, you can simply create your own copy of the | | notation and make it elaborate correctly for your computational type.

[Geoffrey Irving]

Yaël Dillies said:

Geoffrey Irving said:

As a general docs ergonomics note, I'm finding it very difficult to work out where abs is defined. So far I'm about 10 minutes into the search.

What were you trying? I'm 10sec in and I get this.

Hmm, I also get that now, so not sure what I was doing wrong. Possibly I was being dense and searching for things like Reals.abs only.

[Geoffrey Irving]

^ I think the can't-click-on-notation thing was the core problem: I think I was implicitly assuming it was still a typeclass and thus not expecting it to exist as a standalone function, and all the abs lemmas are expressed in notation.

[Yaël Dillies]

Even if it were still a typeclass, searching for abs would have picked up Abs and Abs.abs.

[Geoffrey Irving]

Screenshot-2024-01-22-at-1.17.08PM.png

[Geoffrey Irving]

Only the lowercase search works in mathlib4 docs.

[Yaël Dillies]

Yeah so upper-case letters in a search only match upper-case letters, but lowercase letters match both lower-case and upper-case.

[Geoffrey Irving]

That's useful to know!

[Yaël Dillies]

In particular, lower-case is the way to go if you are not sure that what you're searching for is upper-case.

[Emilie (Shad Amethyst)]

That should probably be written somewhere, I had no idea that was the case

[Damiano Testa]

By the way, should the outputs below display all as 3? And not error?

import Mathlib

-- best
#eval abs (- 3 : Rat)
-- 3

-- ok
#reduce abs (- 3 : Int)
-- Int.ofNat 3

-- sub-par
#reduce abs (- 3 : Rat)
-- Rat.mk' (Int.ofNat 3) 1

-- error
#eval abs (- 3 : Int)
/-
failed to compile definition, consider marking it as 'noncomputable'
because it depends on 'instConditionallyCompleteLinearOrderInt',
and it does not have executable code
-/

[Mario Carneiro]

All of those outputs are expected

[Damiano Testa]

They may be expected, but I can try arguing that they are not all ideal...

[Mario Carneiro]

the first three are because #reduce reduces the expression to constructors, and the constructor of Int is Int.ofNat and the constructor of Rat is Rat.mk'

[Mario Carneiro]

the 3 there is a raw nat literal

[Mario Carneiro]

so it only works on Nat

[Damiano Testa]

Notice that the very first one is #eval, though, not #reduce.

[Mario Carneiro]

Actually the last one seems a bit odd, it should be computable

[Mario Carneiro]

I thought it was over reals

[Mario Carneiro]

I'm willing to bet that it works if you import less

[Damiano Testa]

Over the reals it gives a cauchy sequence, it is not that bad, actually.

[Damiano Testa]

Mario Carneiro said:

I'm willing to bet that it works if you import less

Indeed:

import Mathlib.Algebra.Order.Group.Abs
import Mathlib.Data.Int.Basic

#eval abs (- 3 : Int)
-- 3

[Mario Carneiro]

which means there is an instance priority issue

[Damiano Testa]

#synth Lattice Int
--  with `import Mathlib`: `ConditionallyCompleteLattice.toLattice`
--  with minimal imports: `DistribLattice.toLattice`

[Eric Wieser]

Adding a Lattice Int instance after the DistribLattice instance is the standard fix here

[Eric Wieser]

If the available typeclasses are a graph, you need to ensure that you have a "shield" of shortcut instances between the noncomputable instance and all the computable base classes.

[Damiano Testa]

I'm trying this out in #9946.

[Damiano Testa]

I also think that the only noncomputability came from the file Mathlib/Data/Int/ConditionallyCompleteOrder that is imported by Mathlib only.

[Eric Wieser]

You should probably add a test at the end of that ConditionallyCompleteOrder file of example : DistribLattice \Z := inferInstance (outside of a noncomputable section!)

[Damiano Testa]

The computability of abs in Int should no longer depend on the imports!

[Eric Wieser]

Next question: is that true for Real?

[Eric Wieser]

(and should we redefine abs to need only Sup?)

[Yaël Dillies]

How could abs only need sup?

[Geoffrey Irving]

Presumably Eric means Sup and Neg.

[Eric Wieser]

Sorry, I mean neg + sup

[Yaël Dillies]

Yeah okay

[Eric Wieser]

Crucially, not Lattice

[Yaël Dillies]

It was actually the case until my refactor

[Eric Wieser]

Though maybe that still does the wrong thing for floats depending on what max x nan means :upside_down:

[Geoffrey Irving]

For floats you want to use a custom implementation, via the Abs typeclass.

[Yaël Dillies]

Relevant part of the diff: https://github.com/leanprover-community/mathlib4/commit/cc7c881ae6e0d65a366d58016d7b253d43996c99#diff-04fe7d4ab1d9e83e80baaa4ff56278e736e3ec0a4ddace3fa767ddc86c69821bL27-L29

[Geoffrey Irving]

But I should admit that the neg + sup implementation will also work fine, it’s just slower than a single bitwise &.

[Damiano Testa]

I wonder if the correct answer is to use #norm_num instead of #eval for these kind of computations:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

#norm_num (abs (- 3 : Rat))              -- |3|
#norm_num (abs (- 3.1 : Real))           -- |31 / 10|
#norm_num (abs (- Real.sqrt 3.1 : Real)) -- |Real.sqrt 31 / Real.sqrt 10|
#norm_num (abs (- - Real.pi : Real))     -- |Real.pi|

These all look fairly reasonable to me, except possibly #norm_num could realize that final |·| is superfluous, at least in some cases.