Factored out some proofs that rely only on base being powers of two, and defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.

1 files changed, 4 insertions, 2 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 4f918e147..bb9b1674e 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -45,10 +45,12 @@ Ltac opt_step :=
        destruct e
   end.
 
-Ltac brute_force_indices limb_widths := intros; unfold sum_firstn, limb_widths; simpl in *;
+Ltac brute_force_indices limb_widths :=
+  intros; unfold sum_firstn, limb_widths;  cbv [length limb_widths] in *;
   repeat match goal with
   | _ => progress simpl in *
-  | _ => reflexivity
+  | [H : (0 + _ < _)%nat |- _ ] => simpl in H
+  | [H : (S _ + _ < S _)%nat |- _ ] => simpl in H
   | [H : (S _ < S _)%nat |- _ ] => apply lt_S_n in H
   | [H : (?x + _ < _)%nat |- _ ] => is_var x; destruct x
   | [H : (?x < _)%nat |- _ ] => is_var x; destruct x