[Agda] Newbie question, book exercise problem.

[Jean-Philippe Bernardy]

>> cong : {A B : Set} {x y : A} (f : A -> B) -> x == y -> f x == f y
>> cong f refl = refl
>>
>> lem-tab-! [] = refl
>> lem-tab-! (x :: xs) = cong {! !} {! !} -- you should be able to fill
>> in the blanks easily enough.
>
> I've done it myself with cong. However I wanted to make use of the new
> 'rewrite' feature in the Agda dev version and couldn't make it.
> If it is possible I would like to see how...

It is. Make sure you have the last version of Agda + std lib. (I
pulled earlier today).

Cheers,
-- JP

The code:

open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Data.Function
open import Relation.Binary.PropositionalEquality

_!_ : {n : ℕ}{A : Set} -> Vec A n -> Fin n -> A
[]        ! ()
(x ∷ xs) ! zero    = x
(x ∷ xs) ! (suc i) = xs ! i

tabulate : {n : ℕ}{A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero} f = []
tabulate {suc n} f = f zero ∷ tabulate (f ∘ suc)

-- Prove that they are indeed each other’s inverses.

lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) ≡ xs
lem-tab-! [] = refl
lem-tab-! (x ∷ xs) rewrite lem-tab-! xs = refl