Explore further improving instance search for NonZero instances

[MatthewDaggitt]

Now that it looks very likely we're going to use instance arguments for resolving NonZero proofs we should explore whether it's possible and/or desirable to automatically create derived instances to further improve the user's experience:

Candidates:

• NonZero m → NonZero n → NonZero (m * n)
• NonZero m → NonZero n → NonZero (m / n)
• NonZero p → NonZero (1/ p)
• NonZero m → NonZero (gcd m n)
• NonZero n → NonZero (gcd m n)
• NonZero m → NonZero (m ^ n)
• NonZero n → NonZero (s ◃ n)

(the latter two are an example of where one might get multiple instances for the same proof and where irrelevance would be useful)

A list of proofs that would benefit from these:

• Data.Nat.LCM - all of it
• Data.Rational.Unnormalised.Properties - *-cancelˡ-/ *-cancelʳ-/ 1/-involutive-≡ 1/-involutive
• Data.Rational.Normalised.Properties - normalize-coprime, ↥-normalize, ↧-normalize, normalize-cong, normalize-nonNeg, normalize-pos, normalize-injective-≃, 0/n≡0
• Data.Integer.Properties - *-cancelʳ-≡
• Data.Integer.Divisibility.Signed - ∣ᵤ⇒∣
• System.Clock - show

[JacquesCarette]

Question indirectly from this: does Agda allow irrelevant instance arguments to be filled by 'any' proof? Normally, instance search wants to find a single candidate for a hole.

[MatthewDaggitt]

Question indirectly from this: does Agda allow irrelevant instance arguments to be filled by 'any' proof? Normally, instance search wants to find a single candidate for a hole.

Making an instance argument irrelevant, still means that Agda has to find a valid proof. However unlike for relevant arguments, instance search won't error if it finds multiple valid proofs.

https://agda.readthedocs.io/en/v2.6.2/language/irrelevance.html#irrelevant-instance-arguments

[MatthewDaggitt]

Blocked by agda/agda#5494

[MatthewDaggitt]

Likewise with Positive etc.

Candidates:

• NonPositive p → NonNegative (- p)

Proofs that would benefit:

• Data.Rational.Unnormalised.Properties: *-monoˡ-≤-nonPos, *-monoˡ-<-neg, *-cancelˡ-<-nonPos

[MatthewDaggitt]

As pointed out by @technicalguy in #1581 we should benchmark the library when and if we implement these changes.