aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-08 15:51:28 -0500
committerGravatar Jason Gross <jgross@mit.edu>2019-03-08 15:51:28 -0500
commit8ba8a4021bc4413fc7fe9996f1748fed7494cd0e (patch)
treec7f5fbcd655133a98de6afa1313be0c1ff75dbd0 /src/Util
parentac184af76e778cbc9e9655bc96b90fc76f6161a5 (diff)
Add some eq list_rect lemmas to ListUtil
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/ListUtil.v32
1 files changed, 32 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 5af914ffe..f709e7dd1 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -2449,3 +2449,35 @@ Lemma eq_combine_list_rect {A B} xs ys
end)
xs ys.
Proof using Type. revert ys; induction xs, ys; cbn; f_equal; auto. Qed.
+
+Lemma eq_length_list_rect {A} xs
+ : @List.length A xs
+ = (list_rect _)
+ 0%nat
+ (fun _ xs length_xs => S length_xs)
+ xs.
+Proof using Type. induction xs; cbn; f_equal; auto. Qed.
+
+Lemma eq_rev_list_rect {A} xs
+ : @List.rev A xs
+ = (list_rect _)
+ nil
+ (fun x xs rev_xs => rev_xs ++ [x])
+ xs.
+Proof using Type. induction xs; cbn; f_equal; auto. Qed.
+
+Lemma eq_update_nth_nat_rect {A} n f xs
+ : @update_nth A n f xs
+ = (nat_rect _)
+ (fun xs => match xs with
+ | nil => nil
+ | x' :: xs' => f x' :: xs'
+ end)
+ (fun n' update_nth_n' xs
+ => match xs with
+ | nil => nil
+ | x' :: xs' => x' :: update_nth_n' xs'
+ end)
+ n
+ xs.
+Proof using Type. revert xs; induction n, xs; cbn; f_equal; auto. Qed.