Move more proofs earlier

3 files changed, 48 insertions, 24 deletions

diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index 8bd390635..8de0fdd0a 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -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.
@@ -541,7 +535,7 @@ Section BaseSystemProofs.
                              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.
@@ -568,7 +562,7 @@ Section BaseSystemProofs.
                             | _ => pred (length us + length vs)
                             end)%nat.
   Proof.
-    intros; unfold mul; autorewrite with distr_length; reflexivity.
+    intros; unfold BaseSystem.mul; autorewrite with distr_length; reflexivity.
   Qed.
 
   Hint Rewrite mul_length_exact_full : distr_length.
@@ -579,7 +573,7 @@ Section BaseSystemProofs.
       (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.
@@ -637,3 +631,29 @@ Section BaseSystemProofs.
 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.
diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index d4df6040f..ddf787d21 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -160,3 +160,5 @@ Section ExtendedBaseVector.
     unfold ext_base; rewrite app_length; rewrite map_length; auto.
   Qed.
 End ExtendedBaseVector.
+
+Hint Rewrite @extended_base_length : distr_length.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index daff60220..227a3e77f 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -128,27 +128,29 @@ Section PseudoMersenneProofs.
     subst; auto.
   Qed.
 
-  Lemma decode_short : forall (us : BaseSystem.digits),
-    (length us <= length base)%nat ->
-    BaseSystem.decode base us = BaseSystem.decode ext_base us.
+  Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits),
+      (length us <= length base)%nat
+      -> firstn (length us) base = firstn (length us) ext_base.
   Proof.
-    intros.
-    unfold BaseSystem.decode, BaseSystem.decode'.
-    rewrite combine_truncate_r.
-    rewrite (combine_truncate_r us ext_base).
-    f_equal; f_equal.
-    unfold ext_base.
+    unfold ext_base; intros.
     rewrite firstn_app_inleft; auto; omega.
   Qed.
+  Local Hint Immediate firstn_us_base_ext_base.
+
+  Lemma decode_short : forall (us : BaseSystem.digits),
+    (length us <= length base)%nat ->
+    BaseSystem.decode base us = BaseSystem.decode ext_base us.
+  Proof. auto using decode_short_initial. Qed.
+
+  Local Hint Immediate ExtBaseVector.
 
   Lemma mul_rep_extended : forall (us vs : BaseSystem.digits),
       (length us <= length base)%nat ->
       (length vs <= length base)%nat ->
       (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs).
   Proof.
-      intros.
-      rewrite mul_rep by (apply ExtBaseVector || unfold ext_base; simpl_list; omega).
-      f_equal; rewrite decode_short; auto.
+    intros; apply mul_rep_two_base; auto;
+      autorewrite with distr_length; try omega.
   Qed.
 
   Lemma modulus_nonzero : modulus <> 0.