title: Improving dependently typed reverse function
body: <p>Here is the code I have thus far:</p>
  <pre><code>Section ilist.
  Variable A: Set.
  
  Inductive ilist : nat -&gt; Set :=
  | Nil : ilist O
  | Cons : forall n, A -&gt; ilist n -&gt; ilist (S n).
  
  (* not sure how to use in irev_aux *)
  Lemma same_length: forall n i2, ilist (n + S i2) = ilist (S n + i2).
  Proof.
  intros.
  rewrite Nat.add_succ_comm.
  reflexivity.
  Defined.
  
  Definition same_length' n i2 (l: ilist (n + S i2)): ilist (S n + i2).
  rewrite Nat.add_succ_comm.
  assumption.
  Defined.
  
  Fixpoint irev_aux i1 i2 (ls:ilist i1): ilist i2 -&gt; ilist (i1+i2) :=
  match ls in (ilist i1') return (ilist i2 -&gt; ilist (i1'+i2)) with
  | Nil =&gt; fun rev =&gt; rev
  | Cons h t =&gt; fun rev =&gt;
      same_length' _ _ ((irev_aux t) (Cons h rev))
  end.
  
  Definition same_length'' n (l:ilist (n+0)): ilist n.
  Proof.
  rewrite plus_0_r in l.
  assumption.
  Defined.
  
  Definition irev n (ls:ilist n): ilist n :=
    same_length'' n (irev_aux ls Nil).
  
  End ilist.
  </code></pre>
  <p>This works! Which is an improvement from my previous attempts :) But there are a couple less than desirable aspects that I'd like to try and refine.</p>
  <p>First, having a bunch of proofs hanging out to munge equivalent types seems...annoying. Basically, same_length, same_length', same_length''. Perhaps this is an issue with how I defined irev_aux, but I tried some definitions and others required a type level match which seemed about as annoying.</p>
  <p>I tried using refine, but got a type error...is there a way to invoke refine, where you then have to prove that the types are in fact equivalent? In a sense that's what I did, but who wants those lemmas hanging out.</p>
  <p>Beyond that, I realize there are probably ways to get rid of the equality lemmas, but I'm curious how I can make use of <code>same_length</code>. I've seen cases of matching on equality proofs before to get the typer to unify types...I tried that here but it didn't seem to work.</p>