[Agda] Overlapping patterns in function definition -- strange behavior

[Wojciech Jedynak]

Hello everybody!

This post is a literate Agda file. It was tested with Agda 2.2.10.
I noticed a strange behavior when I defined a function with
overlapping patterns.
Please look below.

\begin{code}

module Test where

open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality

foo : ℕ → Bool → Bool
foo zero b = b
foo n true = true
foo (suc n) b = false

bar : ℕ → Bool → Bool
bar zero b = b
bar (suc n) b = false

fooBarEquiv : ∀ (n : ℕ)(b : Bool) → foo n b ≡ bar n b
fooBarEquiv zero b = refl
fooBarEquiv (suc n) b = refl

\end{code}
I was very surprised that it's possible to prove fooBarEquiv.

The difference between foo and bar is that foo has an extra clause in
the middle.
According to my intuition, foo 1 true should reduce to true, but when
I check it with
C-c C-n I get false. At least it's consistent.

Porting this code to Haskell:

data Nat = Zero | Suc Nat deriving Show

foo :: Nat -> Bool -> Bool
foo Zero b = b
foo n True = True
foo (Suc n) b = False

We get:

ghci> foo (Suc Zero) True
True

I run into this issue, because I wanted to define two (extensionally)
equivalent
functions, with one being an optimized version of the other, and the
optimization
was to yield result in a particular, concrete case without doing matching one of
the arguments at all. When I was working on the proof that the
equivalence indeed
holds, I saw that Agda didn't care for the "missing" pattern. So please tell me,
is it a bug or a feature?

On a similar topic: when patterns are compiled, is the order preserved?

These questions may sound silly, but I have this one function that I really want
to actually run, not only type-check :-) And the unoptimized version
needs around
70 minutes to evaluate :-) [It's much better when I compile it with MAlonzo, but
at some point I will want to write a theorem
lem-certified-result : my-function 0 ≡ result
lem-certified-result = refl
]

Greetings,
Wojciech Jedynak