From b3ddc5cfb84c952785196a9e27e497dc14af9188 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 15 Jun 2016 16:50:33 -0400 Subject: changed representation definition to require digits vector to be the exact length of the base vector --- src/BaseSystemProofs.v | 36 ++++++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) (limited to 'src/BaseSystemProofs.v') 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. -- cgit v1.2.3