Search code examples
agda

Convert indexed Agda data type to record

I have a record type which allowes invalid instances as they might be from an external source. E.g.

record Foo : Set where
    fields
        x : Nat
        y : Nat
        z : Nat

Now I have a validator which returns a proof that a given Foo conforms to certain propositions. The type of the proof could be for example:

data IsValidFoo : Foo → Set where
    validFoo : (foo : Foo) → Even (Foo.x foo) → (Foo.y foo) < (Foo.z foo) → IsValidFoo foo

validateFoo : (foo : Foo) → Maybe (IsValidFoo foo)
…

I want to be able to access the individual proofs in IsValidFoo by name and thought of converting IsValidFoo to a record type. Is this even possible and how could it be achieved given that I want its type to stay IsValidFoo : Foo → Set?

Solution

  • Sure, this is possible by defining IsValidFoo as a record type parametrized over foo : Foo:

    open import Agda.Builtin.Nat hiding (_<_)

postulate
  _<_ : Nat → Nat → Set
  Even : Nat → Set
  Maybe : Set → Set

record Foo : Set where
  field
    x : Nat
    y : Nat
    z : Nat

record IsValidFoo (foo : Foo) : Set where
  constructor validFoo
  field
    even-x : Even (Foo.x foo)
    y<z    : (Foo.y foo) < (Foo.z foo)

validateFoo : (foo : Foo) → Maybe (IsValidFoo foo)