Add some natutil and listutil lemmas

2 files changed, 60 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 1713d22ab..efaea107d 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -2175,3 +2175,33 @@ Proof.
   all: inversion H0; clear H0; subst.
   all: f_equal; eauto using or_introl.
 Qed.
+
+Lemma push_f_list_rect {P P'} (f : P -> P') {A} Pnil Pcons Pcons' ls
+      (Hcons : forall x xs rec, f (Pcons x xs rec)
+                                = Pcons' x xs (f rec))
+  : f (list_rect (fun _ : list A => P) Pnil Pcons ls)
+    = list_rect
+        (fun _ => _)
+        (f Pnil)
+        Pcons'
+        ls.
+Proof.
+  induction ls as [|x xs IHxs]; cbn [list_rect]; [ reflexivity | ].
+  rewrite Hcons, IHxs; reflexivity.
+Qed.
+
+Lemma eq_app_list_rect {A} (ls1 ls2 : list A)
+  : List.app ls1 ls2 = list_rect _ ls2 (fun x _ rec => x :: rec) ls1.
+Proof. revert ls2; induction ls1, ls2; cbn; f_equal; eauto. Qed.
+Lemma eq_flat_map_list_rect {A B} f (ls : list A)
+  : @flat_map A B f ls = list_rect _ nil (fun x _ rec => f x ++ rec) ls.
+Proof. induction ls; cbn; eauto. Qed.
+Lemma eq_partition_list_rect {A} f (ls : list A)
+  : @partition A f ls = list_rect _ (nil, nil) (fun x _ '(a, b) => bool_rect (fun _ => _) (x :: a, b) (a, x :: b) (f x)) ls.
+Proof. induction ls; cbn; eauto. Qed.
+Lemma eq_fold_right_list_rect {A B} f v (ls : list _)
+  : @fold_right A B f v ls = list_rect _ v (fun x _ rec => f x rec) ls.
+Proof. induction ls; cbn; eauto. Qed.
+Lemma eq_map_list_rect {A B} f (ls : list _)
+  : @List.map A B f ls = list_rect _ nil (fun x _ rec => f x :: rec) ls.
+Proof. induction ls; cbn; eauto. Qed.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 1e75b3494..e49fc7c02 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -411,3 +411,33 @@ Qed.
 
 Lemma max_0_iff a b : Nat.max a b = 0%nat <-> (a = 0%nat /\ b = 0%nat).
 Proof. omega **. Qed.
+
+Lemma push_f_nat_rect {P P'} (f : P -> P') PO PS PS' n
+      (HS : forall x rec, f (PS x rec)
+                          = PS' x (f rec))
+  : f (nat_rect (fun _ => P) PO PS n)
+    = nat_rect
+        (fun _ => _)
+        (f PO)
+        PS'
+        n.
+Proof.
+  induction n as [|n IHn]; cbn [nat_rect]; [ reflexivity | ].
+  rewrite HS, IHn; reflexivity.
+Qed.
+
+Lemma push_f_nat_rect_arrow {P P'} (f : P -> P') {A} PO PS PS' n v
+      (HS : forall x rec v, f (PS x rec v)
+                            = PS' x (fun v => f (rec v)) v)
+      (PS'_Proper : Proper (Logic.eq ==> pointwise_relation _ Logic.eq ==> Logic.eq ==> Logic.eq) PS')
+  : f (nat_rect (fun _ => A -> P) PO PS n v)
+    = nat_rect
+        (fun _ => _)
+        (fun v => f (PO v))
+        PS'
+        n
+        v.
+Proof.
+  revert v; induction n as [|n IHn]; cbn [nat_rect]; [ reflexivity | ]; intro.
+  rewrite HS; apply PS'_Proper; eauto.
+Qed.