|
| 1 | +/- |
| 2 | +Copyright (c) 2023 Yury Kudryashov. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Yury Kudryashov |
| 5 | +-/ |
| 6 | +import data.set.image |
| 7 | +import data.list.basic |
| 8 | +import data.fin.basic |
| 9 | + |
| 10 | +/-! |
| 11 | +# Lemmas about `list`s and `set.range` |
| 12 | +
|
| 13 | +In this file we prove lemmas about range of some operations on lists. |
| 14 | +-/ |
| 15 | + |
| 16 | +open list |
| 17 | +variables {α β : Type*} (l : list α) |
| 18 | + |
| 19 | +namespace set |
| 20 | + |
| 21 | +lemma range_list_map (f : α → β) : range (map f) = {l | ∀ x ∈ l, x ∈ range f} := |
| 22 | +begin |
| 23 | + refine subset.antisymm (range_subset_iff.2 $ λ l, forall_mem_map_iff.2 $ λ y _, mem_range_self _) |
| 24 | + (λ l hl, _), |
| 25 | + induction l with a l ihl, { exact ⟨[], rfl⟩ }, |
| 26 | + rcases ihl (λ x hx, hl x $ subset_cons _ _ hx) with ⟨l, rfl⟩, |
| 27 | + rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩, |
| 28 | + exact ⟨a :: l, map_cons _ _ _⟩ |
| 29 | +end |
| 30 | + |
| 31 | +lemma range_list_map_coe (s : set α) : range (map (coe : s → α)) = {l | ∀ x ∈ l, x ∈ s} := |
| 32 | +by rw [range_list_map, subtype.range_coe] |
| 33 | + |
| 34 | +@[simp] lemma range_list_nth_le : range (λ k : fin l.length, l.nth_le k k.2) = {x | x ∈ l} := |
| 35 | +begin |
| 36 | + ext x, |
| 37 | + rw [mem_set_of_eq, mem_iff_nth_le], |
| 38 | + exact ⟨λ ⟨⟨n, h₁⟩, h₂⟩, ⟨n, h₁, h₂⟩, λ ⟨n, h₁, h₂⟩, ⟨⟨n, h₁⟩, h₂⟩⟩ |
| 39 | +end |
| 40 | + |
| 41 | +lemma range_list_nth : range l.nth = insert none (some '' {x | x ∈ l}) := |
| 42 | +begin |
| 43 | + rw [← range_list_nth_le, ← range_comp], |
| 44 | + refine (range_subset_iff.2 $ λ n, _).antisymm (insert_subset.2 ⟨_, _⟩), |
| 45 | + exacts [(le_or_lt l.length n).imp nth_eq_none_iff.2 (λ hlt, ⟨⟨_, _⟩, (nth_le_nth hlt).symm⟩), |
| 46 | + ⟨_, nth_eq_none_iff.2 le_rfl⟩, range_subset_iff.2 $ λ k, ⟨_, nth_le_nth _⟩] |
| 47 | +end |
| 48 | + |
| 49 | +@[simp] lemma range_list_nthd (d : α) : range (λ n, l.nthd n d) = insert d {x | x ∈ l} := |
| 50 | +calc range (λ n, l.nthd n d) = (λ o : option α, o.get_or_else d) '' range l.nth : |
| 51 | + by simp only [← range_comp, (∘), nthd_eq_get_or_else_nth] |
| 52 | +... = insert d {x | x ∈ l} : |
| 53 | + by simp only [range_list_nth, image_insert_eq, option.get_or_else, image_image, image_id'] |
| 54 | + |
| 55 | +@[simp] |
| 56 | +lemma range_list_inth [inhabited α] (l : list α) : range l.inth = insert default {x | x ∈ l} := |
| 57 | +range_list_nthd l default |
| 58 | + |
| 59 | +end set |
| 60 | + |
| 61 | +/-- If each element of a list can be lifted to some type, then the whole list can be lifted to this |
| 62 | +type. -/ |
| 63 | +instance list.can_lift (c) (p) [can_lift α β c p] : |
| 64 | + can_lift (list α) (list β) (list.map c) (λ l, ∀ x ∈ l, p x) := |
| 65 | +{ prf := λ l H, |
| 66 | + begin |
| 67 | + rw [← set.mem_range, set.range_list_map], |
| 68 | + exact λ a ha, can_lift.prf a (H a ha), |
| 69 | + end} |
0 commit comments