[Agda] Difference between "(f o g) x = .." and "(f o g) = \ x -> .."

[Edsko de Vries]

Hi all,

First of all, let me just briefly introduce myself. I have been using
Coq for a number of years now, and though I have been reading this
list I have never actually used Agda -- until yesterday :) I'm not yet
sure how I'm going to survive without tactics :)

Anyhow, I started going through the AGP'08 tutorial, and got stuck in
Exercise 2.2. With the kind help of Andrea Vezzosi on the #agda
channel I figured it out, but we discovered something a little
strange. Here's the full Agda development:

module Test where

{- Basic data types -}

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

data Fin : Nat -> Set where
  fzero : {n : Nat} -> Fin (succ n)
  fsucc : {n : Nat} -> Fin n -> Fin (succ n)

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

{- Function composition -}

_◦_ : {A : Set} {B : A -> Set} {C : (x : A) -> B x -> Set}
      (f : {x : A} (y : B x) -> C x y) (g : (x : A) -> B x)
      (x : A) -> C x (g x)
(f ◦ g) = \ x -> f (g x)

{- Indexing and tabulating -}

_!_ : {n : Nat} {A : Set} -> Vec A n -> Fin n -> A
[]        ! ()
(x :: xs) ! fzero     = x
(x :: xs) ! (fsucc i) = xs ! i

tabulate : {n : Nat} {A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero}   f = []
tabulate {succ n} f = f fzero :: tabulate (f ◦ fsucc)

lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! {A} {zero}   [] = refl
lem-tab-! {A} {succ n} (x :: xs) with tabulate (_!_ xs) | lem-tab-! xs
lem-tab-! {A} {succ _} (x :: xs) | .xs | refl = refl

This typechecks and all is fine. However, if we change the definition
of function composition to

(f ◦ g) x = f (g x)

(which is what it is in the tutorial), this proof does *not* go
through. If we replace the body of the last line in lem-tab-! with a
hole, then Agda shows the following goal:

Goal: (x :: tabulate ((λ {.x} → _!_ (x :: xs)) ◦ fsucc)) == (x :: xs)

instead of (x :: xs) == (x :: xs) with the first definition of
function composition.

Is this expected behaviour?

Thanks!

Edsko