Linear-time implementation of `Data.Nat.Properties.≤′⇒≤`?

[jamesmckinna]

In a recent Zulip thread the question was raised as to whether a linear-time implementation of the coercion from _≤′_ to _≤_ was possible. After some experiments (and not going via recompute), I wondered about the following:

m≤′n⇒m≤o+n′ : m ≤′ n → ∀ {o p} → .(o + n ≡ p) → m ≤ p
m≤′n⇒m≤o+n′ ≤′-refl {o = o} eq = cast-≤ʳ (trans (+-comm _ o) eq) (m≤m+n _ o)
m≤′n⇒m≤o+n′ (≤′-step m≤′n) {o = o} eq = m≤′n⇒m≤o+n′ m≤′n {o = suc o} (trans (sym (+-suc o _)) eq)

m≤′n⇒m≤o+n : m ≤′ n → ∀ o → m ≤ o + n
m≤′n⇒m≤o+n m≤′n o = m≤′n⇒m≤o+n′ m≤′n refl

≤′⇒≤ : _≤′_ ⇒ _≤_
≤′⇒≤ m≤′n = m≤′n⇒m≤o+n m≤′n 0

with (independently useful... for replacing uses of subst when dealing with _≤_...?) linear-time coercions given by:

cast-≤ˡ : .(m ≡ o) → m ≤ n → o ≤ n
cast-≤ˡ {o = zero}  _  z≤n       = z≤n
cast-≤ˡ {o = suc _} eq (s≤s m≤n) = s≤s (cast-≤ˡ (cong pred eq) m≤n)

cast-≤ʳ : .(n ≡ o) → m ≤ n → m ≤ o
cast-≤ʳ             _  z≤n       = z≤n
cast-≤ʳ {o = suc _} eq (s≤s m≤n) = s≤s (cast-≤ʳ (cong pred eq) m≤n)

More generally, should we (now start to) reconsider Data.Nat.Properties from the perspective of making its proofs (as well as the definitions in Data.Nat.Base) more computationally efficient?

NB further optimisation may be possible in the base case

m≤′n⇒m≤o+n′ ≤′-refl {o = o} eq = cast-≤ʳ (trans (+-comm _ o) eq) (m≤m+n _ o)

by fusing cast-≤ʳ and the (linear-time!) call to m≤m+n _ o... but I think the above is opaque enough already ;-)

[jamesmckinna]

Does @gallais 's comment on PR #2440 suggests that changes to intensional/reduction behaviour might be breaking..., so: v3.0? I confess I'm not entirely clear how we arbitrate on such matters: should we suggest/require that users of stdlib not depend on computational content of proofs? This feels like a potential minefield... given the rather careful separation of Data.* into 'definitions' vs. 'properties...?

[MatthewDaggitt]

Hmm, so Total and Decidable proofs are somewhat of an exception I feel as they really are used as "real computations" (whatever that means)... Like you, I'm very reluctant to say that we can't change the reduction behaviour of proofs between minor library versions.

[jamesmckinna]

Hmm, so Total and Decidable proofs are somewhat of an exception I feel as they really are used as "real computations" (whatever that means)... Like you, I'm very reluctant to say that we can't change the reduction behaviour of proofs between minor library versions.

Cf. #2436 / #2440