Add boolean builtins in Nat

[LorenzoMolena]

This PR refactors the definitions of min, max, discreteℕ, <-split, and _≟_
to use boolean builtins, improving the performance of their computation.
For min and max, this improvement applies unconditionally, while for the other
functions it depends on whether proof terms are ignored
(e.g., when defining functions by cases via _≟_).

The main changes are:

• Nat.Base: imports the previously missing boolean builtins.
• Nat.Properties and Nat.Order: update the implementations of the functions listed above.
• Prelude: adds aliases for isContrSingl ... .fst and isContrSinglP ... .fst
  to support with-abstraction without losing information about the orginal terms
  (a workaround for the "with-abstraction equality" available in standard Agda but missing in Cubical).
• DirectSum.Equiv-DSHIT-DSFun, Instances.NatMax, and Truncation.Properties:
  adjusted for compatibility with the updated definitions.

Some notes:

• Only the properties of the boolean builtins necessary for the new implementations are proven.
• The previous implementation of _≟_ remains in the file under the name _≟'_.
• Some comments and names may still need revision to align with the library’s conventions.

Please let me know if this structure and approach are appropriate.

[felixwellen]

Add a comment showing how this can be used

[LorenzoMolena]

Is the comment I just added enough?

[anshwad10]

It looke like this has exactly the same use case as inspect. Is this not redundant?

[LorenzoMolena]

Thank you, I completely missed it. Do you know exactly how should I use it?
Right now I'm trying to case-split on inspect (_≡ᵇ n) m in the proof of discreteness of ℕ, but this doesn't seem to work, since it only gives me the path, but not each boolean case.

[LorenzoMolena]

Nevermind, I got it.

Is this what you meant?

discreteℕ : Discrete ℕ
discreteℕ zero zero = yes refl
discreteℕ zero (suc n) = no znots
discreteℕ (suc m) zero = no snotz
discreteℕ (suc m) (suc n) with m ≡ᵇ n | inspect (m ≡ᵇ_) n
... | false | [ p ]ᵢ = no  (subst Bool→Type p ∘ ≡→≡ᵇ)
... | true  | [ p ]ᵢ = yes (≡ᵇ→≡ (subst Bool→Type (sym p) tt))

[marcinjangrzybowski]

@LorenzoMolena since thowse will be heavily used and critical for performance of various definition, to be safe, I would double check performance benchmark for every variant when you are making changes.

[LorenzoMolena]

@felixwellen I just tried the approach suggested by @anshwad10, i.e. using inspect instead of UsingEq, and everything still typechecks.

However, I find UsingEq better suited for this PR. For example, the with-abstraction in the definition of _≟_ would become something like this:

_≟_ : ∀ m n → Trichotomy m n
zero ≟ zero = eq refl
zero ≟ suc n = lt (n , +-comm n 1)
suc m ≟ zero = gt (m , +-comm m 1)
suc m ≟ suc n with m ∸ n | inspect (m ∸_) n | n ∸ m | inspect (n ∸_) m 
... | zero  | [ p ]ᵢ | zero  | [ q ]ᵢ = eq (∸≡0→≡ p q)
... | zero  | _      | suc _ | [ q ]ᵢ = lt (<ᵇ→< $ ∸→>ᵇ n m $ subst (caseNat ⊥.⊥ Unit) (sym q) tt)
... | suc _ | [ p ]ᵢ | zero  | _      = gt (<ᵇ→< $ ∸→>ᵇ m n $ subst (caseNat ⊥.⊥ Unit) (sym p) tt)
... | suc _ | [ p ]ᵢ | suc _ | [ q ]ᵢ = ⊥.rec $ ¬m<m {m} $ <-trans
 (<ᵇ→< $ ∸→>ᵇ n m $ subst (caseNat ⊥.⊥ Unit) (sym q) tt)
 (<ᵇ→< $ ∸→>ᵇ m n $ subst (caseNat ⊥.⊥ Unit) (sym p) tt)

whilst the corrent definition on the PR is a bit more concise.
For instance, with UsingEq I don’t need to explicitly state which function is applied to the term.

I’d prefer to keep UsingEq, but I admit that’s mostly a matter of personal preference.
Since everything typechecks either way (with comparable perfomances), I can switch to inspect if needed.
Just let me know which version do you prefer

[felixwellen]

You can keep UsingEq, but make a comment there that it is similar to inspect.