lib2.0 : `ℕᵇ `(binary) can be pure unlike `ℕ`.

[mechvel]

I recall it and return to pointing out that: in lib-2.0 the part of Data.Nat.Binary.Properties has several proofs that cannot be considered as reliable. Their badness is in that the proofs

(Ps)   +-assoc, +-comm, *-assoc, *-comm

and some other, rely on similar proofs for ℕ(unary representation) by using the isomoprphism to ℕ. But these proofs for ℕ are not implemented as the first class, are not reliable. Because Nat._+_ and Nat._*_ are implemented as built-in, not in Agda. So that these proofs for ℕ are not about the real algorithms for computing these operations.

And ℕᵇ is different. Its arithmetic is implemented totally in Agda. The corresponding proofs can also be implemented totally in Agda. In this sense, ℕᵇ is a better Agda model for natural numbers than ℕ. So that it is better to untie ℕᵇ from ℕ, because using proofs for ℕ spoils the purity of ℕᵇ.

[mechvel]

On 2024-04-14 22:29, G. Allais wrote:

Because Nat.+ and Nat.* are implemented as built-in, not in Agda.

That is incorrect: these definitions are implemented in Agda, and their proofs are using the Agda definition. It's only during compilation (when the proofs are getting erased anyway) that these definitions are substituted for their more efficient built-ins.

Something is wrong here. If it was in Agda, the module Data.Nat.Base would contain, for example,

+ : Op₂ ℕ -- algorithm "Plus" 0 + n = n suc m + n = suc (m + n)

Instead it contains

open import Agda.Builtin.Nat public  using (_+_ ...) ...

This actually means "believe that this built-in-+ returns the same result as the Plus program in Agda". This is postulation of that Plus is equivalent to this invisible built-in-+.

Binary._+_ is different, its Agda code is in the library written in Agda, nothing is postulated. Therefore Binary needs to have possibly fewer items taken from Nat.

[Taneb]

You can click through to Agda.Buildin.Nat and see exactly the definition you expected here

[JacquesCarette]

Right - Agda.Builtin.Nat is all in Agda, even though it says Builtin. The reason is that all Agda.Builtin are actually 'known' to Agda itself (for the purposes of reflection). It doesn't mean that they are 'builtin' in the usual sense of the word.

[gallais]

I deleted my original message because, even though _+_ is indeed defined in one of the builtin files and that's the definition used during proofs, there is also black magic in the compiler to make some of the nat functions compute faster:

https://github.com/agda/agda/blob/838fbdc7b018006cb01b354f1144139dd945c775/src/full/Agda/TypeChecking/Primitive.hs#L833-L845

So I think this is a somewhat legitimate complaint: this additional magic is used during conversion and so, in a sense, _+_ is not pure.

[mechvel]

On 2024-04-15 00:11, Nathan van Doorn wrote:

You can click through to Agda.Buildin.Nat and see exactly the definition you expected here [1]

I look into lib-2.0 and do not find the folder Agda in
~/agda/stLib/2.0/src/.

[Taneb]

That's because it's bundled with the compiler, not the standard library. The sources for these modules can be found in the repository for the agda compiler, and can be found here: https://github.com/agda/agda/tree/master/src/data/lib/prim

[mechvel]

(Sorry, probably this needs to be in Zulip)

I do not say that Agda.BuiltIn is not needed.
I am trying to show that one needs to avoid it in any case when this solution does not cost much.

Suppose that _+_ and _*_ are defined without using Agda.BuiltIn:

_+_ : Op₂ ℕ               -- algorithm "Plus"                                   
0     + n = n                                                                   
suc m + n = suc (m + n)                                                         
...                                                                             

Then, applying Agda interpreter to 15 ^ 10 ∸ 15 ^ 10 : ℕ
the user knows that each computation step of interpreter will be by pattern matching in the rules like in the definition Plus.
For each step the user can do this matching by hand.
Assuming that pattern matching in Agda is implemented correctly, the user is highly sure that that the above result is found correct.

But _+_ and _*_ are linked to Agda.BuiltIn...
There are tricky wise ways to multiply large numbers, and probably the algorithm for is complex enough in the gmp library.
The data representation is very different.
The method cannot be by a sequence of pattern matching as in Plus. Because in this case it would include billions of pattern matching acts in our example, with spending a great time, while in gmp it is exponentially faster.
And we also have to believe that this complicated algorithm for `__in gmp is correct. There is not any formal proof that gmp.* is correct, and the same is for the Agda pattern matching. But the latter is simpler, the data representation for ℕ is simpler than in gmp, and the user can reproduce pattern matching by hand. Therefore the latter is more reliable. It follows then that the proofs, - sayrefl` for 15 ^ 10 ∸ 15 ^ 10 ≡ 0, - are also more reliable when Agda.BuiltIn is not
used.
With using Agda.BuiltIn, there is a certain danger that the aboove normal form would differ from 0.

Am I missing something?

[JacquesCarette]

I don't think you're missing anything. This exact issue is why, with Bill Farmer and Michael Kohlhasse, we invented 'Realms'. Unfortunately these aren't implemented in Agda (just MMT).