[Agda] Questions regarding non-constructor indexed datatypes

[Ulf Norell]

On Sun, Oct 12, 2008 at 7:19 PM, Shin-Cheng Mu <scm at iis.sinica.edu.tw>wrote:

>
> Question 1: I guess the problem is that Agda tries to unify
>  i + j with suc k. In the case of enqueue, length l + length r
>  is unified with n, which poses no problem. It is not the
>  case with dequeue.
>
>  However, Agda refers to m and n, rather than i and j, so my
>  guess may be wrong. If so, what is going on here?
>

The reason it refers to n and m rather than i and j is that it doesn't
get far enough to see that you named the numbers i and j. It
fails already trying to justify matching on the constructor queue,
regardless of what arguments you give it.


> Question 2: What is the suggested approach to resolve the
>  problem above?
>

The problem is that n + m can't be unified with suc k. To get around this
you can replace
suc k by a fresh variable l and a proof that l ≡ suc k. This will allow you
to pattern match
on the queue:

init' : forall {a k l} -> l ≡ suc k -> Vec a l -> Vec a k
 init' ≡-refl xs = init xs

dequeue' : forall {a k l} {xs : Vec a l} ->
           Queue xs -> (prf : l ≡ suc k) -> Queue (init' prf xs) × a
dequeue' (queue r [])      prf = {! !}
dequeue' (queue l (x ∷ r)) prf = {! !}

dequeue : forall {a k} {xs : Vec a (suc k)} ->
             Queue xs -> (Queue (init xs) × a)
dequeue q = dequeue' q ≡-refl

The proof argument needs to come after the queue argument if you want to
match on
it at a later stage, since pattern matching happens left-to-right.

Question 3:


What Nils Anders wrote.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081013/709ef0a8/attachment.html