Commit 2021-12-18 19:21 9b4a2365

View on Github →

feat: porting Data.List.Defs, Init.Data.List.Basic (#137) This ports the files:

Init.Data.Option.{Basic, Instances}
Init.Data.List.{Basic, Instances, Lemmas}
Data.Option.{Basic, Defs}
Data.List.Defs nearly in their entirety; a few definitions were skipped for missing prerequisites.
length' and append' were removed, since they have been upstreamed
Nat.min is now simp-reduced in favor of min, and existing theorems restated using min
Function.injective now uses {{}} arguments

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

added theorem List.Pairwise_cons

deleted def List.append'

deleted theorem List.append'_eq_append

deleted theorem List.append_bind

added theorem List.append_eq_cons_iff

added theorem List.append_inj'

added theorem List.append_inj

added theorem List.append_inj_left'

added theorem List.append_inj_left

added theorem List.append_inj_right'

added theorem List.append_inj_right

added theorem List.append_left_cancel

added theorem List.append_left_inj

added theorem List.append_left_injective

added theorem List.append_right_cancel

added theorem List.append_right_inj

added theorem List.append_right_injective

deleted theorem List.ball_cons

deleted theorem List.ball_nil

deleted theorem List.bex_cons

deleted theorem List.concat_eq_append'

modified theorem List.concat_eq_append

deleted theorem List.cons_bind

added theorem List.cons_eq_append_iff

deleted theorem List.cons_subset_cons

deleted def List.count

deleted def List.countp

deleted def List.disjoint

deleted theorem List.drop_eq_nil_of_le'

modified theorem List.drop_eq_nil_of_le

deleted theorem List.eq_nil_of_length_eq_zero

added theorem List.eq_of_mem_repeat

deleted theorem List.eq_or_mem_of_mem_cons

deleted def List.eraseDup

modified theorem List.erase_subset

deleted def List.erasep

modified theorem List.erasep_subset

added theorem List.ext

added theorem List.ext_get

added theorem List.get?_append

added theorem List.get?_append_right

added theorem List.get?_concat_length

added theorem List.get?_eq_get

added theorem List.get?_eq_none_iff

added theorem List.get?_eq_some

added theorem List.get?_injective

added theorem List.get?_len_le

added theorem List.get?_map

added theorem List.get?_mem

added theorem List.get?_modifyNth

added theorem List.get?_modifyNth_eq

added theorem List.get?_modifyNth_ne

added theorem List.get?_of_mem

added theorem List.get?_set_eq

added theorem List.get?_set_ne

added theorem List.get?_set_of_lt

added theorem List.get?_zero

added theorem List.get_append

added theorem List.get_append_right

added theorem List.get_append_right_aux

added theorem List.get_cons_length

added theorem List.get_map'

added theorem List.get_map

added theorem List.get_map_rev

added theorem List.get_mem

added theorem List.get_of_eq

added theorem List.get_of_mem

added theorem List.get_repeat

added theorem List.get_set_eq

added theorem List.get_set_ne

added theorem List.get_singleton

added theorem List.get_zero

deleted def List.insert

modified theorem List.insert_of_mem

deleted def List.isInfix

deleted def List.isPrefix

deleted def List.isSuffix

modified theorem List.join_cons

modified theorem List.join_nil

added theorem List.last_append

added theorem List.last_concat

added theorem List.last_cons

added theorem List.last_eq_get

added theorem List.last_singleton

deleted def List.length'

deleted theorem List.length'_eq_length

deleted theorem List.length_map

deleted theorem List.length_repeat

deleted theorem List.map_append

deleted theorem List.map_cons

added theorem List.map_eq_append_split

deleted theorem List.map_id

deleted theorem List.map_map

deleted theorem List.map_nil

deleted theorem List.map_singleton

deleted def List.mem

deleted theorem List.mem_append

deleted theorem List.mem_append_eq

deleted theorem List.mem_append_left

deleted theorem List.mem_append_right

deleted theorem List.mem_cons

deleted theorem List.mem_cons_eq

deleted theorem List.mem_cons_iff

deleted theorem List.mem_cons_of_mem

deleted theorem List.mem_cons_self

modified theorem List.mem_erase_of_ne

added theorem List.mem_iff_get

added theorem List.mem_iff_get?

deleted theorem List.mem_nil

deleted theorem List.mem_nil_iff

added theorem List.mem_or_eq_of_mem_set

added theorem List.mem_repeat

added theorem List.modifyNthTail_id

added theorem List.modifyNthTail_length

added theorem List.modifyNth_eq_set

added theorem List.modify_get?_length

deleted theorem List.ne_nil_of_length_eq_succ

deleted theorem List.nil_bind

deleted theorem List.nil_subset

deleted def List.nodup

deleted theorem List.not_bex_nil

deleted theorem List.not_mem_nil

deleted inductive List.pairwise

deleted theorem List.pairwise_cons

deleted def List.product

modified theorem List.product_spec

deleted def List.pwFilter

added theorem List.removeNth_eq_nth_tail

deleted def List.repeat

modified theorem List.repeat_succ

added theorem List.set_comm

added theorem List.set_eq_modifyNth

added theorem List.set_nil

added theorem List.set_succ

deleted theorem List.subset.refl

deleted theorem List.subset.trans

deleted theorem List.subset_append_left

deleted theorem List.subset_append_right

deleted theorem List.subset_cons

deleted theorem List.subset_cons_of_subset

deleted theorem List.subset_of_cons_subset

added theorem List.take_append_drop

Modified Mathlib/Data/List/Defs.lean

added def List.Chain'

added inductive List.Chain

added inductive List.Forall₂

added def List.Nodup

added inductive List.Pairwise

added def List.allSome

added def List.count

added def List.countp

added def List.disjoint

added def List.eraseDup

added def List.erasep

added def List.extractp

added def List.fillNones

added def List.find

added def List.findIdxs

added def List.foldlIdx

added def List.foldlIdxAux

added def List.foldrIdx

added def List.foldrIdxAux

added def List.getRest

added def List.ilast'

added def List.indexesOf

added def List.indexesValues

added def List.inits

added def List.insertNth

added def List.isInfix

added def List.isPrefix

added def List.isSuffix

added def List.last'

added def List.lookmap

deleted def List.mapIdx

deleted def List.mapIdxM

added def List.mapWithComplement

added def List.mapWithPrefixSuffix

added def List.mapWithPrefixSuffixAux

added def List.map₂Left'

added def List.map₂Left

added def List.map₂Right'

added def List.map₂Right

added def List.mmap'

added def List.mmap'Diag

added def List.mmap

added def List.mmapFilter

added def List.mmapUpperTriangle

added def List.modifyHead

added def List.modifyLast

added def List.modifyNth

added def List.modifyNthTail

added def List.ofFn

added def List.ofFnAux

added def List.ofFnNthVal

added def List.partitionMap

added def List.product

added def List.pwFilter

added def List.range'

modified def List.reduceOption

added def List.revzip

added def List.rotate'

added def List.rotate

added def List.scanl

added def List.scanr

added def List.scanrAux

added def List.sections

added def List.slice

added def List.splitAt

added def List.splitOn

added def List.splitOnP

added def List.splitOnPAux

added def List.sublists'

added def List.sublists'Aux

added def List.sublists

added def List.sublistsAux

added def List.sublistsAux₁

added def List.tails

added def List.takeD

added def List.takeList

added def List.toChunks

added def List.toChunksAux

added def List.transpose

added def List.transposeAux

added def List.zipLeft'

added def List.zipLeft

added def List.zipRight'

added def List.zipRight

added def List.zipWith₃

added def List.zipWith₄

added def List.zipWith₅

Modified Mathlib/Data/Nat/Basic.lean

added theorem Nat.le_zero_iff

added theorem Nat.lt_succ_iff

added theorem Nat.succ_inj'

Created Mathlib/Data/Option/Basic.lean

added theorem Option.ball_ne_none

added theorem Option.bex_ne_none

added theorem Option.bind_assoc

added theorem Option.bind_comm

added theorem Option.bind_eq_none

added theorem Option.bind_eq_some

added theorem Option.bind_id_eq_join

added theorem Option.bind_map_comm

added theorem Option.bind_some

added theorem Option.choice_eq

added theorem Option.choice_isSome_iff_nonempty

added theorem Option.comp_map

added theorem Option.elim_none

added theorem Option.elim_some

added theorem Option.eq_none_iff_forall_not_mem

added theorem Option.eq_some_iff_get_eq

added theorem Option.ext

added theorem Option.getD_map

added theorem Option.getD_none

added theorem Option.getD_of_ne_none

added theorem Option.getD_some

added theorem Option.get_mem

added theorem Option.get_of_mem

added theorem Option.get_some

added theorem Option.guard_eq_some

added theorem Option.isNone_none

added theorem Option.isNone_some

added theorem Option.isSome_iff_exists

added theorem Option.isSome_none

added theorem Option.isSome_some

added theorem Option.join_eq_some

added theorem Option.join_join

added theorem Option.join_map_eq_map_join

added theorem Option.join_ne_none'

added theorem Option.join_ne_none

added theorem Option.lift_or_get_choice

added theorem Option.lift_or_get_none_left

added theorem Option.lift_or_get_none_right

added theorem Option.lift_or_get_some_some

added theorem Option.map_comp_map

added theorem Option.map_congr

added theorem Option.map_eq_map

added theorem Option.map_eq_none'

added theorem Option.map_eq_none

added theorem Option.map_eq_some'

added theorem Option.map_eq_some

added theorem Option.map_id'

added theorem Option.map_injective

added theorem Option.map_map

added theorem Option.map_none'

added theorem Option.map_none

added theorem Option.map_some'

added theorem Option.map_some

added theorem Option.mem_map_of_mem

added theorem Option.mem_of_mem_join

added theorem Option.mem_unique

added theorem Option.ne_none_iff_exists'

added theorem Option.ne_none_iff_exists

added theorem Option.ne_none_iff_isSome

added theorem Option.none_bind

added theorem Option.none_orelse

added theorem Option.not_isSome

added theorem Option.not_isSome_iff_eq_none

added theorem Option.not_mem_none

added theorem Option.orelse_none

added theorem Option.some_bind

added theorem Option.some_get

added theorem Option.some_injective

added theorem Option.some_ne_none

added theorem Option.some_orelse

added theorem Option.to_list_none

added theorem Option.to_list_some

Created Mathlib/Data/Option/Defs.lean

added def Option.decidable_eq_none

added def Option.guard

added theorem Option.isNone_iff_eq_none

added def Option.join

added def Option.lift_or_get

added def Option.maybe.{u,

added def Option.melim

added theorem Option.mem_def

added theorem Option.mem_iff

added theorem Option.mem_toList

added def Option.mgetD

added def Option.mmap.{u,

added def Option.pbind

added def Option.pmap

added inductive Option.rel

added theorem Option.some_inj

added def Option.toList

Modified Mathlib/Data/Prod.lean

Created Mathlib/Init/Data/List/Basic.lean

added def List.after

added def List.band

added def List.bor

added def List.findIdx

added def List.indexOf

added def List.insert

added def List.last!

added def List.last

added def List.mapIdx

added def List.mapIdxAux

added def List.mapIdxM

added def List.mem

added theorem List.mem_cons

added theorem List.mem_nil

added def List.removeNth

added def List.repeat

added def List.tail

Created Mathlib/Init/Data/List/Instances.lean

Created Mathlib/Init/Data/List/Lemmas.lean

added theorem List.append_bind

added theorem List.append_eq_append

added theorem List.ball_cons

added theorem List.ball_nil

added theorem List.bex_cons

added theorem List.cons_bind

added theorem List.cons_subset_cons

added theorem List.eq_nil_of_length_eq_zero

added theorem List.eq_or_mem_of_mem_cons

added theorem List.length_drop

added theorem List.length_le_of_sublist

added theorem List.length_map

added theorem List.length_map₂

added theorem List.length_removeNth

added theorem List.length_repeat

added theorem List.length_tail

added theorem List.length_take

added theorem List.length_take_le

added theorem List.map_append

added theorem List.map_cons

added theorem List.map_id

added theorem List.map_map

added theorem List.map_nil

added theorem List.map_singleton

added theorem List.mem_append

added theorem List.mem_append_eq

added theorem List.mem_append_left

added theorem List.mem_append_right

added theorem List.mem_cons_eq

added theorem List.mem_cons_of_mem

added theorem List.mem_cons_self

added theorem List.mem_nil_iff

added theorem List.ne_nil_of_length_eq_succ

added theorem List.nil_bind

added theorem List.nil_subset

added theorem List.not_bex_nil

added theorem List.not_mem_nil

added inductive List.sublist

added theorem List.subset.refl

added theorem List.subset.trans

added theorem List.subset_append_left

added theorem List.subset_append_right

added theorem List.subset_cons

added theorem List.subset_cons_of_subset

added theorem List.subset_of_cons_subset

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Created Mathlib/Init/Data/Option/Basic.lean

added def Option.get

Created Mathlib/Init/Data/Option/Instances.lean

Modified Mathlib/Init/Function.lean

modified def Function.injective

modified theorem Function.injective_id