2
votes

Given the following fragments (taken from the tutorial by Ulf Norell and James Chapman), I understand the caller of lookup must provide a proof that the index ix of the required item is valid but I just can't find the right form to do it.

data Proven-n : Set where
record Proven-y : Set where

-- using the name 'isProven' instead of 'isTrue' of the tutorial
isProven : Bool -> Set 
isProven true = Proven-y
isProven false = Proven-n

lookup : {A : Set}(xs : List A)(ix : Nat) -> isProven (n < length xs) -> A

I've managed to work out the special case below, but all my attempts for a more general application of lookup, where the vector and the lookup index are produced in another function, have failed. I'd like to understand the concept of passing around proofs. Please help.

aList : List Bool
aList = true :: false :: []

aTest: Bool 
aTest = lookup aList 0 (record {})
1
Could you provide an example application of lookup which doesn't work out for you, including any relevant definitions (like _<_)? It's unclear to me where exactly you are stuck.Jannis Limperg
For instance, I'd like aTest to receive ix as a parameter: aTest (ix : Nat) -> Bool. How do I forward a proof of ix being valid to lookup then: lookup aList ix <???>. (<) is the normal less-than operator for Nat.Attila Karoly
Are you sure you want aTest : Nat -> Bool? That would mean aTest yields a value of Bool for any Nat. I'm guessing you want something like aTest : Nat -> Maybe Bool, returning nothing in case the given index is out-of-bounds.m0davis
You could and should have provided a fully-typechecked Agda program in the OP because, as it stands, it makes the answerers' jobs tougher. You're missing the required imports and a definition of lookup. (It also would have been appropriate to declare lookup as a postulate.) And lookup and aTest contain (obvious?) typos. My suggested (but rejected) edit to the OP is here.m0davis

1 Answers

1
votes

EDIT: The below makes more sense as a response to the question as edited here.

I'm guessing you want something like aTest : Nat -> Maybe Bool, returning nothing in case the given index is out-of-bounds. In that case, the following will do:

data Decide (P : Set) : Set where
  yes : P -> Decide P
  no : (P -> Proven-n) -> Decide P

okay? : ∀ {A : Set} (xs : List A) (ix : Nat) -> Decide (isProven (ix < length xs))
okay? [] ix = no λ ()
okay? (_ ∷ xs) zero = yes record {}
okay? (_ ∷ xs) (suc ix) = okay? xs ix

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A -> Maybe A

aTest : Nat -> Maybe Bool
aTest ix with okay? aList ix
... | yes ix<len = just (lookup aList ix ix<len)
... | no ix≥len = nothing

In the above, aTest uses okay? to decide whether the index is within bounds. If it is, the proof (carried by Decide) is passed to lookup.