diff --git a/Mathlib.lean b/Mathlib.lean index 8ea014c3cf5c0..190c88a1decc9 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1809,6 +1809,7 @@ import Mathlib.Data.List.Permutation import Mathlib.Data.List.Prime import Mathlib.Data.List.ProdSigma import Mathlib.Data.List.Range +import Mathlib.Data.List.ReduceOption import Mathlib.Data.List.Rotate import Mathlib.Data.List.Sections import Mathlib.Data.List.Sigma diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 353dd8eb591a1..69f46d31189a7 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -2917,96 +2917,6 @@ theorem Sublist.map (f : α → β) {l₁ l₂ : List α} (s : l₁ <+ l₂) : m filterMap_eq_map f ▸ s.filterMap _ #align list.sublist.map List.Sublist.map -/-! ### reduceOption -/ - -@[simp] -theorem reduceOption_cons_of_some (x : α) (l : List (Option α)) : - reduceOption (some x :: l) = x :: l.reduceOption := by - simp only [reduceOption, filterMap, id.def, eq_self_iff_true, and_self_iff] -#align list.reduce_option_cons_of_some List.reduceOption_cons_of_some - -@[simp] -theorem reduceOption_cons_of_none (l : List (Option α)) : - reduceOption (none :: l) = l.reduceOption := by simp only [reduceOption, filterMap, id.def] -#align list.reduce_option_cons_of_none List.reduceOption_cons_of_none - -@[simp] -theorem reduceOption_nil : @reduceOption α [] = [] := - rfl -#align list.reduce_option_nil List.reduceOption_nil - -@[simp] -theorem reduceOption_map {l : List (Option α)} {f : α → β} : - reduceOption (map (Option.map f) l) = map f (reduceOption l) := by - induction' l with hd tl hl - · simp only [reduceOption_nil, map_nil] - · cases hd <;> - simpa [true_and_iff, Option.map_some', map, eq_self_iff_true, - reduceOption_cons_of_some] using hl -#align list.reduce_option_map List.reduceOption_map - -theorem reduceOption_append (l l' : List (Option α)) : - (l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption := - filterMap_append l l' id -#align list.reduce_option_append List.reduceOption_append - -theorem reduceOption_length_le (l : List (Option α)) : l.reduceOption.length ≤ l.length := by - induction' l with hd tl hl - · simp [reduceOption_nil, length] - · cases hd - · exact Nat.le_succ_of_le hl - · simpa only [length, Nat.add_le_add_iff_right, reduceOption_cons_of_some] using hl -#align list.reduce_option_length_le List.reduceOption_length_le - -theorem reduceOption_length_eq_iff {l : List (Option α)} : - l.reduceOption.length = l.length ↔ ∀ x ∈ l, Option.isSome x := by - induction' l with hd tl hl - · simp only [forall_const, reduceOption_nil, not_mem_nil, forall_prop_of_false, eq_self_iff_true, - length, not_false_iff] - · cases hd - · simp only [mem_cons, forall_eq_or_imp, Bool.coe_sort_false, false_and_iff, - reduceOption_cons_of_none, length, Option.isSome_none, iff_false_iff] - intro H - have := reduceOption_length_le tl - rw [H] at this - exact absurd (Nat.lt_succ_self _) (not_lt_of_le this) - · simp only [length, mem_cons, forall_eq_or_imp, Option.isSome_some, ← hl, reduceOption, - true_and] - omega -#align list.reduce_option_length_eq_iff List.reduceOption_length_eq_iff - -theorem reduceOption_length_lt_iff {l : List (Option α)} : - l.reduceOption.length < l.length ↔ none ∈ l := by - rw [(reduceOption_length_le l).lt_iff_ne, Ne, reduceOption_length_eq_iff] - induction l <;> simp [*] - rw [@eq_comm _ none, ← Option.not_isSome_iff_eq_none, Decidable.imp_iff_not_or] -#align list.reduce_option_length_lt_iff List.reduceOption_length_lt_iff - -theorem reduceOption_singleton (x : Option α) : [x].reduceOption = x.toList := by cases x <;> rfl -#align list.reduce_option_singleton List.reduceOption_singleton - -theorem reduceOption_concat (l : List (Option α)) (x : Option α) : - (l.concat x).reduceOption = l.reduceOption ++ x.toList := by - induction' l with hd tl hl generalizing x - · cases x <;> simp [Option.toList] - · simp only [concat_eq_append, reduceOption_append] at hl - cases hd <;> simp [hl, reduceOption_append] -#align list.reduce_option_concat List.reduceOption_concat - -theorem reduceOption_concat_of_some (l : List (Option α)) (x : α) : - (l.concat (some x)).reduceOption = l.reduceOption.concat x := by - simp only [reduceOption_nil, concat_eq_append, reduceOption_append, reduceOption_cons_of_some] -#align list.reduce_option_concat_of_some List.reduceOption_concat_of_some - -theorem reduceOption_mem_iff {l : List (Option α)} {x : α} : x ∈ l.reduceOption ↔ some x ∈ l := by - simp only [reduceOption, id.def, mem_filterMap, exists_eq_right] -#align list.reduce_option_mem_iff List.reduceOption_mem_iff - -theorem reduceOption_get?_iff {l : List (Option α)} {x : α} : - (∃ i, l.get? i = some (some x)) ↔ ∃ i, l.reduceOption.get? i = some x := by - rw [← mem_iff_get?, ← mem_iff_get?, reduceOption_mem_iff] -#align list.reduce_option_nth_iff List.reduceOption_get?_iff - /-! ### filter -/ section Filter diff --git a/Mathlib/Data/List/Infix.lean b/Mathlib/Data/List/Infix.lean index 53a45438a0a2d..0dc64b4ad7154 100644 --- a/Mathlib/Data/List/Infix.lean +++ b/Mathlib/Data/List/Infix.lean @@ -277,7 +277,7 @@ theorem cons_prefix_iff : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := rwa [prefix_cons_inj] #align list.cons_prefix_iff List.cons_prefix_iff -theorem IsPrefix.map (h : l₁ <+: l₂) (f : α → β) : l₁.map f <+: l₂.map f := by +protected theorem IsPrefix.map (h : l₁ <+: l₂) (f : α → β) : l₁.map f <+: l₂.map f := by induction' l₁ with hd tl hl generalizing l₂ · simp only [nil_prefix, map_nil] · cases' l₂ with hd₂ tl₂ @@ -286,7 +286,7 @@ theorem IsPrefix.map (h : l₁ <+: l₂) (f : α → β) : l₁.map f <+: l₂.m simp only [List.map_cons, h, prefix_cons_inj, hl, map] #align list.is_prefix.map List.IsPrefix.map -theorem IsPrefix.filter_map (h : l₁ <+: l₂) (f : α → Option β) : +protected theorem IsPrefix.filterMap (h : l₁ <+: l₂) (f : α → Option β) : l₁.filterMap f <+: l₂.filterMap f := by induction' l₁ with hd₁ tl₁ hl generalizing l₂ · simp only [nil_prefix, filterMap_nil] @@ -296,9 +296,11 @@ theorem IsPrefix.filter_map (h : l₁ <+: l₂) (f : α → Option β) : rw [← @singleton_append _ hd₁ _, ← @singleton_append _ hd₂ _, filterMap_append, filterMap_append, h.left, prefix_append_right_inj] exact hl h.right -#align list.is_prefix.filter_map List.IsPrefix.filter_map +#align list.is_prefix.filter_map List.IsPrefix.filterMap -theorem IsPrefix.reduceOption {l₁ l₂ : List (Option α)} (h : l₁ <+: l₂) : +@[deprecated] alias IsPrefix.filter_map := IsPrefix.filterMap + +protected theorem IsPrefix.reduceOption {l₁ l₂ : List (Option α)} (h : l₁ <+: l₂) : l₁.reduceOption <+: l₂.reduceOption := h.filter_map id #align list.is_prefix.reduce_option List.IsPrefix.reduceOption diff --git a/Mathlib/Data/List/ReduceOption.lean b/Mathlib/Data/List/ReduceOption.lean new file mode 100644 index 0000000000000..8c2cf91f15f65 --- /dev/null +++ b/Mathlib/Data/List/ReduceOption.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2020 Yakov Pechersky. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yakov Pechersky +-/ +import Mathlib.Logic.IsEmpty +import Mathlib.Order.Basic +import Mathlib.Init.Data.Bool.Lemmas +import Mathlib.Init.Data.Nat.Lemmas + +/-! +# Properties of `List.reduceOption` + +In this file we prove basic lemmas about `List.reduceOption`. +-/ + +namespace List + +variable {α β : Type*} + +@[simp] +theorem reduceOption_cons_of_some (x : α) (l : List (Option α)) : + reduceOption (some x :: l) = x :: l.reduceOption := by + simp only [reduceOption, filterMap, id.def, eq_self_iff_true, and_self_iff] +#align list.reduce_option_cons_of_some List.reduceOption_cons_of_some + +@[simp] +theorem reduceOption_cons_of_none (l : List (Option α)) : + reduceOption (none :: l) = l.reduceOption := by simp only [reduceOption, filterMap, id.def] +#align list.reduce_option_cons_of_none List.reduceOption_cons_of_none + +@[simp] +theorem reduceOption_nil : @reduceOption α [] = [] := + rfl +#align list.reduce_option_nil List.reduceOption_nil + +@[simp] +theorem reduceOption_map {l : List (Option α)} {f : α → β} : + reduceOption (map (Option.map f) l) = map f (reduceOption l) := by + induction' l with hd tl hl + · simp only [reduceOption_nil, map_nil] + · cases hd <;> + simpa [true_and_iff, Option.map_some', map, eq_self_iff_true, + reduceOption_cons_of_some] using hl +#align list.reduce_option_map List.reduceOption_map + +theorem reduceOption_append (l l' : List (Option α)) : + (l ++ l').reduceOption = l.reduceOption ++ l'.reduceOption := + filterMap_append l l' id +#align list.reduce_option_append List.reduceOption_append + +theorem reduceOption_length_le (l : List (Option α)) : l.reduceOption.length ≤ l.length := by + induction' l with hd tl hl + · simp [reduceOption_nil, length] + · cases hd + · exact Nat.le_succ_of_le hl + · simpa only [length, Nat.add_le_add_iff_right, reduceOption_cons_of_some] using hl +#align list.reduce_option_length_le List.reduceOption_length_le + +theorem reduceOption_length_eq_iff {l : List (Option α)} : + l.reduceOption.length = l.length ↔ ∀ x ∈ l, Option.isSome x := by + induction' l with hd tl hl + · simp only [forall_const, reduceOption_nil, not_mem_nil, forall_prop_of_false, eq_self_iff_true, + length, not_false_iff] + · cases hd + · simp only [mem_cons, forall_eq_or_imp, Bool.coe_sort_false, false_and_iff, + reduceOption_cons_of_none, length, Option.isSome_none, iff_false_iff] + intro H + have := reduceOption_length_le tl + rw [H] at this + exact absurd (Nat.lt_succ_self _) (not_lt_of_le this) + · simp only [length, mem_cons, forall_eq_or_imp, Option.isSome_some, ← hl, reduceOption, + true_and] + omega +#align list.reduce_option_length_eq_iff List.reduceOption_length_eq_iff + +theorem reduceOption_length_lt_iff {l : List (Option α)} : + l.reduceOption.length < l.length ↔ none ∈ l := by + rw [(reduceOption_length_le l).lt_iff_ne, Ne, reduceOption_length_eq_iff] + induction l <;> simp [*] + rw [@eq_comm _ none, ← Option.not_isSome_iff_eq_none, Decidable.imp_iff_not_or] +#align list.reduce_option_length_lt_iff List.reduceOption_length_lt_iff + +theorem reduceOption_singleton (x : Option α) : [x].reduceOption = x.toList := by cases x <;> rfl +#align list.reduce_option_singleton List.reduceOption_singleton + +theorem reduceOption_concat (l : List (Option α)) (x : Option α) : + (l.concat x).reduceOption = l.reduceOption ++ x.toList := by + induction' l with hd tl hl generalizing x + · cases x <;> simp [Option.toList] + · simp only [concat_eq_append, reduceOption_append] at hl + cases hd <;> simp [hl, reduceOption_append] +#align list.reduce_option_concat List.reduceOption_concat + +theorem reduceOption_concat_of_some (l : List (Option α)) (x : α) : + (l.concat (some x)).reduceOption = l.reduceOption.concat x := by + simp only [reduceOption_nil, concat_eq_append, reduceOption_append, reduceOption_cons_of_some] +#align list.reduce_option_concat_of_some List.reduceOption_concat_of_some + +theorem reduceOption_mem_iff {l : List (Option α)} {x : α} : x ∈ l.reduceOption ↔ some x ∈ l := by + simp only [reduceOption, id.def, mem_filterMap, exists_eq_right] +#align list.reduce_option_mem_iff List.reduceOption_mem_iff + +theorem reduceOption_get?_iff {l : List (Option α)} {x : α} : + (∃ i, l.get? i = some (some x)) ↔ ∃ i, l.reduceOption.get? i = some x := by + rw [← mem_iff_get?, ← mem_iff_get?, reduceOption_mem_iff] +#align list.reduce_option_nth_iff List.reduceOption_get?_iff +