[Agda] Agda2 beginner's question

[Nils Anders Danielsson]

On 2009-11-25 03:37, kahl at cas.mcmaster.ca wrote:
> Since my ``group'' application appears to type check,
> I would not have expected to be asked to prove
>
>   concat xss = allFin (n * m)
>
> before I can bind ``xss'' in the concat' pattern.

The function group is written as a view:

  data Group {a : Set} (n k : ℕ) : Vec a (n * k) → Set where
    concat' : (xss : Vec (Vec a k) n) → Group n k (concat xss)

  group : ∀ {a} n k (xs : Vec a (n * k)) → Group n k xs
  group zero    k []                  = concat' []
  group (suc n) k xs                  with splitAt k xs
  group (suc n) k .(ys ++ zs)         | ys ++' zs with group n k zs
  group (suc n) k .(ys ++ concat zss) | ys ++' ._ | concat' zss = concat' (ys ∷ zss)

In some cases this works out well:

  group′ : ∀ {A} n k → Vec A (n * k) → Vec (Vec A k) n
  group′ n k xs            with group n k xs
  group′ n k .(concat xss) | concat' xss = xss

Here we can see at a glance that the vector supplied to group′ is equal
to the concatenation of a certain vector of vectors. However, due to the
use of the index "concat xss" one cannot expect to pattern match on a
value of type Group n k xs unless xs is a variable—the unification will
not succeed, as you have noticed.

I have not used the Group view much, so I do not know if it is useful.
One could reformulate it as follows:

  data Group₂ {A : Set} (n k : ℕ) (xs : Vec A (n * k)) : Set where
    concat′ : (xss : Vec (Vec A k) n) (≡concat : xs ≡ concat xss) →
              Group₂ n k xs

  group₂ : ∀ {A} n k (xs : Vec A (n * k)) → Group₂ n k xs
  group₂ zero    k []                  = concat′ [] refl
  group₂ (suc n) k xs                  with splitAt k xs
  group₂ (suc n) k .(ys ++ zs)         | ys ++' zs with group₂ n k zs
  group₂ (suc n) k .(ys ++ concat zss) | ys ++' ._ | concat′ zss refl =
    concat′ (ys ∷ zss) refl

With this formulation one can choose whether or not to force the
unification to occur, at the cost of more verbosity. Another option is
to remove the equality proof from the group function's result and prove
it as a separate lemma instead. Which design would lead to the most
elegant end-user code? The Group₂ view seems like a nice compromise.

--
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.