Rewrite cast_word so that it's extracted better

It will now be extracted as the identity function automatically, so we
don't need to manually extract it as the empty string.

This should also fix #93.  (I think the issue was that this was an
instance of https://coq.inria.fr/bugs/show_bug.cgi?id=4243.)

src/Experiments/Ed25519Extraction.v

@@ -233,7 +233,7 @@ Extraction Implicit Word.split1 [ 2 ].
 Extraction Implicit Word.split2 [ 2 ].
 Extraction Implicit WordUtil.cast_word [1 2 3].
 Extraction Implicit WordUtil.wfirstn [ 2 4 ].
-Extract Inlined Constant WordUtil.cast_word => "".
+Extraction Inline WordUtil.cast_word.
 Extract Inductive Word.word => "[Prelude.Bool]" [ "[]" "(:)" ]
   "(\fWO fWS w -> {- match_on_word -} case w of {[] -> fWO (); (b:w') -> fWS b w' } )".
 
@@ -296,4 +296,4 @@ True
 
 Import Crypto.Spec.MxDH.
 Extraction Inline MxDH.ladderstep MxDH.montladder.
-Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
+Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.

src/Util/WordUtil.v

@@ -83,16 +83,26 @@ Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
 Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
 Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
 
-Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m :=
-  match n, m return wordsize_eq n m -> word n -> word m with
-  | O, O => fun _ _ => WO
-  | S n', S m' => fun _ w => WS (whd w) (@cast_word _ _ _ (wtl w))
-  | _, _ => fun _ _ => !
+Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y
+  := match x, y with
+     | O, O => fun _ => eq_refl
+     | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf))
+     | _, _ => fun x => x
+     end.
+
+Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl.
+Proof.
+  induction n; [ reflexivity | simpl ].
+  rewrite IHn; reflexivity.
+Qed.
+
+Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m :=
+  match correct_wordsize_eq n m pf in _ = y return word n -> word y with
+  | eq_refl => fun w => w
   end.
-Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *)
 
 Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
-Proof. induction w; simpl; auto using f_equal. Qed.
+Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed.
 
 Lemma wordToNat_cast_word {n} (w:word n) m pf :
   wordToNat (@cast_word n m pf w) = wordToNat w.
@@ -317,4 +327,4 @@ Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _.
 Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
     @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
 Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a.
-Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
+Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.