diff options
author | jadep <jade.philipoom@gmail.com> | 2018-09-16 15:34:59 -0400 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2018-09-17 21:34:36 -0400 |
commit | 9d0f335bd50189239ed6770f4cde0949e27d0344 (patch) | |
tree | de679a809efe3d823b4e2ecda1fd7c9067e0d224 /src | |
parent | 663864c832e2e94d87b8d19bd8163bbd4c4293a3 (diff) |
remove unneeded proof
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 07f2b3a79..e8a814ffb 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -1296,33 +1296,6 @@ Module Partition. Definition partition n x := map (fun i => (x mod weight (S i)) / weight i) (seq 0 n). - (* TODO : move to ListUtil *) - Lemma nth_default_map_seq_equiv {A} l f d n - (Hlength : length l = n) - (Hnth_default : forall i, (i < n)%nat -> @nth_default A d l i = f i) : - l = map f (seq 0 n). - Proof using Type. - apply list_elementwise_eq. subst n. - intro i; destruct (lt_dec i (length l)). - { rewrite !nth_error_Some_nth_default with (x:=d) by distr_length. - autorewrite with push_nth_default. - rewrite map_nth_default with (x:=0%nat) by distr_length. - rewrite Hnth_default by distr_length. - rewrite nth_default_seq_inbounds by distr_length. - f_equal. } - { rewrite !nth_error_length_error by distr_length. - reflexivity. } - Qed. - - Lemma nth_default_partitions x : forall p n, - (forall i, (i < n)%nat -> nth_default 0 p i = (x mod weight (S i)) / weight i) -> - length p = n -> - p = partition n x. - Proof using Type. - cbv [partition]; intros. - eauto using nth_default_map_seq_equiv. - Qed. - Lemma partition_step n x : partition (S n) x = partition n x ++ [(x mod weight (S n)) / weight n]. Proof using Type. @@ -1405,29 +1378,6 @@ Module Partition. intros; distr_length; auto. Qed. Hint Rewrite length_recursive_partition : distr_length. - - (* TODO : move *) - Hint Rewrite Nat.sub_0_l : natsimplify. - - (* TODO : remove if this ends up being unused *) - Lemma recursive_partition_skipn : forall m n i j x, - (m < n)%nat -> - (j = i + m)%nat -> - skipn m (recursive_partition n i (x / weight i)) = recursive_partition (n-m) j (x / weight j). - Proof. - induction m; destruct n; intros; subst; - repeat match goal with - | _ => progress cbn [recursive_partition] - | _ => rewrite weight_0 by assumption - | _ => rewrite weight_multiples by assumption - | _ => rewrite Z.div_div by auto - | _ => rewrite Z.mul_div_eq by auto - | _ => progress autorewrite with zsimplify_fast natsimplify push_skipn - | _ => reflexivity - end. - erewrite IHm by (auto; omega). - repeat (f_equal; try omega). - Qed. End Partition. Hint Rewrite length_partition length_recursive_partition : distr_length. Hint Rewrite eval_partition using auto : push_eval. |