diff options
| -rw-r--r-- | src/BaseSystemProofs.v | 36 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 4 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 18 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 105 | ||||
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseRep.v | 2 |
5 files changed, 87 insertions, 78 deletions
diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index dfb9f5bdf..4414877b4 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -389,8 +389,8 @@ Section BaseSystemProofs. induction us; boring. Qed. - Lemma sub_length_le_max : forall us vs, - (length (sub us vs) <= max (length us) (length vs))%nat. + Lemma sub_length : forall us vs, + (length (sub us vs) = max (length us) (length vs))%nat. Proof. induction us, vs; boring. rewrite sub_nil_length; auto. @@ -511,5 +511,37 @@ Section BaseSystemProofs. rewrite rev_length; omega. Qed. + Lemma add_length_exact : forall us vs, + length (us .+ vs) = max (length us) (length vs). + Proof. + induction us; destruct vs; boring. + Qed. + + Lemma mul'_length_exact: forall us vs, + (length us <= length vs)%nat -> us <> nil -> + (length (mul' us vs) = pred (length us + length vs))%nat. + Proof. + induction us; intros; try solve [boring]. + unfold mul'; fold mul'. + unfold mul_each. + rewrite add_length_exact, map_length, mul_bi_length, length_cons. + destruct us. + + rewrite Max.max_0_r. simpl; omega. + + rewrite Max.max_l; [ omega | ]. + rewrite IHus by ( congruence || simpl in *; omega). + omega. + Qed. + + Lemma mul_length_exact: forall us vs, + (length us <= length vs)%nat -> us <> nil -> + (length (mul us vs) = pred (length us + length vs))%nat. + Proof. + intros; unfold mul. + rewrite mul'_length_exact; rewrite ?rev_length; try omega. + intro rev_nil. + match goal with H : us <> nil |- _ => apply H end. + apply length0_nil; rewrite <-rev_length, rev_nil. + reflexivity. + Qed. End BaseSystemProofs. diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 7989d641d..a1258674e 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -14,11 +14,11 @@ Section PseudoMersenneBase. Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). - Definition rep (us : digits) (x : F modulus) := (length us <= length base)%nat /\ decode us = x. + Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x. Local Notation "u '~=' x" := (rep u x) (at level 70). Local Hint Unfold rep. - Definition encode (x : F modulus) := encode x. + Definition encode (x : F modulus) := encode x ++ BaseSystem.zeros (length base - 1)%nat. (* Converts from length of extended base to length of base by reduction modulo M.*) Definition reduce (us : digits) : digits := diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 71841d871..b2c9ee0fa 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -473,7 +473,6 @@ Section Canonicalization. (c_reduce2 : c <= max_bound 0 - c) (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus). - Print freeze. Definition max_ones_opt := Eval compute in max_ones. Definition max_bound_opt := Eval compute in max_bound. Definition full_carry_chain_opt := Eval compute in full_carry_chain. @@ -552,8 +551,8 @@ Section Canonicalization. := proj2_sig (freeze_opt_sig us). Lemma freeze_opt_canonical: forall us vs x, - @pre_carry_bounds _ _ int_width us -> (length us = length base) -> rep us x -> - @pre_carry_bounds _ _ int_width vs -> (length vs = length base) -> rep vs x -> + @pre_carry_bounds _ _ int_width us -> rep us x -> + @pre_carry_bounds _ _ int_width vs -> rep vs x -> freeze_opt us = freeze_opt vs. Proof. intros. @@ -561,12 +560,21 @@ Section Canonicalization. eapply freeze_canonical with (B := int_width); eauto. Qed. - Lemma freeze_opt_preserves_rep : forall us x, (length us = length base) -> - rep us x -> rep (freeze_opt us) x. + Lemma freeze_opt_preserves_rep : forall us x, rep us x -> rep (freeze_opt us) x. Proof. intros. rewrite freeze_opt_correct. eauto using freeze_preserves_rep. Qed. + Lemma freeze_opt_spec : forall us x, rep us x -> + rep (freeze_opt us) x /\ + (forall vs, rep vs x -> + @pre_carry_bounds _ _ int_width us -> + @pre_carry_bounds _ _ int_width vs -> + freeze_opt us = freeze_opt vs). + Proof. + split; eauto using freeze_opt_preserves_rep; eauto using freeze_opt_canonical. + Qed. + End Canonicalization.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 8ac3a0faa..0aa83ae6b 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -27,9 +27,11 @@ Section PseudoMersenneProofs. intros. unfold encode, rep. split. { unfold encode; simpl. - apply base_length_nonzero. + rewrite length_zeros. + pose proof base_length_nonzero; omega. } { unfold decode. + rewrite decode_highzeros. rewrite encode_rep. apply ZToField_FieldToZ. apply bv. @@ -40,8 +42,7 @@ Section PseudoMersenneProofs. Proof. autounfold; intuition. { unfold add. - rewrite add_length_le_max. - case_max; try rewrite Max.max_r; omega. + auto using add_same_length. } unfold decode in *; unfold decode in *. rewrite add_rep. @@ -49,15 +50,14 @@ Section PseudoMersenneProofs. subst; auto. Qed. - Lemma sub_rep : forall c c_0modq, (length c <= length base)%nat -> + Lemma sub_rep : forall c c_0modq, (length c = length base)%nat -> forall u v x y, u ~= x -> v ~= y -> ModularBaseSystem.sub c c_0modq u v ~= (x-y)%F. Proof. autounfold; unfold ModularBaseSystem.sub; intuition. { - rewrite sub_length_le_max. + rewrite sub_length. case_max; try rewrite Max.max_r; try omega. - rewrite add_length_le_max. - case_max; try rewrite Max.max_r; omega. + auto using add_same_length. } unfold decode in *; unfold BaseSystem.decode in *. rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep. @@ -138,33 +138,15 @@ Section PseudoMersenneProofs. Qed. Lemma reduce_length : forall us, - (length us <= length ext_base)%nat -> - (length (reduce us) <= length base)%nat. + (length base <= length us <= length ext_base)%nat -> + (length (reduce us) = length base)%nat. Proof. - intros. - unfold reduce. - remember (map (Z.mul c) (skipn (length base) us)) as high. - remember (firstn (length base) us) as low. - assert (length low >= length high)%nat. { - subst. rewrite firstn_length. - rewrite map_length. - rewrite skipn_length. - destruct (le_dec (length base) (length us)). { - rewrite Min.min_l by omega. - rewrite extended_base_length in H. omega. - } { - rewrite Min.min_r; omega. - } - } - assert ((length low <= length base)%nat) - by (rewrite Heqlow; rewrite firstn_length; apply Min.le_min_l). - assert (length high <= length base)%nat - by (rewrite Heqhigh; rewrite map_length; rewrite skipn_length; - rewrite extended_base_length in H; omega). - rewrite add_trailing_zeros; auto. - rewrite (add_same_length _ _ (length low)); auto. - rewrite app_length. - rewrite length_zeros; intuition. + rewrite extended_base_length. + unfold reduce; intros. + rewrite add_length_exact. + rewrite map_length, firstn_length, skipn_length. + rewrite Min.min_l by omega. + apply Max.max_l; omega. Qed. Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> u .* v ~= (x*y)%F. @@ -172,14 +154,16 @@ Section PseudoMersenneProofs. autounfold; unfold ModularBaseSystem.mul; intuition. { apply reduce_length. - rewrite mul_length, extended_base_length. - omega. + rewrite mul_length_exact, extended_base_length; try omega. + destruct u; try congruence. + rewrite @nil_length0 in *. + pose proof base_length_nonzero; omega. } { rewrite ZToField_mod, reduce_rep, <-ZToField_mod. rewrite mul_rep by (apply ExtBaseVector || rewrite extended_base_length; omega). subst. - do 2 rewrite decode_short by auto. + do 2 rewrite decode_short by omega. apply ZToField_mul. } Qed. @@ -365,8 +349,8 @@ Section CarryProofs. Qed. Lemma carry_length : forall i us, - (length us <= length base)%nat -> - (length (carry i us) <= length base)%nat. + (length us = length base)%nat -> + (length (carry i us) = length base)%nat. Proof. unfold carry, carry_simple, carry_and_reduce, add_to_nth. intros; break_if; subst; repeat (rewrite length_set_nth); auto. @@ -379,36 +363,19 @@ Section CarryProofs. us ~= x -> carry i us ~= x. Proof. pose carry_length. pose carry_decode_eq_reduce. pose carry_simple_decode_eq. - unfold rep, decode, carry in *; intros. - intuition; break_if; subst; eauto; - apply F_eq; simpl; intuition. + intros; split; auto. + unfold rep, decode, carry in *. + intuition; break_if; subst; eauto; apply F_eq; simpl; intuition. Qed. Hint Resolve carry_rep. Lemma carry_sequence_length: forall is us, - (length us <= length base)%nat -> - (length (carry_sequence is us) <= length base)%nat. - Proof. - induction is; boring. - Qed. - Hint Resolve carry_sequence_length. - - Lemma carry_length_exact : forall i us, - (length us = length base)%nat -> - (length (carry i us) = length base)%nat. - Proof. - unfold carry, carry_simple, carry_and_reduce, add_to_nth. - intros; break_if; subst; repeat (rewrite length_set_nth); auto. - Qed. - - Lemma carry_sequence_length_exact: forall is us, (length us = length base)%nat -> (length (carry_sequence is us) = length base)%nat. Proof. induction is; boring. - apply carry_length_exact; auto. Qed. - Hint Resolve carry_sequence_length_exact. + Hint Resolve carry_sequence_length. Lemma carry_sequence_rep : forall is us x, (forall i, In i is -> (i < length base)%nat) -> @@ -558,7 +525,7 @@ Section CanonicalizationProofs. (* automation *) Ltac carry_length_conditions' := unfold carry_full, add_to_nth; - rewrite ?length_set_nth, ?carry_length_exact, ?carry_sequence_length_exact, ?carry_sequence_length_exact; + rewrite ?length_set_nth, ?carry_length, ?carry_sequence_length; try omega; try solve [pose proof base_length; pose proof base_length_nonzero; omega || auto ]. Ltac carry_length_conditions := try split; try omega; repeat carry_length_conditions'. @@ -1643,8 +1610,7 @@ Section CanonicalizationProofs. unfold rep; auto. Qed. - Lemma freeze_preserves_rep : forall us x, (length us = length base) -> - rep us x -> rep (freeze us) x. + Lemma freeze_preserves_rep : forall us x, rep us x -> rep (freeze us) x. Proof. unfold rep; intros. intuition; rewrite ?freeze_length; auto. @@ -2080,8 +2046,8 @@ Section CanonicalizationProofs. Qed. Lemma minimal_rep_unique : forall us vs x, - length us = length base -> rep us x -> minimal_rep us -> carry_done us -> - length vs = length base -> rep vs x -> minimal_rep vs -> carry_done vs -> + rep us x -> minimal_rep us -> carry_done us -> + rep vs x -> minimal_rep vs -> carry_done vs -> us = vs. Proof. intros. @@ -2090,17 +2056,20 @@ Section CanonicalizationProofs. repeat match goal with Hmin : minimal_rep ?us |- _ => unfold minimal_rep in Hmin; rewrite <- Hmin in eqmod; clear Hmin end. apply Z.compare_eq_iff in eqmod. - rewrite decode_compare in eqmod; auto. + rewrite decode_compare in eqmod; unfold rep in *; auto; intuition; try congruence. apply compare_Eq; auto. congruence. Qed. Lemma freeze_canonical : forall us vs x, - pre_carry_bounds us -> (length us = length base) -> rep us x -> - pre_carry_bounds vs -> (length vs = length base) -> rep vs x -> + pre_carry_bounds us -> rep us x -> + pre_carry_bounds vs -> rep vs x -> freeze us = freeze vs. Proof. - intros; eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. + intros. + assert (length us = length base) by (unfold rep in *; intuition). + assert (length vs = length base) by (unfold rep in *; intuition). + eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. End CanonicalizationProofs.
\ No newline at end of file diff --git a/src/ModularArithmetic/PseudoMersenneBaseRep.v b/src/ModularArithmetic/PseudoMersenneBaseRep.v index c16cc8d38..5f3644cca 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseRep.v +++ b/src/ModularArithmetic/PseudoMersenneBaseRep.v @@ -25,7 +25,7 @@ Class RepZMod (modulus : Z) := { Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := { coeff : BaseSystem.digits; - coeff_length : (length coeff <= length PseudoMersenneBaseParamProofs.base)%nat; + coeff_length : (length coeff = length PseudoMersenneBaseParamProofs.base)%nat; coeff_mod: (BaseSystem.decode PseudoMersenneBaseParamProofs.base coeff) mod m = 0 }. |