[Agda] multiple instance resolution and negation

[Marcus Christian Lehmann]

Dear Guillaume,

Am 29.08.20 um 14:34 schrieb Guillaume Brunerie:
> A better way of preventing a definition to reduce is to use a record:
> ...
> This way you get that `NonNegative x` does not reduce to anything, ...

Thank you for pointing that out! I was wondering about this behavior on 
a different occasion already.

> ... so you can use it as an instance argument without issues, ...

I have successfully tried out your recommendation with

   record !_ {ℓ} (X : Type ℓ) : Type ℓ where
     inductive
     constructor !!_
     field x : X

   open !_ hiding (x)
   infix 1 !!_
   infix 1 !_

for which I can affirm that the the previous code still compiles without 
any changes! (nice!)

> but at the same time it is still equivalent to `0 ≤ x` via the two functions
> NonNegative-in and NonNegative-out (which are definitionally inverse
> to each other).

Yes. One easily gets these three to hold

   !-iso   : ∀{ℓ} {X : Type ℓ} → Iso (! X)   X
   !-≡     : ∀{ℓ} {X : Type ℓ} →     (! X) ≡ X
   !-equiv : ∀{ℓ} {X : Type ℓ} →     (! X) ≃ X

> You could also directly define _≤_ as a record whose only field has
> the definition you currently have as its type, so that it doesn’t
> reduce to a function type (although I have a feeling that a more
> specialized type class like NonNegative might be better).
Well, I like the annotation-like general way since it does not makes 
necessary to come up with new names for each property. But this might 
break in some application where a more explicit fallback might be 
needed. I'll settle for this variant for now and investigate its 
usefulness over time.

kind regards,
Christian


updated EXAMPLE:

{-# OPTIONS --cubical --no-import-sorts #-}

module Test4 where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc 
to ∙-assoc)
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

record !_ {ℓ} (X : Type ℓ) : Type ℓ where
   inductive
   constructor !!_
   field x : X

open !_ hiding (x)
infix 1 !!_
infix 1 !_

   !-iso : ∀{ℓ} {X : Type ℓ} → Iso (! X) X
   Iso.fun      !-iso = !_.x
   Iso.inv      !-iso = !!_
   Iso.rightInv !-iso = λ      x  → refl
   Iso.leftInv  !-iso = λ{ (!! x) → refl }

   !-≡ : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
   !-≡ {X = X} = isoToPath !-iso

   !-equiv : ∀{ℓ} {X : Type ℓ} → (! X) ≃ X
   !-equiv = !_.x , λ where .equiv-proof x → ((!! x) , refl) , λ{ ((!! 
y) , p) → λ i → (!! p (~ i)) , (λ j → p (~ i ∨ j)) }

hPropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
hPropRel A B ℓ' = A → B → hProp ℓ'

module TestB {ℓ ℓ'} (X : Type ℓ)
              (0ˣ : X) (_+_ _·_ : X → X → X) (_<_ : hPropRel X X ℓ')
              (let infixl 5 _+_; _+_ = _+_) where

   _≤_ : hPropRel X X ℓ'
   x ≤ y = ¬(y < x)

   postulate
     sqrt : (x : X) → {{ ! [ 0ˣ ≤ x ] }} → X
     0≤x² : ∀ x → [ 0ˣ ≤ (x · x) ]

   instance -- module-scope instances
     _ = λ {x} → !! 0≤x² x

   test4 : (x y z : X) → [ 0ˣ ≤ x ] → [ 0ˣ ≤ y ] → X
   test4 x y z 0≤x 0≤y =
     let instance -- let-scope instances
           _ = !! 0≤x
           _ = !! 0≤y
           _ = !! 0≤x² x -- preferred over the instance from module-scope
     in ( (sqrt x)       -- works
        + (sqrt y)       -- also works
        + (sqrt (z · z)) -- uses instance from module scope
        + (sqrt (x · x)) -- uses instance from let-scope (?)
        )