[TYPES] An efficient program for the function (mod 3) in type theories

[Yong Luo]

Dear all,

I am looking for an efficient program of the following function in the
Martin-Lof's type theory or UTT.

Nat is the type of natural numbers with constructors zero and succ.

f :: Nat -> Nat

f (zero) = zero
f (succ(zero)) = succ(zero)
f (succ(succ(zero))) =  succ(succ(zero))
f (succ(succ(succ(x)))) = f (x)

If a type theory has pattern matching such as
http://www.cs.kent.ac.uk/people/staff/yl41/TPF.htm

then this function can be easily programmed with a very good efficiency, for
example f (100) only takes 34 reduction steps.

In the Martin-Lof's type theory or UTT, every function is defined by
eliminators of inductive data types. I would like to know whether it is
possible to have an efficient program for the function f.

Thank you,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent