[Agda] Agda2 beginner's question

[Andreas Abel]

Dear Wolfram,

welcome to Agda!  We help you suffer through the first steps... ;-)

kahl at cas.mcmaster.ca wrote:
> Dear Agda list,
> 
>   I know Haskell, including GADTs, and have used Isabelle before;
> now I am just starting to try to get going with Agda2
> and hit a serious roadblock in trying to unwrap a Data.Vec.Group
> from the standard library (lib-0.2) to get at the enclosed Vec (Vec ...).
> 
> 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.
> And even if I really have to do it, I have no idea how to start...

Yeah, I think that is an over-eagerly typing of "group" in the standard 
library.  To use it, you have to first prove that your vector is 
splittable into a vector of vectors who concat together to your original 
vector.  But group is supposed to do the splitting for you...  Da beisst 
sich die Katze in den Schwanz!

I can implement your example with the following, not so ambitiously 
typed version of group.

group : ∀ {a} n k (xs : Vec a (n * k)) → Vec (Vec a k) n
group zero    k []                  = []
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 ++' zs | zss = ys ∷ zss

Btw. your mat1 contained some bug as well (m and n switched).

mat1 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
mat1 m n with group m n (allFin (m * n))
mat1 m n | xss  = map (map toℕ) xss

Maybe I am missing something at 1 a.m. in the night, but the parts of my 
brain that are still working tell me that the group function of the 
stdlib needs to be rewritten, or at least there needs to be a comment 
how on earth you are supposed to use it!

Cheers,
Andreas



> 
> 
> What am I overlooking?
> 
> 
> Wolfram
> 
> 
> ----
> module Matrix where
> 
> open import Data.Nat
> open import Data.Vec
> open import Data.Function using (_$_)
> open import Data.Fin using (toℕ)
> 
> Matrix : Set → ℕ → ℕ → Set
> Matrix A m n = Vec (Vec A n) m
> 
> 
> transpose : ∀ {A m n} → Matrix A m n → Matrix A n m
> transpose [] = replicate []
> transpose (xs ∷ xss) = zipWith _∷_ xs (transpose xss)
> 
> 
> mat1 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
> mat1 m n with group n m (allFin (n * m))
> mat1 m n | concat' xss  = map (map toℕ) xss
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/