1 files changed, 71 insertions, 21 deletions

diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index eb7f31ba6..8de0fdd0a 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -1,7 +1,7 @@
-Require Import List.
-Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
-Require Import ZArith.ZArith ZArith.Zdiv.
-Require Import Omega NPeano Arith.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
+Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.BaseSystem.
 Require Import Crypto.Util.Notations.
 Local Open Scope Z.
@@ -474,14 +474,8 @@ Section BaseSystemProofs.
     auto.
   Qed.
 
-  (* mul' is multiplication with the FIRST ARGUMENT REVERSED *)
-  Fixpoint mul' (usr vs:digits) : digits :=
-    match usr with
-      | u::usr' =>
-        mul_each u (mul_bi base (length usr') vs) .+ mul' usr' vs
-      | _ => nil
-    end.
-  Definition mul us := mul' (rev us).
+  Local Notation mul' := (mul' base).
+  Local Notation mul := (mul base).
 
   Lemma mul'_rep : forall us vs,
     (length us + length vs <= length base)%nat ->
@@ -521,7 +515,7 @@ Section BaseSystemProofs.
   Lemma mul_length: forall us vs,
       (length (mul us vs) <= length us + length vs)%nat.
   Proof.
-    intros; unfold mul.
+    intros; unfold BaseSystem.mul.
     rewrite mul'_length.
     rewrite rev_length; omega.
   Qed.
@@ -532,26 +526,54 @@ Section BaseSystemProofs.
     induction us; destruct vs; boring.
   Qed.
 
-  Lemma mul'_length_exact: forall us vs,
-      (length us <= length vs)%nat -> us <> nil ->
-      (length (mul' us vs) = pred (length us + length vs))%nat.
+  Hint Rewrite add_length_exact : distr_length.
+
+  Lemma mul'_length_exact_full: forall us vs,
+      (length (mul' us vs) = match length us with
+                             | 0 => 0%nat
+                             | _ => pred (length us + length vs)
+                             end)%nat.
   Proof.
     induction us; intros; try solve [boring].
-    unfold mul'; fold mul'.
+    unfold BaseSystem.mul'; fold mul'.
     unfold mul_each.
     rewrite add_length_exact, map_length, mul_bi_length, length_cons.
     destruct us.
     + rewrite Max.max_0_r. simpl; omega.
     + rewrite Max.max_l; [ omega | ].
       rewrite IHus by ( congruence || simpl in *; omega).
-      omega.
+      simpl; omega.
   Qed.
 
+  Hint Rewrite mul'_length_exact_full : distr_length.
+
+  (* TODO(@jadephilipoom, from jgross): one of these conditions isn't
+  needed.  Should it be dropped, or was there a reason to keep it? *)
+  Lemma mul'_length_exact: forall us vs,
+      (length us <= length vs)%nat -> us <> nil ->
+      (length (mul' us vs) = pred (length us + length vs))%nat.
+  Proof.
+    intros; rewrite mul'_length_exact_full; destruct us; simpl; congruence.
+  Qed.
+
+  Lemma mul_length_exact_full: forall us vs,
+      (length (mul us vs) = match length us with
+                            | 0 => 0
+                            | _ => pred (length us + length vs)
+                            end)%nat.
+  Proof.
+    intros; unfold BaseSystem.mul; autorewrite with distr_length; reflexivity.
+  Qed.
+
+  Hint Rewrite mul_length_exact_full : distr_length.
+
+  (* TODO(@jadephilipoom, from jgross): one of these conditions isn't
+  needed.  Should it be dropped, or was there a reason to keep it? *)
   Lemma mul_length_exact: forall us vs,
       (length us <= length vs)%nat -> us <> nil ->
       (length (mul us vs) = pred (length us + length vs))%nat.
   Proof.
-    intros; unfold mul.
+    intros; unfold BaseSystem.mul.
     rewrite mul'_length_exact; rewrite ?rev_length; try omega.
     intro rev_nil.
     match goal with H : us <> nil |- _ => apply H end.
@@ -559,7 +581,7 @@ Section BaseSystemProofs.
     reflexivity.
   Qed.
   Definition encode'_zero z max  : encode' base z max 0%nat = nil := eq_refl.
-  Definition encode'_succ z max i : encode' base z max (S i) = 
+  Definition encode'_succ z max i : encode' base z max (S i) =
     encode' base z max i ++ ((z mod (nth_default max base (S i))) / (nth_default max base i)) :: nil := eq_refl.
   Opaque encode'.
   Hint Resolve encode'_zero encode'_succ.
@@ -606,4 +628,32 @@ Section BaseSystemProofs.
     apply Z.mod_small; omega.
   Qed.
 
-End BaseSystemProofs.
\ No newline at end of file
+End BaseSystemProofs.
+
+Hint Rewrite @add_length_exact @mul'_length_exact_full @mul_length_exact_full @encode'_length @sub_length : distr_length.
+
+Section MultiBaseSystemProofs.
+  Context base0 (base_vector0 : @BaseVector base0) base1 (base_vector1 : @BaseVector base1).
+
+  Lemma decode_short_initial : forall (us : digits),
+      (firstn (length us) base0 = firstn (length us) base1)
+      -> decode base0 us = decode base1 us.
+  Proof.
+    intros us H.
+    unfold decode, decode'.
+    rewrite (combine_truncate_r us base0), (combine_truncate_r us base1), H.
+    reflexivity.
+  Qed.
+
+  Lemma mul_rep_two_base : forall (us vs : digits),
+      (length us + length vs <= length base1)%nat
+      -> firstn (length us) base0 = firstn (length us) base1
+      -> firstn (length vs) base0 = firstn (length vs) base1
+      -> (decode base0 us) * (decode base0 vs) = decode base1 (mul base1 us vs).
+  Proof.
+      intros.
+      rewrite mul_rep by trivial.
+      apply f_equal2; apply decode_short_initial; assumption.
+  Qed.
+
+End MultiBaseSystemProofs.