From 230009bd4d71e52b4f53058db38818da39d99d93 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 26 Oct 2016 20:06:45 -0400 Subject: add extra convenience lemmas about boundedness of convert --- src/ModularArithmetic/Conversion.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/Conversion.v b/src/ModularArithmetic/Conversion.v index 8ad19c4c6..4f28d7eec 100644 --- a/src/ModularArithmetic/Conversion.v +++ b/src/ModularArithmetic/Conversion.v @@ -276,6 +276,29 @@ Section Conversion. end. Qed. + (* This is part of convert'_invariant, but proving it separately strips preconditions *) + Lemma convert'_bounded : forall inp i out, + bounded limb_widthsB out -> + bounded limb_widthsB (convert' inp i out). + Proof. + intros; functional induction (convert' inp i out); auto. + apply IHl. + apply convert'_bounded_step; auto. + clear IHl. + pose proof (bit_index_not_done limb_widthsA (Z.of_nat i)). + pose proof (bit_index_not_done limb_widthsB (Z.of_nat i)). + specialize_by lia. + lia. + Qed. + + Lemma convert_bounded : forall us, bounded limb_widthsB (convert us). + Proof. + intros; apply convert'_bounded. + apply bounded_iff; intros. + rewrite nth_default_zeros. + split; zero_bounds. + Qed. + (* This is part of convert'_invariant, but proving it separately strips preconditions *) Lemma length_convert' : forall inp i out, length (convert' inp i out) = length out. -- cgit v1.2.3