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 .
import Mt.Utils.Fin
namespace Mt.Utils.List
theorem get_in { T : Type u } ( l : List : Type ?u.4 → Type ?u.4
T ) ( idx : Fin l . length : {α : Type ?u.7 } → List α Nat )
: ( l . get idx ) ∈ l := match l , idx with
| a :: _ , ⟨ 0 , _⟩ => List.Mem.head : ∀ {α : Type ?u.88 } (a : α ) (as : List α List.Mem a (a :: as a _
| _ :: as , ⟨ n + 1 , isLt ⟩ => List.Mem.tail _ <| get_in as ⟨ n , Nat.le_of_succ_le_succ isLt ⟩
theorem get_of_set { T : Type u } ( l : List : Type ?u.672 → Type ?u.672
T ) ( idx : Nat ) ( a : T )
( isLt : idx < ( l . set idx a ). length : {α : Type ?u.687 } → List α Nat length )
: ( l . set idx a ). get ⟨ idx , isLt ⟩ = a := match l , idx with
| _::_, 0 => rfl : ∀ {α : Sort ?u.784 } {a : α }, a = a
| _:: xs , n + 1 => get_of_set xs n a <| Nat.lt_of_succ_lt_succ isLt
theorem erase_subset { T : Type u } { a : T } ( l : List : Type ?u.1483 → Type ?u.1483
T ) ( idx : Nat )
: a ∈ ( l . eraseIdx idx ) → a ∈ l := match l , idx with
| [], _ => id : ∀ {α : Sort ?u.1545 }, α → α
| x :: xs , 0 => fun h => List.Mem.tail _ h
| x :: xs , n +1 => by
intro h ; cases h
. exact List.Mem.head : ∀ {α : Type ?u.2103 } (a : α ) (as : List α List.Mem a (a :: as ..
. exact List.Mem.tail x <| erase_subset xs n ( by assumption )
theorem set_subset : ∀ {T : Type u } {a : T } (l : List T idx : Nat ) (new_value : T ), a ∈ List.set l idx new_value a = new_value ∨ a ∈ l set_subset { T : Type u } { a : T } ( l : List : Type ?u.2325 → Type ?u.2325
T ) ( idx : Nat ) ( new_value : T )
: a ∈ ( l . set idx new_value ) → a = new_value ∨ a ∈ l := match l , idx with
| [], _ => Or.inr : ∀ {a b : Prop }, b → a ∨ b
| x :: xs , 0 => by
T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T intro h a = new_value ∨ a ∈ x :: xs T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T ; a = new_value ∨ a ∈ x :: xs T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T cases h head T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T tail a = new_value ∨ a ∈ x :: xs
T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T . head T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T tail a = new_value ∨ a ∈ x :: xs exact Or.inl : ∀ {a b : Prop }, a → a ∨ b rfl : ∀ {α : Sort ?u.2892 } {a : α }, a = a
T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T . T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T tail a = new_value ∨ a ∈ x :: xs T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T tail a = new_value ∨ a ∈ x :: xs exact Or.inr : ∀ {a b : Prop }, b → a ∨ b <| List.Mem.tail _ ( T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T tail a = new_value ∨ a ∈ x :: xs by T : Type u a : T l : List T idx : Nat new_value, x : T xs : List T assumption )
| x :: xs , n +1 => by
intro h a = new_value ∨ a ∈ x :: xs ; a = new_value ∨ a ∈ x :: xs cases h head a = new_value ∨ a ∈ a :: xs tail a = new_value ∨ a ∈ x :: xs
. head a = new_value ∨ a ∈ a :: xs head a = new_value ∨ a ∈ a :: xs tail a = new_value ∨ a ∈ x :: xs exact Or.inr : ∀ {a b : Prop }, b → a ∨ b <| List.Mem.head : ∀ {α : Type ?u.3159 } (a : α ) (as : List α List.Mem a (a :: as ..
. tail a = new_value ∨ a ∈ x :: xs tail a = new_value ∨ a ∈ x :: xs cases set_subset : ∀ {T : Type u } {a : T } (l : List T idx : Nat ) (new_value : T ), a ∈ List.set l idx new_value a = new_value ∨ a ∈ l set_subset xs n new_value ( tail a = new_value ∨ a ∈ x :: xs by assumption ) tail.inl a = new_value ∨ a ∈ x :: xs tail.inr a = new_value ∨ a ∈ x :: xs
tail a = new_value ∨ a ∈ x :: xs . tail.inl a = new_value ∨ a ∈ x :: xs tail.inl a = new_value ∨ a ∈ x :: xs tail.inr a = new_value ∨ a ∈ x :: xs exact Or.inl : ∀ {a b : Prop }, a → a ∨ b ( tail.inl a = new_value ∨ a ∈ x :: xs by assumption )
tail a = new_value ∨ a ∈ x :: xs . tail.inr a = new_value ∨ a ∈ x :: xs tail.inr a = new_value ∨ a ∈ x :: xs exact Or.inr : ∀ {a b : Prop }, b → a ∨ b <| List.Mem.tail _ ( tail.inr a = new_value ∨ a ∈ x :: xs by assumption )
theorem index_exists : ∀ {T : Type u } {a : T } (l : List T a ∈ l ∃ i , List.get l i = a index_exists { T : Type u } { a : T } ( l : List : Type ?u.3681 → Type ?u.3681
T )
: a ∈ l → ∃ i : Fin l . length : {α : Type ?u.3704 } → List α Nat , l . get i = a := fun a_in_l => match l , a_in_l with
| x :: xs , a_in_l => by
T : Type u a : T l : List T x : T xs : List T a_in_l : a ∈ x :: xs cases a_in_l T : Type u a : T l : List T a_in_l : a ∈ l xs : List T head T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail
T : Type u a : T l : List T x : T xs : List T a_in_l : a ∈ x :: xs . T : Type u a : T l : List T a_in_l : a ∈ l xs : List T head T : Type u a : T l : List T a_in_l : a ∈ l xs : List T head T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail exists ⟨ 0 , T : Type u a : T l : List T a_in_l : a ∈ l xs : List T head by T : Type u a : T l : List T a_in_l : a ∈ l xs : List T simp_arith ⟩
T : Type u a : T l : List T x : T xs : List T a_in_l : a ∈ x :: xs . T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail apply ( index_exists : ∀ {T : Type u } {a : T } (l : List T a ∈ l ∃ i , List.get l i = a index_exists xs ( T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail by T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T assumption )). elim : ∀ {α : Sort ?u.4577 } {p : α → Prop b : Prop }, (∃ x , p x ) → (∀ (a : α ), p a b ) → b
elim T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail
T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail intro i xs_get_i
T : Type u a : T l : List T a_in_l : a ∈ l x : T xs : List T tail exists ⟨ i . val + 1 , by simp_arith only [ List.length : {α : Type ?u.4777 } → List α Nat ] ; exact i . isLt : ∀ {n : Nat } (self : Fin n self .val< n ⟩
theorem erase_set { T : Type u } ( l : List : Type ?u.5691 → Type ?u.5691
T ) ( idx : Nat ) ( new_value : T )
: ( l . set idx new_value ). eraseIdx idx = l . eraseIdx idx := match l , idx with
| [], _ => rfl : ∀ {α : Sort ?u.5739 } {a : α }, a = a
| _::_, 0 => rfl : ∀ {α : Sort ?u.5796 } {a : α }, a = a
| x :: xs , n +1 => congrArg : ∀ {α : Sort ?u.5926 } {β : Sort ?u.5925 } {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ ( x :: .) <| erase_set xs n new_value
theorem eq_of_in_map : ∀ {U V : Type u } {f : U → V l : List U v : V }, v ∈ List.map f l ∃ u , u ∈ l ∧ v = f u eq_of_in_map { U V : Type u } { f : U -> V } { l : List : Type ?u.6207 → Type ?u.6207
U } { v : V }
: v ∈ ( l . map : {α : Type ?u.6219 } → {β : Type ?u.6218 } → (α → β List α List β f ) → ∃ u , u ∈ l ∧ v = f u := by
U, V : Type u f : U → V l : List U v : V intro v_in_map
U, V : Type u f : U → V l : List U v : V induction l U, V : Type u f : U → V v : V v_in_map : v ∈ List.map f [] nil U, V : Type u f : U → V v : V head✝ : U tail✝ : List U v_in_map : v ∈ List.map f (head✝ :: tail✝ cons ∃ u , u ∈ head✝ :: tail✝ ∧ v = f u
U, V : Type u f : U → V l : List U v : V . U, V : Type u f : U → V v : V v_in_map : v ∈ List.map f [] nil U, V : Type u f : U → V v : V v_in_map : v ∈ List.map f [] nil U, V : Type u f : U → V v : V head✝ : U tail✝ : List U v_in_map : v ∈ List.map f (head✝ :: tail✝ cons ∃ u , u ∈ head✝ :: tail✝ ∧ v = f u contradiction
U, V : Type u f : U → V l : List U v : V . U, V : Type u f : U → V v : V head✝ : U tail✝ : List U v_in_map : v ∈ List.map f (head✝ :: tail✝ cons ∃ u , u ∈ head✝ :: tail✝ ∧ v = f u U, V : Type u f : U → V v : V head✝ : U tail✝ : List U v_in_map : v ∈ List.map f (head✝ :: tail✝ cons ∃ u , u ∈ head✝ :: tail✝ ∧ v = f u rename_i head tail IH cons ∃ u , u ∈ head :: tail ∧ v = f u
U, V : Type u f : U → V v : V head✝ : U tail✝ : List U v_in_map : v ∈ List.map f (head✝ :: tail✝ cons ∃ u , u ∈ head✝ :: tail✝ ∧ v = f u cases v_in_map U, V : Type u f : U → V head : U tail : List U IH : f head ∈ List.map f tail ∃ u , u ∈ tail ∧ f head = f u cons.head ∃ u , u ∈ head :: tail ∧ f head = f u U, V : Type u f : U → V v : V head : U tail : List U IH : v ∈ List.map f tail ∃ u , u ∈ tail ∧ v = f u cons.tail ∃ u , u ∈ head :: tail ∧ v = f u
U, V : Type u f : U → V v : V head✝ : U tail✝ : List U v_in_map : v ∈ List.map f (head✝ :: tail✝ cons ∃ u , u ∈ head✝ :: tail✝ ∧ v = f u . U, V : Type u f : U → V head : U tail : List U IH : f head ∈ List.map f tail ∃ u , u ∈ tail ∧ f head = f u cons.head ∃ u , u ∈ head :: tail ∧ f head = f u U, V : Type u f : U → V head : U tail : List U IH : f head ∈ List.map f tail ∃ u , u ∈ tail ∧ f head = f u cons.head ∃ u , u ∈ head :: tail ∧ f head = f u U, V : Type u f : U → V v : V head : U tail : List U IH : v ∈ List.map f tail ∃ u , u ∈ tail ∧ v = f u cons.tail ∃ u , u ∈ head :: tail ∧ v = f u exact ⟨ head , List.Mem.head : ∀ {α : Type ?u.6695 } (a : α ) (as : List α List.Mem a (a :: as .., rfl : ∀ {α : Sort ?u.6699 } {a : α }, a = a ⟩
U, V : Type u f : U → V v : V head✝ : U tail✝ : List U v_in_map : v ∈ List.map f (head✝ :: tail✝ cons ∃ u , u ∈ head✝ :: tail✝ ∧ v = f u . U, V : Type u f : U → V v : V head : U tail : List U IH : v ∈ List.map f tail ∃ u , u ∈ tail ∧ v = f u cons.tail ∃ u , u ∈ head :: tail ∧ v = f u U, V : Type u f : U → V v : V head : U tail : List U IH : v ∈ List.map f tail ∃ u , u ∈ tail ∧ v = f u cons.tail ∃ u , u ∈ head :: tail ∧ v = f u rename_i v_in_map_of_tail cons.tail ∃ u , u ∈ head :: tail ∧ v = f u
U, V : Type u f : U → V v : V head : U tail : List U IH : v ∈ List.map f tail ∃ u , u ∈ tail ∧ v = f u cons.tail ∃ u , u ∈ head :: tail ∧ v = f u cases IH v_in_map_of_tail cons.tail.intro ∃ u , u ∈ head :: tail ∧ v = f u
U, V : Type u f : U → V v : V head : U tail : List U IH : v ∈ List.map f tail ∃ u , u ∈ tail ∧ v = f u cons.tail ∃ u , u ∈ head :: tail ∧ v = f u rename_i u u_hyp cons.tail.intro ∃ u , u ∈ head :: tail ∧ v = f u
U, V : Type u f : U → V v : V head : U tail : List U IH : v ∈ List.map f tail ∃ u , u ∈ tail ∧ v = f u cons.tail ∃ u , u ∈ head :: tail ∧ v = f u exact ⟨ u , List.Mem.tail _ u_hyp . left : ∀ {a b : Prop }, a ∧ b a , u_hyp . right : ∀ {a b : Prop }, a ∧ b b ⟩
theorem get_congr { T : Type u } { l l' : List : Type ?u.6901 → Type ?u.6901
T } ( idx : Fin l . length : {α : Type ?u.6904 } → List α Nat )
( eq : l = l' )
: l . get idx = l' . get ( Fin.cast idx ( congrArg : ∀ {α : Sort ?u.6930 } {β : Sort ?u.6929 } {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ _ eq )) := Eq.rec : ∀ {α : Sort ?u.6952 } {a : α } {motive : (a_1 : α ) → a = a_1 Sort ?u.6953 },
motive a (_ : a = a ∀ {a_1 : α } (t : a = a_1 motive a_1 t
(motive :=λ l' eq => l . get idx = l' . get ( Fin.cast idx ( congrArg : ∀ {α : Sort ?u.7042 } {β : Sort ?u.7041 } {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ _ eq )))
rfl : ∀ {α : Sort ?u.6991 } {a : α }, a = a eq
theorem get_congr' { T : Type u } { l l' : List : Type ?u.7065 → Type ?u.7065
T }
{ i : Fin l . length : {α : Type ?u.7068 } → List α Nat }
{ j : Fin l' . length : {α : Type ?u.7075 } → List α Nat }
( l_eq : l = l' )
( i_eq : i . val = j . val )
: l . get i = l' . get j := by
have : j = Fin.cast i ( congrArg : ∀ {α : Sort ?u.7119 } {β : Sort ?u.7118 } {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ _ l_eq ) := Fin.eq_of_val_eq : ∀ {n : Nat } {i j : Fin n i .val= j .vali = j i_eq . symm : ∀ {α : Sort ?u.7136 } {a b : α }, a = b b = a
rw [ this : j = Fin.cast i (_ : ?m.7124 ?m.7122 = ?m.7124 ?m.7123 this ]
exact get_congr _ l_eq
theorem get_of_map { U V : Type u } { f : U -> V } { l : List : Type ?u.7199 → Type ?u.7199
U }
{ idx : Fin ( l . map : {α : Type ?u.7203 } → {β : Type ?u.7202 } → (α → β List α List β f ). length : {α : Type ?u.7214 } → List α Nat length }
: ( l . map : {α : Type ?u.7222 } → {β : Type ?u.7221 } → (α → β List α List β f ). get idx = f ( l . get ( Fin.cast idx ( List.length_map l f ))) :=
match l , idx with
| head :: tail , ⟨ 0 , isLt ⟩ => rfl : ∀ {α : Sort ?u.7308 } {a : α }, a = a
| head :: tail , ⟨ n + 1 , isLt ⟩ => by
simp only [ List.map : {α : Type ?u.7822 } → {β : Type ?u.7821 } → (α → β List α List β , List.get ]
rw [ get_of_map ]
rfl
theorem set_map_commutes { U V : Type u } ( f : U -> V ) ( l : List : Type ?u.9080 → Type ?u.9080
U )
( idx : Nat ) ( new_val : U ) :
( l . set idx new_val ). map : {α : Type ?u.9096 } → {β : Type ?u.9095 } → (α → β List α List β map f = ( l . map : {α : Type ?u.9107 } → {β : Type ?u.9106 } → (α → β List α List β f ). set idx ( f new_val ) := by
U, V : Type u f : U → V l : List U idx : Nat new_val : U revert idx U, V : Type u f : U → V l : List U new_val : U
U, V : Type u f : U → V l : List U idx : Nat new_val : U induction l U, V : Type u f : U → V new_val : U
nil U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons
U, V : Type u f : U → V l : List U idx : Nat new_val : U . U, V : Type u f : U → V new_val : U
nil U, V : Type u f : U → V new_val : U
nil U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons intros U, V : Type u f : U → V new_val : U idx✝ : Nat nil U, V : Type u f : U → V new_val : U
nil U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons ; U, V : Type u f : U → V new_val : U idx✝ : Nat nil U, V : Type u f : U → V new_val : U
nil U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons rfl
U, V : Type u f : U → V l : List U idx : Nat new_val : U . U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons rename_i head tail IH
U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons intro idx
U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons cases idx
U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons . rfl
U, V : Type u f : U → V new_val, head✝ : U tail✝ : List U cons . simp only [ List.set : {α : Type ?u.9272 } → List α Nat → α → List α , List.map : {α : Type ?u.9989 } → {β : Type ?u.9988 } → (α → β List α List β ]
rename_i n
rw [ IH n ]
theorem erase_map_commutes { U V : Type u } ( f : U -> V ) ( l : List : Type ?u.10157 → Type ?u.10157
U )
( idx : Nat ) :
( l . eraseIdx idx ). map : {α : Type ?u.10170 } → {β : Type ?u.10169 } → (α → β List α List β map f = ( l . map : {α : Type ?u.10181 } → {β : Type ?u.10180 } → (α → β List α List β f ). eraseIdx idx := by
U, V : Type u f : U → V l : List U idx : Nat revert idx U, V : Type u f : U → V l : List U
U, V : Type u f : U → V l : List U idx : Nat induction l U, V : Type u f : U → V
nil U, V : Type u f : U → V head✝ : U tail✝ : List U cons
U, V : Type u f : U → V l : List U idx : Nat . U, V : Type u f : U → V
nil U, V : Type u f : U → V head✝ : U tail✝ : List U cons intros U, V : Type u f : U → V idx✝ : Nat nil U, V : Type u f : U → V
nil U, V : Type u f : U → V head✝ : U tail✝ : List U cons ; U, V : Type u f : U → V idx✝ : Nat nil U, V : Type u f : U → V
nil U, V : Type u f : U → V head✝ : U tail✝ : List U cons rfl
U, V : Type u f : U → V l : List U idx : Nat . U, V : Type u f : U → V head✝ : U tail✝ : List U cons U, V : Type u f : U → V head✝ : U tail✝ : List U cons rename_i head tail IH
U, V : Type u f : U → V head✝ : U tail✝ : List U cons intro idx
U, V : Type u f : U → V head✝ : U tail✝ : List U cons cases idx
U, V : Type u f : U → V head✝ : U tail✝ : List U cons . rfl
U, V : Type u f : U → V head✝ : U tail✝ : List U cons . simp only [ List.eraseIdx : {α : Type ?u.10351 } → List α Nat → List α , List.map : {α : Type ?u.10896 } → {β : Type ?u.10895 } → (α → β List α List β ]
rename_i n
rw [ IH n ]
end Mt.Utils.List