Move weqb_hetero to Bedrock.Word

2 files changed, 30 insertions, 32 deletions

diff --git a/Bedrock/Word.v b/Bedrock/Word.v
index 2c518807d..10bd452bb 100644
--- a/Bedrock/Word.v
+++ b/Bedrock/Word.v
@@ -300,6 +300,16 @@ Definition weq : forall sz (x y : word sz), {x = y} + {x <> y}.
   abstract (rewrite (shatter_word y); simpl; intro; injection H; auto).
 Defined.
 
+Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool :=
+  match x, y with
+  | WO, WO => true
+  | WO, _ => false
+  | WS b _ x', WS b' _ y'
+    => eqb b b' && @weqb_hetero _ _ x' y'
+  | WS _ _ _, _
+    => false
+  end%bool.
+Global Arguments weqb_hetero {_ _} _ _.
 Fixpoint weqb sz (x : word sz) : word sz -> bool :=
   match x in word sz return word sz -> bool with
     | WO => fun _ => true
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 7f8d7b824..d36292f95 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -22,38 +22,6 @@ Create HintDb push_wordToN discriminated.
 Hint Extern 1 => autorewrite with pull_wordToN in * : pull_wordToN.
 Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN.
 
-Module Word.
-  Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool :=
-    match x, y with
-    | WO, WO => true
-    | WO, _ => false
-    | WS b _ x', WS b' _ y'
-      => eqb b b' && @weqb_hetero _ _ x' y'
-    | WS _ _ _, _
-      => false
-    end%bool.
-  Global Arguments weqb_hetero {_ _} _ _.
-  Theorem weqb_hetero_true_iff : forall sz1 x sz2 y,
-      @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y.
-  Proof.
-    induction x; intros sz2 y; (split; [ destruct y | ]);
-      repeat first [ progress simpl
-                   | intro
-                   | congruence
-                   | exists eq_refl
-                   | progress destruct_head ex
-                   | progress destruct_head bool
-                   | progress subst
-                   | progress split_andb
-                   | match goal with
-                     | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ]
-                       => apply IHx in H
-                     | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ]
-                       => apply IHx
-                     end ].
-  Qed.
-End Word.
-
 (* Utility Tactics *)
 
 Ltac word_util_arith := omega.
@@ -1244,3 +1212,23 @@ Lemma wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
 Proof.
   intros; unfold wlast; rewrite split2_combine; cbv; reflexivity.
 Qed.
+
+Theorem weqb_hetero_true_iff : forall sz1 x sz2 y,
+    @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y.
+Proof.
+  induction x; intros sz2 y; (split; [ destruct y | ]);
+    repeat first [ progress simpl
+                 | intro
+                 | congruence
+                 | exists eq_refl
+                 | progress destruct_head ex
+                 | progress destruct_head bool
+                 | progress subst
+                 | progress split_andb
+                 | match goal with
+                   | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ]
+                     => apply IHx in H
+                   | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ]
+                     => apply IHx
+                   end ].
+Qed.