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, Sean Leather
! This file was ported from Lean 3 source module data.list.sigma
! leanprover-community/mathlib commit f808feb6c18afddb25e66a71d317643cf7fb5fbb
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.Range
import Mathlib.Data.List.Perm
/-!
# Utilities for lists of sigmas
This file includes several ways of interacting with `List (Sigma β)`, treated as a key-value store.
If `α : Type _` and `β : α → Type _`, then we regard `s : Sigma β` as having key `s.1 : α` and value
`s.2 : β s.1`. Hence, `List (Sigma β)` behaves like a key-value store.
## Main Definitions
- `List.keys` extracts the list of keys.
- `List.NodupKeys` determines if the store has duplicate keys.
- `List.lookup`/`lookup_all` accesses the value(s) of a particular key.
- `List.kreplace` replaces the first value with a given key by a given value.
- `List.kerase` removes a value.
- `List.kinsert` inserts a value.
- `List.kunion` computes the union of two stores.
- `List.kextract` returns a value with a given key and the rest of the values.
-/
universe u v
namespace List
variable { α : Type u } { β : α → Type v } { l l₁ l₂ : List ( Sigma : {α : Type ?u.60123} → (α → Type ?u.60122Type (max?u.60123?u.60122) β )}
/-! ### `keys` -/
/-- List of keys from a list of key-value pairs -/
def keys : List ( Sigma : {α : Type ?u.71} → (α → Type ?u.70Type (max?u.71?u.70) β ) → List α :=
map Sigma.fst
#align list.keys List.keys
@[ simp ]
theorem keys_nil : @ keys α β [] = [] :=
rfl : ∀ {α : Sort ?u.291} {a : α }, a = a
#align list.keys_nil List.keys_nil
@[ simp ]
theorem keys_cons { s } { l : List ( Sigma : {α : Type ?u.360} → (α → Type ?u.359Type (max?u.360?u.359) β )} : ( s :: l ). keys = s . 1 :: l . keys :=
rfl : ∀ {α : Sort ?u.404} {a : α }, a = a
#align list.keys_cons List.keys_cons
theorem mem_keys_of_mem { s : Sigma : {α : Type ?u.486} → (α → Type ?u.485Type (max?u.486?u.485) β } { l : List ( Sigma : {α : Type ?u.495} → (α → Type ?u.494Type (max?u.495?u.494) β )} : s ∈ l → s . 1 ∈ l . keys :=
mem_map_of_mem : ∀ {α : Type ?u.576} {β : Type ?u.577} {a : α } {l : List α f : α → β a ∈ l f a ∈ map f l Sigma.fst : {α : Type ?u.583} → {β : α → Type ?u.582Sigma β α
#align list.mem_keys_of_mem List.mem_keys_of_mem
theorem exists_of_mem_keys : ∀ {α : Type u} {β : α → Type va : α } {l : List (Sigma β a ∈ keys l ∃ b , { fst := a , snd := b } ∈ l exists_of_mem_keys { a } { l : List ( Sigma : {α : Type ?u.673} → (α → Type ?u.672Type (max?u.673?u.672) β )} ( h : a ∈ l . keys ) :
∃ b : β a , Sigma.mk : {α : Type ?u.731} → {β : α → Type ?u.730(fst : α ) → β fst Sigma β a b ∈ l :=
let ⟨⟨ _ , b' ⟩, m : { fst := fst✝ , snd := b' } ∈ l m , e : { fst := fst✝ , snd := b' } .fst= a e ⟩ := exists_of_mem_map : ∀ {α : Type ?u.750} {b : α } {α_1 : Type ?u.751} {f : α_1 → α l : List α_1 b ∈ map f l ∃ a , a ∈ l ∧ f a = b h
Eq.recOn : ∀ {α : Sort ?u.870} {a : α } {motive : (a_1 : α ) → a = a_1 Sort ?u.871 } {a_1 : α } (t : a = a_1 motive a (_ : a = a motive a_1 t e : { fst := fst✝ , snd := b' } .fst= a e ( Exists.intro : ∀ {α : Sort ?u.908} {p : α → Prop w : α ), p w Exists p b' m : { fst := fst✝ , snd := b' } ∈ l m )
#align list.exists_of_mem_keys List.exists_of_mem_keys : ∀ {α : Type u} {β : α → Type va : α } {l : List (Sigma β a ∈ keys l ∃ b , { fst := a , snd := b } ∈ l
theorem mem_keys { a } { l : List ( Sigma : {α : Type ?u.1120} → (α → Type ?u.1119Type (max?u.1120?u.1119) β )} : a ∈ l . keys ↔ ∃ b : β a , Sigma.mk : {α : Type ?u.1166} → {β : α → Type ?u.1165(fst : α ) → β fst Sigma β a b ∈ l :=
⟨ exists_of_mem_keys : ∀ {α : Type ?u.1193} {β : α → Type ?u.1192a : α } {l : List (Sigma β a ∈ keys l ∃ b , { fst := a , snd := b } ∈ l , fun ⟨_, h : { fst := a , snd := w✝ } ∈ l h ⟩ => mem_keys_of_mem h : { fst := a , snd := w✝ } ∈ l h ⟩
#align list.mem_keys List.mem_keys : ∀ {α : Type u} {β : α → Type va : α } {l : List (Sigma β a ∈ keys l ↔ ∃ b , { fst := a , snd := b } ∈ l
theorem not_mem_keys : ∀ {α : Type u} {β : α → Type va : α } {l : List (Sigma β ¬ a ∈ keys l ↔ ∀ (b : β a ¬ { fst := a , snd := b } ∈ l not_mem_keys { a } { l : List ( Sigma : {α : Type ?u.1395} → (α → Type ?u.1394Type (max?u.1395?u.1394) β )} : a ∉ l . keys ↔ ∀ b : β a , Sigma.mk : {α : Type ?u.1440} → {β : α → Type ?u.1439(fst : α ) → β fst Sigma β a b ∉ l :=
( not_congr : ∀ {a b : Prop }, (a ↔ b ¬ a ↔ ¬ b mem_keys : ∀ {α : Type ?u.1460} {β : α → Type ?u.1459a : α } {l : List (Sigma β a ∈ keys l ↔ ∃ b , { fst := a , snd := b } ∈ l ). trans : ∀ {a b c : Prop }, (a ↔ b (b ↔ c a ↔ c trans not_exists : ∀ {α : Sort ?u.1488} {p : α → Prop (¬ ∃ x , p x ↔ ∀ (x : α ), ¬ p x
#align list.not_mem_keys List.not_mem_keys : ∀ {α : Type u} {β : α → Type va : α } {l : List (Sigma β ¬ a ∈ keys l ↔ ∀ (b : β a ¬ { fst := a , snd := b } ∈ l
theorem not_eq_key { a } { l : List ( Sigma : {α : Type ?u.1544} → (α → Type ?u.1543Type (max?u.1544?u.1543) β )} : a ∉ l . keys ↔ ∀ s : Sigma : {α : Type ?u.1582} → (α → Type ?u.1581Type (max?u.1582?u.1581) β , s ∈ l → a ≠ s . 1 :=
Iff.intro : ∀ {a b : Prop }, (a → b (b → a a ↔ b ( fun h₁ s h₂ e => absurd : ∀ {a : Prop } {b : Sort ?u.1645}, a → ¬ a b ( mem_keys_of_mem h₂ ) ( by rwa [ e ] at h₁ )) fun f h₁ =>
let ⟨ b , h₂ : { fst := a , snd := b } ∈ l h₂ ⟩ := exists_of_mem_keys : ∀ {α : Type ?u.1682} {β : α → Type ?u.1681a : α } {l : List (Sigma β a ∈ keys l ∃ b , { fst := a , snd := b } ∈ l h₁
f _ h₂ : { fst := a , snd := b } ∈ l h₂ rfl : ∀ {α : Sort ?u.1738} {a : α }, a = a
#align list.not_eq_key List.not_eq_key
/-! ### `NodupKeys` -/
/-- Determines whether the store uses a key several times. -/
def NodupKeys ( l : List ( Sigma : {α : Type ?u.1895} → (α → Type ?u.1894Type (max?u.1895?u.1894) β )) : Prop :=
l . keys . Nodup
#align list.nodupkeys List.NodupKeys
theorem nodupKeys_iff_pairwise { l } : NodupKeys l ↔ Pairwise ( fun s s' : Sigma : {α : Type ?u.1982} → (α → Type ?u.1981Type (max?u.1982?u.1981) β => s . 1 ≠ s' . 1 ) l :=
pairwise_map
#align list.nodupkeys_iff_pairwise List.nodupKeys_iff_pairwise
theorem NodupKeys.pairwise_ne { l } ( h : NodupKeys l ) :
Pairwise ( fun s s' : Sigma : {α : Type ?u.2114} → (α → Type ?u.2113Type (max?u.2114?u.2113) β => s . 1 ≠ s' . 1 ) l :=
nodupKeys_iff_pairwise . 1 : ∀ {a b : Prop }, (a ↔ b a → b h
#align list.nodupkeys.pairwise_ne List.NodupKeys.pairwise_ne
@[ simp ]
theorem nodupKeys_nil : @ NodupKeys α β [] :=
Pairwise.nil
#align list.nodupkeys_nil List.nodupKeys_nil
@[ simp ]
theorem nodupKeys_cons { s : Sigma : {α : Type ?u.2292} → (α → Type ?u.2291Type (max?u.2292?u.2291) β } { l : List ( Sigma : {α : Type ?u.2301} → (α → Type ?u.2300Type (max?u.2301?u.2300) β )} :
NodupKeys ( s :: l ) ↔ s . 1 ∉ l . keys ∧ NodupKeys l := by simp [ keys , NodupKeys ]
#align list.nodupkeys_cons List.nodupKeys_cons
theorem not_mem_keys_of_nodupKeys_cons { s : Sigma : {α : Type ?u.10081} → (α → Type ?u.10080Type (max?u.10081?u.10080) β } { l : List ( Sigma : {α : Type ?u.10090} → (α → Type ?u.10089Type (max?u.10090?u.10089) β )} ( h : NodupKeys ( s :: l )) :
s . 1 ∉ l . keys :=
( nodupKeys_cons . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 1 : ∀ {a b : Prop }, a ∧ b a
#align list.not_mem_keys_of_nodupkeys_cons List.not_mem_keys_of_nodupKeys_cons
theorem nodupKeys_of_nodupKeys_cons { s : Sigma : {α : Type ?u.10213} → (α → Type ?u.10212Type (max?u.10213?u.10212) β } { l : List ( Sigma : {α : Type ?u.10222} → (α → Type ?u.10221Type (max?u.10222?u.10221) β )} ( h : NodupKeys ( s :: l )) :
NodupKeys l :=
( nodupKeys_cons . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 2 : ∀ {a b : Prop }, a ∧ b b
#align list.nodupkeys_of_nodupkeys_cons List.nodupKeys_of_nodupKeys_cons
theorem NodupKeys.eq_of_fst_eq { l : List ( Sigma : {α : Type ?u.10326} → (α → Type ?u.10325Type (max?u.10326?u.10325) β )} ( nd : NodupKeys l ) { s s' : Sigma : {α : Type ?u.10346} → (α → Type ?u.10345Type (max?u.10346?u.10345) β } ( h : s ∈ l )
( h' : s' ∈ l ) : s . 1 = s' . 1 → s = s' :=
@ Pairwise.forall_of_forall : ∀ {α : Type ?u.10430} {R : α → α → Prop l : List α Symmetric R (∀ (x : α ), x ∈ l R x x ) → Pairwise R l ∀ ⦃x : α ⦄, x ∈ l ∀ ⦃y : α ⦄, y ∈ l R x y _ ( fun s s' : Sigma : {α : Type ?u.10442} → (α → Type ?u.10441Type (max?u.10442?u.10441) β => s . 1 = s' . 1 → s = s' ) _
( fun _ _ H h => ( H h . symm : ∀ {α : Sort ?u.10487} {a b : α }, a = b b = a ). symm : ∀ {α : Sort ?u.10498} {a b : α }, a = b b = a symm ) ( fun _ _ _ => rfl : ∀ {α : Sort ?u.10526} {a : α }, a = a )
(( nodupKeys_iff_pairwise . 1 : ∀ {a b : Prop }, (a ↔ b a → b nd ). imp fun h h' => ( h h' ). elim ) _ h _ h'
#align list.nodupkeys.eq_of_fst_eq List.NodupKeys.eq_of_fst_eq
theorem NodupKeys.eq_of_mk_mem : ∀ {a : α } {b b' : β a l : List (Sigma β NodupKeys l { fst := a , snd := b } ∈ l { fst := a , snd := b' } ∈ l b = b' NodupKeys.eq_of_mk_mem { a : α } { b b' : β a } { l : List ( Sigma : {α : Type ?u.11663} → (α → Type ?u.11662Type (max?u.11663?u.11662) β )} ( nd : NodupKeys l )
( h : { fst := a , snd := b } ∈ l h : Sigma.mk : {α : Type ?u.11698} → {β : α → Type ?u.11697(fst : α ) → β fst Sigma β a b ∈ l ) ( h' : { fst := a , snd := b' } ∈ l h' : Sigma.mk : {α : Type ?u.11732} → {β : α → Type ?u.11731(fst : α ) → β fst Sigma β a b' ∈ l ) : b = b' := by
cases nd . eq_of_fst_eq h : { fst := a , snd := b } ∈ l h h' : { fst := a , snd := b' } ∈ l h' rfl : ∀ {α : Sort ?u.11776} {a : α }, a = a ; rfl
#align list.nodupkeys.eq_of_mk_mem List.NodupKeys.eq_of_mk_mem : ∀ {α : Type u} {β : α → Type va : α } {b b' : β a l : List (Sigma β NodupKeys l { fst := a , snd := b } ∈ l { fst := a , snd := b' } ∈ l b = b'
theorem nodupKeys_singleton ( s : Sigma : {α : Type ?u.11954} → (α → Type ?u.11953Type (max?u.11954?u.11953) β ) : NodupKeys [ s ] :=
nodup_singleton : ∀ {α : Type ?u.11982} (a : α ), Nodup [a ] _
#align list.nodupkeys_singleton List.nodupKeys_singleton
theorem NodupKeys.sublist { l₁ l₂ : List ( Sigma : {α : Type ?u.12048} → (α → Type ?u.12047Type (max?u.12048?u.12047) β )} ( h : l₁ <+ l₂ ) : NodupKeys l₂ → NodupKeys l₁ :=
Nodup.sublist <| h . map _
#align list.nodupkeys.sublist List.NodupKeys.sublist
protected theorem NodupKeys.nodup { l : List ( Sigma : {α : Type ?u.12193} → (α → Type ?u.12192Type (max?u.12193?u.12192) β )} : NodupKeys l → Nodup l :=
Nodup.of_map _
#align list.nodupkeys.nodup List.NodupKeys.nodup
theorem perm_nodupKeys { l₁ l₂ : List ( Sigma : {α : Type ?u.12293} → (α → Type ?u.12292Type (max?u.12293?u.12292) β )} ( h : l₁ ~ l₂ ) : NodupKeys l₁ ↔ NodupKeys l₂ :=
( h . map : ∀ {α : Type ?u.12339} {β : Type ?u.12338} (f : α → β l₁ l₂ : List α l₁ ~ l₂ map f l₁ ~ map f l₂ _ ). nodup_iff
#align list.perm_nodupkeys List.perm_nodupKeys
theorem nodupKeys_join { L : List ( List ( Sigma : {α : Type ?u.12438} → (α → Type ?u.12437Type (max?u.12438?u.12437) β ))} :
NodupKeys ( join L ) ↔ (∀ l ∈ L , NodupKeys l ) ∧ Pairwise Disjoint ( L . map keys ) := by
rw [ nodupKeys_iff_pairwise , pairwise_join , pairwise_map ]
refine' and_congr : ∀ {a c b d : Prop }, (a ↔ c (b ↔ d a ∧ b ↔ c ∧ d ( ball_congr : ∀ {α : Sort ?u.12662} {p : α → Prop P Q : (x : α ) → p x Prop },
(∀ (x : α ) (h : p x P x h ↔ Q x h ) → ((∀ (x : α ) (h : p x P x h ) ↔ ∀ (x : α ) (h : p x Q x h ) fun l _ => by simp [ nodupKeys_iff_pairwise ] ) _
apply iff_of_eq : ∀ {a b : Prop }, a = b a ↔ b ; congr with ( l₁ l₂ )
simp [ keys , disjoint_iff_ne : ∀ {α : Type ?u.13653} {l₁ l₂ : List α Disjoint l₁ l₂ ↔ ∀ (a : α ), a ∈ l₁ ∀ (b : α ), b ∈ l₂ a ≠ b ]
#align list.nodupkeys_join List.nodupKeys_join
theorem nodup_enum_map_fst ( l : List α ) : ( l . enum . map Prod.fst : {α : Type ?u.39937} → {β : Type ?u.39936} → α × β α ). Nodup := by simp [ List.nodup_range ]
#align list.nodup_enum_map_fst List.nodup_enum_map_fst
theorem mem_ext { l₀ l₁ : List ( Sigma : {α : Type ?u.40119} → (α → Type ?u.40118Type (max?u.40119?u.40118) β )} ( nd₀ : l₀ . Nodup ) ( nd₁ : l₁ . Nodup )
( h : ∀ x , x ∈ l₀ ↔ x ∈ l₁ ) : l₀ ~ l₁ :=
( perm_ext nd₀ nd₁ ). 2 : ∀ {a b : Prop }, (a ↔ b b → a h
#align list.mem_ext List.mem_ext
variable [ DecidableEq : Sort ?u.41095 → Sort (max1?u.41095) α ]
/-! ### `dlookup` -/
--Porting note: renaming to `dlookup` since `lookup` already exists
/-- `dlookup a l` is the first value in `l` corresponding to the key `a`,
or `none` if no such element exists. -/
def dlookup ( a : α ) : List ( Sigma : {α : Type ?u.40298} → (α → Type ?u.40297Type (max?u.40298?u.40297) β ) → Option ( β a )
| [] => none
| ⟨ a' , b ⟩ :: l => if h : a' = a then some ( Eq.recOn : {α : Sort ?u.40384} →
{a : α } →
{motive : (a_1 : α ) → a = a_1 Sort ?u.40385 } → {a_1 : α } → (t : a = a_1 motive a (_ : a = a motive a_1 t h b ) else dlookup a l
#align list.lookup List.dlookup
@[ simp ]
theorem dlookup_nil ( a : α ) : dlookup a [] = @ none ( β a ) :=
rfl : ∀ {α : Sort ?u.41010} {a : α }, a = a
#align list.lookup_nil List.dlookup_nil
@[ simp ]
theorem dlookup_cons_eq ( l ) ( a : α ) ( b : β a ) : dlookup a (⟨ a , b ⟩ :: l ) = some b :=
dif_pos rfl : ∀ {α : Sort ?u.41187} {a : α }, a = a
#align list.lookup_cons_eq List.dlookup_cons_eq
@[ simp ]
theorem dlookup_cons_ne ( l ) { a } : ∀ s : Sigma : {α : Type ?u.41328} → (α → Type ?u.41327Type (max?u.41328?u.41327) β , a ≠ s . 1 → dlookup a ( s :: l ) = dlookup a l
| ⟨_, _⟩, h : a ≠ { fst := fst✝ , snd := snd✝ } .fsth => dif_neg h : a ≠ { fst := fst✝ , snd := snd✝ } .fsth . symm : ∀ {α : Sort ?u.41478} {a b : α }, a ≠ b b ≠ a
#align list.lookup_cons_ne List.dlookup_cons_ne
theorem dlookup_isSome { a : α } : ∀ { l : List ( Sigma : {α : Type ?u.41723} → (α → Type ?u.41722Type (max?u.41723?u.41722) β )}, ( dlookup a l ). isSome ↔ a ∈ l . keys
| [] => by simp
| ⟨ a' , b ⟩ :: l => by
by_cases h : a = a'
· subst a'
simp
· simp [ h , dlookup_isSome ]
#align list.lookup_is_some List.dlookup_isSome
theorem dlookup_eq_none { a : α } { l : List ( Sigma : {α : Type ?u.50668} → (α → Type ?u.50667Type (max?u.50668?u.50667) β )} : dlookup a l = none ↔ a ∉ l . keys := by
simp [← dlookup_isSome , Option.isNone_iff_eq_none ]
#align list.lookup_eq_none List.dlookup_eq_none
theorem of_mem_dlookup { a : α } { b : β a } :
∀ { l : List ( Sigma : {α : Type ?u.51624} → (α → Type ?u.51623Type (max?u.51624?u.51623) β )}, b ∈ dlookup a l → Sigma.mk : {α : Type ?u.51723} → {β : α → Type ?u.51722(fst : α ) → β fst Sigma β a b ∈ l
| ⟨ a' , b' ⟩ :: l , H => by
{ fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l by_cases h : a = a' pos { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l neg { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l
{ fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l · pos { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l pos { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l neg { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l subst a' pos { fst := a , snd := b } ∈ { fst := a , snd := b' } :: l
pos { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l simp at H pos { fst := a , snd := b } ∈ { fst := a , snd := b' } :: l
pos { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l simp [ H ]
{ fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l · neg { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l neg { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l simp only [ ne_eq : ∀ {α : Sort ?u.55746} (a b : α ), (a ≠ b = ¬ a = b , h , not_false_iff , dlookup_cons_ne ] at H neg { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l
neg { fst := a , snd := b } ∈ { fst := a' , snd := b' } :: l simp [ of_mem_dlookup : ∀ {a : α } {b : β a l : List (Sigma β b ∈ dlookup a l { fst := a , snd := b } ∈ l of_mem_dlookup H ]
#align list.of_mem_lookup List.of_mem_dlookup
theorem mem_dlookup { a } { b : β a } { l : List ( Sigma : {α : Type ?u.59592} → (α → Type ?u.59591Type (max?u.59592?u.59591) β )} ( nd : l . NodupKeys ) ( h : { fst := a , snd := b } ∈ l h : Sigma.mk : {α : Type ?u.59629} → {β : α → Type ?u.59628(fst : α ) → β fst Sigma β a b ∈ l ) :
b ∈ dlookup a l := by
cases' Option.isSome_iff_exists . mp : ∀ {a b : Prop }, (a ↔ b a → b ( dlookup_isSome . mpr : ∀ {a b : Prop }, (a ↔ b b → a ( mem_keys_of_mem h : { fst := a , snd := b } ∈ l h )) with b' h'
cases nd . eq_of_mk_mem : ∀ {α : Type ?u.59891} {β : α → Type ?u.59890a : α } {b b' : β a l : List (Sigma β NodupKeys l { fst := a , snd := b } ∈ l { fst := a , snd := b' } ∈ l b = b' h : { fst := a , snd := b } ∈ l h ( of_mem_dlookup h' )
exact h'
#align list.mem_lookup List.mem_dlookup
theorem map_dlookup_eq_find ( a : α ) :
∀ l : List ( Sigma : {α : Type ?u.60162} → (α → Type ?u.60161Type (max?u.60162?u.60161) β ), ( dlookup a l ). map ( Sigma.mk : {α : Type ?u.60228} → {β : α → Type ?u.60227(fst : α ) → β fst Sigma β a ) = find? ( fun s => a = s . 1 ) l
| [] => rfl : ∀ {α : Sort ?u.60317} {a : α }, a = a
| ⟨ a' , b' ⟩ :: l => by
by_cases h : a = a'
· subst a'
simp
· simp [ h ]
exact map_dlookup_eq_find a l
#align list.map_lookup_eq_find List.map_dlookup_eq_find
theorem mem_dlookup_iff { a : α } { b : β a } { l : List ( Sigma : {α : Type ?u.62409} → (α → Type ?u.62408Type (max?u.62409?u.62408) β )} ( nd : l . NodupKeys ) :
b ∈ dlookup a l ↔ Sigma.mk : {α : Type ?u.62499} → {β : α → Type ?u.62498(fst : α ) → β fst Sigma β a b ∈ l :=
⟨ of_mem_dlookup , mem_dlookup nd ⟩
#align list.mem_lookup_iff List.mem_dlookup_iff
theorem perm_dlookup ( a : α ) { l₁ l₂ : List ( Sigma : {α : Type ?u.62762} → (α → Type ?u.62761Type (max?u.62762?u.62761) β )} ( nd₁ : l₁ . NodupKeys ) ( nd₂ : l₂ . NodupKeys )
( p : l₁ ~ l₂ ) : dlookup a l₁ = dlookup a l₂ := by
ext b ; simp only [ mem_dlookup_iff nd₁ , mem_dlookup_iff nd₂ ] a { fst := a , snd := b } ∈ l₁ ↔ { fst := a , snd := b } ∈ l₂ ; a { fst := a , snd := b } ∈ l₁ ↔ { fst := a , snd := b } ∈ l₂ exact p . mem_iff : ∀ {α : Type ?u.63174} {a : α } {l₁ l₂ : List α l₁ ~ l₂ a ∈ l₁ ↔ a ∈ l₂
#align list.perm_lookup List.perm_dlookup
theorem lookup_ext { l₀ l₁ : List ( Sigma : {α : Type ?u.63263} → (α → Type ?u.63262Type (max?u.63263?u.63262) β )} ( nd₀ : l₀ . NodupKeys ) ( nd₁ : l₁ . NodupKeys )
( h : ∀ x y , y ∈ l₀ . dlookup x ↔ y ∈ l₁ . dlookup x ) : l₀ ~ l₁ :=
mem_ext nd₀ . nodup nd₁ . nodup fun ⟨ a , b ⟩ => by
{ fst := a , snd := b } ∈ l₀ ↔ { fst := a , snd := b } ∈ l₁ rw [ { fst := a , snd := b } ∈ l₀ ↔ { fst := a , snd := b } ∈ l₁ ← mem_dlookup_iff , { fst := a , snd := b } ∈ l₀ ↔ { fst := a , snd := b } ∈ l₁ ← mem_dlookup_iff , { fst := a , snd := b } ∈ l₀ ↔ { fst := a , snd := b } ∈ l₁ h ] { fst := a , snd := b } ∈ l₀ ↔ { fst := a , snd := b } ∈ l₁ <;> { fst := a , snd := b } ∈ l₀ ↔ { fst := a , snd := b } ∈ l₁ assumption
#align list.lookup_ext List.lookup_ext
/-! ### `lookup_all` -/
/-- `lookup_all a l` is the list of all values in `l` corresponding to the key `a`. -/
def lookupAll ( a : α ) : List ( Sigma : {α : Type ?u.63955} → (α → Type ?u.63954Type (max?u.63955?u.63954) β ) → List ( β a )
| [] => []
| ⟨ a' , b ⟩ :: l => if h : a' = a then Eq.recOn : {α : Sort ?u.64041} →
{a : α } →
{motive : (a_1 : α ) → a = a_1 Sort ?u.64042 } → {a_1 : α } → (t : a = a_1 motive a (_ : a = a motive a_1 t h b :: lookupAll a l else lookupAll a l
#align list.lookup_all List.lookupAll
@[ simp ]
theorem lookupAll_nil ( a : α ) : lookupAll a [] = @ nil ( β a ) :=
rfl : ∀ {α : Sort ?u.64647} {a : α }, a = a
#align list.lookup_all_nil List.lookupAll_nil
@[ simp ]
theorem lookupAll_cons_eq ( l ) ( a : α ) ( b : β a ) : lookupAll a (⟨ a , b ⟩ :: l ) = b :: lookupAll a l :=
dif_pos rfl : ∀ {α : Sort ?u.64838} {a : α }, a = a
#align list.lookup_all_cons_eq List.lookupAll_cons_eq
@[ simp ]
theorem lookupAll_cons_ne ( l ) { a } : ∀ s : Sigma : {α : Type ?u.64980} → (α → Type ?u.64979Type (max?u.64980?u.64979) β , a ≠ s . 1 → lookupAll a ( s :: l ) = lookupAll a l
| ⟨_, _⟩, h : a ≠ { fst := fst✝ , snd := snd✝ } .fsth => dif_neg h : a ≠ { fst := fst✝ , snd := snd✝ } .fsth . symm : ∀ {α : Sort ?u.65130} {a b : α }, a ≠ b b ≠ a
#align list.lookup_all_cons_ne List.lookupAll_cons_ne
theorem lookupAll_eq_nil : ∀ {a : α } {l : List (Sigma β lookupAll a l = [] ↔ ∀ (b : β a ¬ { fst := a , snd := b } ∈ l lookupAll_eq_nil { a : α } :
∀ { l : List ( Sigma : {α : Type ?u.65362} → (α → Type ?u.65361Type (max?u.65362?u.65361) β )}, lookupAll a l = [] ↔ ∀ b : β a , Sigma.mk : {α : Type ?u.65459} → {β : α → Type ?u.65458(fst : α ) → β fst Sigma β a b ∉ l
| [] => by simp
| ⟨ a' , b ⟩ :: l => by
lookupAll a ({ fst := a' , snd := b } :: l = [] ↔ ∀ (b_1 : β a ¬ { fst := a , snd := b_1 } ∈ { fst := a' , snd := b } :: l by_cases h : a = a' pos lookupAll a ({ fst := a' , snd := b } :: l = [] ↔ ∀ (b_1 : β a ¬ { fst := a , snd := b_1 } ∈ { fst := a' , snd := b } :: l neg lookupAll a ({ fst := a' , snd := b } :: l = [] ↔ ∀ (b_1 : β a ¬ { fst := a , snd := b_1 } ∈ { fst := a' , snd := b } :: l
lookupAll a ({ fst := a' , snd := b } :: l = [] ↔ ∀ (b_1 : β a ¬ { fst := a , snd := b_1 } ∈ { fst := a' , snd := b } :: l · pos lookupAll a ({ fst := a' , snd := b } :: l = [] ↔ ∀ (b_1 : β a ¬ { fst := a ,