Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
! This file was ported from Lean 3 source module data.list.of_fn
! leanprover-community/mathlib commit bf27744463e9620ca4e4ebe951fe83530ae6949b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fin.Tuple.Basic
import Mathlib.Data.List.Join
import Mathlib.Data.List.Pairwise
/-!
# Lists from functions
Theorems and lemmas for dealing with `List.ofFn`, which converts a function on `Fin n` to a list
of length `n`.
## Main Statements
The main statements pertain to lists generated using `List.ofFn`
- `List.length_ofFn`, which tells us the length of such a list
- `List.get?_ofFn`, which tells us the nth element of such a list
- `List.equivSigmaTuple`, which is an `Equiv` between lists and the functions that generate them
via `List.ofFn`.
-/
universe u
variable { α : Type u }
open Nat
namespace List
#noalign list.length_of_fn_aux
/-- The length of a list converted from a function is the size of the domain. -/
@[ simp ]
theorem length_ofFn { n } ( f : Fin n → α ) : length ( ofFn f ) = n := by
simp [ ofFn ]
#align list.length_of_fn List.length_ofFn
#noalign list.nth_of_fn_aux
--Porting note: new theorem
@[ simp ]
theorem get_ofFn { n } ( f : Fin n → α ) ( i ) : get ( ofFn f ) i = f ( Fin.cast ( by simp ) i ) := by
have := Array.getElem_ofFn f i ( by simpa using i . 2 : ∀ {n : ℕ } (self : Fin n ↑self < n )
cases' i with i hi α : Type un : ℕ f : Fin n α i : ℕ hi : i < length (ofFn f this : (Array.ofFn f ↑{ val := i , isLt := hi } ] = f { val := ↑{ val := i , isLt := hi } , isLt := (_ : ↑{ val := i , isLt := hi } < n } mk
simp only [ getElem : {cont : Type ?u.1418} →
{idx : Type ?u.1417} →
{elem : outParam (Type ?u.1416){dom : outParam (cont → idx → Prop [self : GetElem cont idx elem dom (xs : cont ) → (i : idx ) → dom xs i elem , Array.get ] at this : (Array.ofFn f ↑{ val := i , isLt := hi } ] = f { val := ↑{ val := i , isLt := hi } , isLt := (_ : ↑{ val := i , isLt := hi } < n } this
simp only [ Fin.cast_mk : ∀ {n m : ℕ } (h : n = m i : ℕ ) (hn : i < n ↑(Fin.cast h { val := i , isLt := hn } = { val := i , isLt := (_ : i < m } ] mk get (ofFn f { val := i , isLt := hi } = f { val := i , isLt := (_ : i < n }
rw [ mk get (ofFn f { val := i , isLt := hi } = f { val := i , isLt := (_ : i < n } ← this ]
congr mk.h.e_2.h mk.h.e_3.e_1.e_a mk.h.e_3.e_3 <;> mk.h.e_2.h mk.h.e_3.e_1.e_a mk.h.e_3.e_3 simp [ ofFn ]
/-- The `n`th element of a list -/
@[ simp ]
theorem get?_ofFn { n } ( f : Fin n → α ) ( i ) : get? ( ofFn f ) i = ofFnNthVal f i :=
if h : i < ( ofFn f ). length
then by
rw [ get?_eq_get h , get_ofFn ]
. simp at h ; simp [ ofFnNthVal , h ]
else by
rw [ ofFnNthVal , get? (ofFn f i = if h : i < n some (f { val := i , isLt := h } none dif_neg ] <;>
simpa using h
#align list.nth_of_fn List.get?_ofFn
set_option linter.deprecated false in
@[ deprecated get_ofFn ]
theorem nthLe_ofFn { n } ( f : Fin n → α ) ( i : Fin n ) :
nthLe ( ofFn f ) i (( length_ofFn f ). symm : ∀ {α : Sort ?u.17560} {a b : α }, a = b b = a symm ▸ i . 2 : ∀ {n : ℕ } (self : Fin n ↑self < n ) = f i := by
simp [ nthLe ]
#align list.nth_le_of_fn List.nthLe_ofFn
set_option linter.deprecated false in
@[ simp , deprecated get_ofFn ]
theorem nthLe_ofFn' { n } ( f : Fin n → α ) { i : ℕ } ( h : i < ( ofFn f ). length ) :
nthLe ( ofFn f ) i h = f ⟨ i , length_ofFn f ▸ h ⟩ :=
nthLe_ofFn f ⟨ i , length_ofFn f ▸ h ⟩
#align list.nth_le_of_fn' List.nthLe_ofFn'
@[ simp ]
theorem map_ofFn { β : Type _ : Type (?u.18457+1)} { n : ℕ } ( f : Fin n → α ) ( g : α → β ) :
map g ( ofFn f ) = ofFn ( g ∘ f ) :=
ext_get ( by simp ) fun i h h' => by simp
#align list.map_of_fn List.map_ofFn
--Porting note: we don't have Array' in mathlib4
-- /-- Arrays converted to lists are the same as `of_fn` on the indexing function of the array. -/
-- theorem array_eq_of_fn {n} (a : Array' n α) : a.toList = ofFn a.read :=
-- by
-- suffices ∀ {m h l}, DArray.revIterateAux a (fun i => cons) m h l =
-- ofFnAux (DArray.read a) m h l
-- from this
-- intros ; induction' m with m IH generalizing l; · rfl
-- simp only [DArray.revIterateAux, of_fn_aux, IH]
-- #align list.array_eq_of_fn List.array_eq_of_fn
@[congr]
theorem ofFn_congr { m n : ℕ } ( h : m = n ) ( f : Fin m → α ) :
ofFn f = ofFn fun i : Fin n => f ( Fin.cast h . symm : ∀ {α : Sort ?u.20537} {a b : α }, a = b b = a i ) := by
subst h
simp_rw [ Fin.cast_refl , OrderIso.refl_apply ]
#align list.of_fn_congr List.ofFn_congr
/-- `ofFn` on an empty domain is the empty list. -/
@[ simp ]
theorem ofFn_zero ( f : Fin 0 → α ) : ofFn f = [] :=
rfl : ∀ {α : Sort ?u.21074} {a : α }, a = a
#align list.of_fn_zero List.ofFn_zero
@[ simp ]
theorem ofFn_succ { n } ( f : Fin ( succ n ) → α ) : ofFn f = f 0 :: ofFn fun i => f i . succ :=
ext_get ( by simp ) ( fun i hi₁ hi₂ => by
cases i
. simp
. simp )
#align list.of_fn_succ List.ofFn_succ
theorem ofFn_succ' { n } ( f : Fin ( succ n ) → α ) :
ofFn f = ( ofFn fun i => f ( Fin.castSucc i )). concat ( f ( Fin.last : (n : ℕ ) → Fin (n + 1 _ )) := by
induction' n with n IH
· rw [ ofFn_zero : ∀ {α : Type ?u.25759} (f : Fin 0 α ofFn f = [] , concat_nil : ∀ {α : Type ?u.25794} (a : α ), concat [] a = [a ] , ofFn_succ , ofFn_zero : ∀ {α : Type ?u.25814} (f : Fin 0 α ofFn f = [] ]
rfl
· rw [ ofFn_succ , IH , ofFn_succ , concat_cons , Fin.castSucc_zero : ∀ {n : ℕ } [inst : NeZero n ↑Fin.castSucc 0 = 0 ]
congr
#align list.of_fn_succ' List.ofFn_succ'
@[ simp ]
theorem ofFn_eq_nil_iff : ∀ {α : Type u} {n : ℕ } {f : Fin n α ofFn f = [] ↔ n = 0 ofFn_eq_nil_iff { n : ℕ } { f : Fin n → α } : ofFn f = [] ↔ n = 0 := by
cases n <;> simp only [ ofFn_zero : ∀ {α : Type ?u.26948} (f : Fin 0 α ofFn f = [] , ofFn_succ , eq_self_iff_true : ∀ {α : Sort ?u.26835} (a : α ), a = a ↔ True , Nat.succ_ne_zero : ∀ (n : ℕ ), succ n ≠ 0 ]
#align list.of_fn_eq_nil_iff List.ofFn_eq_nil_iff : ∀ {α : Type u} {n : ℕ } {f : Fin n α ofFn f = [] ↔ n = 0
theorem last_ofFn { n : ℕ } ( f : Fin n → α ) ( h : ofFn f ≠ [] )
( hn : n - 1 < n := Nat.pred_lt : ∀ {n : ℕ }, n ≠ 0 pred n < n <| ofFn_eq_nil_iff : ∀ {α : Type ?u.27282} {n : ℕ } {f : Fin n α ofFn f = [] ↔ n = 0 . not : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b . mp : ∀ {a b : Prop }, (a ↔ b a → b h ) :
getLast : {α : Type ?u.27380} → (as : List α as ≠ [] α ( ofFn f ) h = f ⟨ n - 1 , hn ⟩ := by simp [ getLast_eq_get ]
#align list.last_of_fn List.last_ofFn
theorem last_ofFn_succ { n : ℕ } ( f : Fin n . succ → α )
( h : ofFn f ≠ [] := mt : ∀ {a b : Prop }, (a → b ¬ b ¬ a ofFn_eq_nil_iff : ∀ {α : Type ?u.28933} {n : ℕ } {f : Fin n α ofFn f = [] ↔ n = 0 . mp : ∀ {a b : Prop }, (a ↔ b a → b ( Nat.succ_ne_zero : ∀ (n : ℕ ), succ n ≠ 0 _ )) :
getLast : {α : Type ?u.28962} → (as : List α as ≠ [] α ( ofFn f ) h = f ( Fin.last : (n : ℕ ) → Fin (n + 1 _ ) :=
last_ofFn f h
#align list.last_of_fn_succ List.last_ofFn_succ
/-- Note this matches the convention of `List.ofFn_succ'`, putting the `Fin m` elements first. -/
theorem ofFn_add { m n } ( f : Fin ( m + n ) → α ) :
List.ofFn : {α : Type ?u.29069} → {n : ℕ } → (Fin n α List α f =
( List.ofFn : {α : Type ?u.29079} → {n : ℕ } → (Fin n α List α fun i => f ( Fin.castAdd n i )) ++ List.ofFn : {α : Type ?u.29271} → {n : ℕ } → (Fin n α List α fun j => f ( Fin.natAdd m j ) := by
induction' n with n IH
· rw [ ofFn_zero : ∀ {α : Type ?u.29496} (f : Fin 0 α ofFn f = [] , append_nil : ∀ {α : Type ?u.29542} (as : List α as ++ [] = as , Fin.castAdd_zero , Fin.cast_refl ]
rfl
· rw [ ofFn_succ' , ofFn_succ' , IH , append_concat ]
rfl
#align list.of_fn_add List.ofFn_add
@[ simp ]
theorem ofFn_fin_append { m n } ( a : Fin m → α ) ( b : Fin n → α ) :
List.ofFn : {α : Type ?u.30122} → {n : ℕ } → (Fin n α List α ( Fin.append : {m n : ℕ } → {α : Type ?u.30125} → (Fin m α (Fin n α Fin (m + n α a b ) = List.ofFn : {α : Type ?u.30144} → {n : ℕ } → (Fin n α List α a ++ List.ofFn : {α : Type ?u.30150} → {n : ℕ } → (Fin n α List α b := by
simp_rw [ ofFn_add , Fin.append_left , Fin.append_right ]
#align list.of_fn_fin_append List.ofFn_fin_append
/-- This breaks a list of `m*n` items into `m` groups each containing `n` elements. -/
theorem ofFn_mul : ∀ {α : Type u} {m n : ℕ } (f : Fin (m * n α ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j isLt := (_ : ↑i * n + ↑j < m * n } ofFn_mul { m n } ( f : Fin ( m * n ) → α ) :
List.ofFn : {α : Type ?u.31190} → {n : ℕ } → (Fin n α List α f = List.join ( List.ofFn : {α : Type ?u.31199} → {n : ℕ } → (Fin n α List α fun i : Fin m => List.ofFn : {α : Type ?u.31205} → {n : ℕ } → (Fin n α List α fun j : Fin n => f ⟨ i * n + j ,
calc
↑ i * n + j < ( i + 1 ) * n := ( add_lt_add_left : ∀ {α : Type ?u.31939} [inst : Add α inst_1 : LT α inst_2 : CovariantClass α α (fun x x_1 => x + x_1 ) fun x x_1 => x < x_1 b c : α }, b < c ∀ (a : α ), a + b < a + c j . prop : ∀ {n : ℕ } (a : Fin n ↑a < n _ ). trans_eq : ∀ {α : Type ?u.32211} [inst : Preorder α a b c : α }, a < b b = c a < c trans_eq ( add_one_mul ( _ : ℕ ) _ ). symm : ∀ {α : Sort ?u.32320} {a b : α }, a = b b = a symm
_ ≤ _ := Nat.mul_le_mul_right : ∀ {n m : ℕ } (k : ℕ ), n ≤ m n * k ≤ m * k _ i . prop : ∀ {n : ℕ } (a : Fin n ↑a < n ⟩) := by
induction' m with m IH
· simp [ ofFn_zero : ∀ {α : Type ?u.32468} (f : Fin 0 α ofFn f = [] , zero_mul , ofFn_zero : ∀ {α : Type ?u.32495} (f : Fin 0 α ofFn f = [] , join ]
· simp_rw [ ofFn_succ' , succ_mul : ∀ (n m : ℕ ), succ n * m = n * m + m , join_concat , ofFn_add , IH ]
rfl
#align list.of_fn_mul List.ofFn_mul : ∀ {α : Type u} {m n : ℕ } (f : Fin (m * n α ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j isLt := (_ : ↑i * n + ↑j < m * n }
/-- This breaks a list of `m*n` items into `n` groups each containing `m` elements. -/
theorem ofFn_mul' : ∀ {m n : ℕ } (f : Fin (m * n α ofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j isLt := (_ : m * ↑i + ↑j < m * n } ofFn_mul' { m n } ( f : Fin ( m * n ) → α ) :
List.ofFn : {α : Type ?u.34758} → {n : ℕ } → (Fin n α List α f = List.join ( List.ofFn : {α : Type ?u.34767} → {n : ℕ } → (Fin n α List α fun i : Fin n => List.ofFn : {α : Type ?u.34773} → {n : ℕ } → (Fin n α List α fun j : Fin m => f ⟨ m * i + j ,
calc
m * i + j < m * ( i + 1 ) := ( add_lt_add_left : ∀ {α : Type ?u.35587} [inst : Add α inst_1 : LT α inst_2 : CovariantClass α α (fun x x_1 => x + x_1 ) fun x x_1 => x < x_1 b c : α }, b < c ∀ (a : α ), a + b < a + c j . prop : ∀ {n : ℕ } (a : Fin n ↑a < n _ ). trans_eq : ∀ {α : Type ?u.35859} [inst : Preorder α a b c : α }, a < b b = c a < c trans_eq ( mul_add_one ( _ : ℕ ) _ ). symm : ∀ {α : Sort ?u.35968} {a b : α }, a = b b = a symm
_ ≤ _ := Nat.mul_le_mul_left : ∀ {n m : ℕ } (k : ℕ ), n ≤ m k * n ≤ k * m _ i . prop : ∀ {n : ℕ } (a : Fin n ↑a < n ⟩) := by
simp_rw [ mul_comm m n , mul_comm m , ofFn_mul : ∀ {α : Type ?u.36693} {m n : ℕ } (f : Fin (m * n α ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j isLt := (_ : ↑i * n + ↑j < m * n } , Fin.cast_mk ]
#align list.of_fn_mul' List.ofFn_mul' : ∀ {α : Type u} {m n : ℕ } (f : Fin (m * n α ofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j isLt := (_ : m * ↑i + ↑j < m * n }
theorem ofFn_get : ∀ l : List α , ( ofFn ( get l )) = l
| [] => rfl : ∀ {α : Sort ?u.37221} {a : α }, a = a
| a :: l => by
rw [ ofFn_succ ]
congr
simp only [ Fin.val_succ ]
exact ofFn_get l
set_option linter.deprecated false in
@[ deprecated ofFn_get ]
theorem ofFn_nthLe : ∀ l : List α , ( ofFn fun i => nthLe l i i . 2 : ∀ {n : ℕ } (self : Fin n ↑self < n ) = l :=
ofFn_get
#align list.of_fn_nth_le List.ofFn_nthLe
-- not registered as a simp lemma, as otherwise it fires before `forall_mem_ofFn_iff` which
-- is much more useful
theorem mem_ofFn { n } ( f : Fin n → α ) ( a : α ) : a ∈ ofFn f ↔ a ∈ Set.range : {α : Type ?u.39492} → {ι : Sort ?u.39491} → (ι → α Set α f := by
simp only [ mem_iff_get : ∀ {α : Type ?u.39523} {a : α } {l : List α a ∈ l ↔ ∃ n , get l n = a , Set.mem_range : ∀ {α : Type ?u.39542} {ι : Sort ?u.39543} {f : ι → α x : α }, x ∈ Set.range f ↔ ∃ y , f y = x , get_ofFn ]
exact ⟨ fun ⟨ i , hi ⟩ => ⟨ Fin.cast ( by simp ) i , hi ⟩, fun ⟨ i , hi ⟩ => ⟨ Fin.cast ( by simp ) i , hi ⟩⟩
#align list.mem_of_fn List.mem_ofFn
@[ simp ]
theorem forall_mem_ofFn_iff : ∀ {α : Type u} {n : ℕ } {f : Fin n α P : α → Prop (∀ (