[Agda] multiple instance resolution and negation

[Guillaume Brunerie]

Hi Marcus,

A better way of preventing a definition to reduce is to use a record:


record NonNegative (x : X) : Set where
  constructor NonNegative-in
  field
    NonNegative-out : 0 ≤ x


This way you get that `NonNegative x` does not reduce to anything, so
you can use it as an instance argument without issues, 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).
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).

Best,
Guillaume

Den lör 29 aug. 2020 kl 13:50 skrev Marcus Christian Lehmann
<lehmann at tet.tu-berlin.de>:
>
> For everyone with a similar problem:
>
> I found that using an identity function `!_` declared in an `abstract` block
>
>    abstract
>      !_ : ∀{ℓ} {X : Type ℓ} → X → X
>      ! x = x
>
> does the trick of "blocking" Agda's instance inspection. Within that
> `abstract` block it is possible to proof
>
>    !-≡ : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
>    !-≡ = refl
>
> which can be used to define
>
>    !!_ : ∀{ℓ} {X : Type ℓ} → X → ! X
>    !!_ {X = X} x = transport (sym (!-≡ {X = X})) x
>
> I've assembled a minimal example how this works and I hope this instance
> resolution behavior does not change in the future.
>
> kind regards,
> Christian
>
> EXAMPLE:
>
> {-# OPTIONS --cubical --no-import-sorts #-}
>
> module Test3 where
>
> open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc
> to ∙-assoc)
> open import Cubical.Foundations.Logic
>
> abstract
>    !_ : ∀{ℓ} {X : Type ℓ} → X → X
>    ! x = x
>
>    !-≡ : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
>    !-≡ = refl -- makes use of the definition of `!_` within this block
>
>    !!_ : ∀{ℓ} {X : Type ℓ} → X → ! X
>    !!_ {X = X} x = transport (sym (!-≡ {X = X})) x
>
>    !!⁻¹_ : ∀{ℓ} {X : Type ℓ} → ! X → X
>    !!⁻¹_ {X = X} x = transport (!-≡ {X = X}) x
>
>    infix 1 !_
>    infix 1 !!_
>    infix 1 !!⁻¹_
>
> -- !-≡' : ∀{ℓ} {X : Type ℓ} → (! X) ≡ X
> -- !-≡' = refl -- cannot make use of the definition of `!_` anymore
>
> 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 (?)
>         )
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda