title: Proofs about functions that depend on the ordering of their alternatives
body: <p>Having quite some experience in Haskell, I just recently started to use Idris for theorem proving. This is a minimal example that illustrates a problem I encountered when trying to prove rather simple statements.</p>
  
  <p>Consider we have a total function <code>test</code>:</p>
  
  <pre><code>total test : Integer -&gt; Integer
  test 1 = 1
  test n = n
  </code></pre>
  
  <p>Of course we see that the function could be simplified to <code>test n = n</code>, but let's prove it. I am simply going over all the cases:</p>
  
  <pre><code>total lemma_test : (n : Integer) -&gt; test n = n
  lemma_test 1 = Refl
  lemma_test n = Refl
  </code></pre>
  
  <p>But, this doesn't type-check:</p>
  
  <pre><code>Type mismatch between
          n = n (Type of Refl) and
          test n = n (Expected type)
  
  Specifically:
          Type mismatch between
                  n
          and
                  test n
  </code></pre>
  
  <p>So, the problem seems to be that Idris cannot infer for the second case of <code>lemma_test</code> that <code>n</code> is not equal to <code>1</code> and that also the second case of <code>test</code> must be applied.</p>
  
  <p>We can, of course, try to explicitly list ALL the cases, which can be cumbersome, or impossible, as in the case for <code>Integer</code>s:</p>
  
  <pre><code>total lemma_test : (n : Integer) -&gt; test n = n
  lemma_test 1 = Refl
  lemma_test 2 = Refl
  lemma_test 3 = Refl
  ...
  </code></pre>
  
  <p>Is there a way to prove statements like this for functions that are not defined over a finite set of data constructors but instead depend on the fact that pattern-matching works from top to bottom, like <code>test</code> in this example?</p>
  
  <p>Maybe there is a rather simple solution that I just fail to see, considering that functions like this occur quite often.</p>