diff options
| -rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 206 |
1 files changed, 151 insertions, 55 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 154951973..21570c6b0 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -230,23 +230,34 @@ Module Associational. _ nil (fun t ts acc - => let '(t, c_t, two_c_t, two_t) := t in - (if ((fst t * fst t) mod s =? 0) - then div_s (mul [t] c_t) - else mul [t] [t]) - ++ (flat_map - (fun '(t', c_t', two_c_t', two_t') - => if ((fst t * fst t') mod s =? 0) - then div_s - (if fst t' <=? fst t - then mul [t'] two_c_t - else mul [t] two_c_t') - else (if fst t' <=? fst t - then mul [t'] two_t - else mul [t] two_t')) - ts) + => (let '(t, c_t, two_c_t, two_t) := t in + (if ((fst t * fst t) mod s =? 0) + then div_s (mul [t] c_t) + else mul [t] [t]) + ++ (flat_map + (fun '(t', c_t', two_c_t', two_t') + => if ((fst t * fst t') mod s =? 0) + then div_s + (if fst t' <=? fst t + then mul [t'] two_c_t + else mul [t] two_c_t') + else (if fst t' <=? fst t + then mul [t'] two_t + else mul [t] two_t')) + ts)) ++ acc) p. + Lemma eval_map_div s p (s_nz:s <> 0) (Hmod : forall v, In v p -> fst v mod s = 0) + : eval (map (fun x => (fst x / s, snd x)) p) = eval p / s. + Proof. + assert (Hmod' : forall v, In v p -> (fst v * snd v) mod s = 0). + { intros; push_Zmod; rewrite Hmod by assumption; autorewrite with zsimplify_const; reflexivity. } + induction p as [|p ps IHps]; push. + { autorewrite with zsimplify_const; reflexivity. } + { cbn [In] in *; rewrite Z.div_add_exact by eauto. + rewrite !Z.Z_divide_div_mul_exact', IHps by auto using Znumtheory.Zmod_divide. + nsatz. } + Qed. Lemma eval_map_mul_div s a b c (s_nz:s <> 0) (a_mod : (a*a) mod s = 0) : eval (map (fun x => ((a * (a * fst x)) / s, b * (b * snd x))) c) = ((a * a) / s) * (b * b) * eval c. Proof. @@ -275,52 +286,137 @@ Module Associational. Proof. case b; reflexivity. Qed. Hint Rewrite eval_if : push_eval. + Lemma split_app s p q : + split s (p ++ q) = (fst (split s p) ++ fst (split s q), snd (split s p) ++ snd (split s q)). + Proof. + cbv [split]; rewrite !partition_app; cbn [fst snd]. + rewrite !map_app; reflexivity. + Qed. + Lemma fst_split_app s p q : + fst (split s (p ++ q)) = fst (split s p) ++ fst (split s q). + Proof. rewrite split_app; reflexivity. Qed. + Lemma snd_split_app s p q : + snd (split s (p ++ q)) = snd (split s p) ++ snd (split s q). + Proof. rewrite split_app; reflexivity. Qed. + Hint Rewrite fst_split_app snd_split_app : push_eval. + + Lemma eval_reduce_list_rect_app A s c N C p : + eval (reduce s c (@list_rect A _ N (fun x xs acc => C x xs ++ acc) p)) + = eval (@list_rect A _ (reduce s c N) (fun x xs acc => reduce s c (C x xs) ++ acc) p). + Proof. + cbv [reduce]; induction p as [|p ps IHps]; cbn [list_rect]; push; [ nsatz | rewrite <- IHps; clear IHps ]. + push; nsatz. + Qed. + Hint Rewrite eval_reduce_list_rect_app : push_eval. + + Lemma eval_list_rect_app A N C p : + eval (@list_rect A _ N (fun x xs acc => C x xs ++ acc) p) + = @list_rect A _ (eval N) (fun x xs acc => eval (C x xs) + acc) p. + Proof. induction p; cbn [list_rect]; push; nsatz. Qed. + Hint Rewrite eval_list_rect_app : push_eval. + Local Existing Instances list_rect_Proper pointwise_map flat_map_Proper. Local Hint Extern 0 (Proper _ _) => solve_Proper_eq : typeclass_instances. + Lemma reduce_nil s c : reduce s c nil = nil. + Proof. cbv [reduce]; induction c; cbn; intuition auto. Qed. + Hint Rewrite reduce_nil : push_eval. + + Lemma eval_reduce_app s c p q : eval (reduce s c (p ++ q)) = eval (reduce s c p) + eval (reduce s c q). + Proof. cbv [reduce]; push; nsatz. Qed. + Hint Rewrite eval_reduce_app : push_eval. + + Lemma eval_reduce_cons s c p q : + eval (reduce s c (p :: q)) + = (if fst p mod s =? 0 then eval c * ((fst p / s) * snd p) else fst p * snd p) + + eval (reduce s c q). + Proof. + cbv [reduce split]; cbn [partition fst snd]; eta_expand; push. + break_innermost_match; cbn [fst snd map]; push; nsatz. + Qed. + Hint Rewrite eval_reduce_cons : push_eval. + + Lemma mul_cons_l t ts p : + mul (t::ts) p = map (fun t' => (fst t * fst t', snd t * snd t')) p ++ mul ts p. + Proof. reflexivity. Qed. + Lemma mul_nil_l p : mul nil p = nil. + Proof. reflexivity. Qed. + Lemma mul_nil_r p : mul p nil = nil. + Proof. cbv [mul]; induction p; cbn; intuition auto. Qed. + Hint Rewrite mul_nil_l mul_nil_r : push_eval. + Lemma mul_app_l p p' q : + mul (p ++ p') q = mul p q ++ mul p' q. + Proof. cbv [mul]; rewrite flat_map_app; reflexivity. Qed. + Lemma mul_singleton_l_app_r p q q' : + mul [p] (q ++ q') = mul [p] q ++ mul [p] q'. + Proof. cbv [mul flat_map]; rewrite !map_app, !app_nil_r; reflexivity. Qed. + Hint Rewrite mul_singleton_l_app_r : push_eval. + Lemma mul_singleton_singleton p q : + mul [p] [q] = [(fst p * fst q, snd p * snd q)]. + Proof. reflexivity. Qed. + + Lemma eval_reduce_square_step_helper s c t' t v (s_nz:s <> 0) : + (fst t * fst t') mod s = 0 \/ (fst t' * fst t) mod s = 0 -> In v (mul [t'] (mul (mul [t] c) [(1, 2)])) -> fst v mod s = 0. + Proof. + cbv [mul]; cbn [map flat_map fst snd]. + rewrite !app_nil_r, flat_map_singleton, !map_map; cbn [fst snd]; rewrite in_map_iff; intros [H|H] [? [? ?] ]; subst; revert H. + all:cbn [fst snd]; autorewrite with zsimplify_const; intro H; rewrite Z.mul_assoc, Z.mul_mod_l. + all:rewrite H || rewrite (Z.mul_comm (fst t')), H; autorewrite with zsimplify_const; reflexivity. + Qed. + + Lemma eval_reduce_square_step s c t ts (s_nz : s <> 0) : + eval (flat_map + (fun t' => if (fst t * fst t') mod s =? 0 + then map (fun t => (fst t / s, snd t)) + (if fst t' <=? fst t + then mul [t'] (mul (mul [t] c) [(1, 2)]) + else mul [t] (mul (mul [t'] c) [(1, 2)])) + else (if fst t' <=? fst t + then mul [t'] (mul [t] [(1, 2)]) + else mul [t] (mul [t'] [(1, 2)]))) + ts) + = eval (reduce s c (mul [(1, 2)] (mul [t] ts))). + Proof. + induction ts as [|t' ts IHts]; cbn [flat_map]; [ push; nsatz | rewrite eval_app, IHts; clear IHts ]. + change (t'::ts) with ([t'] ++ ts); rewrite !mul_singleton_l_app_r, !mul_singleton_singleton; autorewrite with zsimplify_const; push. + break_match; Z.ltb_to_lt; push; try nsatz. + all:rewrite eval_map_div by eauto using eval_reduce_square_step_helper; push; autorewrite with zsimplify_const. + all:rewrite ?Z.mul_assoc, <- !(Z.mul_comm (fst t')), ?Z.mul_assoc. + all:rewrite ?Z.mul_assoc, <- !(Z.mul_comm (fst t)), ?Z.mul_assoc. + all:rewrite <- !Z.mul_assoc, Z.mul_assoc. + all:rewrite !Z.Z_divide_div_mul_exact' by auto using Znumtheory.Zmod_divide. + all:nsatz. + Qed. + + Lemma eval_reduce_square_helper s c x y v (s_nz:s <> 0) : + (fst x * fst y) mod s = 0 \/ (fst y * fst x) mod s = 0 -> In v (mul [x] (mul [y] c)) -> fst v mod s = 0. + Proof. + cbv [mul]; cbn [map flat_map fst snd]. + rewrite !app_nil_r, ?flat_map_singleton, !map_map; cbn [fst snd]; rewrite in_map_iff; intros [H|H] [? [? ?] ]; subst; revert H. + all:cbn [fst snd]; autorewrite with zsimplify_const; intro H; rewrite Z.mul_assoc, Z.mul_mod_l. + all:rewrite H || rewrite (Z.mul_comm (fst x)), H; autorewrite with zsimplify_const; reflexivity. + Qed. + Lemma eval_reduce_square_exact s c p (s_nz:s<>0) (modulus_nz:s-eval c<>0) : eval (reduce_square s c p) = eval (reduce s c (square p)). Proof. - cbv [reduce_square Let_In let_bind_for_reduce_square reduce square split]; cbn [map]. - push; auto; []. - induction p as [|a p IHp]; cbn [list_rect map]; push; [ nsatz | rewrite IHp; clear IHp ]. - cbn [List.app mul flat_map map]; push; cbn [fst snd]; auto; []. - rewrite !partition_app, !map_map, !flat_map_map, !app_nil_r; cbn [fst snd map flat_map]. - progress repeat setoid_rewrite app_nil_r. - progress repeat setoid_rewrite flat_map_singleton. - progress repeat setoid_rewrite map_map. - progress cbn [fst snd]. - progress repeat setoid_rewrite Z.mul_1_r. - progress repeat setoid_rewrite Z.mul_assoc. - progress repeat setoid_rewrite (Z.mul_comm (fst a)). - progress repeat setoid_rewrite (Z.mul_comm (snd a)). - progress repeat setoid_rewrite if_const. - progress repeat setoid_rewrite map_map. - progress repeat setoid_rewrite <- (Z.mul_comm 2). - progress repeat setoid_rewrite Z.mul_assoc. - progress repeat setoid_rewrite <- (Z.mul_comm (snd a)). - progress repeat setoid_rewrite Z.mul_assoc. - rewrite !partition_map. - progress cbn [fst snd]. - rewrite !eval_flat_map_if, !flat_map_singleton. - push. - apply Zminus_eq; ring_simplify. - simple refine (let pf := _ in _); [ shelve | | clearbody pf ]; cycle 1. - { break_innermost_match; Z.ltb_to_lt; push; ring_simplify; - rewrite !map_map; cbn [fst snd]; - rewrite ?Z.mul_opp_l, (Z.mul_comm (eval c)), <- eval_mul; - cbv [mul]; - rewrite flat_map_map; cbn [fst snd]. - { exact pf. } - { omega. } } - { rewrite Z.add_opp_l. - apply Zeq_minus. - f_equal. - apply flat_map_ext; intro x. - rewrite fst_partition_In; intros [? ?]; Z.ltb_to_lt. - apply map_ext; intro. - rewrite !Z.Z_divide_div_mul_exact' by auto using Znumtheory.Zmod_divide. - f_equal; nia. } + cbv [let_bind_for_reduce_square reduce_square square Let_In]; rewrite list_rect_map; push. + apply list_rect_Proper; [ | repeat intro; subst | reflexivity ]; cbv [split]; push; [ nsatz | ]. + rewrite flat_map_map, eval_reduce_square_step by auto. + break_match; Z.ltb_to_lt; push. + 1:rewrite eval_map_div by eauto using eval_reduce_square_helper; push. + all:cbv [mul]; cbn [map flat_map fst snd]; rewrite !app_nil_r, !map_map; cbn [fst snd]. + all:autorewrite with zsimplify_const. + all:rewrite <- ?Z.mul_assoc, !(Z.mul_comm (fst a)), <- ?Z.mul_assoc. + all:rewrite ?Z.mul_assoc, <- (Z.mul_assoc _ (fst a) (fst a)), <- !(Z.mul_comm (fst a * fst a)). + 1:rewrite !Z.Z_divide_div_mul_exact' by auto using Znumtheory.Zmod_divide. + all:idtac; + let LHS := match goal with |- ?LHS = ?RHS => LHS end in + let RHS := match goal with |- ?LHS = ?RHS => RHS end in + let f := match LHS with context[eval (reduce _ _ (map ?f _))] => f end in + let g := match RHS with context[eval (reduce _ _ (map ?f _))] => f end in + rewrite (map_ext f g) by (intros; f_equal; nsatz). + all:nsatz. Qed. Lemma eval_reduce_square s c p (s_nz:s<>0) (modulus_nz:s-eval c<>0) : eval (reduce_square s c p) mod (s - eval c) |