Integer absolute difference

Stream: mathlib4

[Chris Bailey]

I'm writing some code that involves SI units and does some conversion, an example is converting some quantity base which is in a more coarse unit to a more fine unit, where the base quantity is always an integer:

    -- quantity coarse fine : Int
    quantity * (10 ^ (coarse - fine).natAbs)

When I have to reason about this later, I encounter enough resistance that I feel like I'm not using Mathlib effectively. The issues arise from goals like R (.. * 10 ^ x) (.. * 10 ^ y) where x and y have some relationship that can eventually be shown with enough work. Is there a more idiomatic way to work with the absolute difference of two integers when it needs to be used as an exponent?

[Kim Morrison]

Why not work in a field where you don't need Nat in the exponent?

[Chris Bailey]

I think because the return type needs to be an Int. This is in a larger CS context that uses Int for everything else.

[Eric Wieser]

Do you really want the absolute value there? If fine is greater than coarse, then the result is nonsense, right?

[Eric Wieser]

docs#Int.toNat might be easier to work with if you don't care about the junk value anyway

[Chris Bailey]

The actual function requires a hypothesis fine <= coarse.

[Chris Bailey]

It's sort of nonsense in that it's known to be non-negative; I previously had a match on the result of the subtraction that was

| Int.ofNat n => n
| Int.negSucc => False.elim ...

But that wasn't much easier to use.

[Kyle Miller]

I guess mathlib has docs#Nat.dist (nevermind, I didn't see that course fine : Int)

[Yaël Dillies]

You have docs#Int.natAbs, if you didn't know about it