title: Agda: how does one obtain a value of a dependent type?
body: <p>I recently asked this question:
  <a href="https://stackoverflow.com/questions/18296161/an-agda-proposition-used-in-the-type-what-does-it-mean">An agda proposition used in the type -- what does it mean?</a>
  and received a very well thought out answer on how to make types implicit and get a real compile time error.</p>
  
  <p>However, it is still unclear to me, how to create a value with a dependent type.</p>
  
  <p>Consider:</p>
  
  <pre><code>div : (n : N) -&gt; even n -&gt; N
  div zero p = zero
  div (succ (succ n)) p= succ (div n p)
  div (succ zero) ()
  </code></pre>
  
  <p>Where N is the natural numbers and even is the following proposition.</p>
  
  <pre><code>even : N -&gt; Set
  even zero = \top
  even (succ zero) = \bot
  even (succ (succ n)) = even n
  data \bot : Set where
  record \top : Set where
  </code></pre>
  
  <p>Suppose I want to write a function as follows:</p>
  
  <pre><code>f : N -&gt; N
  f n = if even n then div n else div (succ n)
  </code></pre>
  
  <p>I have no idea how to do something like this in the way I want...  In my eyes the best thing to do would be have a proof that (not (even n)) \to even (succ n).  I don't really know how to express this in agda.  I am able to write</p>
  
  <pre><code>g : (n:N) -&gt; (even n) -&gt; (even (succ n)) -&gt; N
  g n p q = if evenB n then (div n p) else (div (succ n) q)
  </code></pre>
  
  <p>From this, I could do things like:</p>
  
  <pre><code>g 5 _ _ 
  </code></pre>
  
  <p>and evaluate to normal form ... to get an answer.  If I want to write f, I can then do</p>
  
  <pre><code>f n = g n ? ?
  </code></pre>
  
  <p>And I get f n = g n { }1 { }2 where ?1 = even n, and ?2 = even (succ n).  I can then do things like f five and evaluate to a normal form.  I don't really understand why this is valid...  Is there a way I can tell agda more information about f defined in this way.  Can I tell for sure that if ?1 fails ?2 will succeed, and so tell agda that evaluating f always makes sense?</p>
  
  <p>I interpret g as a function which takes a number n, a proof that n is even, a proof that (succ n) is even, and gives back a number.  (Is this the correct way to read this -- or can anyone suggest a better way to read this?)  I would really love to understand exactly (or more precisely) how the above type checks.  Does it use induction -- does it connect (evenB n) with p : even n??  Etc.  I am confused for now because it knows that </p>
  
  <pre><code>if evenB n then (div n q) else (whatever)
  if evenB n then div (succ n) q else div n p
  </code></pre>
  
  <p>are incorrect.  The first I understand why -- the q is for succ n, so it doesn't match.  But the second fails, and the reason is more mysterious, and seems like Agda is more powerful than I would have guessed...</p>
  
  <p>Here is a first step I would really love if I could figure out how to do (if it makes sense).</p>
  
  <pre><code>g : (n : N) -&gt; (even n) -&gt; N
  g n p = if evenB n then (div n p) else (div (succ n) (odd p))
  </code></pre>
  
  <p>Where odd p is a proof that if even n is absurd then succ n is even.  I guess, this would require me to able to work with values that are dependently typed.</p>
  
  <p>Ultimately, I would love to be able to write something like this:</p>
  
  <pre><code>g : N -&gt; N
  g n = 
    let p = proofthat n is even
    in
        if evenB n then div n p else (div (succ n) (odd p))
  </code></pre>
  
  <p>Or something along those lines.  Or even</p>
  
  <pre><code>g : N -&gt; N
  g n = if evenB n then let p = proofThatEven n in div n p else let q = proofThatEven succ n in div n q
  </code></pre>
  
  <p>I would really like to know how to make a proof that corresponds to a dependent type, so that I can use it in the program.  Any suggestions?</p>