ModularBaseSystem: carry_rep has boring modular arithmetic proofs

1 files changed, 160 insertions, 38 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index c8ee7bd9d..7f5bea670 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -201,39 +201,6 @@ Proof.
   break_if; break_if; auto; omega.
 Qed.
 
-Ltac nth_error_inbounds :=
-  match goal with
-  | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] =>
-    case_eq (nth_error xs i);
-    match goal with 
-      | [ |- forall _, nth_error xs i = Some _ -> _ ] =>
-          let x := fresh "x" in
-          let H := fresh "H" in
-          intros x H;
-          repeat progress erewrite H;
-          repeat progress erewrite (nth_error_value_eq_nth_default i xs x); auto
-      | [ |- nth_error xs i = None -> _ ] =>
-          let H := fresh "H" in
-          intros H;
-          destruct (nth_error_length_not_error _ _ H);
-          try omega
-    end;
-    idtac
-  end.
-
-Ltac set_nth_inbounds :=
-  match goal with
-  | [ |- context[set_nth ?i ?x ?xs] ] =>
-    rewrite (set_nth_equiv_splice_nth i x xs);
-    destruct (lt_dec i (length xs));
-    match goal with
-    | [ H : ~ (i < (length xs))%nat |- _ ] => destruct H
-    | [ H :   (i < (length xs))%nat |- _ ] => try omega
-    end;
-    idtac
-  end.
-
-Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds.
 
 Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B),
   combine (set_nth n x xs) ys =
@@ -295,6 +262,13 @@ Proof.
   induction xs; destruct ys; boring.
 Qed.
 
+Lemma combine_app_samelength : forall {A B} (xs xs':list A) (ys ys':list B),
+  length xs = length ys ->
+  combine (xs ++ xs') (ys ++ ys') = combine xs ys ++ combine xs' ys'.
+Proof.
+  induction xs, xs', ys, ys'; boring; omega.
+Qed.
+
 Lemma firstn_nil : forall {A} n, firstn n nil = @nil A.
 Proof.
   destruct n; auto.
@@ -328,15 +302,33 @@ Lemma skipn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
 Proof.
   induction n, xs, ys; boring; try omega.
 Qed.
-    
-Lemma firstn_app_sharp : forall A (l l': list A), firstn (length l) (l ++ l') = l.
+
+Lemma firstn_all : forall {A} n (xs:list A), n = length xs -> firstn n xs = xs.
 Proof.
-  induction l; boring.
+  induction n, xs; boring; omega.
+Qed.
+
+Lemma skipn_all : forall {T} n (xs:list T),
+  (n >= length xs)%nat ->
+  skipn n xs = nil.
+Proof.
+  induction n, xs; boring; omega.
+Qed.
+
+Lemma firstn_app_sharp : forall {A} n (l l': list A),
+  length l = n ->
+  firstn n (l ++ l') = l.
+Proof.
+  intros.
+  rewrite firstn_app_inleft; auto using firstn_all; omega.
 Qed.
     
-Lemma skipn_app_sharp : forall A (l l': list A), skipn (length l) (l ++ l') = l'.
+Lemma skipn_app_sharp : forall {A} n (l l': list A),
+  length l = n ->
+  skipn n (l ++ l') = l'.
 Proof.
-  induction l; boring.
+  intros.
+  rewrite skipn_app_inleft; try rewrite skipn_all; auto; omega.
 Qed.
 
 Lemma skipn_length : forall {A} n (xs : list A),
@@ -344,3 +336,133 @@ Lemma skipn_length : forall {A} n (xs : list A),
 Proof.
   induction n, xs; boring.
 Qed.
+
+Lemma fold_right_cons : forall {A B} (f:B->A->A) a b bs,
+  fold_right f a (b::bs) = f b (fold_right f a bs).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs).
+  reflexivity.
+Qed.
+
+Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat.
+Proof.
+  destruct a; omega.
+Qed.
+
+Lemma firstn_combine : forall {A B} n (xs:list A) (ys:list B),
+  firstn n (combine xs ys) = combine (firstn n xs) (firstn n ys).
+Proof.
+  induction n, xs, ys; boring.
+Qed.
+
+Lemma combine_nil_r : forall {A B} (xs:list A),
+  combine xs (@nil B) = nil.
+Proof.
+  induction xs; boring.
+Qed.
+
+Lemma skipn_combine : forall {A B} n (xs:list A) (ys:list B),
+  skipn n (combine xs ys) = combine (skipn n xs) (skipn n ys).
+Proof.
+  induction n, xs, ys; boring.
+  rewrite combine_nil_r; reflexivity.
+Qed.
+
+Lemma break_list_last: forall {T} (xs:list T),
+  xs = nil \/ exists xs' y, xs = xs' ++ y :: nil.
+Proof.
+  destruct xs using rev_ind; auto.
+  right; do 2 eexists; auto.
+Qed.
+
+Lemma break_list_first: forall {T} (xs:list T),
+  xs = nil \/ exists x xs', xs = x :: xs'.
+Proof.
+  destruct xs; auto.
+  right; do 2 eexists; auto.
+Qed.
+
+Lemma list012 : forall {T} (xs:list T),
+  xs = nil
+  \/ (exists x, xs = x::nil)
+  \/ (exists x xs' y, xs = x::xs'++y::nil).
+Proof.
+  destruct xs; auto.
+  right.
+  destruct xs using rev_ind. {
+    left; eexists; auto.
+  } {
+    right; repeat eexists; auto.
+  }
+Qed.
+ 
+Lemma nil_length0 : forall {T}, length (@nil T) = 0%nat.
+Proof.
+  auto.
+Qed.
+
+Lemma nth_default_cons : forall {T} (x u0 : T) us, nth_default x (u0 :: us) 0 = u0.
+Proof.
+  auto.
+Qed.
+
+Lemma set_nth_cons : forall {T} (x u0 : T) us, set_nth 0 x (u0 :: us) = x :: us.
+Proof.
+  auto.
+Qed.
+
+Create HintDb distr_length discriminated.
+Hint Rewrite
+  @nil_length0
+  @length_cons
+  @app_length
+  @rev_length
+  @map_length
+  @seq_length
+  @fold_left_length
+  @split_length_l
+  @split_length_r
+  @firstn_length
+  @skipn_length
+  @combine_length
+  @prod_length
+  @length_set_nth
+  : distr_length.
+Ltac distr_length := autorewrite with distr_length in *;
+  try solve [simpl in *; omega].
+
+Ltac nth_error_inbounds :=
+  match goal with
+  | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] =>
+    case_eq (nth_error xs i);
+    match goal with 
+      | [ |- forall _, nth_error xs i = Some _ -> _ ] =>
+          let x := fresh "x" in
+          let H := fresh "H" in
+          intros x H;
+          repeat progress erewrite H;
+          repeat progress erewrite (nth_error_value_eq_nth_default i xs x); auto
+      | [ |- nth_error xs i = None -> _ ] =>
+          let H := fresh "H" in
+          intros H;
+          destruct (nth_error_length_not_error _ _ H);
+          try solve [distr_length]
+    end;
+    idtac
+  end.
+Ltac set_nth_inbounds :=
+  match goal with
+  | [ |- context[set_nth ?i ?x ?xs] ] =>
+    rewrite (set_nth_equiv_splice_nth i x xs);
+    destruct (lt_dec i (length xs));
+    match goal with
+    | [ H : ~ (i < (length xs))%nat |- _ ] => destruct H
+    | [ H :   (i < (length xs))%nat |- _ ] => try solve [distr_length]
+    end;
+    idtac
+  end.
+
+Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds.