[Agda] isHead x (x :: xs)

[Paolo Capriotti]

On Fri, May 17, 2013 at 9:57 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> Please, how to prove the following?
>
>   isHead : ℕ → List ℕ → Bool
>   isHead _ []        = false
>   isHead x (y ∷ ys)  with  x ≟ y
>   ...              | yes _ = true
>   ...              | no _  = false
>
>   isHP : (x : ℕ) → (xs : List ℕ) → isHead x (x ∷ xs) ≡ true
>   isHP x xs =
>               ??

isHP : (x : ℕ) → (xs : List ℕ) → isHead x (x ∷ xs) ≡ true
isHP x xs with x ≟ x
... | yes _ = refl
... | no p = ⊥-elim (p refl)

As a general rule of thumb, a proof about a function defined by cases
usually needs to have the same cases, so that beta-reduction can
happen in each of them.

Paolo