[Agda] Ensuring termination during equality checking

[Andreas Abel]

Hi Ulf,

in my experience, it is easier to come up with a strongly normalizing 
reduction relation for "rewriting", where recursion and pattern matching 
are tied together, than for "functional languages" where recursion and 
case trees are used in separation.  [cf. Nicolas Oury's talk at DTP]

Now I am interested in the strategy for equality checking used in Agda2.

It seems that complications are avoided at the moment by omitting 
congruence rules for case (and recursion?) altogether.

Is this correct?

I have attached my experiments.

Cheers,
Andreas

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

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

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

add : Nat -> Nat -> Nat
add x zero    = x
add x (suc y) = suc (add x y)

mult : Nat -> Nat -> Nat
mult x zero = zero
mult x (suc y) with x 
... | zero = zero
... | _    = add x (mult x y)

ifzero : {A : Set} -> Nat -> A -> A -> A
ifzero zero     a b = a
ifzero (suc _) a b = b

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

{-
p1 : (x : Nat) -> mult x (suc zero) == ifzero x zero x
p1 x = refl  

-- FAILS:  mult x (suc zero) | x != ifzero x zero x of type Nat
-}

ifzero' : {A : Set} -> Nat -> A -> A -> A
ifzero' x a b with x
... | zero = a
... | _    = b

{-
p2 : (x : Nat) -> mult x (suc zero) == ifzero' x zero x
p2 x = refl  

-- FAILS as well
-- no congruence rule for with (case) !?
 -}


add' : Nat -> Nat -> Nat
add' x zero    = x
add' x (suc y) = suc (add x y)

{-
p3 : add == add'
p3 = refl

-- FAILS:  add x x != add' x x of type Nat
-- no congruence rule for recursion
-}

{-
p4 : (x y : Nat) -> add x y == add' x y
p4 x y = refl

-- FAILS for the same reason
-}