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/BaseSystemProofs.v | 44 ++++++++++++++++++------- src/ModularArithmetic/ExtendedBaseVector.v | 2 ++ src/ModularArithmetic/ModularBaseSystemProofs.v | 26 ++++++++------- 3 files changed, 48 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 8bd390635..8de0fdd0a 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -474,14 +474,8 @@ Section BaseSystemProofs. auto. Qed. - (* mul' is multiplication with the FIRST ARGUMENT REVERSED *) - Fixpoint mul' (usr vs:digits) : digits := - match usr with - | u::usr' => - mul_each u (mul_bi base (length usr') vs) .+ mul' usr' vs - | _ => nil - end. - Definition mul us := mul' (rev us). + Local Notation mul' := (mul' base). + Local Notation mul := (mul base). Lemma mul'_rep : forall us vs, (length us + length vs <= length base)%nat -> @@ -521,7 +515,7 @@ Section BaseSystemProofs. Lemma mul_length: forall us vs, (length (mul us vs) <= length us + length vs)%nat. Proof. - intros; unfold mul. + intros; unfold BaseSystem.mul. rewrite mul'_length. rewrite rev_length; omega. Qed. @@ -541,7 +535,7 @@ Section BaseSystemProofs. end)%nat. Proof. induction us; intros; try solve [boring]. - unfold mul'; fold mul'. + unfold BaseSystem.mul'; fold mul'. unfold mul_each. rewrite add_length_exact, map_length, mul_bi_length, length_cons. destruct us. @@ -568,7 +562,7 @@ Section BaseSystemProofs. | _ => pred (length us + length vs) end)%nat. Proof. - intros; unfold mul; autorewrite with distr_length; reflexivity. + intros; unfold BaseSystem.mul; autorewrite with distr_length; reflexivity. Qed. Hint Rewrite mul_length_exact_full : distr_length. @@ -579,7 +573,7 @@ Section BaseSystemProofs. (length us <= length vs)%nat -> us <> nil -> (length (mul us vs) = pred (length us + length vs))%nat. Proof. - intros; unfold mul. + intros; unfold BaseSystem.mul. rewrite mul'_length_exact; rewrite ?rev_length; try omega. intro rev_nil. match goal with H : us <> nil |- _ => apply H end. @@ -637,3 +631,29 @@ Section BaseSystemProofs. End BaseSystemProofs. Hint Rewrite @add_length_exact @mul'_length_exact_full @mul_length_exact_full @encode'_length @sub_length : distr_length. + +Section MultiBaseSystemProofs. + Context base0 (base_vector0 : @BaseVector base0) base1 (base_vector1 : @BaseVector base1). + + Lemma decode_short_initial : forall (us : digits), + (firstn (length us) base0 = firstn (length us) base1) + -> decode base0 us = decode base1 us. + Proof. + intros us H. + unfold decode, decode'. + rewrite (combine_truncate_r us base0), (combine_truncate_r us base1), H. + reflexivity. + Qed. + + Lemma mul_rep_two_base : forall (us vs : digits), + (length us + length vs <= length base1)%nat + -> firstn (length us) base0 = firstn (length us) base1 + -> firstn (length vs) base0 = firstn (length vs) base1 + -> (decode base0 us) * (decode base0 vs) = decode base1 (mul base1 us vs). + Proof. + intros. + rewrite mul_rep by trivial. + apply f_equal2; apply decode_short_initial; assumption. + Qed. + +End MultiBaseSystemProofs. 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