aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/NewBaseSystem.v35
-rw-r--r--src/Util/ListUtil.v20
-rw-r--r--src/Util/Tuple.v79
-rw-r--r--src/Util/ZUtil.v8
4 files changed, 142 insertions, 0 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v
index 70c44fd48..690ddade6 100644
--- a/src/NewBaseSystem.v
+++ b/src/NewBaseSystem.v
@@ -765,7 +765,42 @@ Module B.
Logic.eq (Fdecode a) (Fdecode b) <-> eq m a b.
Proof. cbv [Fdecode]; rewrite <-F.eq_of_Z_iff; reflexivity. Qed.
End F.
+
+
End Positional.
+
+ (* Helper lemmas and definitions for [eval]; this needs to be in a
+ separate section so the weight function can change. *)
+ Section EvalHelpers.
+ Lemma eval_single wt (x:Z) : eval (n:=1) wt x = wt 0%nat * x.
+ Proof. cbv - [Z.mul Z.add]. ring. Qed.
+
+ Lemma eval_step {n} (x:tuple Z n) : forall wt z,
+ eval wt (Tuple.append z x) = wt 0%nat * z + eval (fun i => wt (S i)) x.
+ Proof.
+ destruct n; [reflexivity|].
+ intros; cbv [eval to_associational_cps].
+ autorewrite with uncps. rewrite map_S_seq. reflexivity.
+ Qed.
+
+ Lemma eval_wt_equiv {n} :forall wta wtb (x:tuple Z n),
+ (forall i, wta i = wtb i) -> eval wta x = eval wtb x.
+ Proof.
+ destruct n; [reflexivity|].
+ induction n; intros; [rewrite !eval_single, H; reflexivity|].
+ simpl tuple in *; destruct x.
+ change (t, z) with (Tuple.append (n:=S n) z t).
+ rewrite !eval_step. rewrite (H 0%nat). apply Group.cancel_left.
+ apply IHn; auto.
+ Qed.
+
+ Definition eval_from {n} weight (offset:nat) (x : tuple Z n) : Z :=
+ eval (fun i => weight (i+offset)%nat) x.
+
+ Lemma eval_from_0 {n} wt x : @eval_from n wt 0 x = eval wt x.
+ Proof. cbv [eval_from]. auto using eval_wt_equiv. Qed.
+ End EvalHelpers.
+
End Positional.
Hint Unfold
Positional.add_cps
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index b5bc1a6e6..3904b1c2e 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -216,6 +216,8 @@ Local Arguments error / _.
Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l).
+Definition sum xs := sum_firstn xs (length xs).
+
Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C :=
match la with
| nil => nil
@@ -884,6 +886,10 @@ Qed.
Hint Rewrite @length_cons : distr_length.
+Lemma length_cons_full {T} n (x:list T) (t:T) (H: length (t :: x) = S n)
+ : length x = n.
+Proof. distr_length. Qed.
+
Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs).
Proof.
auto.
@@ -900,6 +906,10 @@ Proof.
boring; simpl_list; boring.
Qed.
+Lemma combine_cons : forall {A B} a b (xs:list A) (ys:list B),
+ combine (a :: xs) (b :: ys) = (a,b) :: combine xs ys.
+Proof. reflexivity. 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.
@@ -1121,6 +1131,10 @@ Qed.
Hint Rewrite @map_nth_default_always : push_nth_default.
+Lemma map_S_seq {A} (f:nat->A) len : forall start,
+ List.map (fun i => f (S i)) (seq start len) = List.map f (seq (S start) len).
+Proof. induction len; intros; simpl; rewrite ?IHlen; reflexivity. Qed.
+
Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop),
(forall x, In x l -> P x) <-> fold_right and True (map P l).
Proof.
@@ -1407,6 +1421,12 @@ Proof.
Qed.
Hint Rewrite @sum_firstn_app_sum : simpl_sum_firstn.
+Lemma sum_cons xs x : sum (x :: xs) = (x + sum xs)%Z.
+Proof. reflexivity. Qed.
+
+Lemma sum_nil : sum nil = 0%Z.
+Proof. reflexivity. Qed.
+
Lemma nth_error_skipn : forall {A} n (l : list A) m,
nth_error (skipn n l) m = nth_error l (n + m).
Proof.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 1e3e5f9a0..fc0bf4b90 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -169,6 +169,10 @@ Proof.
eapply from_list'_to_list'; assumption. }
Qed.
+Lemma to_list_S {A n} (x : tuple A (S n)) (a:A)
+ : to_list (T:=A) (S (S n)) (x,a) = a :: to_list (S n) x.
+Proof. reflexivity. Qed.
+
Fixpoint curry'T (R T : Type) (n : nat) : Type
:= match n with
| 0 => T -> R
@@ -711,5 +715,80 @@ Lemma strip_eta_rtuple {T n B} (f : rtuple T n -> B) ts
: eta_rtuple f ts = f ts.
Proof. exact (strip_eta_rtuple_dep _ _ _). Qed.
+Definition append {A n} (a : A) : tuple A n -> tuple A (S n) :=
+ match n as n0 return (tuple A n0 -> tuple A (S n0)) with
+ | O => fun t => a
+ | S n' => fun t => (t,a)
+ end.
+
+Lemma hd_append {A n} (x: tuple A n) (a:A) : hd (append a x) = a.
+Proof. destruct n; reflexivity. Qed.
+
+Lemma tl_append {A n} (x: tuple A n) (a:A) : tl (append a x) = x.
+Proof. destruct n; try destruct x; reflexivity. Qed.
+
+Lemma from_list'_cons {A n} (a0 a1:A) (xs:list A) H :
+ from_list' a0 (S n) (a1::xs) H = append (n:=S n) a0 (from_list' a1 n xs (length_cons_full _ _ _ H)).
+Proof. simpl; rewrite <-!from_list_default'_eq with (d:=a0); eauto. Qed.
+
+Lemma from_list_cons {A n}:
+ forall (xs : list A) a (H:length (a::xs)=S n),
+ from_list (S n) (a :: xs) H = append a (from_list n xs (length_cons_full _ _ _ H)).
+Proof.
+ destruct n; intros; destruct xs; distr_length; [reflexivity|].
+ cbv [from_list]; rewrite !from_list'_cons.
+ rewrite <-!from_list_default'_eq with (d:=a).
+ reflexivity.
+Qed.
+
+Lemma map_append' {A B n} (f:A->B) : forall (x:tuple' A n) (a:A),
+ map f (append (n:=S n) a x) = append (f a) (map (n:=S n) f x).
+Proof.
+ cbv [map append on_tuple]; intros.
+ simpl to_list. simpl List.map. rewrite from_list_cons.
+ cbv [append]; f_equal. rewrite <-!from_list_default_eq with (d:=f a).
+ reflexivity.
+Qed.
+
+Lemma map_append {A B n} (f:A->B) : forall (x:tuple A n) (a:A),
+ map f (append a x) = append (f a) (map f x).
+Proof. destruct n; auto using map_append'. Qed.
+
+(* map operation that carries state*)
+Fixpoint map_with' {S A B n} (f: S->A->S*B) (start:S)
+ : tuple' A n -> S * tuple' B n :=
+ match n as n0 return (tuple' A n0 -> S * tuple' B n0) with
+ | O => fun ys => f start ys
+ | S n' => fun ys =>
+ (fst (map_with' f (fst (f start (hd ys))) (tl ys)),
+ (snd (map_with' f (fst (f start (hd ys))) (tl ys)),
+ snd (f start (hd ys))))
+ end.
+
+Fixpoint map_with {S A B n} (f: S->A->S*B) (start:S)
+ : tuple A n -> S * tuple B n :=
+ match n as n0 return (tuple A n0 -> S * tuple B n0) with
+ | O => fun ys => (start, tt)
+ | S n' => fun ys => map_with' f start ys
+ end.
+
+Lemma map_with_invariant {T A B} (f: T->A->T*B)
+ (P : forall n, T -> T -> tuple A n -> tuple B n -> Prop)
+ (P_holds : forall n starter rem inp out,
+ P n (fst (f starter (hd inp))) rem (tl inp) out
+ -> P (S n) starter rem inp (append (snd (f starter (hd inp))) out))
+ (P_base : forall rem, P 0%nat rem rem tt tt)
+ :
+ forall {n} (start : T) (input : tuple A n),
+ P n start (fst (map_with f start input)) input (snd (map_with f start input)).
+Proof.
+ destruct n. { intros; destruct input; apply P_base. }
+ induction n; intros.
+ { specialize (P_holds 0%nat start (fst (f start input)) input tt).
+ apply P_holds. apply P_base. }
+ { specialize (P_holds (S n) start (fst (map_with f start input)) input).
+ simpl. apply P_holds. apply IHn. }
+Qed.
+
Require Import Crypto.Util.ListUtil. (* To initialize [distr_length] database *)
Hint Rewrite length_to_list' @length_to_list : distr_length.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 07e9af549..38709174e 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -596,6 +596,14 @@ Module Z.
Hint Rewrite mul_div_eq mul_div_eq' using zutil_arith : zdiv_to_mod.
Hint Rewrite <- mul_div_eq' using zutil_arith : zmod_to_div.
+ Lemma mul_div_eq_full : forall a m, m <> 0 -> m * (a / m) = (a - a mod m).
+ Proof.
+ intros. rewrite (Z_div_mod_eq_full a m) at 2 by auto. ring.
+ Qed.
+
+ Hint Rewrite mul_div_eq_full using zutil_arith : zdiv_to_mod.
+ Hint Rewrite <-mul_div_eq_full using zutil_arith : zmod_to_div.
+
Ltac prime_bound := match goal with
| [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
end.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 00:39:14 +0000