From 724b7b2acb9b857d7c511a320973cead308117c6 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Fri, 11 Mar 2016 16:32:48 -0500 Subject: Refactored BaseSystem and ModularBaseSystem. --- src/BaseSystem.v | 103 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 53 insertions(+), 50 deletions(-) (limited to 'src/BaseSystem.v') diff --git a/src/BaseSystem.v b/src/BaseSystem.v index f0e0db077..e9e4bc9d4 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -5,19 +5,18 @@ Require Import Omega NPeano Arith. Local Open Scope Z. -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 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_good : +Class BaseVector (base : list Z):= { + base_positive : forall b, In b base -> b > 0; (* nonzero would probably work too... *) + b0_1 : forall x, nth_default x base 0 = 1; + 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. -End BaseCoefs. + b i * b j = r * b (i+j)%nat +}. -Module BaseSystem (Import B:BaseCoefs). +Section BaseSystem. + Context (base : list Z) (base_vector : BaseVector base). (** [BaseSystem] implements an constrained positional number system. A wide variety of bases are supported: the base coefficients are not required to be powers of 2, and it is NOT necessarily the case that @@ -221,9 +220,15 @@ Module BaseSystem (Import B:BaseCoefs). Proof. unfold mul_bi, decode. destruct m; simpl; simpl_list; simpl; intros. { - pose proof nth_error_base_nonzero. - boring; destruct base; nth_tac. + pose proof nth_error_base_nonzero as nth_nonzero. + case_eq base; [intros; boring | intros z l base_eq]. + specialize (b0_1 0); intro b0_1'. + rewrite base_eq in *. + rewrite nth_default_cons in b0_1'. + rewrite b0_1' in *. + boring; nth_tac. rewrite Z_div_mul'; eauto. + destruct x; ring. } { ssimpl_list. autorewrite with core. @@ -542,19 +547,14 @@ Module BaseSystem (Import B:BaseCoefs). 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. - (** PolynomialBaseCoeffs generates base vectors for [BaseSystem] using the extra assumption that $b_{i+j} = b_j b_j$. *) +Section PolynomialBaseCoefs. + Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : NPeano.ltb 0 baseLength = true). + (** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *) Definition bi i := (Zpos b1)^(Z.of_nat i). - Definition base := map bi (seq 0 baseLength). + Definition poly_base := map bi (seq 0 baseLength). - Lemma b0_1 : forall x, nth_default x base 0 = 1. - unfold base, bi, nth_default. + Lemma poly_b0_1 : forall x, nth_default x poly_base 0 = 1. + unfold poly_base, bi, nth_default. case_eq baseLength; intros. { assert ((0 < baseLength)%nat) by (rewrite <-NPeano.ltb_lt; apply baseLengthNonzero). @@ -563,9 +563,9 @@ Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs. auto. Qed. - Lemma base_positive : forall b, In b base -> b > 0. + Lemma poly_base_positive : forall b, In b poly_base -> b > 0. Proof. - unfold base. + unfold poly_base. intros until 0; intro H. rewrite in_map_iff in *. destruct H; destruct H. @@ -573,20 +573,20 @@ 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. + Lemma poly_base_defn : forall i, (i < length poly_base)%nat -> + nth_default 0 poly_base i = bi i. Proof. - unfold base, nth_default; nth_tac. + unfold poly_base, nth_default; nth_tac. Qed. - Lemma base_succ : - forall i, ((S i) < length base)%nat -> - let b := nth_default 0 base in + Lemma poly_base_succ : + forall i, ((S i) < length poly_base)%nat -> + let b := nth_default 0 poly_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. + repeat rewrite poly_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 @@ -598,13 +598,13 @@ Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs. 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 + Lemma poly_base_good: + forall i j, (i + j < length poly_base)%nat -> + let b := nth_default 0 poly_base in let r := (b i * b j) / b (i+j)%nat in b i * b j = r * b (i+j)%nat. Proof. - unfold base, nth_default; nth_tac. + unfold poly_base, nth_default; nth_tac. clear. unfold bi. @@ -614,24 +614,27 @@ Module PolynomialBaseCoefs (Import P:PolynomialBaseParams) <: BaseCoefs. rewrite <- Z.neq_mul_0. split; apply Z.pow_nonzero; try apply Zle_0_nat; try solve [intro H; inversion H]. Qed. + + Print BaseVector. + Instance PolyBaseVector : BaseVector poly_base := { + base_positive := poly_base_positive; + b0_1 := poly_b0_1; + base_good := poly_base_good + }. + End PolynomialBaseCoefs. -Module BasePoly2Degree32Params <: PolynomialBaseParams. - Definition b1 := 2%positive. +Import ListNotations. + +Section BaseSystemExample. Definition baseLength := 32%nat. Lemma baseLengthNonzero : NPeano.ltb 0 baseLength = true. compute; reflexivity. Qed. -End BasePoly2Degree32Params. - -Import ListNotations. - -Module BaseSystemExample. - Module BasePoly2Degree32Coefs := PolynomialBaseCoefs BasePoly2Degree32Params. - Module BasePoly2Degree32 := BaseSystem BasePoly2Degree32Coefs. - Import BasePoly2Degree32. + Definition base2 := poly_base 2 baseLength. - Example three_times_two : mul [1;1;0] [0;1;0] = [0;1;1;0;0]. + About mul. + Example three_times_two : @mul base2 [1;1;0] [0;1;0] = [0;1;1;0;0]. Proof. reflexivity. Qed. @@ -639,20 +642,20 @@ Module BaseSystemExample. (* python -c "e = lambda x: '['+''.join(reversed(bin(x)[2:])).replace('1','1;').replace('0','0;')[:-1]+']'; print(e(19259)); print(e(41781))" *) Definition a := [1;1;0;1;1;1;0;0;1;1;0;1;0;0;1]. Definition b := [1;0;1;0;1;1;0;0;1;1;0;0;0;1;0;1]. - Example da : decode a = 19259. + Example da : decode base2 a = 19259. Proof. reflexivity. Qed. - Example db : decode b = 41781. + Example db : decode base2 b = 41781. Proof. reflexivity. Qed. Example encoded_ab : - 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]. + mul base2 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 (mul a b) = 804660279. + Example dab : decode base2 (mul base2 a b) = 804660279. Proof. reflexivity. Qed. -- cgit v1.2.3