Added base_succ precondition to BaseSystem to help prove carrying.

3 files changed, 92 insertions, 3 deletions

diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
index 19fc90dba..f09f87eb6 100644
--- a/src/Galois/BaseSystem.v
+++ b/src/Galois/BaseSystem.v
@@ -17,6 +17,10 @@ Module Type BaseCoefs.
   Parameter base : list Z.
   Axiom base_positive : forall b, In b base -> b > 0. (* nonzero would probably work too... *)
   Axiom b0_1 : forall x, nth_default x base 0 = 1.
+  Axiom base_succ : forall i, ((S i) < length base)%nat ->
+    let b := nth_default 0 base in
+    let r := (b (S i)  / b i) in  
+    b (S i) = r * b i.
   Axiom base_good :
     forall i j, (i+j < length base)%nat ->
     let b := nth_default 0 base in
@@ -594,6 +598,31 @@ Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs.
     apply pos_pow_nat_pos.
   Qed.
 
+  Lemma base_defn : forall i, (i < length base)%nat ->
+      nth_default 0 base i = bi i.
+  Proof.
+    unfold base, nth_default; nth_tac.
+  Qed.
+
+  Lemma base_succ :
+    forall i, ((S i) < length base)%nat -> 
+    let b := nth_default 0 base in
+    let r := (b (S i) / b i) in
+    b (S i) = r * b i.
+  Proof.
+    intros; subst b; subst r.
+    repeat rewrite base_defn in * by omega.
+    unfold bi.
+    replace (Z.pos b1 ^ Z.of_nat (S i)) 
+      with (Z.pos b1 * (Z.pos b1 ^ Z.of_nat i)) by
+      (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition).
+    replace (Z.pos b1 * Z.pos b1 ^ Z.of_nat i / Z.pos b1 ^ Z.of_nat i)
+      with (Z.pos b1); auto.
+    rewrite Z_div_mult_full; auto.
+    apply Z.pow_nonzero; intuition.
+    pose proof (Zgt_pos_0 b1); omega.
+  Qed.
+
   Lemma base_good:
     forall i j, (i + j < length base)%nat ->
     let b := nth_default 0 base in
diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v
index b320680e9..48a166540 100644
--- a/src/Galois/ModularBaseSystem.v
+++ b/src/Galois/ModularBaseSystem.v
@@ -110,6 +110,22 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
       erewrite map_nth_default; auto.
     Qed.
 
+    Lemma base_succ : forall i, ((S i) < length base)%nat ->
+    let b := nth_default 0 base in
+    let r := (b (S i)  / b i) in  
+    b (S i) = r * b i.
+    Proof.
+      intros; subst b; subst r; unfold base.
+      repeat rewrite nth_default_app.
+      do 2 break_if; try apply BC.base_succ; try omega. {
+        destruct (lt_eq_lt_dec (S i) (length BC.base)). {
+          destruct s; intuition.
+          rewrite map_nth_default_base_high. 
+        }
+        assert (length BC.base <= i)%nat by (apply lt_n_Sm_le; auto); omega.
+      }
+    Qed. 
+
     Lemma base_good_over_boundary : forall
       (i : nat)
       (l : (i < length BC.base)%nat)
@@ -417,14 +433,50 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     boring.
   Qed.
 
+  Lemma div_mul_divide: forall n m, n = (n / m) * m -> (m | n).
+  Proof.
+    intros; apply (Znumtheory.Zdivide_intro m n (n/m)); auto.
+  Qed.
+
+  Lemma mul_divide_l : forall m n p, n <> 0 -> ((m * n) | p) -> (m | p).
+  Proof.
+    intros; apply (Z.mul_divide_cancel_l m p n); auto.
+    rewrite Z.mul_comm; apply Z.divide_mul_r; auto.
+  Qed.
 
-  Lemma base_div_2k : forall l x, BC.base = l ++ x :: nil ->
+  Lemma base_divide_2k : forall x, In x BC.base -> (x | 2 ^ P.k).
+  Proof.
+    intros.
+    destruct (In_nth_error_value BC.base _ H).
+    pose proof (nth_error_value_length _ _ BC.base _ H0).
+    destruct x0. {
+      replace x with (nth_default 0 BC.base 0) by
+       (unfold nth_default; replace (nth_error BC.base 0) with (Some x); auto).
+      rewrite BC.b0_1.
+      apply Z.divide_1_l.
+    } {
+      assert (length (BC.base) - S x0 < length BC.base)%nat as A0 by (apply lt_minus; omega).
+      remember (S x0) as y.
+      assert (length BC.base - y + y >= length BC.base)%nat as A2 by omega.
+      pose proof (P.base_matches_modulus ((length BC.base) - y) y A0 H1 A2) as P0.
+      remember (length BC.base) as l.
+      replace (l - y + y - l)%nat with 0%nat in P0 by 
+        (rewrite NPeano.Nat.sub_add; try rewrite minus_diag; auto; apply lt_le_weak; subst;
+        eapply nth_error_value_length; eauto).
+      simpl in *.
+      rewrite BC.b0_1 in P0.
+      SearchAbout Z.divide.
+  Admitted.
+
+  Lemma base_tail_div_mul_2k : forall l x, BC.base = l ++ x :: nil ->
     2 ^ P.k = (2 ^ P.k / x) * x.
   Proof.
     intros.
     rewrite Z.mul_comm.
     apply Z_div_exact_full_2; apply In_app_nil in H; try (apply BC.base_positive in H; omega).
-  Admitted.
+    rewrite Z.mod_divide by (intro; subst; pose proof (BC.base_positive 0 H); omega).
+    apply base_divide_2k; auto.
+  Qed.
 
   Lemma nth_error_last : forall {T} l (x y : T),
     nth_error (l ++ x :: nil) (length l) = Some y -> y = x.
@@ -524,7 +576,7 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
           ring_simplify.
           rewrite Zplus_assoc_reverse.
           rewrite (Z.add_cancel_l _ _ x3).
-          rewrite (base_div_2k (x0 :: x1) x2) at 3; auto.
+          rewrite (base_tail_div_mul_2k (x0 :: x1) x2) at 3; auto.
           rewrite Z.mul_assoc.
           do 2 rewrite <- (Z.mul_comm x2).
           rewrite <- (Zmult_plus_distr_r).
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 7f5bea670..ba1d8326a 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -223,6 +223,14 @@ Proof.
   induction n; destruct xs; nth_tac.
 Qed.
 
+Lemma In_nth_error_value : forall {T} xs (x:T),
+  In x xs -> exists n, nth_error xs n = Some x.
+Proof.
+  induction xs; nth_tac; break_or_hyp.
+  - exists 0; reflexivity.
+  - edestruct IHxs; eauto. exists (S x0). eauto.
+Qed.
+
 Lemma nth_value_index : forall {T} i xs (x:T),
   nth_error xs i = Some x -> In i (seq 0 (length xs)).
 Proof.