From 5597e03e4db81700bb0774a2986cd22e45810409 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 21 Jan 2017 18:46:03 -0500
Subject: Add weqb_hetero

---
 src/Util/WordUtil.v | 34 +++++++++++++++++++++++++++++++++-
 1 file changed, 33 insertions(+), 1 deletion(-)

(limited to 'src/Util/WordUtil.v')

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index acf27e225..7f8d7b824 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -7,6 +7,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
 Require Import Coq.micromega.Psatz.
 Require Import Coq.Bool.Bool.
 
+Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.
 
@@ -21,6 +22,38 @@ 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.
@@ -1211,4 +1244,3 @@ 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.
-
-- 
cgit v1.2.3