diff options
-rw-r--r-- | src/Util/ListUtil.v | 17 | ||||
-rw-r--r-- | src/Util/NatUtil.v | 3 |
2 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 0a0b0c5da..f9e3457a1 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2048,3 +2048,20 @@ Proof. | [ H : forall j, f j ?v = _ |- context[f _ ?v] ] => rewrite H end. } Qed. + +Lemma fold_left_push A (x y : A) (f : A -> A -> A) + (f_assoc : forall x y z, f (f x y) z = f x (f y z)) + ls + : f x (fold_left f ls y) = fold_left f ls (f x y). +Proof. + revert x y; induction ls as [|l ls IHls]; cbn; [ reflexivity | ]. + intros; rewrite IHls; f_equal; auto. +Qed. + +Lemma fold_right_push A (x y : A) (f : A -> A -> A) + (f_assoc : forall x y z, f (f x y) z = f x (f y z)) + ls + : f (fold_right f x ls) y = fold_right f (f x y) ls. +Proof. + rewrite <- (rev_involutive ls), !fold_left_rev_right, fold_left_push with (f:=fun x y => f y x); auto. +Qed. diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 087f0a6c7..08fd8a92a 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -392,3 +392,6 @@ Proof. end; rewrite H'' in *; assumption. } } Qed. + +Lemma max_0_iff a b : Nat.max a b = 0%nat <-> (a = 0%nat /\ b = 0%nat). +Proof. omega **. Qed. |