title: How can I convince Agda that my function has a certain value?
body: <p>I'm used to writing human proofs in mathematics, but I'm very new to writing Agda. The following is a toy example of something that I can't figure out how to prove with Agda.</p>
  
  <p>Informally, I want to write a function f which takes a natural number x and a pair of naturals. If the first element in the pair equals x, return the second element of the pair. Otherwise, return 0.</p>
  
  <p>Here are my definitions for natural number equality:</p>
  
  <pre><code>data N : Set where
    zero : N
    s : N → N
  
  data _≡_ {X : Set} : X → X → Set where
    refl : (x : X) → (x ≡ x)
  
  data _≢_ : N → N → Set where
    &lt;   : {n : N} → (zero ≢ (s n))
    &gt;   : {n : N} → ((s n) ≢ zero)
    rec : {n m : N} → (n ≢ m) → ((s n) ≢ (s m))
  
  data _=?_ (n m : N) : Set where
    true  : (n ≡ m) → (n =? m)
    false : (n ≢ m) → (n =? m)
  
  equal? : (n m : N) → (n =? m)
  equal? zero zero = true (refl zero)
  equal? zero (s _) = false &lt;
  equal? (s _) zero = false &gt;
  equal? (s n) (s m) with (equal? n m)
  ... | (true (refl a)) = (true (refl (s a)))
  ... | (false p) = (false (rec p))
  </code></pre>
  
  <p>and here is the function.</p>
  
  <pre><code>data Npair : Set where
    pair : (n m : N) → Npair
  
  f : N → Npair → N
  f a (pair b c) with equal? a b
  ... | (true (refl _)) = c
  ... | (false _) = zero
  </code></pre>
  
  <p>I cannot prove</p>
  
  <pre><code>lemma : (x y : N) → (y ≡ (f x (pair x y)))
  </code></pre>
  
  <p>because when I try to introduce the <code>refl</code> constructor in the definition, it complains that</p>
  
  <pre><code>y != f x (pair x y) | equal? x x of type N
  </code></pre>
  
  <p>What do I have to change in order to prove this lemma?</p>