Merge branch 'base0_1' into jade

1 files changed, 15 insertions, 0 deletions

diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
index dc41740bc..4467a900e 100644
--- a/src/Galois/BaseSystem.v
+++ b/src/Galois/BaseSystem.v
@@ -27,6 +27,7 @@ Admitted.
 Module Type BaseCoefs.
   (** [BaseCoefs] represent the weights of each digit in a positional number system, with the weight of least significant digit presented first. The following requirements on the base are preconditions for using it with BaseSystem. *)
   Parameter base : list Z.
+  Axiom b0_1 : nth_default 0 base 0 = 1.
   Axiom base_positive : forall b, In b base -> b > 0. (* nonzero would probably work too... *)
   Axiom base_good :
     forall i j, (i+j < length base)%nat ->
@@ -409,6 +410,7 @@ End BaseSystem.
 Module Type PolynomialBaseParams.
   Parameter b1 : positive. (* the value at which the polynomial is evaluated *)
   Parameter baseLength : nat. (* 1 + degree of the polynomial *)
+  Axiom baseLengthNonzero : NPeano.ltb 0 baseLength = true.
 End PolynomialBaseParams.
 
 Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs.
@@ -416,6 +418,16 @@ Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs.
   Definition bi i := (Zpos b1)^(Z.of_nat i).
   Definition base := map bi (seq 0 baseLength).
 
+  Lemma b0_1 : nth_default 0 base 0 = 1.
+    unfold base, bi, nth_default.
+    case_eq baseLength; intros. {
+      assert ((0 < baseLength)%nat) by
+        (rewrite <-NPeano.ltb_lt; apply baseLengthNonzero).
+      subst; omega.
+    }
+    auto.
+  Qed.
+
   Lemma base_positive : forall b, In b base -> b > 0.
     unfold base.
     intros until 0; intro H.
@@ -457,6 +469,9 @@ End PolynomialBaseCoefs.
 Module BasePoly2Degree32Params <: PolynomialBaseParams.
   Definition b1 := 2%positive.
   Definition baseLength := 32%nat.
+  Lemma baseLengthNonzero : NPeano.ltb 0 baseLength = true.
+    compute; reflexivity.
+  Qed.
 End BasePoly2Degree32Params.
 
 Import ListNotations.