From 526a60b8dcee4bcec55e50a7b6056b9c9090d73d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 15:49:42 -0700 Subject: Move more proofs earlier --- src/ModularArithmetic/ExtendedBaseVector.v | 2 ++ src/ModularArithmetic/ModularBaseSystemProofs.v | 26 +++++++++++++------------ 2 files changed, 16 insertions(+), 12 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index d4df6040f..ddf787d21 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -160,3 +160,5 @@ Section ExtendedBaseVector. unfold ext_base; rewrite app_length; rewrite map_length; auto. Qed. End ExtendedBaseVector. + +Hint Rewrite @extended_base_length : distr_length. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index daff60220..227a3e77f 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -128,27 +128,29 @@ Section PseudoMersenneProofs. subst; auto. Qed. - Lemma decode_short : forall (us : BaseSystem.digits), - (length us <= length base)%nat -> - BaseSystem.decode base us = BaseSystem.decode ext_base us. + Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), + (length us <= length base)%nat + -> firstn (length us) base = firstn (length us) ext_base. Proof. - intros. - unfold BaseSystem.decode, BaseSystem.decode'. - rewrite combine_truncate_r. - rewrite (combine_truncate_r us ext_base). - f_equal; f_equal. - unfold ext_base. + unfold ext_base; intros. rewrite firstn_app_inleft; auto; omega. Qed. + Local Hint Immediate firstn_us_base_ext_base. + + Lemma decode_short : forall (us : BaseSystem.digits), + (length us <= length base)%nat -> + BaseSystem.decode base us = BaseSystem.decode ext_base us. + Proof. auto using decode_short_initial. Qed. + + Local Hint Immediate ExtBaseVector. Lemma mul_rep_extended : forall (us vs : BaseSystem.digits), (length us <= length base)%nat -> (length vs <= length base)%nat -> (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs). Proof. - intros. - rewrite mul_rep by (apply ExtBaseVector || unfold ext_base; simpl_list; omega). - f_equal; rewrite decode_short; auto. + intros; apply mul_rep_two_base; auto; + autorewrite with distr_length; try omega. Qed. Lemma modulus_nonzero : modulus <> 0. -- cgit v1.2.3