ModularBaseSystem: continuing to prove base_good.

2 files changed, 69 insertions, 20 deletions

diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v
index 379f7c4d8..70903536f 100644
--- a/src/Galois/ModularBaseSystem.v
+++ b/src/Galois/ModularBaseSystem.v
@@ -85,32 +85,43 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
       }
     Qed.
 
+    Lemma map_nth_default_base_high : forall n, (n < (length BC.base))%nat -> 
+      nth_default 0 (map (Z.mul (2 ^ P.k)) BC.base) n =
+      (2 ^ P.k) * (nth_default 0 BC.base n).
+    Proof.
+      intros.
+      erewrite map_nth_default; auto.
+    Qed.
+
     Lemma base_good :
       forall i j, (i+j < length base)%nat ->
       let b := nth_default 0 base in
       let r := (b i * b j) / b (i+j)%nat in
       b i * b j = r * b (i+j)%nat.
     Proof.
-        (* TODO: move to listutil *)
-        Lemma nth_error_app : forall {T} n (xs ys:list T), nth_error (xs ++ ys) n =
-            if lt_dec n (length xs)
-            then nth_error xs n
-            else nth_error ys (n - length xs).
-       Proof.
-           induction n; destruct xs; destruct ys; nth_tac.
-       Admitted.
-       
-       intros.
-       subst b.
-       unfold base, nth_default.
-       repeat rewrite nth_error_app.
-       destruct (lt_dec i (length BC.base)); destruct (lt_dec j (length BC.base)).
-       nth_tac. destruct (lt_dec (i + j) (length BC.base)); try omega.
-       SearchAbout nth_error.
-        
-
-    Admitted.
-
+      intros.
+      subst b. subst r.
+      unfold base in *.
+      rewrite app_length in H; rewrite map_length in H.
+      repeat rewrite nth_default_app.
+      destruct (lt_dec i (length BC.base)); destruct (lt_dec j (length BC.base)); destruct (lt_dec (i + j) (length BC.base)); try omega.
+      {
+        (* i < length BC.base, j < length BC.base, i + j < length BC.base *)
+        apply BC.base_good; auto.
+      } {
+        (* i < length BC.base, j < length BC.base, i + j >= length BC.base *)
+        admit.
+      } {
+        (* i < length BC.base, j >= length BC.base, i + j >= length BC.base *)
+        do 2 rewrite map_nth_default_base_high by omega.
+        remember (nth_default 0 BC.base) as b.
+        remember (j - length BC.base)%nat as j'.
+        admit.
+      } {
+        (* i >= length BC.base, j < length BC.base, i + j >= length BC.base *)
+        admit.
+      }
+    Qed.
   End EC.
 
   Module E := BaseSystem EC.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index e8be33dac..c5c1eba4a 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1,6 +1,7 @@
 Require Import List.
 Require Import Omega.
 Require Import Arith.Peano_dec.
+Require Import VerdiTactics.
 
 Ltac boring :=
   simpl; intuition;
@@ -12,8 +13,14 @@ Ltac boring :=
            | _ => progress intuition
          end; eauto.
 
+Lemma nth_error_nil_error : forall {A} n, nth_error (@nil A) n = None.
+Proof.
+intros. induction n; boring.
+Qed.
+
 Ltac nth_tac' := 
   intros; simpl in *; unfold error,value in *; repeat progress (match goal with
+    | [  |- context[nth_error nil ?n] ] => rewrite nth_error_nil_error
     | [ H: ?x = Some _  |- context[match ?x with Some _ => ?a | None => ?a end ] ] => destruct x
     | [ H: ?x = None _  |- context[match ?x with Some _ => ?a | None => ?a end ] ] => destruct x
     | [  |- context[match ?x with Some _ => ?a | None => ?a end ] ] => destruct x
@@ -63,6 +70,18 @@ Proof.
 Qed.
 Hint Resolve nth_error_length_error.
 
+Lemma map_nth_default : forall (A B : Type) (f : A -> B) n x y l,
+  (n < length l) -> nth_default y (map f l) n = f (nth_default x l n).
+Proof.
+  intros.
+  unfold nth_default.
+  erewrite map_nth_error.
+  reflexivity.
+  nth_tac'.
+  pose proof (nth_error_error_length A n l H0).
+  omega.  
+Qed.
+
 Ltac nth_tac := 
   repeat progress (try nth_tac'; try (match goal with
     | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H
@@ -143,6 +162,25 @@ Proof.
   rewrite <- seq_shift; apply in_map; eapply IHi; eauto.
 Qed.
 
+Lemma nth_error_app : forall {T} n (xs ys:list T), nth_error (xs ++ ys) n =
+  if lt_dec n (length xs)
+  then nth_error xs n
+  else nth_error ys (n - length xs).
+Proof.
+  induction n; destruct xs; destruct ys; nth_tac.
+Admitted.
+
+Lemma nth_default_app : forall {T} n x (xs ys:list T), nth_default x (xs ++ ys) n =
+  if lt_dec n (length xs)
+  then nth_default x xs n
+  else nth_default x ys (n - length xs).
+Proof.
+  intros.
+  unfold nth_default.
+  rewrite nth_error_app.
+  destruct (lt_dec n (length xs)); auto.
+Qed.
+
 Lemma combine_truncate_r : forall {A} (xs ys : list A),
   combine xs ys = combine xs (firstn (length xs) ys).
 Proof.