Add useful list lemmas

1 files changed, 61 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index f13511ba5..d49db025b 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -5,6 +5,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Pointed.
+Require Import Crypto.Util.Prod.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Export Crypto.Util.Tactics.BreakMatch.
 Require Export Crypto.Util.Tactics.DestructHead.
@@ -22,6 +23,17 @@ Definition list_case
      | cons x xs => C x xs
      end.
 
+Global Instance list_rect_Proper A P : Proper (eq ==> pointwise_relation _ (pointwise_relation _ (pointwise_relation _ eq)) ==> eq ==> eq) (@list_rect A (fun _ => P)).
+Proof.
+  intros N N' HN C C' HC xs ys Hxs; subst N' ys.
+  induction xs; cbn; trivial; rewrite IHxs; apply HC.
+Qed.
+Global Instance list_case_Proper A P : Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq) (@list_case A (fun _ => P)).
+Proof.
+  cbv [pointwise_relation respectful].
+  intros N N' HN C C' HC xs ys Hxs; subst N' ys; destruct xs; cbn; auto.
+Qed.
+
 Create HintDb distr_length discriminated.
 Create HintDb simpl_set_nth discriminated.
 Create HintDb simpl_update_nth discriminated.
@@ -1908,3 +1920,52 @@ Lemma single_list_rect_to_match A (P:list A -> Type) (Pnil: P nil) (PS: forall a
                                                    | nil => Pnil
                                                    end.
 Proof. destruct ls; reflexivity. Qed.
+
+Lemma partition_app A (f : A -> bool) (a b : list A)
+  : partition f (a ++ b) = (fst (partition f a) ++ fst (partition f b),
+                            snd (partition f a) ++ snd (partition f b)).
+Proof.
+  revert b; induction a, b; cbn; rewrite ?app_nil_r; eta_expand; try reflexivity.
+  rewrite !IHa; cbn; break_match; reflexivity.
+Qed.
+
+Lemma flat_map_map A B C (f : A -> B) (g : B -> list C) (xs : list A)
+  : flat_map g (map f xs) = flat_map (fun x => g (f x)) xs.
+Proof. induction xs; cbn; congruence. Qed.
+Lemma flat_map_singleton A B (f : A -> B) (xs : list A)
+  : flat_map (fun x => cons (f x) nil) xs = map f xs.
+Proof. induction xs; cbn; congruence. Qed.
+Lemma flat_map_ext A B (f g : A -> list B) xs (H : forall x, In x xs -> f x = g x)
+  : flat_map f xs = flat_map g xs.
+Proof. induction xs; cbn in *; [ reflexivity | rewrite IHxs; f_equal ]; intros; intuition auto. Qed.
+Global Instance flat_map_Proper A B : Proper (pointwise_relation _ eq ==> eq ==> eq) (@flat_map A B).
+Proof. repeat intro; subst; apply flat_map_ext; auto. Qed.
+
+Lemma partition_map A B (f : B -> bool) (g : A -> B) xs
+  : partition f (map g xs) = (map g (fst (partition (fun x => f (g x)) xs)),
+                              map g (snd (partition (fun x => f (g x)) xs))).
+Proof. induction xs; cbn; [ | rewrite !IHxs ]; break_match; reflexivity. Qed.
+Lemma map_fst_partition A B (f : B -> bool) (g : A -> B) xs
+  : map g (fst (partition (fun x => f (g x)) xs)) = fst (partition f (map g xs)).
+Proof. rewrite partition_map; reflexivity. Qed.
+Lemma map_snd_partition A B (f : B -> bool) (g : A -> B) xs
+  : map g (snd (partition (fun x => f (g x)) xs)) = snd (partition f (map g xs)).
+Proof. rewrite partition_map; reflexivity. Qed.
+Lemma partition_In A (f:A -> bool) xs : forall x, @In A x xs <-> @In A x (if f x then fst (partition f xs) else snd (partition f xs)).
+Proof.
+  intro x; destruct (f x) eqn:?; split; intros; repeat apply conj; revert dependent x;
+    (induction xs as [|x' xs IHxs]; cbn; [ | destruct (f x') eqn:?, (partition f xs) ]; cbn in *; subst; intuition (subst; auto));
+    congruence.
+Qed.
+Lemma fst_partition_In A f xs : forall x, @In A x (fst (partition f xs)) <-> f x = true /\ @In A x xs.
+Proof.
+  intro x; split; intros; repeat apply conj; revert dependent x;
+    (induction xs as [|x' xs IHxs]; cbn; [ | destruct (f x') eqn:?, (partition f xs) ]; cbn in *; subst; intuition (subst; auto));
+    congruence.
+Qed.
+Lemma snd_partition_In A f xs : forall x, @In A x (snd (partition f xs)) <-> f x = false /\ @In A x xs.
+Proof.
+  intro x; split; intros; repeat apply conj; revert dependent x;
+    (induction xs as [|x' xs IHxs]; cbn; [ | destruct (f x') eqn:?, (partition f xs) ]; cbn in *; subst; intuition (subst; auto));
+    congruence.
+Qed.