ModularBaseSystem: finished most admits for addition and multiplication, moved some lemmas to ListUtil.

3 files changed, 96 insertions, 46 deletions

diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
index 8e83fc2c1..badfd3bcb 100644
--- a/src/Galois/BaseSystem.v
+++ b/src/Galois/BaseSystem.v
@@ -558,6 +558,31 @@ Module BaseSystem (Import B:BaseCoefs).
     }
   Qed.
 
+  Lemma length_add_ge : forall us vs, (length us >= length vs)%nat ->
+    (length (us .+ vs) <= length us)%nat.
+  Proof.
+    intros.
+    rewrite add_trailing_zeros; auto.
+    rewrite (add_same_length _ _ (length us)); try omega.
+    rewrite app_length.
+    rewrite length_zeros.
+    omega.
+  Qed.
+
+  Lemma add_length_le_max : forall us vs,
+      (length (us .+ vs) <= max (length us) (length vs))%nat.
+  Proof.
+    intros.
+    destruct (ge_dec (length us) (length vs)). {
+      rewrite Max.max_l by omega.
+      rewrite length_add_ge; auto.
+    } {
+      rewrite add_comm.
+      rewrite Max.max_r by omega.
+      apply length_add_ge; omega.
+    }
+  Qed.
+
   Lemma mul_bi_length : forall us n, length (mul_bi n us) = (length us + n)%nat.
   Proof.
     induction us; intros; simpl. {
@@ -682,10 +707,32 @@ Module BaseSystem (Import B:BaseCoefs).
     exact mul'_rep.
   Qed.
 
-  Lemma mul_length: forall us vs, (~ (us = nil)) ->
-      length (mul us vs) = (length us + length vs)%nat.
+  Ltac case_max :=
+    match goal with [ |- context[max ?x ?y] ] =>
+        destruct (le_dec x y); try ( rewrite Max.max_l by omega
+                              || rewrite Max.max_r by omega)
+    end.
+
+  Lemma mul'_length: forall us vs,
+      (length (mul' us vs) <= length us + length vs)%nat.
+  Proof.
+    induction us; intros; simpl; try omega.
+    rewrite add_length_le_max.
+    unfold mul_each; rewrite map_length; rewrite mul_bi_length.
+    case_max. {
+      rewrite Max.max_l by (rewrite plus_comm; eauto); omega.
+    } {
+      omega.
+    }
+  Qed.
+
+  Lemma mul_length: forall us vs,
+      (length (mul us vs) <= length us + length vs)%nat.
   Proof.
-  Admitted.
+    intros; unfold mul.
+    rewrite mul'_length.
+    rewrite rev_length; omega.
+  Qed.
 
 (* Print Assumptions mul_rep. *)
 
@@ -755,7 +802,7 @@ Module BaseSystemExample.
   Module BasePoly2Degree32 := BaseSystem BasePoly2Degree32Coefs.
   Import BasePoly2Degree32.
 
-  Example three_times_two : [1;1;0] #* [0;1;0] = [0;1;1;0;0].
+  Example three_times_two : mul [1;1;0] [0;1;0] = [0;1;1;0;0].
   Proof.
     reflexivity.
   Qed.
@@ -772,11 +819,11 @@ Module BaseSystemExample.
     reflexivity.
   Qed.
   Example encoded_ab :
-    a #*b =[1;1;1;2;2;4;2;2;4;5;3;3;3;6;4;2;5;3;4;3;2;1;2;2;2;0;1;1;0;1].
+    mul a b =[1;1;1;2;2;4;2;2;4;5;3;3;3;6;4;2;5;3;4;3;2;1;2;2;2;0;1;1;0;1].
   Proof.
     reflexivity.
   Qed.
-  Example dab : decode (a #* b) = 804660279.
+  Example dab : decode (mul a b) = 804660279.
   Proof.
     reflexivity.
   Qed.
diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v
index 4a4c94d45..d2f6a0f2c 100644
--- a/src/Galois/ModularBaseSystem.v
+++ b/src/Galois/ModularBaseSystem.v
@@ -50,9 +50,6 @@ Module Type GFrep (Import M:Modulus).
   Parameter mul : T -> T -> T.
   Axiom mul_rep : forall u v x y, u ~= x -> v ~= y -> mul u v ~= (x*y)%GF.
 
-  Parameter square : T -> T.
-  Axiom square_rep : forall u x, u ~= x -> square u ~= (x^2)%GF.
-  (* we will want a non-trivial implementation later, currently square x = mul x x *)
 End GFrep.
 
 Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBaseParams BC M) (* TODO(jadep): "<: GFrep M" *).
@@ -168,7 +165,7 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
   Local Hint Unfold T.
   Definition toGF (us : T) : GF := GF.inject (B.decode us).
   Local Hint Unfold toGF.
-  Definition rep (us : T) (x : GF) := length us = length BC.base /\ toGF us = x.
+  Definition rep (us : T) (x : GF) := (length us <= length BC.base)%nat /\ toGF us = x.
   Local Notation "u '~=' x" := (rep u x) (at level 70).
   Local Hint Unfold rep.
 
@@ -182,7 +179,12 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
   Proof.
     autounfold; intuition. {
       unfold add.
-      apply B.add_same_length; auto.
+      rewrite B.add_length_le_max.
+      B.case_max. {
+        rewrite Max.max_r; omega.
+      } {
+        omega.
+      }
     }
     unfold toGF in *; unfold B.decode in *.
     rewrite B.add_rep.
@@ -192,14 +194,6 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     subst; auto.
   Qed.
 
-  (* TODO: move to ListUtil *)
-  Lemma firstn_app : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
-      firstn n xs = firstn n (xs ++ ys).
-  Proof.
-    induction n; destruct xs; destruct ys; simpl_list; boring; try omega.
-    rewrite (IHn xs (a0 :: ys)) by omega; auto.
-  Qed.
-    
   Lemma decode_short : forall (us : B.digits), 
     (length us <= length BC.base)%nat -> B.decode us = E.decode us.
   Proof.
@@ -292,40 +286,45 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     rewrite B.mul_each_rep; auto.
   Qed.
 
-  (* TODO: move to listutil *)
-  Lemma skipn_length : forall {A} n (xs : list A),
-      length (skipn n xs) = (length xs - n)%nat.
-  Proof.
-    induction n; destruct xs; boring.
-  Qed.
-
   Lemma reduce_length : forall us, 
       (length us <= length EC.base)%nat ->
-      (length us >= length BC.base)%nat ->
-      length (reduce us) = length (BC.base).
+      (length (reduce us) <= length (BC.base))%nat.
   Proof.
     intros.
     unfold reduce.
     remember (map (Z.mul P.c) (skipn (length BC.base) us)) as high.
     remember (firstn (length BC.base) us) as low.
-    assert (length low = length BC.base)
-      by (rewrite Heqlow; rewrite firstn_length; rewrite min_l; auto).
+    assert (length low >= length high)%nat. {
+      subst. rewrite firstn_length.
+      rewrite map_length.
+      rewrite skipn_length.
+      destruct (le_dec (length BC.base) (length us)). {
+        rewrite Min.min_l by omega.
+        rewrite extended_base_length in H. omega.
+      } {
+        rewrite Min.min_r by omega. omega.
+      }
+    }
+    assert ((length low <= length BC.base)%nat)
+      by (rewrite Heqlow; rewrite firstn_length; apply Min.le_min_l).
     assert (length high <= length BC.base)%nat 
       by (rewrite Heqhigh; rewrite map_length; rewrite skipn_length;
       rewrite extended_base_length in H; omega).
-    rewrite B.add_trailing_zeros.
-    rewrite (B.add_same_length _ _ (length BC.base)); try apply H1; auto. {
-      rewrite app_length.
-      rewrite B.length_zeros; intuition.
-    }
-    omega.
+    rewrite B.add_trailing_zeros; auto.
+    rewrite (B.add_same_length _ _ (length low)); auto.
+    rewrite app_length.
+    rewrite B.length_zeros; intuition.
   Qed.
 
   Definition mul (us vs : T) := reduce (E.mul us vs).
   Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> mul u v ~= (x*y)%GF.
   Proof.
-    autounfold; unfold mul; intuition; try apply reduce_length;
-    try (rewrite E.mul_length; try rewrite extended_base_length; omega).
+    autounfold; unfold mul; intuition. {
+      rewrite reduce_length; try omega.
+      rewrite E.mul_length.
+      rewrite extended_base_length.
+      omega.
+    }
     unfold mul.
     unfold toGF in *.
     assert (forall x, inject x = inject (x mod modulus)) as Hm by admit;
@@ -341,8 +340,6 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     auto.
   Qed.
 
-  Parameter square : T -> T.
-  Axiom square_rep : forall u x, u ~= x -> square u ~= (x^2)%GF.
-  (* we will want a non-trivial implementation later, currently square x = mul x x *)
+  (* Still missing: subtraction, fromGF *)
 
 End GFPseudoMersenneBase.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 229fb7488..626a33f02 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -204,15 +204,21 @@ Proof.
   destruct n; auto.
 Qed.
 
-Lemma firstn_app : forall A (l l': list A), firstn (length l) (l ++ l') = l.
+Lemma firstn_app : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
+  firstn n xs = firstn n (xs ++ ys).
 Proof.
-  intros.
-  induction l; simpl; auto.
-  f_equal; auto.
+  induction n; destruct xs; destruct ys; simpl_list; boring; try omega.
+  rewrite (IHn xs (a0 :: ys)) by omega; auto.
 Qed.
-
+    
 Lemma skipn_app : forall A (l l': list A), skipn (length l) (l ++ l') = l'.
 Proof.
   intros.
   induction l; simpl; auto.
 Qed.
+
+Lemma skipn_length : forall {A} n (xs : list A),
+  length (skipn n xs) = (length xs - n)%nat.
+Proof.
+induction n; destruct xs; boring.
+Qed.