From 57f2c40634ba291af4f2cf9921faa7c108d3de7b Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Sun, 25 Oct 2015 12:38:21 -0400 Subject: progress on proving properties about multiplication in positional number system --- src/Galois/BaseSystem.v | 152 ++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 134 insertions(+), 18 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index ac42b7c79..3baeb26cf 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -23,12 +23,12 @@ Module BaseSystem (Import B:BaseCoefs). Definition decode bs u := fold_right accumulate 0 (combine u bs). Hint Unfold decode accumulate. - Fixpoint add (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => (u+v)::(add us' vs') - | _, nil => us - | _, _ => vs - end. + Fixpoint add (us vs:digits) : digits := + match us,vs with + | u::us', v::vs' => (u+v)::(add us' vs') + | _, nil => us + | _, _ => vs + end. Local Infix ".+" := add (at level 50). Lemma add_rep : forall bs us vs, decode bs (add us vs) = decode bs us + decode bs vs. @@ -43,10 +43,10 @@ Module BaseSystem (Import B:BaseCoefs). (* mul_geomseq is a valid multiplication algorithm if b_i = b_1^i *) Fixpoint mul_geomseq (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs - | _, _ => nil - end. + match us,vs with + | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs + | _, _ => nil + end. Definition mul_each u := map (Z.mul u). Lemma mul_each_rep : forall bs u vs, decode bs (mul_each u vs) = u * decode bs vs. @@ -69,16 +69,39 @@ Module BaseSystem (Import B:BaseCoefs). Qed. Lemma app_zeros_zeros : forall n m, (zeros n ++ zeros m) = zeros (n + m). - Admitted. + Proof. + intros; + induction n; simpl; auto. + rewrite IHn; auto. + Qed. Lemma zeros_app0 : forall m, (zeros m ++ 0 :: nil) = zeros (S m). - Admitted. + Proof. + intros. + assert (0 :: nil = zeros 1) by auto. + rewrite H. + rewrite app_zeros_zeros. + rewrite NPeano.Nat.add_1_r; auto. + Qed. Lemma rev_zeros : forall n, rev (zeros n) = zeros n. - Admitted. + Proof. + intros. + induction n. { + unfold zeros; auto. + } { + replace (rev (zeros (S n))) with (rev (zeros n) ++ 0 :: nil) by auto. + rewrite IHn. + rewrite zeros_app0; auto. + } + Qed. Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys. - Admitted. + Proof. + intros. + rewrite app_assoc_reverse. + replace ((y :: nil) ++ ys) with (y :: ys); auto. + Qed. (* mul' is multiplication with the SECOND ARGUMENT REVERSED and OUTPUT REVERSED *) Fixpoint mul_bi' (i:nat) (vsr:digits) := @@ -178,10 +201,103 @@ Module BaseSystem (Import B:BaseCoefs). simpl; f_equal; auto. Qed. + (* TODO: add this to preconditions for base *) + Lemma b0_1 : forall bs, nth_default 0 bs 0 = 1. + Admitted. + + (* TODO: add this to preconditions for base *) + Lemma bn_nonzero : forall n bs, nth_default 0 bs n <> 0. + Admitted. + + Lemma crosscoef_0_n : forall n, crosscoef 0 n = 1. + induction n; unfold crosscoef. + rewrite Z_div_mult_full. + apply b0_1. + rewrite plus_O_n. + rewrite b0_1; intuition. + simpl. + rewrite Z_div_mult_full. + apply b0_1. + apply bn_nonzero. + Qed. + + Lemma mul_bi'_0_us : forall us, mul_bi' 0 us = us. + Proof. + intros. + induction us; simpl; auto. + rewrite IHus. + rewrite crosscoef_0_n. + rewrite <- Zred_factor0; auto. + Qed. + + Lemma mul_bi'_n_nil : forall n, mul_bi' n nil = nil. + Proof. + intros. + unfold mul_bi; auto. + Qed. + + Lemma add_nil_l : forall us, nil .+ us = us. + induction us; auto. + Qed. + + Lemma mul_bi_0_us : forall us, mul_bi 0 us = us. + Proof. + intros. + unfold mul_bi; simpl. + rewrite mul_bi'_0_us. + rewrite rev_involutive; auto. + Qed. + + Lemma mul_bi'_app : forall n x us, + mul_bi' n (x :: us) = x * crosscoef n (length us) :: mul_bi' n us. + Proof. + unfold mul_bi'; auto. + Qed. + + Lemma mul_bi'_add : forall n us vs, + mul_bi' n (us .+ vs) = mul_bi' n us .+ mul_bi' n vs. + Proof. + intros. + (* induction us. { + rewrite mul_bi'_n_nil. + rewrite add_nil_l. + rewrite add_nil_l; auto. + } { + induction vs; auto. + rewrite mul_bi'_app. + + apply IHus. + } + + induction n. { + rewrite mul_bi'_0_us. + replace (mul_bi' 0 us) with us by (rewrite mul_bi'_0_us; auto). + replace (mul_bi' 0 vs) with vs by (rewrite mul_bi'_0_us; auto). + auto. + } { + unfold mul_bi'; simpl. + simpl. *) + Admitted. + + Lemma add_leading_zeroes : forall n us vs, + (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs). + Admitted. + + Lemma rev_add : forall us vs, + rev(us .+ vs) = rev us .+ rev vs. + Admitted. + Lemma mul_bi_add : forall n us vs, mul_bi n (us .+ vs) = mul_bi n us .+ mul_bi n vs. Proof. - Admitted. + intros. + unfold mul_bi; simpl. + replace (rev (us .+ vs)) with (rev us .+ rev vs). + rewrite mul_bi'_add. + rewrite add_leading_zeroes. + rewrite rev_add; auto. + rewrite <- rev_add; auto. + Qed. Lemma mul_bi_rep : forall i vs, decode base (mul_bi i vs) = decode base vs * nth_default 0 base i. induction vs using rev_ind; intros; simpl. { @@ -203,10 +319,10 @@ Module BaseSystem (Import B:BaseCoefs). (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) Fixpoint mul' (usr vs:digits) : digits := - match usr with - | u::usr' => + match usr with + | u::usr' => mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs - | _ => nil + | _ => nil end. Definition mul us := mul' (rev us). Local Infix "#*" := mul (at level 40). -- cgit v1.2.3 From beaf00fdf971ee0a8955b5358943562af554a20f Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Sun, 25 Oct 2015 13:28:26 -0400 Subject: progress on proving properties about multiplication in positional number system --- src/Galois/BaseSystem.v | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 3baeb26cf..3ddd92004 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -23,12 +23,12 @@ Module BaseSystem (Import B:BaseCoefs). Definition decode bs u := fold_right accumulate 0 (combine u bs). Hint Unfold decode accumulate. - Fixpoint add (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => (u+v)::(add us' vs') - | _, nil => us - | _, _ => vs - end. + Fixpoint add (us vs:digits) : digits := + match us,vs with + | u::us', v::vs' => (u+v)::(add us' vs') + | _, nil => us + | _, _ => vs + end. Local Infix ".+" := add (at level 50). Lemma add_rep : forall bs us vs, decode bs (add us vs) = decode bs us + decode bs vs. @@ -43,10 +43,10 @@ Module BaseSystem (Import B:BaseCoefs). (* mul_geomseq is a valid multiplication algorithm if b_i = b_1^i *) Fixpoint mul_geomseq (us vs:digits) : digits := - match us,vs with - | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs - | _, _ => nil - end. + match us,vs with + | u::us', v::vs' => u*v :: map (Z.mul u) vs' .+ mul_geomseq us' vs + | _, _ => nil + end. Definition mul_each u := map (Z.mul u). Lemma mul_each_rep : forall bs u vs, decode bs (mul_each u vs) = u * decode bs vs. @@ -247,7 +247,7 @@ Module BaseSystem (Import B:BaseCoefs). rewrite mul_bi'_0_us. rewrite rev_involutive; auto. Qed. - + Lemma mul_bi'_app : forall n x us, mul_bi' n (x :: us) = x * crosscoef n (length us) :: mul_bi' n us. Proof. @@ -265,7 +265,6 @@ Module BaseSystem (Import B:BaseCoefs). } { induction vs; auto. rewrite mul_bi'_app. - apply IHus. } @@ -279,10 +278,10 @@ Module BaseSystem (Import B:BaseCoefs). simpl. *) Admitted. - Lemma add_leading_zeroes : forall n us vs, + Lemma add_leading_zeroes : forall n us vs, (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs). Admitted. - + Lemma rev_add : forall us vs, rev(us .+ vs) = rev us .+ rev vs. Admitted. @@ -319,10 +318,10 @@ Module BaseSystem (Import B:BaseCoefs). (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) Fixpoint mul' (usr vs:digits) : digits := - match usr with - | u::usr' => + match usr with + | u::usr' => mul_each u (mul_bi (length usr') vs) .+ mul' usr' vs - | _ => nil + | _ => nil end. Definition mul us := mul' (rev us). Local Infix "#*" := mul (at level 40). -- cgit v1.2.3 From 3ecf80e98f556f86ae9c89fedef2434aad935212 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 25 Oct 2015 16:05:34 -0400 Subject: base[0] = 1 --- src/Galois/BaseSystem.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 4c50a193e..2bd4fb14b 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 -> @@ -294,6 +295,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. @@ -301,6 +303,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. @@ -342,6 +354,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. -- cgit v1.2.3 From c15762f44e92b3a2be6ccb945ff2ec8402418908 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Sun, 25 Oct 2015 22:45:59 -0400 Subject: Modified to use formal preconditions for b0_1 and base_positive. --- src/Galois/BaseSystem.v | 47 +++++++++++++++++++++++++++++++++++------------ 1 file changed, 35 insertions(+), 12 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 4467a900e..9c1d02ff2 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -240,33 +240,54 @@ Module BaseSystem (Import B:BaseCoefs). simpl; f_equal; auto. Qed. - (* TODO: add this to preconditions for base *) - Lemma b0_1 : forall bs, nth_default 0 bs 0 = 1. + Lemma In_base : forall n, + (length base > n)%nat -> In (nth_default 0 base n) base. Admitted. - (* TODO: add this to preconditions for base *) - Lemma bn_nonzero : forall n bs, nth_default 0 bs n <> 0. - Admitted. + Lemma base_nonzero : forall n, + (length base > n)%nat -> nth_default 0 base n > 0. + Proof. + intros. + assert (In (nth_default 0 base n) base) by (apply In_base; auto). + remember (nth_default 0 base n) as x in *; auto. + assert (In x base -> x > 0). + apply base_positive. + auto. + Qed. - Lemma crosscoef_0_n : forall n, crosscoef 0 n = 1. + Lemma crosscoef_0_n : forall n, (length base > n)%nat -> crosscoef 0 n = 1. + Proof. induction n; unfold crosscoef. rewrite Z_div_mult_full. - apply b0_1. + rewrite b0_1; auto. rewrite plus_O_n. rewrite b0_1; intuition. - simpl. + simpl. + intros. rewrite Z_div_mult_full. - apply b0_1. - apply bn_nonzero. + rewrite b0_1; auto. + assert (nth_default 0 base (S n) > 0). + try apply base_nonzero; apply H. + intuition. Qed. - Lemma mul_bi'_0_us : forall us, mul_bi' 0 us = us. + Lemma mul_bi'_0_us : forall us, + (length base > length us)%nat -> mul_bi' 0 us = us. Proof. intros. induction us; simpl; auto. + assert (length base > length us)%nat. + assert (length (a :: us) > length us)%nat. + replace (a :: us) with ((a :: nil) ++ us) by auto. + rewrite app_length. + replace (length (a :: nil)) with 1%nat; auto. + intros. + assert ((length base > length (a :: us))%nat -> (length (a :: us) > length us)%nat -> (length base > length us)%nat) by (apply gt_trans). + auto. rewrite IHus. rewrite crosscoef_0_n. rewrite <- Zred_factor0; auto. + apply H0. apply H0. Qed. Lemma mul_bi'_n_nil : forall n, mul_bi' n nil = nil. @@ -279,12 +300,14 @@ Module BaseSystem (Import B:BaseCoefs). induction us; auto. Qed. - Lemma mul_bi_0_us : forall us, mul_bi 0 us = us. + Lemma mul_bi_0_us : forall us, + (length base > length us)%nat -> mul_bi 0 us = us. Proof. intros. unfold mul_bi; simpl. rewrite mul_bi'_0_us. rewrite rev_involutive; auto. + rewrite rev_length; auto. Qed. Lemma mul_bi'_app : forall n x us, -- cgit v1.2.3 From 70b898ced954636ceaae3451e4de8659ff697cc1 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 26 Oct 2015 08:36:24 -0400 Subject: More work on proving linearity of multiply. --- src/Galois/BaseSystem.v | 42 ++++++++++++++++++++++++++++-------------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 9c1d02ff2..83051c167 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -316,29 +316,43 @@ Module BaseSystem (Import B:BaseCoefs). unfold mul_bi'; auto. Qed. + + Lemma mul_bi'_add_zeros : forall m n a vs, + mul_bi' n ((a :: zeros m) .+ vs) = + mul_bi' n (a :: zeros m) .+ mul_bi' n vs. + Proof. + induction m; intros. + simpl zeros. + case_eq vs; intros. + Focus 2. + simpl add. + simpl mul_bi'. + Admitted. + + Lemma add_assoc : forall us vs ws, us .+ (vs .+ ws) = us .+ vs .+ ws. + Admitted. + + Lemma app_zeros : forall a us, (a :: (zeros (length us))) .+ us = a :: us. + Admitted. + Lemma mul_bi'_add : forall n us vs, mul_bi' n (us .+ vs) = mul_bi' n us .+ mul_bi' n vs. Proof. intros. - (* induction us. { + induction us. { rewrite mul_bi'_n_nil. rewrite add_nil_l. rewrite add_nil_l; auto. } { - induction vs; auto. - rewrite mul_bi'_app. - apply IHus. + rewrite <- app_zeros. + rewrite mul_bi'_add_zeros. + rewrite <- add_assoc. + rewrite mul_bi'_add_zeros. + rewrite IHus. + rewrite add_assoc. + f_equal. } - - induction n. { - rewrite mul_bi'_0_us. - replace (mul_bi' 0 us) with us by (rewrite mul_bi'_0_us; auto). - replace (mul_bi' 0 vs) with vs by (rewrite mul_bi'_0_us; auto). - auto. - } { - unfold mul_bi'; simpl. - simpl. *) - Admitted. + Qed. Lemma add_leading_zeroes : forall n us vs, (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs). -- cgit v1.2.3 From d0a8f3e1168466ae2e3d4948aed4ec829a0c8b01 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Tue, 27 Oct 2015 16:58:04 -0400 Subject: Multiply rep mostly proven, working on admits. --- src/Galois/BaseSystem.v | 159 +++++++++++++++++++----------------------------- 1 file changed, 61 insertions(+), 98 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 83051c167..e399a93d4 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -240,56 +240,6 @@ Module BaseSystem (Import B:BaseCoefs). simpl; f_equal; auto. Qed. - Lemma In_base : forall n, - (length base > n)%nat -> In (nth_default 0 base n) base. - Admitted. - - Lemma base_nonzero : forall n, - (length base > n)%nat -> nth_default 0 base n > 0. - Proof. - intros. - assert (In (nth_default 0 base n) base) by (apply In_base; auto). - remember (nth_default 0 base n) as x in *; auto. - assert (In x base -> x > 0). - apply base_positive. - auto. - Qed. - - Lemma crosscoef_0_n : forall n, (length base > n)%nat -> crosscoef 0 n = 1. - Proof. - induction n; unfold crosscoef. - rewrite Z_div_mult_full. - rewrite b0_1; auto. - rewrite plus_O_n. - rewrite b0_1; intuition. - simpl. - intros. - rewrite Z_div_mult_full. - rewrite b0_1; auto. - assert (nth_default 0 base (S n) > 0). - try apply base_nonzero; apply H. - intuition. - Qed. - - Lemma mul_bi'_0_us : forall us, - (length base > length us)%nat -> mul_bi' 0 us = us. - Proof. - intros. - induction us; simpl; auto. - assert (length base > length us)%nat. - assert (length (a :: us) > length us)%nat. - replace (a :: us) with ((a :: nil) ++ us) by auto. - rewrite app_length. - replace (length (a :: nil)) with 1%nat; auto. - intros. - assert ((length base > length (a :: us))%nat -> (length (a :: us) > length us)%nat -> (length base > length us)%nat) by (apply gt_trans). - auto. - rewrite IHus. - rewrite crosscoef_0_n. - rewrite <- Zred_factor0; auto. - apply H0. apply H0. - Qed. - Lemma mul_bi'_n_nil : forall n, mul_bi' n nil = nil. Proof. intros. @@ -300,78 +250,90 @@ Module BaseSystem (Import B:BaseCoefs). induction us; auto. Qed. - Lemma mul_bi_0_us : forall us, - (length base > length us)%nat -> mul_bi 0 us = us. - Proof. - intros. - unfold mul_bi; simpl. - rewrite mul_bi'_0_us. - rewrite rev_involutive; auto. - rewrite rev_length; auto. + Lemma add_nil_r : forall us, us .+ nil = us. + induction us; auto. Qed. - - Lemma mul_bi'_app : forall n x us, + + Lemma add_first_terms : forall us vs a b, + (a :: us) .+ (b :: vs) = (a + b) :: (us .+ vs). + auto. + Qed. + + Lemma mul_bi'_cons : forall n x us, mul_bi' n (x :: us) = x * crosscoef n (length us) :: mul_bi' n us. Proof. unfold mul_bi'; auto. Qed. - - Lemma mul_bi'_add_zeros : forall m n a vs, - mul_bi' n ((a :: zeros m) .+ vs) = - mul_bi' n (a :: zeros m) .+ mul_bi' n vs. - Proof. - induction m; intros. - simpl zeros. - case_eq vs; intros. - Focus 2. - simpl add. - simpl mul_bi'. + Lemma add_same_length : forall us vs l, (length us = l) -> (length vs = l) -> + length (us .+ vs) = l. Admitted. - Lemma add_assoc : forall us vs ws, us .+ (vs .+ ws) = us .+ vs .+ ws. + Lemma add_app_same_length : forall us vs a b l, (length (us ++ a :: nil) = l) + -> (length (vs ++ a :: nil) = l) -> + (us ++ a :: nil) .+ (vs ++ b :: nil) = (us .+ vs) ++ (a + b) :: nil. Admitted. - Lemma app_zeros : forall a us, (a :: (zeros (length us))) .+ us = a :: us. - Admitted. - - Lemma mul_bi'_add : forall n us vs, - mul_bi' n (us .+ vs) = mul_bi' n us .+ mul_bi' n vs. + Lemma mul_bi'_add : forall us n vs l, (length us = l) -> (length vs = l) -> + mul_bi' n (rev (us .+ vs)) = + mul_bi' n (rev us) .+ mul_bi' n (rev vs). Proof. - intros. - induction us. { - rewrite mul_bi'_n_nil. + induction us using rev_ind; intros. { rewrite add_nil_l. + rewrite mul_bi'_n_nil. rewrite add_nil_l; auto. - } { - rewrite <- app_zeros. - rewrite mul_bi'_add_zeros. - rewrite <- add_assoc. - rewrite mul_bi'_add_zeros. - rewrite IHus. - rewrite add_assoc. - f_equal. - } - Qed. + } { + destruct vs using rev_ind. { + rewrite add_nil_r. + rewrite mul_bi'_n_nil. + rewrite add_nil_r; auto. + } { + simpl in *. + simpl_list. + rewrite (add_app_same_length us vs x x0 l); auto. + Focus 2. + replace l with (length (vs ++ x0 :: nil)) by (apply H0). + simpl_list; simpl; auto. + (* end focus 2 *) + rewrite rev_unit. + rewrite mul_bi'_cons. + rewrite mul_bi'_cons. + rewrite mul_bi'_cons. + rewrite add_first_terms. + rewrite rev_length. + rewrite rev_length. + rewrite rev_length. + assert (length us = pred l). + replace l with (length (us ++ x :: nil)) by (apply H). + rewrite app_length; simpl; omega. + assert (length vs = pred l). + replace l with (length (vs ++ x0 :: nil)) by (apply H0). + rewrite app_length; simpl; omega. + rewrite (IHus n vs (pred l)). + replace (length us) with (pred l) by (apply H). + replace (length vs) with (pred l) by (apply H). + rewrite (add_same_length us vs (pred l)). + f_equal; ring. + apply H1. apply H2. apply H1. apply H2. + } + } + Qed. Lemma add_leading_zeroes : forall n us vs, (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs). Admitted. - - Lemma rev_add : forall us vs, - rev(us .+ vs) = rev us .+ rev vs. + + Lemma rev_add_rev : forall us vs, (rev us) .+ (rev vs) = rev (us .+ vs). Admitted. - Lemma mul_bi_add : forall n us vs, + Lemma mul_bi_add : forall n us vs, (length us = length vs) -> mul_bi n (us .+ vs) = mul_bi n us .+ mul_bi n vs. Proof. intros. unfold mul_bi; simpl. - replace (rev (us .+ vs)) with (rev us .+ rev vs). - rewrite mul_bi'_add. rewrite add_leading_zeroes. - rewrite rev_add; auto. - rewrite <- rev_add; auto. + rewrite mul_bi'_add. + rewrite rev_add_rev; auto. Qed. Lemma mul_bi_rep : forall i vs, @@ -442,6 +404,7 @@ Module BaseSystem (Import B:BaseCoefs). Proof. exact mul'_rep. Qed. +Print Assumptions mul_rep. End BaseSystem. Module Type PolynomialBaseParams. -- cgit v1.2.3 From 612d7242648366fd9eb6a9c4c5444a48cd192d1a Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Tue, 27 Oct 2015 17:26:30 -0400 Subject: Proved add_same_length lemma. --- src/Galois/BaseSystem.v | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index e399a93d4..3e1fd0f74 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -265,9 +265,36 @@ Module BaseSystem (Import B:BaseCoefs). unfold mul_bi'; auto. Qed. + Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs). + Proof. + auto. + Qed. + Lemma add_same_length : forall us vs l, (length us = l) -> (length vs = l) -> length (us .+ vs) = l. - Admitted. + Proof. + induction us; intros. { + rewrite add_nil_l. + apply H0. + } { + destruct vs. { + rewrite add_nil_r; apply H. + } { + rewrite add_first_terms. + rewrite cons_length. + rewrite (IHus vs (pred l)). + apply NPeano.Nat.succ_pred_pos. + replace l with (length (a :: us)) by (apply H). + rewrite cons_length; simpl. + SearchAbout S. + apply gt_Sn_O. + replace l with (length (a :: us)) by (apply H). + rewrite cons_length; simpl; auto. + replace l with (length (z :: vs)) by (apply H). + rewrite cons_length; simpl; auto. + } + } + Qed. Lemma add_app_same_length : forall us vs a b l, (length (us ++ a :: nil) = l) -> (length (vs ++ a :: nil) = l) -> -- cgit v1.2.3 From a4cb5c05c66c66c09ab3531e9633d524c63f4da5 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Wed, 28 Oct 2015 15:28:34 -0400 Subject: BaseSystem: proved all admits. --- src/Galois/BaseSystem.v | 275 +++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 248 insertions(+), 27 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 3e1fd0f74..5496ed3d8 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -170,6 +170,11 @@ Module BaseSystem (Import B:BaseCoefs). rewrite IHxs; auto. Qed. + Lemma mul_bi'_zeros : forall n m, mul_bi' n (zeros m) = zeros m. + induction m; intros; auto. + simpl; f_equal; apply IHm. + Qed. + Lemma mul_bi_single : forall m n x, (n + m < length base)%nat -> decode (mul_bi n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n. @@ -181,7 +186,6 @@ Module BaseSystem (Import B:BaseCoefs). rewrite plus_0_r. ring_simplify. replace (nth_default 0 base n * nth_default 0 base 0) with (nth_default 0 base 0 * nth_default 0 base n) by ring. - SearchAbout Z.div. rewrite Z_div_mult; try ring. apply base_positive. @@ -191,12 +195,14 @@ Module BaseSystem (Import B:BaseCoefs). auto. } { simpl; ssimpl_list; simpl. - replace (mul_bi' n (rev (zeros m) ++ 0 :: nil)) with (zeros (S m)) by admit. - intros; simpl; ssimpl_list; simpl. + rewrite rev_zeros. + rewrite zeros_app0. + rewrite mul_bi'_zeros. + simpl; ssimpl_list; simpl. rewrite length_zeros. rewrite app_cons_app_app. rewrite rev_zeros. - intros; simpl; ssimpl_list; simpl. + simpl; ssimpl_list; simpl. rewrite zeros_app0. rewrite app_assoc. rewrite app_zeros_zeros. @@ -204,7 +210,7 @@ Module BaseSystem (Import B:BaseCoefs). unfold crosscoef; simpl; ring_simplify. rewrite NPeano.Nat.add_1_r. rewrite base_good by auto. - rewrite Z_div_mult. + rewrite Z_div_mult by (apply base_positive; rewrite nth_default_eq; apply nth_In; auto). rewrite <- Z.mul_assoc. rewrite <- Z.mul_comm. rewrite <- Z.mul_assoc. @@ -213,11 +219,7 @@ Module BaseSystem (Import B:BaseCoefs). rewrite Z.mul_cancel_l by auto. rewrite <- base_good by auto. ring. - - apply base_positive. - rewrite nth_default_eq. - apply nth_In; auto. - } + } Qed. Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil). @@ -286,7 +288,6 @@ Module BaseSystem (Import B:BaseCoefs). apply NPeano.Nat.succ_pred_pos. replace l with (length (a :: us)) by (apply H). rewrite cons_length; simpl. - SearchAbout S. apply gt_Sn_O. replace l with (length (a :: us)) by (apply H). rewrite cons_length; simpl; auto. @@ -296,10 +297,68 @@ Module BaseSystem (Import B:BaseCoefs). } Qed. - Lemma add_app_same_length : forall us vs a b l, (length (us ++ a :: nil) = l) - -> (length (vs ++ a :: nil) = l) -> + Lemma length0_nil : forall A (xs : list A), length xs = 0%nat -> xs = nil. + Proof. + induction xs; intros; auto. + elimtype False. + assert (0 <> length (a :: xs))%nat. + rewrite cons_length. + apply O_S. + contradiction H0. + rewrite H; auto. + Qed. + + Lemma add_app_same_length : forall l us vs a b, + (length us = l) -> (length vs = l) -> (us ++ a :: nil) .+ (vs ++ b :: nil) = (us .+ vs) ++ (a + b) :: nil. - Admitted. + Proof. + induction l; intros. { + assert (us = nil) by (apply length0_nil; apply H). + assert (vs = nil) by (apply length0_nil; apply H0). + rewrite H1; rewrite app_nil_l. + rewrite H2; rewrite app_nil_l. + rewrite add_nil_l. + rewrite app_nil_l. + auto. + } { + destruct us. { + rewrite app_nil_l. + rewrite add_nil_l. + destruct vs. { + rewrite app_nil_l. + rewrite app_nil_l. + auto. + } { + elimtype False. + replace (length nil) with (0%nat) in H by auto. + assert (0 <> S l)%nat. + apply O_S. + contradiction H1. + } + } { + destruct vs. { + elimtype False. + replace (length nil) with (0%nat) in H0 by auto. + assert (0 <> S l)%nat. + apply O_S. + contradiction H1. + } { + rewrite add_first_terms. + rewrite <- app_comm_cons. + rewrite <- app_comm_cons. + rewrite add_first_terms. + rewrite <- app_comm_cons. + rewrite IHl; f_equal. + assert (length (z :: us) = S (length us)) by (apply cons_length). + assert (S (length us) = S l) by auto. + auto. + assert (length (z0 :: vs) = S (length vs)) by (apply cons_length). + assert (S (length vs) = S l) by auto. + auto. + } + } + } + Qed. Lemma mul_bi'_add : forall us n vs l, (length us = l) -> (length vs = l) -> mul_bi' n (rev (us .+ vs)) = @@ -317,11 +376,7 @@ Module BaseSystem (Import B:BaseCoefs). } { simpl in *. simpl_list. - rewrite (add_app_same_length us vs x x0 l); auto. - Focus 2. - replace l with (length (vs ++ x0 :: nil)) by (apply H0). - simpl_list; simpl; auto. - (* end focus 2 *) + rewrite (add_app_same_length (pred l) us vs x x0); auto. rewrite rev_unit. rewrite mul_bi'_cons. rewrite mul_bi'_cons. @@ -342,25 +397,191 @@ Module BaseSystem (Import B:BaseCoefs). rewrite (add_same_length us vs (pred l)). f_equal; ring. apply H1. apply H2. apply H1. apply H2. + assert (length (us ++ x :: nil) = S (length us)). + rewrite app_length. + replace (length (x :: nil)) with 1%nat by auto; omega. + assert (S (length us) = l). + rewrite <- H1. apply H. + replace l with (S (length us)) by apply H2. auto. + assert (length (vs ++ x0 :: nil) = S (length vs)). + rewrite app_length. + replace (length (x0 :: nil)) with 1%nat by auto; omega. + assert (S (length vs) = l). + rewrite <- H1. apply H0. + replace l with (S (length vs)) by apply H2. auto. } } Qed. - Lemma add_leading_zeroes : forall n us vs, + Lemma zeros_cons0 : forall n, 0 :: zeros n = zeros (S n). + auto. + Qed. + + Lemma add_leading_zeros : forall n us vs, (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs). - Admitted. + induction n; intros; auto. + rewrite <- zeros_cons0; simpl. + rewrite IHn; auto. + Qed. - Lemma rev_add_rev : forall us vs, (rev us) .+ (rev vs) = rev (us .+ vs). - Admitted. + Lemma rev_add_rev : forall us vs l, (length us = l) -> (length vs = l) -> + (rev us) .+ (rev vs) = rev (us .+ vs). + Proof. + induction us; intros. { + rewrite add_nil_l. + rewrite add_nil_l; auto. + } { + destruct vs. { + elimtype False. + replace (length nil) with 0%nat in H0 by auto. + rewrite cons_length in H. + assert (0 <> l)%nat by (rewrite <- H; apply O_S). + contradiction. + } { + rewrite add_first_terms. + simpl. + assert (length us = pred l). + rewrite cons_length in H. + rewrite <- H; auto. + assert (length vs = pred l). + rewrite cons_length in H0. + rewrite <- H0; auto. + rewrite (add_app_same_length (pred l) _ _ _ _); try (rewrite rev_length; auto). + rewrite (IHus vs (pred l)); auto. + } + } + Qed. - Lemma mul_bi_add : forall n us vs, (length us = length vs) -> + Lemma mul_bi'_length : forall us n, length (mul_bi' n us) = length us. + Proof. + induction us; intros; auto. + rewrite mul_bi'_cons. + rewrite cons_length. + rewrite cons_length. + replace (length (mul_bi' n us)) with (length us); auto. + Qed. + + Lemma add_comm : forall us vs, us .+ vs = vs .+ us. + Proof. + induction us; intros. { + rewrite add_nil_l. + rewrite add_nil_r. + auto. + } { + destruct vs. { + rewrite add_nil_l. + rewrite add_nil_r; auto. + } { + rewrite add_first_terms. + rewrite add_first_terms. + rewrite IHus; f_equal; omega. + } + } + Qed. + + Lemma mul_bi_add_same_length : forall n us vs l, (length us = l) -> (length vs = l) -> mul_bi n (us .+ vs) = mul_bi n us .+ mul_bi n vs. Proof. intros. unfold mul_bi; simpl. - rewrite add_leading_zeroes. - rewrite mul_bi'_add. - rewrite rev_add_rev; auto. + rewrite add_leading_zeros. + rewrite (mul_bi'_add us n vs l); auto. + rewrite (rev_add_rev _ _ l). + rewrite add_comm; f_equal. + rewrite mul_bi'_length; rewrite rev_length. + apply H. + rewrite mul_bi'_length; rewrite rev_length. + apply H0. + Qed. + + Lemma add_zeros_same_length : forall us, us .+ (zeros (length us)) = us. + Proof. + induction us; auto; simpl. + rewrite IHus; f_equal; ring. + Qed. + + Lemma add_trailing_zeros : forall us vs, (length us >= length vs)%nat -> + us .+ vs = us .+ (vs ++ (zeros (length us - length vs))). + Proof. + induction us; intros. { + rewrite add_nil_l. + rewrite add_nil_l. + simpl in *. + assert (length vs = 0%nat) by omega. + simpl_list; auto. + } { + destruct vs. { + rewrite add_nil_r. + rewrite app_nil_l. + simpl. + f_equal; try ring. + symmetry. + apply add_zeros_same_length. + } { + rewrite add_first_terms; simpl. + f_equal. + apply IHus. + rewrite cons_length in H. + rewrite cons_length in H. + intuition. + } + } + Qed. + + Lemma mul_bi_length : forall us n, length (mul_bi n us) = (length us + n)%nat. + Proof. + induction us; intros; simpl. { + unfold mul_bi; simpl; simpl_list. + apply length_zeros. + } { + unfold mul_bi; simpl; simpl_list. + rewrite length_zeros. + rewrite mul_bi'_length; simpl_list; simpl. + omega. + } + Qed. + + Lemma mul_bi_trailing_zeros : forall m n us, mul_bi n us ++ zeros m = mul_bi n (us ++ zeros m). + Proof. + unfold mul_bi. + induction m; intros; simpl_list; auto. + rewrite <- zeros_app0. + rewrite app_assoc. + rewrite IHm; clear IHm. + simpl. + repeat (rewrite rev_app_distr). + simpl. + repeat (rewrite rev_zeros). + rewrite app_assoc. + auto. + Qed. + + Lemma mul_bi_add_longer : forall n us vs, (length us >= length vs)%nat -> + mul_bi n (us .+ vs) = mul_bi n us .+ mul_bi n vs. + Proof. + intros. + rewrite add_trailing_zeros by auto. + rewrite (add_trailing_zeros (mul_bi n us) (mul_bi n vs)) by (repeat (rewrite mul_bi_length); omega). + erewrite mul_bi_add_same_length by (eauto; simpl_list; rewrite length_zeros; omega). + f_equal. + rewrite mul_bi_trailing_zeros. + repeat (rewrite mul_bi_length). + f_equal. f_equal. f_equal. + omega. + Qed. + + Lemma mul_bi_add : forall n us vs, + mul_bi n (us .+ vs) = mul_bi n us .+ mul_bi n vs. + Proof. + intros. + destruct (le_ge_dec (length us) (length vs)). { + assert (length vs >= length us)%nat by auto. + rewrite add_comm. + replace (mul_bi n us .+ mul_bi n vs) with (mul_bi n vs .+ mul_bi n us) by (apply add_comm). + apply (mul_bi_add_longer n vs us); auto. + } { + apply mul_bi_add_longer; auto. + } Qed. Lemma mul_bi_rep : forall i vs, -- cgit v1.2.3 From 7abc73670c7b7bc2cce159ee4e1d00f812f8186a Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Wed, 28 Oct 2015 15:57:16 -0400 Subject: BaseSystem: removed axiom b0_1. --- src/Galois/BaseSystem.v | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index f0bc0af09..b9821ded0 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -54,7 +54,6 @@ Qed. 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 -> -- cgit v1.2.3 From 2c586f398aa8eaca45b99937cb1068923b87e060 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 30 Oct 2015 15:11:32 -0400 Subject: ModularBaseSystem skeleton --- src/Galois/ModularBaseSystem.v | 56 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 src/Galois/ModularBaseSystem.v diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v new file mode 100644 index 000000000..4aceacfca --- /dev/null +++ b/src/Galois/ModularBaseSystem.v @@ -0,0 +1,56 @@ +Require Import Zpower ZArith. +Require Import List. +Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. +Open Scope Z_scope. + +Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus). + (* TODO: do we actually want B and M "up there" in the type parameters? I was + * imagining writing something like "Paramter Module M : Modulus". *) + + Parameter k : Z. + Parameter c : Z. + Axiom modulus_pseudomersenne : primeToZ modulus = 2^k - c. + + Axiom base_matches_modulus : + forall i j, + (i < length base)%nat -> + (j < length base)%nat -> + (i+j >= length base)%nat-> + let b := nth_default 0 base in + let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in + b i * b j = r * 2^k * b (i+j-length base)%nat. + + Axiom b0_1 : nth_default 0 base 1 = 1. +End PseudoMersenneBaseParams. + +Module Type GFrep (Import M:Modulus). + Module Import GF := GaloisTheory M. + (* TODO: could GF notation be in Galois, not GaloisTheory *) + Parameter T : Type. + Parameter fromGF : GF -> T. + Parameter toGF : T -> GF. + + Parameter rep : T -> GF -> Prop. + Local Notation "u '~=' x" := (rep u x) (at level 70). + Axiom fromGF_rep : forall x, fromGF x ~= x. + Axiom rep_toGF : forall u x, u ~= x -> toGF u = x. + + Parameter add : T -> T -> T. + Axiom add_rep : forall u v x y, u ~= x -> v ~= y -> add u v ~= (x+y)%GF. + + Parameter sub : T -> T -> T. + Axiom sub_rep : forall u v x y, u ~= x -> v ~= y -> sub u v ~= (x-y)%GF. + (* TBD: sub may need to be in BaseSystem as well *) + + 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 (B:BaseCoefs) (M:Modulus) (P:PseudoMersenneBaseParams B M) <: GFrep M. + Module Import GF := GaloisTheory M. + (* good luck *) +End GFPseudoMersenneBase. -- cgit v1.2.3 From 75f3b3313ebcab5ddd27aa343e5345a14ef29cb3 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Wed, 4 Nov 2015 00:14:36 -0500 Subject: Relocated boring tactic to ListUtil and added combine_truncate lemma. --- src/Galois/BaseSystem.v | 10 ---------- src/Util/ListUtil.v | 16 ++++++++++++++++ 2 files changed, 16 insertions(+), 10 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 835cea5f9..fff37f75a 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -86,16 +86,6 @@ Module BaseSystem (Import B:BaseCoefs). induction n; simpl; auto. Qed. - Ltac boring := - simpl; intuition; - repeat match goal with - | [ H : _ |- _ ] => rewrite H; clear H - | _ => progress autounfold in * - | _ => progress try autorewrite with core - | _ => progress simpl in * - | _ => progress intuition - end; ring || eauto. - Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m). Proof. induction n; boring. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index d1c12dbfd..5a3f304a7 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2,6 +2,16 @@ Require Import List. Require Import Omega. Require Import Arith.Peano_dec. +Ltac boring := + simpl; intuition; + repeat match goal with + | [ H : _ |- _ ] => rewrite H; clear H + | _ => progress autounfold in * + | _ => progress try autorewrite with core + | _ => progress simpl in * + | _ => progress intuition + end; eauto. + Ltac nth_tac' := intros; simpl in *; unfold error,value in *; repeat progress (match goal with | [ H: ?x = Some _ |- context[match ?x with Some _ => ?a | None => ?a end ] ] => destruct x @@ -125,3 +135,9 @@ Proof. assert (Some b0=Some b1) as HA by (rewrite <-H, <-H0; auto). injection HA; intros; subst; auto. Qed. + +Lemma combine_truncate : forall {A} (xs ys : list A), + combine xs ys = combine xs (firstn (length xs) ys). +Proof. + induction xs; destruct ys; boring. +Qed. -- cgit v1.2.3 From d79d415ec2a268aea2cf9f331abad3bb93016b42 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Wed, 4 Nov 2015 00:16:01 -0500 Subject: ModularBaseSystem: defined an extended base system to represent unreduced products. --- src/Galois/ModularBaseSystem.v | 108 ++++++++++++++++++++++++++++++----------- 1 file changed, 81 insertions(+), 27 deletions(-) diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v index 4aceacfca..52297e6ef 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/Galois/ModularBaseSystem.v @@ -1,6 +1,7 @@ Require Import Zpower ZArith. Require Import List. Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. +Require Import Util.ListUtil. Open Scope Z_scope. Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus). @@ -24,33 +25,86 @@ Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus). End PseudoMersenneBaseParams. Module Type GFrep (Import M:Modulus). - Module Import GF := GaloisTheory M. - (* TODO: could GF notation be in Galois, not GaloisTheory *) - Parameter T : Type. - Parameter fromGF : GF -> T. - Parameter toGF : T -> GF. - - Parameter rep : T -> GF -> Prop. - Local Notation "u '~=' x" := (rep u x) (at level 70). - Axiom fromGF_rep : forall x, fromGF x ~= x. - Axiom rep_toGF : forall u x, u ~= x -> toGF u = x. - - Parameter add : T -> T -> T. - Axiom add_rep : forall u v x y, u ~= x -> v ~= y -> add u v ~= (x+y)%GF. - - Parameter sub : T -> T -> T. - Axiom sub_rep : forall u v x y, u ~= x -> v ~= y -> sub u v ~= (x-y)%GF. - (* TBD: sub may need to be in BaseSystem as well *) - - 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 *) + Module Import GF := GaloisTheory M. + (* TODO: could GF notation be in Galois, not GaloisTheory *) + Parameter T : Type. + Parameter fromGF : GF -> T. + Parameter toGF : T -> GF. + + Parameter rep : T -> GF -> Prop. + Local Notation "u '~=' x" := (rep u x) (at level 70). + Axiom fromGF_rep : forall x, fromGF x ~= x. + Axiom rep_toGF : forall u x, u ~= x -> toGF u = x. + + Parameter add : T -> T -> T. + Axiom add_rep : forall u v x y, u ~= x -> v ~= y -> add u v ~= (x+y)%GF. + + Parameter sub : T -> T -> T. + Axiom sub_rep : forall u v x y, u ~= x -> v ~= y -> sub u v ~= (x-y)%GF. + (* TBD: sub may need to be in BaseSystem as well *) + + 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 (B:BaseCoefs) (M:Modulus) (P:PseudoMersenneBaseParams B M) <: GFrep M. - Module Import GF := GaloisTheory M. - (* good luck *) +Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBaseParams BC M) <: GFrep M. + Module Import GF := GaloisTheory M. + Module EC <: BaseCoefs. + Definition base := BC.base ++ (map (Z.mul (2^(P.k))) BC.base). + + Lemma base_positive : forall b, In b base -> b > 0. + Proof. + Admitted. + + 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. + Admitted. + + End EC. + + Module E := BaseSystem EC. + Module B := BaseSystem BC. + + (* 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. + intros. + unfold B.decode, B.decode', E.decode, E.decode'. + rewrite combine_truncate. + rewrite (combine_truncate us EC.base). + f_equal; f_equal. + unfold EC.base. + rewrite (firstn_app _ _ (map (Z.mul (2 ^ P.k)) BC.base)); auto. + Qed. + + + Lemma mul_rep_extended : forall (us vs : B.digits), + (length us <= length BC.base)%nat -> + (length vs <= length BC.base)%nat -> + B.decode us * B.decode vs = E.decode (E.mul us vs). + Proof. + intros. + rewrite E.mul_rep by (unfold EC.base; simpl_list; omega). + f_equal; rewrite decode_short; auto. + Qed. + + (* a = r + s(2^k) = r + s(2^k - c + c) = r + s(2^k - c) + cs = r + cs *) + (* Fixpoint reduce (us : unreduced_digits) : digits := *) + + End GFPseudoMersenneBase. -- cgit v1.2.3 From 78382dea5eec746c5359e103462d9974e5bc64c7 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Thu, 5 Nov 2015 13:48:27 -0500 Subject: ModularBaseSystem: Implemented reduce and proved reduce_rep, currently working on admits (extended_shiftadd and reduce_defn). --- src/Galois/ModularBaseSystem.v | 73 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 71 insertions(+), 2 deletions(-) diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v index 52297e6ef..b3c310969 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/Galois/ModularBaseSystem.v @@ -103,8 +103,77 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara f_equal; rewrite decode_short; auto. Qed. + (* Converts from length of E.base to length of B.base by reduction modulo M.*) + Fixpoint reduce (us : E.digits) : B.digits := + let high := skipn (length BC.base) us in + let low := firstn (length BC.base) us in + let wrap := map (Z.mul P.c) high in + B.add low wrap. + + (* TODO: move this somewhere more appropriate/improve strategy? *) + Lemma Prime_nonzero: forall (p : Prime), primeToZ p <> 0. + Admitted. + + Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b. + Proof. + intros. + rewrite Zplus_mod. + rewrite Z.mod_mul; auto; simpl. + rewrite Zmod_mod; auto. + Qed. + (* a = r + s(2^k) = r + s(2^k - c + c) = r + s(2^k - c) + cs = r + cs *) - (* Fixpoint reduce (us : unreduced_digits) : digits := *) - + Lemma pseudomersenne_add: forall x y, (x + ((2^P.k) * y)) mod modulus = (x + (P.c * y)) mod modulus. + Proof. + intros. + replace (2^P.k) with (((2^P.k) - P.c) + P.c) by auto. + rewrite Z.mul_add_distr_r. + rewrite Zplus_mod. + rewrite <- P.modulus_pseudomersenne. + rewrite Z.mul_comm. + rewrite mod_mult_plus; try apply Prime_nonzero. + rewrite <- Zplus_mod; auto. + Qed. + + Lemma extended_shiftadd: forall (us : E.digits), E.decode us = + B.decode (firstn (length BC.base) us) + + (2^P.k * B.decode (skipn (length BC.base) us)). + Proof. + intros. + rewrite decode_short; try (rewrite firstn_length; rewrite Min.le_min_l; auto). + Admitted. + + (* TODO: definition of reduce, but isn't unfolding and solving automatically. *) + Lemma reduce_defn : forall (us : E.digits), reduce us = + B.add (firstn (length BC.base) us) (map (Z.mul P.c) (skipn (length BC.base) us)). + Proof. + Admitted. + + (* TODO: add in preconditions for B *) + Lemma base_bounds : forall us, 0 <= B.decode us < modulus. + Admitted. + + Lemma decode_mod : forall us, B.decode us = B.decode us mod modulus. + Proof. + intros; rewrite Zmod_small; auto. + apply base_bounds. + Qed. + + Lemma reduce_rep : forall us, B.decode (reduce us) = (E.decode us) mod modulus. + Proof. + intros. + rewrite decode_mod. + rewrite extended_shiftadd. + rewrite pseudomersenne_add. + remember (firstn (length BC.base) us) as low. + remember (skipn (length BC.base) us) as high. + replace (reduce us) with (B.add low (map (Z.mul P.c) high)) by (rewrite reduce_defn; rewrite Heqlow; rewrite Heqhigh; auto). + unfold B.decode. + rewrite B.add_rep. + replace (map (Z.mul P.c) high) with (B.mul_each P.c high) by auto. + rewrite B.mul_each_rep; auto. + Qed. + +Print Assumptions reduce_rep. End GFPseudoMersenneBase. -- cgit v1.2.3 From 33193a5fb30b39d794d4c77f2229145e90130410 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Thu, 5 Nov 2015 22:54:39 -0500 Subject: Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem. --- src/Galois/BaseSystem.v | 72 ++++++++++++++++++++++++++++++++++++++++++------- src/Util/ListUtil.v | 31 ++++++++++++++++++++- 2 files changed, 93 insertions(+), 10 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index fff37f75a..345929475 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -40,7 +40,14 @@ Module BaseSystem (Import B:BaseCoefs). Definition decode' bs u := fold_right accumulate 0 (combine u bs). Definition decode := decode' base. Hint Unfold accumulate. - + + Lemma decode_truncate : forall us, decode us = decode (firstn (length base) us). + Proof. + intros. + unfold decode, decode'. + rewrite combine_truncate_l; auto. + Qed. + Fixpoint add (us vs:digits) : digits := match us,vs with | u::us', v::vs' => u+v :: add us' vs' @@ -59,6 +66,13 @@ Module BaseSystem (Import B:BaseCoefs). auto. Qed. + Lemma decode_base_nil : forall us, decode' nil us = 0. + Proof. + intros. + unfold decode'. + rewrite combine_truncate_l; auto. + Qed. + (* mul_geomseq is a valid multiplication algorithm if b_i = b_1^i *) Fixpoint mul_geomseq (us vs:digits) : digits := match us,vs with @@ -73,6 +87,54 @@ Module BaseSystem (Import B:BaseCoefs). induction bs; destruct vs; auto; simpl; try rewrite IHbs; ring. Qed. + Lemma decode'_cons : forall x1 x2 xs1 xs2, + decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2. + Proof. + unfold decode'; boring. + Qed. + + Hint Rewrite decode'_cons. + + Lemma mul_each_base : forall us bs c, + decode' bs (mul_each c us) = decode' (mul_each c bs) us. + Proof. + induction us; intros; simpl; auto. + destruct bs. + apply decode_base_nil. + unfold mul_each; boring. + replace (z * (c * a)) with (c * z * a) by ring; f_equal. + unfold mul_each in IHus. + apply IHus. + Qed. + + Lemma base_app : forall us low high, + decode' (low ++ high) us = decode' low (firstn (length low) us) + decode' high (skipn (length low) us). + Proof. + induction us; intros. { + rewrite firstn_nil. + rewrite skipn_nil. + do 3 rewrite decode_nil; auto. + } { + destruct low; auto. + replace (skipn (length (z :: low)) (a :: us)) with (skipn (length (low)) (us)) by auto. + simpl. + do 2 rewrite decode'_cons. + rewrite IHus. + ring. + } + Qed. + + Lemma base_mul_app : forall low c us, + decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) + + c * decode' low (skipn (length low) us). + Proof. + intros. + rewrite base_app; f_equal. + rewrite <- mul_each_rep. + symmetry; apply mul_each_base. + Qed. + + Definition crosscoef i j : Z := let b := nth_default 0 base in (b(i) * b(j)) / b(i+j)%nat. @@ -129,14 +191,6 @@ Module BaseSystem (Import B:BaseCoefs). Hint Extern 1 (@eq Z _ _) => ring. - Lemma decode'_cons : forall x1 x2 xs1 xs2, - decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2. - Proof. - unfold decode'; boring. - Qed. - - Hint Rewrite decode'_cons. - Lemma decode_single : forall n bs x, decode' bs (zeros n ++ x :: nil) = nth_default 0 bs n * x. Proof. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 5a3f304a7..4d807c779 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -136,8 +136,37 @@ Proof. injection HA; intros; subst; auto. Qed. -Lemma combine_truncate : forall {A} (xs ys : list A), +Lemma combine_truncate_r : forall {A} (xs ys : list A), combine xs ys = combine xs (firstn (length xs) ys). Proof. induction xs; destruct ys; boring. Qed. + +Lemma combine_truncate_l : forall {A} (xs ys : list A), + combine xs ys = combine (firstn (length ys) xs) ys. +Proof. + induction xs; destruct ys; boring. +Qed. + +Lemma firstn_nil : forall {A} n, firstn n nil = @nil A. +Proof. + destruct n; auto. +Qed. + +Lemma skipn_nil : forall {A} n, skipn n nil = @nil A. +Proof. + destruct n; auto. +Qed. + +Lemma firstn_app : forall A (l l': list A), firstn (length l) (l ++ l') = l. +Proof. + intros. + induction l; simpl; auto. + f_equal; auto. +Qed. + +Lemma skipn_app : forall A (l l': list A), skipn (length l) (l ++ l') = l'. +Proof. + intros. + induction l; simpl; auto. +Qed. -- cgit v1.2.3 From 42ba677296b78b93396f031c57045116b9361897 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Thu, 5 Nov 2015 22:55:54 -0500 Subject: ModularBaseSystem: finished proving all admits for reduce_rep; proved base_positive for extended base system. --- src/Galois/ModularBaseSystem.v | 74 +++++++++++++++++++++++++----------------- 1 file changed, 45 insertions(+), 29 deletions(-) diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v index b3c310969..61ca58442 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/Galois/ModularBaseSystem.v @@ -22,6 +22,10 @@ Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus). b i * b j = r * 2^k * b (i+j-length base)%nat. Axiom b0_1 : nth_default 0 base 1 = 1. + + (* Probably implied by modulus_pseudomersenne. *) + Axiom k_pos : 0 <= k. + End PseudoMersenneBaseParams. Module Type GFrep (Import M:Modulus). @@ -58,13 +62,34 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara Lemma base_positive : forall b, In b base -> b > 0. Proof. - Admitted. + unfold base. intros. + rewrite in_app_iff in H. + destruct H. { + apply BC.base_positive; auto. + } { + specialize BC.base_positive. + induction BC.base; intros. { + simpl in H; intuition. + } { + simpl in H. + destruct H; subst. + replace 0 with (2 ^ P.k * 0) by auto. + apply (Zmult_gt_compat_l a 0 (2 ^ P.k)). + rewrite Z.gt_lt_iff. + apply Z.pow_pos_nonneg; intuition. + apply P.k_pos. + apply H0; left; auto. + apply IHl; auto. + intros. apply H0; auto. right; 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. + b i * b j = r * b (i+j)%nat. Admitted. End EC. @@ -85,8 +110,8 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara Proof. intros. unfold B.decode, B.decode', E.decode, E.decode'. - rewrite combine_truncate. - rewrite (combine_truncate us EC.base). + rewrite combine_truncate_r. + rewrite (combine_truncate_r us EC.base). f_equal; f_equal. unfold EC.base. rewrite (firstn_app _ _ (map (Z.mul (2 ^ P.k)) BC.base)); auto. @@ -104,15 +129,20 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara Qed. (* Converts from length of E.base to length of B.base by reduction modulo M.*) - Fixpoint reduce (us : E.digits) : B.digits := + Definition reduce (us : E.digits) : B.digits := let high := skipn (length BC.base) us in let low := firstn (length BC.base) us in let wrap := map (Z.mul P.c) high in B.add low wrap. - (* TODO: move this somewhere more appropriate/improve strategy? *) Lemma Prime_nonzero: forall (p : Prime), primeToZ p <> 0. - Admitted. + Proof. + unfold Prime. intros. + destruct p. + simpl. intro. + subst. + apply Znumtheory.not_prime_0; auto. + Qed. Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b. Proof. @@ -140,40 +170,26 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara (2^P.k * B.decode (skipn (length BC.base) us)). Proof. intros. - rewrite decode_short; try (rewrite firstn_length; rewrite Min.le_min_l; auto). - Admitted. - - (* TODO: definition of reduce, but isn't unfolding and solving automatically. *) - Lemma reduce_defn : forall (us : E.digits), reduce us = - B.add (firstn (length BC.base) us) (map (Z.mul P.c) (skipn (length BC.base) us)). - Proof. - Admitted. - - (* TODO: add in preconditions for B *) - Lemma base_bounds : forall us, 0 <= B.decode us < modulus. - Admitted. - - Lemma decode_mod : forall us, B.decode us = B.decode us mod modulus. - Proof. - intros; rewrite Zmod_small; auto. - apply base_bounds. + unfold B.decode, E.decode; rewrite <- B.mul_each_rep. + replace B.decode' with E.decode' by auto. + unfold EC.base. + replace (map (Z.mul (2 ^ P.k)) BC.base) with (E.mul_each (2 ^ P.k) BC.base) by auto. + rewrite E.base_mul_app. + rewrite <- E.mul_each_rep; auto. Qed. - Lemma reduce_rep : forall us, B.decode (reduce us) = (E.decode us) mod modulus. + Lemma reduce_rep : forall us, B.decode (reduce us) mod modulus = (E.decode us) mod modulus. Proof. intros. - rewrite decode_mod. rewrite extended_shiftadd. rewrite pseudomersenne_add. + unfold reduce. remember (firstn (length BC.base) us) as low. remember (skipn (length BC.base) us) as high. - replace (reduce us) with (B.add low (map (Z.mul P.c) high)) by (rewrite reduce_defn; rewrite Heqlow; rewrite Heqhigh; auto). unfold B.decode. rewrite B.add_rep. replace (map (Z.mul P.c) high) with (B.mul_each P.c high) by auto. rewrite B.mul_each_rep; auto. Qed. -Print Assumptions reduce_rep. - End GFPseudoMersenneBase. -- cgit v1.2.3