diff options
author | Jade Philipoom <jadep@google.com> | 2018-03-08 16:11:06 +0100 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2018-04-03 09:00:55 -0400 |
commit | 39a7ef1f4787381bf7013025cae1d8edc980500c (patch) | |
tree | 7f3f1ebabf12a8b0d46a0a73e75a3a5f44a95943 /src | |
parent | ab4bea12d33f3c4225d0af577242c1bbae12d420 (diff) |
move some lemmas to ZUtil/ListUtil
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 25 | ||||
-rw-r--r-- | src/Util/ListUtil.v | 18 | ||||
-rw-r--r-- | src/Util/ZUtil/Div.v | 3 |
3 files changed, 20 insertions, 26 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 62168b9a8..990f45a37 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -786,14 +786,6 @@ Module Columns. apply Positional.eval_snoc; distr_length. Qed. Hint Rewrite eval_snoc using (solve [distr_length]) : push_eval. - (* TODO: move to ListUtil *) - Lemma list_rect_to_match A (P:list A -> Type) (Pnil: P []) (PS: forall a tl, P (a :: tl)) ls : - @list_rect A P Pnil (fun a tl _ => PS a tl) ls = match ls with - | cons a tl => PS a tl - | nil => Pnil - end. - Proof. destruct ls; reflexivity. Qed. - Hint Rewrite <- Z.div_add' using omega : pull_Zdiv. Ltac cases := @@ -924,10 +916,6 @@ Module Columns. Lemma flatten_snoc x inp : flatten (inp ++ [x]) = flatten_step x (flatten inp). Proof. cbv [flatten]. rewrite rev_unit. reflexivity. Qed. - (* TODO: move to ZUtil *) - Lemma Z_divide_div_mul_exact' a b c : b <> 0 -> (b | a) -> a * c / b = c * (a / b). - Proof. intros. rewrite Z.mul_comm. auto using Z.divide_div_mul_exact. Qed. - Lemma flatten_partitions inp: forall n i, length inp = n -> (i < n)%nat -> nth_default 0 (fst (flatten inp)) i = ((eval n inp) mod (weight (S i))) / weight i. @@ -1385,19 +1373,6 @@ Module Rows. let first_row := hd nil inp in flatten' (first_row, 0) (hd (Positional.zeros (length first_row)) (tl inp) :: tl (tl inp)). - (* TODO : move to ListUtil *) - Lemma rev_cons {A} x ls : @rev A (x :: ls) = rev ls ++ [x]. Proof. reflexivity. Qed. - Hint Rewrite @rev_cons : list. - - (* TODO: move to ListUtil *) - Lemma fold_right_snoc {A B} f a x ls: - @fold_right A B f a (ls ++ [x]) = fold_right f (f x a) ls. - Proof. - rewrite <-(rev_involutive ls), <-rev_cons. - rewrite !fold_left_rev_right; reflexivity. - Qed. - Hint Rewrite @fold_right_snoc : push_fold_right. - Lemma flatten'_cons state r inp : flatten' state (r :: inp) = flatten' (fst (sum_rows r (fst state)), snd state + snd (sum_rows r (fst state))) inp. Proof. cbv [flatten']; autorewrite with list push_fold_right. reflexivity. Qed. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 081ef54b5..e162c2daf 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -107,6 +107,9 @@ Module Export List. End FlatMap. Hint Rewrite @flat_map_cons @flat_map_nil : push_flat_map. + Lemma rev_cons {A} x ls : @rev A (x :: ls) = rev ls ++ [x]. Proof. reflexivity. Qed. + Hint Rewrite @rev_cons : list. + Section FoldRight. Context {A B} (f:B->A->A). Lemma fold_right_nil : forall {A B} (f:B->A->A) a, @@ -115,8 +118,14 @@ Module Export List. Lemma fold_right_cons : forall a b bs, fold_right f a (b::bs) = f b (fold_right f a bs). Proof. reflexivity. Qed. + Lemma fold_right_snoc a x ls: + @fold_right A B f a (ls ++ [x]) = fold_right f (f x a) ls. + Proof. + rewrite <-(rev_involutive ls), <-rev_cons. + rewrite !fold_left_rev_right; reflexivity. + Qed. End FoldRight. - Hint Rewrite @fold_right_nil @fold_right_cons : simpl_fold_right push_fold_right. + Hint Rewrite @fold_right_nil @fold_right_cons @fold_right_snoc : simpl_fold_right push_fold_right. Section Partition. Lemma partition_nil {A} (f:A->_) : partition f nil = (nil, nil). @@ -1869,3 +1878,10 @@ Ltac expand_lists _ := | _ => idtac end; subst v; reflexivity ]. + +Lemma list_rect_to_match A (P:list A -> Type) (Pnil: P nil) (PS: forall a tl, P (a :: tl)) ls : + @list_rect A P Pnil (fun a tl _ => PS a tl) ls = match ls with + | cons a tl => PS a tl + | nil => Pnil + end. +Proof. destruct ls; reflexivity. Qed. diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index d660a9935..c596dbab3 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -124,6 +124,9 @@ Module Z. Qed. Hint Rewrite div_add_exact using zutil_arith : zsimplify. + Lemma Z_divide_div_mul_exact' a b c : b <> 0 -> (b | a) -> a * c / b = c * (a / b). + Proof. intros. rewrite Z.mul_comm. auto using Z.divide_div_mul_exact. Qed. + Lemma div_sub_mod_exact a b : b <> 0 -> a / b = (a - a mod b) / b. Proof. intro. |