[Agda] Re: Overlapping patterns in function definition -- strange behavior [more examples]

[Wojciech Jedynak]

Hello again!

I realized that swapping the first two lines of foo results in a more
intuitive behavior. See below:

\begin{code}

module Test where

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

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

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 true = refl
fooBarEquiv (suc n) true = {!!} -- goal : true ≡ false -- OK!
fooBarEquiv zero false = refl
fooBarEquiv (suc n) false = refl

foo'BarEquiv : ∀ (n : ℕ)(b : Bool) → foo' n b ≡ bar n b
foo'BarEquiv zero true = refl
foo'BarEquiv (suc n) true = refl
foo'BarEquiv zero false = refl
foo'BarEquiv (suc n) false = refl

\end{code}

This "trick" seems to work also in my "real code" example.

Greetings,
Wojciech Jedynak