Hello!<div><br></div><div>I'm new to Agda and dependent types at all.</div><div>Now I am reading "Dependently typed programming in Agda" by Ulf Norell.</div><div>I got stuck with exercise 2.2.b</div><div><br>
</div><div>Here it is:</div><div><br></div><div>(Nat, Fin and Vec are as usual)</div><div><br></div><div><div>_!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A</div><div>[] ! ()</div><div>(x :: xs) ! fzero = x</div>
<div>(x :: xs) ! (fsuc i) = xs ! i</div><div><br></div><div><div>tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n</div><div>tabulate {zero} f = []</div><div>tabulate {suc n} f = f fzero :: tabulate (f ◦ fsuc)</div>
<div><br></div><div><div>Prove that they are indeed each other’s inverses.</div><div><br></div></div><div><div>lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs</div><div>lem-tab-! xs = {! !}</div><div>
<br></div><div>I figured out the proof on the paper but can't translate it to Agda code...</div><div><br></div></div><div>Thanks.</div></div></div>