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) 2019 Seul Baek. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Seul Baek
! This file was ported from Lean 3 source module data.list.func
! leanprover-community/mathlib commit d11893b411025250c8e61ff2f12ccbd7ee35ab15
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Order.Basic
/-!
# Lists as Functions
Definitions for using lists as finite representations of finitely-supported functions with domain
ℕ.
These include pointwise operations on lists, as well as get and set operations.
## Notations
An index notation is introduced in this file for setting a particular element of a list. With `as`
as a list `m` as an index, and `a` as a new element, the notation is `as {m ↦ a}`.
So, for example
`[1, 3, 5] {1 ↦ 9}` would result in `[1, 9, 5]`
This notation is in the locale `list.func`.
-/
open List
universe u v w
variable { α : Type u } { β : Type v } { γ : Type w }
namespace List
namespace Func
variable { a : α }
variable { as as1 as2 as3 : List α }
/-- Elementwise negation of a list -/
def neg : [inst : Neg α (as : List α ?m.63 as neg [ Neg α ] ( as : List α ) :=
as . map fun a ↦ - a
#align list.func.neg List.Func.neg
variable [ Inhabited : Sort ?u.18210 → Sort (max1?u.18210) α ] [ Inhabited : Sort ?u.15708 → Sort (max1?u.15708) β ]
/-- Update element of a list by index. If the index is out of range, extend the list with default
elements
-/
@[ simp ]
def set ( a : α ) : List α → ℕ → List α
| _ :: as , 0 => a :: as
| [], 0 => [ a ]
| h :: as , k + 1 => h :: set a as k
| [], k + 1 => default :: set a ( [] : List α ) k
#align list.func.set List.Func.set
-- mathport name: list.func.set
@[inherit_doc]
scoped notation as " {" m " ↦ " a "}" => List.Func.set a as m
/-- Get element of a list by index. If the index is out of range, return the default element -/
@[ simp ]
def get : ℕ → List α → α
| _, [] => default
| 0 , a :: _ => a
| n + 1, _ :: as => get n as
#align list.func.get List.Func.get
/-- Pointwise equality of lists. If lists are different lengths, compare with the default
element.
-/
def Equiv ( as1 as2 : List α ) : Prop :=
∀ m : Nat , get m as1 = get m as2
#align list.func.equiv List.Func.Equiv
/-- Pointwise operations on lists. If lists are different lengths, use the default element. -/
@[ simp ]
def pointwise ( f : α → β → γ ) : List α → List β → List γ
| [], [] => []
| [], b :: bs => map ( f default ) ( b :: bs )
| a :: as , [] => map ( fun x ↦ f x default ) ( a :: as )
| a :: as , b :: bs => f a b :: pointwise f as bs
#align list.func.pointwise List.Func.pointwise
/-- Pointwise addition on lists. If lists are different lengths, use zero. -/
def add { α : Type u } [ Zero α ] [ Add α ] : List α → List α → List α :=
@ pointwise α α α ⟨ 0 ⟩ ⟨ 0 ⟩ (· + ·)
#align list.func.add List.Func.add
/-- Pointwise subtraction on lists. If lists are different lengths, use zero. -/
def sub { α : Type u } [ Zero α ] [ Sub α ] : List α → List α → List α :=
@ pointwise α α α ⟨ 0 ⟩ ⟨ 0 ⟩ (@ Sub.sub : {α : Type ?u.18126} → [self : Sub α α → α → α α _)
#align list.func.sub List.Func.sub
-- set
theorem length_set : ∀ { m : ℕ } { as : List α }, as { m ↦ a }. length = max : {α : Type ?u.18237} → [self : Max α α → α → α as . length ( m + 1 )
| 0 , [] => rfl : ∀ {α : Sort ?u.18350} {a : α }, a = a
| 0 , a :: as => by
rw [ max_eq_left ]
· rfl
· simp [ Nat.le_add_right : ∀ (n k : ℕ ), n ≤ n + k ]
exact Nat.succ_le_succ ( Nat.zero_le : ∀ (n : ℕ ), 0 ≤ n _ )
| m + 1, [] => by
have := @ length_set m []
simp [ set , length , @ length_set m , Nat.zero_max : ∀ {n : ℕ }, max 0 n = n ]
| m + 1, _ :: as => by
simp [ set , length , @ length_set m , Nat.max_succ_succ ]
#align list.func.length_set List.Func.length_set
-- porting note : @[simp] has been removed since `#lint` says this is
theorem get_nil : ∀ {k : ℕ }, get k [] = default get_nil { k : ℕ } : ( get k [] : α ) = default := by cases k <;> rfl
#align list.func.get_nil List.Func.get_nil
theorem get_eq_default_of_le : ∀ (k : ℕ ) {as : List α length as ≤ k get k as = default get_eq_default_of_le : ∀ ( k : ℕ ) { as : List α }, as . length ≤ k → get k as = default
| 0 , [], _ => rfl : ∀ {α : Sort ?u.24619} {a : α }, a = a
| 0 , a :: as , h1 => by cases h1
| k + 1, [], _ => rfl : ∀ {α : Sort ?u.24775} {a : α }, a = a
| k + 1, _ :: as , h1 => by
get (k + 1 head✝ :: as = default apply get_eq_default_of_le : ∀ (k : ℕ ) {as : List α length as ≤ k get k as = default get_eq_default_of_le k
get (k + 1 head✝ :: as = default rw [ ← Nat.succ_le_succ_iff ] ; get (k + 1 head✝ :: as = default apply h1
#align list.func.get_eq_default_of_le List.Func.get_eq_default_of_le
@[ simp ]
theorem get_set { a : α } : ∀ { k : ℕ } { as : List α }, get k ( as { k ↦ a }) = a
| 0 , as => by cases as <;> rfl
| k + 1, as => by cases as <;> simp [ get_set : ∀ {a : α } {k : ℕ } {as : List α get k (as { k ↦ a } = a get_set ]
#align list.func.get_set List.Func.get_set
theorem eq_get_of_mem : ∀ {a : α } {as : List α a ∈ as ∃ n , a = get n as eq_get_of_mem { a : α } : ∀ { as : List α }, a ∈ as → ∃ n : Nat , a = get n as
| [], h => by cases h
| b :: as , h => by
rw [ mem_cons : ∀ {α : Type ?u.26645} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l ] at h -- porting note : `mem_cons_iff` is now named `mem_cons`
cases h with
| inl : ∀ {a b : Prop }, a → a ∨ b h => exact ⟨ 0 , h ⟩
| inr : ∀ {a b : Prop }, b → a ∨ b h =>
rcases eq_get_of_mem : ∀ {a : α } {as : List α a ∈ as ∃ n , a = get n as eq_get_of_mem h with ⟨n, h⟩ : ∃ n , a = get n as n ⟨n, h⟩ : ∃ n , a = get n as h ⟨n, h⟩ : ∃ n , a = get n as
exact ⟨ n + 1 , h ⟩
#noalign list.func.eq_get_of_mem
-- porting note : the signature has been changed to correct what was presumably a bug,
-- hence the #noalign
theorem mem_get_of_le : ∀ { n : ℕ } { as : List α }, n < as . length → get n as ∈ as
| _, [], h1 => by cases h1
-- porting note : needed to add to `rw [mem_cons] here` in the two cases below
-- and in other lemmas (presumably because previously lean could see through the def of `mem` ?)
| 0 , a :: as , _ => by rw [ mem_cons : ∀ {α : Type ?u.27767} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l ] ; exact Or.inl : ∀ {a b : Prop }, a → a ∨ b rfl : ∀ {α : Sort ?u.27793} {a : α }, a = a
| n + 1, a :: as , h1 => by
rw [ mem_cons : ∀ {α : Type ?u.27812} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l ] ; apply Or.inr : ∀ {a b : Prop }, b → a ∨ b ; unfold get
apply mem_get_of_le
apply Nat.lt_of_succ_lt_succ h1
#align list.func.mem_get_of_le List.Func.mem_get_of_le
theorem mem_get_of_ne_zero : ∀ {n : ℕ } {as : List α get n as ≠ default get n as ∈ as mem_get_of_ne_zero : ∀ { n : ℕ } { as : List α }, get n as ≠ default → get n as ∈ as
| _, [], h1 => by exfalso ; apply h1 ; rw [ get_nil ]
| 0 , a :: as , _ => by rw [ mem_cons : ∀ {α : Type ?u.29774} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l ] ; exact Or.inl : ∀ {a b : Prop }, a → a ∨ b rfl : ∀ {α : Sort ?u.29800} {a : α }, a = a
| n + 1, a :: as , h1 : get (n + 1 a :: as ≠ default h1 => by
rw [ mem_cons : ∀ {α : Type ?u.29819} {a b : α } {l : List α a ∈ b :: l ↔ a = b ∨ a ∈ l ] ; unfold get
apply Or.inr : ∀ {a b : Prop }, b → a ∨ b ( mem_get_of_ne_zero : ∀ {n : ℕ } {as : List α get n as ≠ default get n as ∈ as mem_get_of_ne_zero _ : get ?m.29949 ?m.29950 ≠ default )
apply h1 : get (n + 1 a :: as ≠ default h1
#align list.func.mem_get_of_ne_zero List.Func.mem_get_of_ne_zero
theorem get_set_eq_of_ne { a : α } :
∀ { as : List α } ( k : ℕ ) ( m : ℕ ), m ≠ k → get m ( as { k ↦ a }) = get m as
| as , 0 , m , h1 => by
cases m
contradiction
cases as <;> simp only [ set , get , get_nil ]
| as , k + 1, m , h1 => by
-- porting note : I somewhat rearranged the case split
cases as <;> cases m
case nil =>
simp only [ set , get ]
case nil m =>
have h3 : get m ( nil { k ↦ a }) = default := by
rw [ get_set_eq_of_ne : ∀ {a : α } {as : List α k m : ℕ ), m ≠ k get m (as { k ↦ a } = get m as get_set_eq_of_ne k m , get_nil ]
intro hc
apply h1
simp [ hc ]
apply h3
case zero =>
simp only [ set , get ]
case _ _ m =>
apply get_set_eq_of_ne : ∀ {a : α } {as : List α k m : ℕ ), m ≠ k get m (as { k ↦ a } = get m as get_set_eq_of_ne k m
intro hc
apply h1
simp [ hc ]
#align list.func.get_set_eq_of_ne List.Func.get_set_eq_of_ne
theorem get_map { f : α → β } :
∀ { n : ℕ } { as : List α }, n < as . length → get n ( as . map f ) = f ( get n as )
| _, [], h => by cases h
| 0 , a :: as , _ => rfl : ∀ {α : Sort ?u.32888} {a : α }, a = a
| n + 1, _ :: as , h1 => by
have h2 : n < length as := by
rw [ ← Nat.succ_le_iff , ← Nat.lt_succ_iff ]
apply h1
apply get_map h2
#align list.func.get_map List.Func.get_map
theorem get_map' : ∀ {f : α → β n : ℕ } {as : List α f default = default get n (map f as = f (get n as get_map' { f : α → β } { n : ℕ } { as : List α } :
f default = default → get n ( as . map f ) = f ( get n as ) := by
intro h1 ; by_cases h2 : n < as . length
· apply get_map h2
· rw [ not_lt ] at h2
rw [ get_eq_default_of_le _ h2 , get_eq_default_of_le , h1 ]
rw [ length_map ]
apply h2
#align list.func.get_map' List.Func.get_map'
theorem forall_val_of_forall_mem : ∀ {α : Type u} [inst : Inhabited α as : List α p : α → Prop p default (∀ (x : α ), x ∈ as p x ) → ∀ (n : ℕ ), p (get n as forall_val_of_forall_mem { as : List α } { p : α → Prop } :
p default → (∀ x ∈ as , p x ) → ∀ n , p ( get n as ) := by
p default (∀ (x : α ), x ∈ as p x ) → ∀ (n : ℕ ), p (get n as intro h1 h2 : ∀ (x : α ), x ∈ as p x h2 n
p default (∀ (x : α ), x ∈ as p x ) → ∀ (n : ℕ ), p (get n as by_cases h3 : n < as . length
p default (∀ (x : α ), x ∈ as p x ) → ∀ (n : ℕ ), p (get n as · apply h2 : ∀ (x : α ), x ∈ as p x h2 _ ( mem_get_of_le h3 )
p default (∀ (x : α ), x ∈ as p x ) → ∀ (n : ℕ ), p (get n as · rw [ not_lt ] at h3
rw [