chore: Option cleanup (#7897)
This PR cleans up the `Option` development, upstreaming some results from mathlib in the process. Notable changes: - the name `<op>_eq_some_iff` is preferred over `<op>_eq_some` - the `simp` normal form for `<$>` is `Option.map`, for `>>=` is `Option.bind` and for `<|>` is `Option.orElse` (for the former two, this was already true before this PR). All further lemmas about these operations are now stated only in terms of `Option.map`/`Option.bind`/`Option.orElse`. Previously, in some cases both versions were available, with a prime used to disambiguate (the primed version was usually the "non-ascii-art" version). Now, there are no lemmas about the ascii-art versions besides the ones turning them into the non-ascii-art operations, and there is only one version of every lemma, about the non-ascii-art operation, and named without a prime.
This commit is contained in:
Markus Himmel
GitHub
parent
09ab15dc6d
commit
cf3b257ccd
16 changed files with 199 additions and 98 deletions
|
|
@ -477,7 +477,7 @@ theorem attach_filterMap {l : List α} {f : α → Option β} :
|
|||
· simp only [h]
|
||||
rfl
|
||||
rw [ih]
|
||||
simp only [map_filterMap, Option.map_pbind, Option.map_some']
|
||||
simp only [map_filterMap, Option.map_pbind, Option.map_some]
|
||||
rfl
|
||||
· simp only [Option.pbind_eq_some_iff] at h
|
||||
obtain ⟨a, h, w⟩ := h
|
||||
|
|
|
|||
|
|
@ -95,10 +95,10 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
|
|||
| cons x xs ih =>
|
||||
simp [guard, findSome?, find?]
|
||||
split <;> rename_i h
|
||||
· simp only [Option.guard_eq_some] at h
|
||||
· simp only [Option.guard_eq_some_iff] at h
|
||||
obtain ⟨rfl, h⟩ := h
|
||||
simp [h]
|
||||
· simp only [Option.guard_eq_none] at h
|
||||
· simp only [Option.guard_eq_none_iff] at h
|
||||
simp [ih, h]
|
||||
|
||||
theorem find?_eq_findSome?_guard {l : List α} : find? p l = findSome? (Option.guard fun x => p x) l :=
|
||||
|
|
@ -768,7 +768,7 @@ theorem findIdx?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {i : Nat}
|
|||
not_and, Classical.not_forall, Bool.not_eq_false]
|
||||
intros
|
||||
refine ⟨0, zero_lt_succ i, ‹_›⟩
|
||||
· simp only [Option.map_eq_some', ih, Bool.not_eq_true, length_cons]
|
||||
· simp only [Option.map_eq_some_iff, ih, Bool.not_eq_true, length_cons]
|
||||
constructor
|
||||
· rintro ⟨a, ⟨⟨h, h₁, h₂⟩, rfl⟩⟩
|
||||
refine ⟨Nat.succ_lt_succ_iff.mpr h, by simpa, fun j hj => ?_⟩
|
||||
|
|
@ -824,7 +824,7 @@ abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none
|
|||
(xs ++ ys : List α).findIdx? p =
|
||||
(xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.length) := by
|
||||
induction xs with simp
|
||||
| cons _ _ _ => split <;> simp_all [Option.map_or', Option.map_map]; rfl
|
||||
| cons _ _ _ => split <;> simp_all [Option.map_or, Option.map_map]; rfl
|
||||
|
||||
theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
|
||||
l.flatten.findIdx? p =
|
||||
|
|
|
|||
|
|
@ -339,7 +339,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
|
|||
if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]?
|
||||
| [], acc, i => by
|
||||
simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList,
|
||||
← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
|
||||
← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none]
|
||||
| a :: l, acc, i => by
|
||||
rw [mapIdx.go, getElem?_mapIdx_go]
|
||||
simp only [Array.size_push]
|
||||
|
|
|
|||
|
|
@ -141,11 +141,11 @@ theorem toList_attach (o : Option α) :
|
|||
cases o <;> simp
|
||||
|
||||
theorem attach_map {o : Option α} (f : α → β) :
|
||||
(o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some.2 ⟨_, h, rfl⟩⟩) := by
|
||||
(o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
|
||||
(o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some.2 ⟨_, h, rfl⟩))).map
|
||||
(o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some_iff.2 ⟨_, h, rfl⟩))).map
|
||||
fun ⟨x, h⟩ => ⟨f x, h⟩ := by
|
||||
cases o <;> simp
|
||||
|
||||
|
|
@ -174,7 +174,7 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o
|
|||
|
||||
theorem attach_bind {o : Option α} {f : α → Option β} :
|
||||
(o.bind f).attach =
|
||||
o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some.2 ⟨_, h, h'⟩⟩ := by
|
||||
o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some_iff.2 ⟨_, h, h'⟩⟩ := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
|
||||
|
|
|
|||
|
|
@ -231,13 +231,12 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
|
|||
@[simp] theorem getD_none : getD none a = a := rfl
|
||||
@[simp] theorem getD_some : getD (some a) b = a := rfl
|
||||
|
||||
@[simp] theorem map_none' (f : α → β) : none.map f = none := rfl
|
||||
@[simp] theorem map_some' (a) (f : α → β) : (some a).map f = some (f a) := rfl
|
||||
@[simp] theorem map_none (f : α → β) : none.map f = none := rfl
|
||||
@[simp] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl
|
||||
|
||||
@[simp] theorem none_bind (f : α → Option β) : none.bind f = none := rfl
|
||||
@[simp] theorem some_bind (a) (f : α → Option β) : (some a).bind f = f a := rfl
|
||||
|
||||
|
||||
/--
|
||||
A case analysis function for `Option`.
|
||||
|
||||
|
|
|
|||
|
|
@ -39,18 +39,24 @@ This is not an instance because it is not definitionally equal to the standard i
|
|||
|
||||
Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead.
|
||||
-/
|
||||
@[inline] def decidable_eq_none {o : Option α} : Decidable (o = none) :=
|
||||
@[inline] def decidableEqNone {o : Option α} : Decidable (o = none) :=
|
||||
decidable_of_decidable_of_iff isNone_iff_eq_none
|
||||
|
||||
instance {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∀ a, a ∈ o → p a)
|
||||
| none => isTrue nofun
|
||||
| some a =>
|
||||
if h : p a then isTrue fun _ e => some_inj.1 e ▸ h
|
||||
else isFalse <| mt (· _ rfl) h
|
||||
@[deprecated decidableEqNone (since := "2025-04-10"), inline]
|
||||
def decidable_eq_none {o : Option α} : Decidable (o = none) :=
|
||||
decidableEqNone
|
||||
|
||||
instance {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (Exists fun a => a ∈ o ∧ p a)
|
||||
| none => isFalse nofun
|
||||
| some a => if h : p a then isTrue ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ => h hn
|
||||
instance decidableForallMem {p : α → Prop} [DecidablePred p] :
|
||||
∀ o : Option α, Decidable (∀ a, a ∈ o → p a)
|
||||
| none => isTrue nofun
|
||||
| some a =>
|
||||
if h : p a then isTrue fun _ e => some_inj.1 e ▸ h
|
||||
else isFalse <| mt (· _ rfl) h
|
||||
|
||||
instance decidableExistsMem {p : α → Prop} [DecidablePred p] :
|
||||
∀ o : Option α, Decidable (Exists fun a => a ∈ o ∧ p a)
|
||||
| none => isFalse nofun
|
||||
| some a => if h : p a then isTrue ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ => h hn
|
||||
|
||||
/--
|
||||
Given an optional value and a function that can be applied when the value is `some`, returns the
|
||||
|
|
|
|||
|
|
@ -17,6 +17,8 @@ theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
|
|||
|
||||
theorem mem_some {a b : α} : a ∈ some b ↔ b = a := by simp
|
||||
|
||||
theorem mem_some_iff {a b : α} : a ∈ some b ↔ b = a := mem_some
|
||||
|
||||
theorem mem_some_self (a : α) : a ∈ some a := rfl
|
||||
|
||||
theorem some_ne_none (x : α) : some x ≠ none := nofun
|
||||
|
|
@ -29,6 +31,9 @@ protected theorem «exists» {p : Option α → Prop} :
|
|||
⟨fun | ⟨none, hx⟩ => .inl hx | ⟨some x, hx⟩ => .inr ⟨x, hx⟩,
|
||||
fun | .inl h => ⟨_, h⟩ | .inr ⟨_, hx⟩ => ⟨_, hx⟩⟩
|
||||
|
||||
theorem eq_none_or_eq_some (a : Option α) : a = none ∨ ∃ x, a = some x :=
|
||||
Option.exists.mp exists_eq'
|
||||
|
||||
theorem get_mem : ∀ {o : Option α} (h : isSome o), o.get h ∈ o
|
||||
| some _, _ => rfl
|
||||
|
||||
|
|
@ -88,6 +93,9 @@ set_option Elab.async false
|
|||
theorem eq_none_iff_forall_ne_some : o = none ↔ ∀ a, o ≠ some a := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem eq_none_iff_forall_some_ne : o = none ↔ ∀ a, some a ≠ o := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem eq_none_iff_forall_not_mem : o = none ↔ ∀ a, a ∉ o :=
|
||||
eq_none_iff_forall_ne_some
|
||||
|
||||
|
|
@ -102,9 +110,30 @@ theorem isSome_of_mem {x : Option α} {y : α} (h : y ∈ x) : x.isSome := by
|
|||
theorem isSome_of_eq_some {x : Option α} {y : α} (h : x = some y) : x.isSome := by
|
||||
cases x <;> trivial
|
||||
|
||||
@[simp] theorem not_isSome : isSome a = false ↔ a.isNone = true := by
|
||||
@[simp] theorem isSome_eq_false_iff : isSome a = false ↔ a.isNone = true := by
|
||||
cases a <;> simp
|
||||
|
||||
@[simp] theorem isNone_eq_false_iff : isNone a = false ↔ a.isSome = true := by
|
||||
cases a <;> simp
|
||||
|
||||
@[simp]
|
||||
theorem not_isSome (a : Option α) : (!a.isSome) = a.isNone := by
|
||||
cases a <;> simp
|
||||
|
||||
@[simp]
|
||||
theorem not_comp_isSome : (! ·) ∘ @Option.isSome α = Option.isNone := by
|
||||
funext
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
theorem not_isNone (a : Option α) : (!a.isNone) = a.isSome := by
|
||||
cases a <;> simp
|
||||
|
||||
@[simp]
|
||||
theorem not_comp_isNone : (!·) ∘ @Option.isNone α = Option.isSome := by
|
||||
funext x
|
||||
simp
|
||||
|
||||
theorem eq_some_iff_get_eq : o = some a ↔ ∃ h : o.isSome, o.get h = a := by
|
||||
cases o <;> simp
|
||||
|
||||
|
|
@ -146,17 +175,25 @@ abbrev ball_ne_none := @forall_ne_none
|
|||
|
||||
@[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl
|
||||
|
||||
@[simp] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
|
||||
|
||||
@[simp] theorem bind_some (x : Option α) : x.bind some = x := by cases x <;> rfl
|
||||
|
||||
@[simp] theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
|
||||
cases x <;> rfl
|
||||
|
||||
theorem bind_eq_some : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by
|
||||
theorem bind_eq_some_iff : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by
|
||||
cases x <;> simp
|
||||
|
||||
@[simp] theorem bind_eq_none {o : Option α} {f : α → Option β} :
|
||||
@[deprecated bind_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev bind_eq_some := @bind_eq_some_iff
|
||||
|
||||
@[simp] theorem bind_eq_none_iff {o : Option α} {f : α → Option β} :
|
||||
o.bind f = none ↔ ∀ a, o = some a → f a = none := by cases o <;> simp
|
||||
|
||||
@[deprecated bind_eq_none_iff (since := "2025-04-10")]
|
||||
abbrev bind_eq_none := @bind_eq_none_iff
|
||||
|
||||
theorem bind_eq_none' {o : Option α} {f : α → Option β} :
|
||||
o.bind f = none ↔ ∀ b a, o = some a → f a ≠ some b := by
|
||||
cases o <;> simp [eq_none_iff_forall_ne_some]
|
||||
|
|
@ -193,50 +230,67 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α →
|
|||
(isSome_apply_of_isSome_bind h) := by
|
||||
cases x <;> trivial
|
||||
|
||||
theorem join_eq_some : x.join = some a ↔ x = some (some a) := by
|
||||
simp [bind_eq_some]
|
||||
theorem join_eq_some_iff : x.join = some a ↔ x = some (some a) := by
|
||||
simp [bind_eq_some_iff]
|
||||
|
||||
@[deprecated join_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev join_eq_some := @join_eq_some_iff
|
||||
|
||||
theorem join_ne_none : x.join ≠ none ↔ ∃ z, x = some (some z) := by
|
||||
simp only [ne_none_iff_exists', join_eq_some, iff_self]
|
||||
simp only [ne_none_iff_exists', join_eq_some_iff, iff_self]
|
||||
|
||||
theorem join_ne_none' : ¬x.join = none ↔ ∃ z, x = some (some z) :=
|
||||
join_ne_none
|
||||
|
||||
theorem join_eq_none : o.join = none ↔ o = none ∨ o = some none :=
|
||||
theorem join_eq_none_iff : o.join = none ↔ o = none ∨ o = some none :=
|
||||
match o with | none | some none | some (some _) => by simp
|
||||
|
||||
@[deprecated join_eq_none_iff (since := "2025-04-10")]
|
||||
abbrev join_eq_none := @join_eq_none_iff
|
||||
|
||||
theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
|
||||
|
||||
@[simp] theorem map_eq_map : Functor.map f = Option.map f := rfl
|
||||
|
||||
theorem map_none : f <$> none = none := rfl
|
||||
@[deprecated map_none (since := "2025-04-10")]
|
||||
abbrev map_none' := @map_none
|
||||
|
||||
theorem map_some : f <$> some a = some (f a) := rfl
|
||||
@[deprecated map_some (since := "2025-04-10")]
|
||||
abbrev map_some' := @map_some
|
||||
|
||||
@[simp] theorem map_eq_some' : x.map f = some b ↔ ∃ a, x = some a ∧ f a = b := by cases x <;> simp
|
||||
|
||||
theorem map_eq_some : f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b := map_eq_some'
|
||||
|
||||
@[simp] theorem map_eq_none' : x.map f = none ↔ x = none := by
|
||||
cases x <;> simp [map_none', map_some', eq_self_iff_true]
|
||||
|
||||
theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by
|
||||
@[simp] theorem map_eq_some_iff : x.map f = some b ↔ ∃ a, x = some a ∧ f a = b := by
|
||||
cases x <;> simp
|
||||
|
||||
@[simp] theorem isSome_map' {x : Option α} : (x.map f).isSome = x.isSome := by
|
||||
@[deprecated map_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev map_eq_some := @map_eq_some_iff
|
||||
|
||||
@[deprecated map_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev map_eq_some' := @map_eq_some_iff
|
||||
|
||||
@[simp] theorem map_eq_none_iff : x.map f = none ↔ x = none := by
|
||||
cases x <;> simp [map_none, map_some, eq_self_iff_true]
|
||||
|
||||
@[deprecated map_eq_none_iff (since := "2025-04-10")]
|
||||
abbrev map_eq_none := @map_eq_none_iff
|
||||
|
||||
@[deprecated map_eq_none_iff (since := "2025-04-10")]
|
||||
abbrev map_eq_none' := @map_eq_none_iff
|
||||
|
||||
@[simp] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
|
||||
cases x <;> simp
|
||||
|
||||
@[simp] theorem isNone_map' {x : Option α} : (x.map f).isNone = x.isNone := by
|
||||
cases x <;> simp
|
||||
@[deprecated isSome_map (since := "2025-04-10")]
|
||||
abbrev isSome_map' := @isSome_map
|
||||
|
||||
theorem map_eq_none : f <$> x = none ↔ x = none := map_eq_none'
|
||||
@[simp] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by
|
||||
cases x <;> simp
|
||||
|
||||
theorem map_eq_bind {x : Option α} : x.map f = x.bind (some ∘ f) := by
|
||||
cases x <;> simp [Option.bind]
|
||||
|
||||
theorem map_congr {x : Option α} (h : ∀ a, x = some a → f a = g a) :
|
||||
x.map f = x.map g := by
|
||||
cases x <;> simp only [map_none', map_some', h]
|
||||
cases x <;> simp only [map_none, map_some, h]
|
||||
|
||||
@[simp] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
|
||||
funext; simp [map_id]
|
||||
|
|
@ -254,7 +308,7 @@ theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
|
|||
|
||||
@[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
|
||||
(x.map g).map h = x.map (h ∘ g) := by
|
||||
cases x <;> simp only [map_none', map_some', ·∘·]
|
||||
cases x <;> simp only [map_none, map_some, ·∘·]
|
||||
|
||||
theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ g) = (x.map g).map h :=
|
||||
(map_map ..).symm
|
||||
|
|
@ -262,7 +316,7 @@ theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘
|
|||
@[simp] theorem map_comp_map (f : α → β) (g : β → γ) :
|
||||
Option.map g ∘ Option.map f = Option.map (g ∘ f) := by funext x; simp
|
||||
|
||||
theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some' ..
|
||||
theorem mem_map_of_mem (g : α → β) (h : a ∈ x) : g a ∈ Option.map g x := h.symm ▸ map_some ..
|
||||
|
||||
theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y → x = y) :
|
||||
o.map f = o'.map f ↔ o = o' := by
|
||||
|
|
@ -292,11 +346,14 @@ theorem isSome_of_isSome_filter (p : α → Bool) (o : Option α) (h : (o.filter
|
|||
@[deprecated isSome_of_isSome_filter (since := "2025-03-18")]
|
||||
abbrev isSome_filter_of_isSome := @isSome_of_isSome_filter
|
||||
|
||||
@[simp] theorem filter_eq_none {o : Option α} {p : α → Bool} :
|
||||
@[simp] theorem filter_eq_none_iff {o : Option α} {p : α → Bool} :
|
||||
o.filter p = none ↔ ∀ a, o = some a → ¬ p a := by
|
||||
cases o <;> simp [filter_some]
|
||||
|
||||
@[simp] theorem filter_eq_some {o : Option α} {p : α → Bool} :
|
||||
@[deprecated filter_eq_none_iff (since := "2025-04-10")]
|
||||
abbrev filter_eq_none := @filter_eq_none_iff
|
||||
|
||||
@[simp] theorem filter_eq_some_iff {o : Option α} {p : α → Bool} :
|
||||
o.filter p = some a ↔ o = some a ∧ p a := by
|
||||
cases o with
|
||||
| none => simp
|
||||
|
|
@ -310,6 +367,9 @@ abbrev isSome_filter_of_isSome := @isSome_of_isSome_filter
|
|||
rintro rfl
|
||||
simpa using h
|
||||
|
||||
@[deprecated filter_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev filter_eq_some := @filter_eq_some_iff
|
||||
|
||||
theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
|
||||
a ∈ o.filter p ↔ a ∈ o ∧ p a := by
|
||||
simp
|
||||
|
|
@ -383,29 +443,43 @@ theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join)
|
|||
cases x <;> simp
|
||||
|
||||
theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a ∈ x.join) : some a ∈ x :=
|
||||
h.symm ▸ join_eq_some.1 h
|
||||
h.symm ▸ join_eq_some_iff.1 h
|
||||
|
||||
@[simp] theorem some_orElse (a : α) (x : Option α) : (some a <|> x) = some a := rfl
|
||||
@[simp] theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
|
||||
|
||||
@[simp] theorem none_orElse (x : Option α) : (none <|> x) = x := rfl
|
||||
@[simp] theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl
|
||||
|
||||
@[simp] theorem orElse_none (x : Option α) : (x <|> none) = x := by cases x <;> rfl
|
||||
@[simp] theorem orElse_none (x : Option α) : x.orElse (fun _ => none) = x := by cases x <;> rfl
|
||||
|
||||
theorem map_orElse {x y : Option α} : (x <|> y).map f = (x.map f <|> y.map f) := by
|
||||
theorem orElse_eq_some_iff (o : Option α) (f) (x : α) :
|
||||
(o.orElse f) = some x ↔ o = some x ∨ o = none ∧ f () = some x := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem orElse_eq_none_iff (o : Option α) (f) : (o.orElse f) = none ↔ o = none ∧ f () = none := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem map_orElse {x : Option α} {y} :
|
||||
(x.orElse y).map f = (x.map f).orElse (fun _ => (y ()).map f) := by
|
||||
cases x <;> simp
|
||||
|
||||
@[simp] theorem guard_eq_some [DecidablePred p] : guard p a = some b ↔ a = b ∧ p a :=
|
||||
@[simp] theorem guard_eq_some_iff [DecidablePred p] : guard p a = some b ↔ a = b ∧ p a :=
|
||||
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
|
||||
|
||||
@[deprecated guard_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev guard_eq_some := @guard_eq_some_iff
|
||||
|
||||
@[simp] theorem isSome_guard [DecidablePred p] : (Option.guard p a).isSome ↔ p a :=
|
||||
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
|
||||
|
||||
@[deprecated isSome_guard (since := "2025-03-18")]
|
||||
abbrev guard_isSome := @isSome_guard
|
||||
|
||||
@[simp] theorem guard_eq_none [DecidablePred p] : Option.guard p a = none ↔ ¬ p a :=
|
||||
@[simp] theorem guard_eq_none_iff [DecidablePred p] : Option.guard p a = none ↔ ¬ p a :=
|
||||
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
|
||||
|
||||
@[deprecated guard_eq_none_iff (since := "2025-04-10")]
|
||||
abbrev guard_eq_none := @guard_eq_none_iff
|
||||
|
||||
@[simp] theorem guard_pos [DecidablePred p] (h : p a) : Option.guard p a = some a := by
|
||||
simp [Option.guard, h]
|
||||
|
||||
|
|
@ -475,6 +549,22 @@ theorem liftOrGet_none_right {f} {a : Option α} : merge f a none = a :=
|
|||
theorem liftOrGet_some_some {f} {a b : α} : merge f (some a) (some b) = f a b :=
|
||||
merge_some_some
|
||||
|
||||
instance commutative_merge (f : α → α → α) [Std.Commutative f] :
|
||||
Std.Commutative (merge f) :=
|
||||
⟨fun a b ↦ by cases a <;> cases b <;> simp [merge, Std.Commutative.comm]⟩
|
||||
|
||||
instance associative_merge (f : α → α → α) [Std.Associative f] :
|
||||
Std.Associative (merge f) :=
|
||||
⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [merge, Std.Associative.assoc]⟩
|
||||
|
||||
instance idempotentOp_merge (f : α → α → α) [Std.IdempotentOp f] :
|
||||
Std.IdempotentOp (merge f) :=
|
||||
⟨fun a ↦ by cases a <;> simp [merge, Std.IdempotentOp.idempotent]⟩
|
||||
|
||||
instance lawfulIdentity_merge (f : α → α → α) : Std.LawfulIdentity (merge f) none where
|
||||
left_id a := by cases a <;> simp [merge]
|
||||
right_id a := by cases a <;> simp [merge]
|
||||
|
||||
@[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
|
||||
|
||||
@[simp] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
|
||||
|
|
@ -535,12 +625,18 @@ theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
|
|||
@[simp] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
|
||||
cases o <;> rfl
|
||||
|
||||
@[simp] theorem or_eq_none : or o o' = none ↔ o = none ∧ o' = none := by
|
||||
@[simp] theorem or_eq_none_iff : or o o' = none ↔ o = none ∧ o' = none := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp] theorem or_eq_some : or o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a) := by
|
||||
@[deprecated or_eq_none_iff (since := "2025-04-10")]
|
||||
abbrev or_eq_none := @or_eq_none_iff
|
||||
|
||||
@[simp] theorem or_eq_some_iff : or o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a) := by
|
||||
cases o <;> simp
|
||||
|
||||
@[deprecated or_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev or_eq_some := @or_eq_some_iff
|
||||
|
||||
theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
|
||||
cases o₁ <;> cases o₂ <;> rfl
|
||||
instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩
|
||||
|
|
@ -564,11 +660,11 @@ instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
|
|||
theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
|
||||
cases o <;> rfl
|
||||
|
||||
theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o') := by
|
||||
theorem map_or : (or o o').map f = (o.map f).or (o'.map f) := by
|
||||
cases o <;> rfl
|
||||
|
||||
theorem map_or' : (or o o').map f = (o.map f).or (o'.map f) := by
|
||||
cases o <;> rfl
|
||||
@[deprecated map_or (since := "2025-04-10")]
|
||||
abbrev map_or' := @map_or
|
||||
|
||||
theorem or_of_isSome {o o' : Option α} (h : o.isSome) : o.or o' = o := by
|
||||
match o, h with
|
||||
|
|
@ -804,7 +900,7 @@ theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H)
|
|||
|
||||
theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) :
|
||||
pmap g (o.map f) H =
|
||||
pmap (fun a h => g (f a) h) o (fun a m => H (f a) (map_eq_some.2 ⟨_, m, rfl⟩)) := by
|
||||
pmap (fun a h => g (f a) h) o (fun a m => H (f a) (map_eq_some_iff.2 ⟨_, m, rfl⟩)) := by
|
||||
cases o <;> simp
|
||||
|
||||
theorem pmap_pred_congr {α : Type u}
|
||||
|
|
|
|||
|
|
@ -1511,7 +1511,7 @@ theorem map_eq_iff {f : α → β} {as : Vector α n} {bs : Vector β n} :
|
|||
if h : i < as.size then
|
||||
simpa [h, h'] using w i h
|
||||
else
|
||||
rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega
|
||||
rw [getElem?_neg, getElem?_neg, Option.map_none] <;> omega
|
||||
|
||||
@[simp] theorem map_set {f : α → β} {xs : Vector α n} {i : Nat} {h : i < n} {a : α} :
|
||||
(xs.set i a).map f = (xs.map f).set i (f a) (by simpa using h) := by
|
||||
|
|
|
|||
|
|
@ -215,7 +215,7 @@ theorem modify_eq_alter [BEq α] [LawfulBEq α] {a : α} {f : β a → β a} {l
|
|||
modify a f l = alter a (·.map f) l := by
|
||||
induction l
|
||||
· rfl
|
||||
· next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih]
|
||||
· next ih => simp only [modify, beq_iff_eq, alter, Option.map_some, ih]
|
||||
|
||||
namespace Const
|
||||
|
||||
|
|
@ -235,7 +235,7 @@ theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : Ass
|
|||
modify a f l = alter a (·.map f) l := by
|
||||
induction l
|
||||
· rfl
|
||||
· next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih]
|
||||
· next ih => simp only [modify, beq_iff_eq, alter, Option.map_some, ih]
|
||||
|
||||
end Const
|
||||
|
||||
|
|
|
|||
|
|
@ -630,7 +630,7 @@ theorem Const.getThenInsertIfNew?_eq_insertIfNewₘ [BEq α] [Hashable α] (m :
|
|||
(a : α) (b : β) : (Const.getThenInsertIfNew? m a b).2 = m.insertIfNewₘ a b := by
|
||||
rw [getThenInsertIfNew?, insertIfNewₘ, containsₘ, bucket]
|
||||
dsimp only [Array.ugetElem_eq_getElem, Array.uset]
|
||||
split <;> simp_all [consₘ, updateBucket, List.containsKey_eq_isSome_getValue?, -Option.not_isSome]
|
||||
split <;> simp_all [consₘ, updateBucket, List.containsKey_eq_isSome_getValue?, -Option.isSome_eq_false_iff]
|
||||
|
||||
theorem Const.getThenInsertIfNew?_eq_get?ₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α)
|
||||
(b : β) : (Const.getThenInsertIfNew? m a b).1 = Const.get?ₘ m a := by
|
||||
|
|
|
|||
|
|
@ -964,7 +964,7 @@ theorem isHashSelf_filterMapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHasha
|
|||
IsHashSelf (m.filterMapₘ f).1.buckets := by
|
||||
refine h.buckets_hash_self.updateAllBuckets (fun l p hp => ?_)
|
||||
have hp := AssocList.toList_filterMap.mem_iff.1 hp
|
||||
simp only [mem_filterMap, Option.map_eq_some'] at hp
|
||||
simp only [mem_filterMap, Option.map_eq_some_iff] at hp
|
||||
obtain ⟨p, ⟨hkv, ⟨d, ⟨-, rfl⟩⟩⟩⟩ := hp
|
||||
exact containsKey_of_mem hkv
|
||||
|
||||
|
|
|
|||
|
|
@ -1031,7 +1031,7 @@ theorem ordered_filterMap [Ord α] {t : Impl α β} {h} {f : (a : α) → β a
|
|||
simp only [Ordered, toListModel_filterMap]
|
||||
apply ho.filterMap
|
||||
intro e f hef e' he' f' hf'
|
||||
simp only [Option.map_eq_some'] at he' hf'
|
||||
simp only [Option.map_eq_some_iff] at he' hf'
|
||||
obtain ⟨_, _, rfl⟩ := he'
|
||||
obtain ⟨_, _, rfl⟩ := hf'
|
||||
exact hef
|
||||
|
|
|
|||
|
|
@ -169,7 +169,7 @@ theorem getValue?_eq_getEntry? [BEq α] {l : List ((_ : α) × β)} {a : α} :
|
|||
· next k v l ih =>
|
||||
cases h : k == a
|
||||
· rw [getEntry?_cons_of_false h, getValue?_cons_of_false h, ih]
|
||||
· rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some']
|
||||
· rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some]
|
||||
|
||||
theorem getValue?_congr [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α}
|
||||
(h : a == b) : getValue? a l = getValue? b l := by
|
||||
|
|
@ -338,7 +338,7 @@ theorem getEntry?_eq_none [BEq α] {l : List ((a : α) × β a)} {a : α} :
|
|||
@[simp]
|
||||
theorem getValue?_eq_none {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
|
||||
getValue? a l = none ↔ containsKey a l = false := by
|
||||
rw [getValue?_eq_getEntry?, Option.map_eq_none', getEntry?_eq_none]
|
||||
rw [getValue?_eq_getEntry?, Option.map_eq_none_iff, getEntry?_eq_none]
|
||||
|
||||
theorem containsKey_eq_isSome_getValue? {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
|
||||
containsKey a l = (getValue? a l).isSome := by
|
||||
|
|
@ -613,7 +613,7 @@ theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} :
|
|||
· next k v l ih =>
|
||||
cases h : k == a
|
||||
· rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih]
|
||||
· rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some']
|
||||
· rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some]
|
||||
|
||||
theorem fst_mem_keys_of_mem [BEq α] [EquivBEq α] {a : (a : α) × β a} {l : List ((a : α) × β a)}
|
||||
(hm : a ∈ l) : a.1 ∈ keys l :=
|
||||
|
|
@ -1515,7 +1515,7 @@ theorem containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a
|
|||
cases h : k == a
|
||||
· simp
|
||||
· rw [containsKey_eq_isSome_getEntry?, getEntry?_congr h]
|
||||
simp
|
||||
simp [-Option.not_isSome]
|
||||
|
||||
theorem containsKey_insertEntryIfNew_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
|
||||
{v : β k} : containsKey k (insertEntryIfNew k v l) := by
|
||||
|
|
@ -2098,7 +2098,7 @@ theorem containsKey_append_of_not_contains_right [BEq α] {l l' : List ((a : α)
|
|||
@[simp]
|
||||
theorem getValue?_append {β : Type v} [BEq α] {l l' : List ((_ : α) × β)} {a : α} :
|
||||
getValue? a (l ++ l') = (getValue? a l).or (getValue? a l') := by
|
||||
simp [getValue?_eq_getEntry?, Option.map_or']
|
||||
simp [getValue?_eq_getEntry?, Option.map_or]
|
||||
|
||||
theorem getValue?_append_of_containsKey_eq_false {β : Type v} [BEq α] {l l' : List ((_ : α) × β)}
|
||||
{a : α} (h : containsKey a l' = false) : getValue? a (l ++ l') = getValue? a l := by
|
||||
|
|
@ -2233,7 +2233,7 @@ theorem mem_map_toProd_iff_mem {β : Type v} {k : α} {v : β} {l : List ((_ :
|
|||
theorem mem_iff_getValue?_eq_some [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β}
|
||||
{l : List ((_ : α) × β)} (h : DistinctKeys l) :
|
||||
⟨k, v⟩ ∈ l ↔ getValue? k l = some v := by
|
||||
simp only [mem_iff_getEntry?_eq_some h, getValue?_eq_getEntry?, Option.map_eq_some']
|
||||
simp only [mem_iff_getEntry?_eq_some h, getValue?_eq_getEntry?, Option.map_eq_some_iff]
|
||||
constructor
|
||||
· intro h
|
||||
exists ⟨k, v⟩
|
||||
|
|
@ -2256,7 +2256,7 @@ theorem find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some [BEq
|
|||
| nil => simp
|
||||
| cons hd tl ih =>
|
||||
simp only [List.map_cons, List.find?_cons_eq_some, Prod.mk.injEq, Bool.not_eq_eq_eq_not,
|
||||
Bool.not_true, Option.map_eq_some', getKey?, cond_eq_if, getValue?]
|
||||
Bool.not_true, Option.map_eq_some_iff, getKey?, cond_eq_if, getValue?]
|
||||
by_cases hdfst_k: hd.fst == k
|
||||
· simp only [hdfst_k, true_and, Bool.true_eq_false, false_and, or_false, ↓reduceIte,
|
||||
Option.some.injEq]
|
||||
|
|
@ -2271,7 +2271,7 @@ theorem mem_iff_getKey?_eq_some_and_getValue?_eq_some [BEq α] [EquivBEq α]
|
|||
theorem getValue?_eq_some_iff_exists_beq_and_mem_toList {β : Type v} [BEq α] [EquivBEq α]
|
||||
{l : List ((_ : α) × β)} {k: α} {v : β} (h : DistinctKeys l) :
|
||||
getValue? k l = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ l.map (fun x => (x.fst, x.snd)) := by
|
||||
simp only [getValue?_eq_getEntry?, Option.map_eq_some', ← mem_map_toProd_iff_mem,
|
||||
simp only [getValue?_eq_getEntry?, Option.map_eq_some_iff, ← mem_map_toProd_iff_mem,
|
||||
mem_iff_getEntry?_eq_some h]
|
||||
constructor
|
||||
· intro h'
|
||||
|
|
@ -2635,7 +2635,7 @@ theorem getKey?_insertList_of_mem [BEq α] [EquivBEq α]
|
|||
rcases List.mem_map.1 mem with ⟨⟨k, v⟩, pair_mem, rfl⟩
|
||||
rw [getKey?_eq_getEntry?, getEntry?_insertList distinct_l distinct_toInsert,
|
||||
getEntry?_of_mem (DistinctKeys.def.2 distinct_toInsert) k_beq pair_mem, Option.some_or,
|
||||
Option.map_some']
|
||||
Option.map_some]
|
||||
|
||||
theorem getKey_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
|
||||
{l toInsert : List ((a : α) × β a)} {k : α}
|
||||
|
|
@ -3074,7 +3074,7 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [B
|
|||
(h': containsKey k l = false) (h : toInsert.contains k = false) :
|
||||
getKey? k (insertListIfNewUnit l toInsert) = none := by
|
||||
rw [getKey?_eq_getEntry?,
|
||||
getEntry?_insertListIfNewUnit_of_contains_eq_false h, Option.map_eq_none', getEntry?_eq_none]
|
||||
getEntry?_insertListIfNewUnit_of_contains_eq_false h, Option.map_eq_none_iff, getEntry?_eq_none]
|
||||
exact h'
|
||||
|
||||
theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α]
|
||||
|
|
@ -3083,8 +3083,8 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivB
|
|||
(mem' : containsKey k l = false)
|
||||
(distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert) :
|
||||
getKey? k' (insertListIfNewUnit l toInsert) = some k := by
|
||||
simp only [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.map_eq_some',
|
||||
Option.or_eq_some, getEntry?_eq_none]
|
||||
simp only [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.map_eq_some_iff,
|
||||
Option.or_eq_some_iff, getEntry?_eq_none]
|
||||
exists ⟨k, ()⟩
|
||||
simp only [and_true]
|
||||
right
|
||||
|
|
@ -4301,8 +4301,8 @@ theorem minEntry?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
|||
theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minKey? l = some k ↔ getKey? k l = some k ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd]
|
||||
simp only [getKey?_eq_getEntry?, Option.map_eq_some', getEntry?_eq_some_iff hd]
|
||||
simp only [minKey?, Option.map_eq_some_iff, minEntry?_eq_some_iff _ hd]
|
||||
simp only [getKey?_eq_getEntry?, Option.map_eq_some_iff, getEntry?_eq_some_iff hd]
|
||||
apply Iff.intro
|
||||
· rintro ⟨_, ⟨hm, hcmp⟩, rfl⟩
|
||||
exact ⟨⟨_, ⟨BEq.refl, hm⟩, rfl⟩, hcmp⟩
|
||||
|
|
@ -4312,7 +4312,7 @@ theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [B
|
|||
theorem minKey?_eq_some_iff_mem_and_forall [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α]
|
||||
[LawfulBEqOrd α] {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minKey? l = some k ↔ containsKey k l ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd]
|
||||
simp only [minKey?, Option.map_eq_some_iff, minEntry?_eq_some_iff _ hd]
|
||||
apply Iff.intro
|
||||
· rintro ⟨_, ⟨hm, hcmp⟩, rfl⟩
|
||||
exact ⟨containsKey_of_mem hm, hcmp⟩
|
||||
|
|
@ -4361,7 +4361,7 @@ theorem isNone_minKey?_eq_isEmpty [Ord α] {l : List ((a : α) × β a)} :
|
|||
|
||||
theorem isSome_minEntry?_eq_not_isEmpty [Ord α] {l : List ((a : α) × β a)} :
|
||||
(minEntry? l).isSome = !l.isEmpty := by
|
||||
rw [← Bool.not_inj_iff, Bool.not_not, Bool.eq_iff_iff, Bool.not_eq_true', Option.not_isSome,
|
||||
rw [← Bool.not_inj_iff, Bool.not_not, Bool.eq_iff_iff, Bool.not_eq_true', Option.isSome_eq_false_iff,
|
||||
Option.isNone_iff_eq_none]
|
||||
apply minEntry?_eq_none_iff_isEmpty
|
||||
|
||||
|
|
@ -4384,7 +4384,7 @@ theorem minEntry?_map [Ord α] (l : List ((a : α) × β a)) (f : (a : α) × β
|
|||
simp only [minEntry?, List.min?]
|
||||
cases l <;> try rfl
|
||||
rename_i e es
|
||||
simp only [List.map_cons, Option.map_some', Option.some.injEq]
|
||||
simp only [List.map_cons, Option.map_some, Option.some.injEq]
|
||||
rw [← List.foldr_reverse, ← List.foldr_reverse, ← List.map_reverse]
|
||||
induction es.reverse with
|
||||
| nil => rfl
|
||||
|
|
@ -4442,7 +4442,7 @@ theorem minEntry?_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
|||
cases h : containsKey k l
|
||||
· simp only [cond_false, minEntry?_cons, Option.some.injEq]
|
||||
rfl
|
||||
· rw [cond_true, minEntry?_replaceEntry hl, Option.map_eq_some']
|
||||
· rw [cond_true, minEntry?_replaceEntry hl, Option.map_eq_some_iff]
|
||||
have := isSome_minEntry?_of_contains ‹_›
|
||||
simp only [Option.isSome_iff_exists] at this
|
||||
obtain ⟨a, ha⟩ := this
|
||||
|
|
@ -4538,7 +4538,7 @@ theorem minKey?_bind_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
|||
theorem containsKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)}
|
||||
(hd : DistinctKeys l) {km} (hkm : minKey? l = some km) :
|
||||
containsKey km l := by
|
||||
simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd] at hkm
|
||||
simp only [minKey?, Option.map_eq_some_iff, minEntry?_eq_some_iff _ hd] at hkm
|
||||
obtain ⟨e, ⟨hm, _⟩, rfl⟩ := hkm
|
||||
exact containsKey_of_mem hm
|
||||
|
||||
|
|
@ -4710,7 +4710,7 @@ theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
|
|||
minKey? (alterKey k f l) = some k ↔
|
||||
(f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.alterKey, getKey?_alterKey _ hd,
|
||||
beq_self_eq_true, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true, Option.not_isSome,
|
||||
beq_self_eq_true, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true, Option.isSome_eq_false_iff,
|
||||
Option.isNone_iff_eq_none, reduceCtorEq, imp_false, ← Option.isSome_iff_ne_none,
|
||||
containsKey_alterKey hd, beq_iff_eq, Bool.ite_eq_true_distrib, and_congr_right_iff]
|
||||
intro hf
|
||||
|
|
@ -4753,18 +4753,18 @@ theorem minKey?_modifyKey_eq_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqO
|
|||
simp only [minKey?_modifyKey hd]
|
||||
cases minKey? l
|
||||
· rfl
|
||||
· simp only [beq_iff_eq, Option.map_some', Option.some.injEq, ite_eq_right_iff]
|
||||
· simp only [beq_iff_eq, Option.map_some, Option.some.injEq, ite_eq_right_iff]
|
||||
exact Eq.symm
|
||||
|
||||
theorem isSome_minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
|
||||
{l : List ((_ : α) × β)} :
|
||||
(modifyKey k f l |> minKey?).isSome = !l.isEmpty := by
|
||||
simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
|
||||
simp [Option.isSome_map, isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
|
||||
|
||||
theorem isSome_minKey?_modifyKey_eq_isSome [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
|
||||
{l : List ((_ : α) × β)} :
|
||||
(modifyKey k f l |> minKey?).isSome = (minKey? l).isSome := by
|
||||
simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
|
||||
simp [Option.isSome_map, isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
|
||||
|
||||
theorem minKey?_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f km kmm}
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) (hkm : minKey? l = some km)
|
||||
|
|
@ -4784,7 +4784,7 @@ theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
|
|||
(f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.constAlterKey, getKey?_alterKey _ hd,
|
||||
← compare_eq_iff_beq, compare_self, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true,
|
||||
Option.not_isSome, Option.isNone_iff_eq_none, reduceCtorEq, imp_false,
|
||||
Option.isSome_eq_false_iff, Option.isNone_iff_eq_none, reduceCtorEq, imp_false,
|
||||
← Option.isSome_iff_ne_none, containsKey_alterKey hd, Bool.ite_eq_true_distrib,
|
||||
and_congr_right_iff]
|
||||
intro hf
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ theorem getElem!_of_getElem?' [Inhabited α] :
|
|||
∀ {l : List α} {i : Nat}, l[i]? = some b → l[i]! = b := by
|
||||
grind
|
||||
|
||||
attribute [local grind =] Option.map_some' Option.map_none' in
|
||||
attribute [local grind =] Option.map_some Option.map_none in
|
||||
attribute [local grind =] getElem?_map in
|
||||
attribute [local grind =] getElem?_replicate in
|
||||
theorem map_replicate' : (replicate n a).map f = replicate n (f a) := by
|
||||
|
|
|
|||
|
|
@ -318,20 +318,20 @@ example {α β} (f : α → β) (a : α) : ∃ a', f a' = f a := by
|
|||
|
||||
open List in
|
||||
example : (replicate n a).map f = replicate n (f a) := by
|
||||
grind +splitIndPred only [Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
|
||||
grind +splitIndPred only [Option.map_some, Option.map_none, getElem?_map, getElem?_replicate]
|
||||
|
||||
open List in
|
||||
example : (replicate n a).map f = replicate n (f a) := by
|
||||
grind only [cases Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
|
||||
grind only [cases Exists, Option.map_some, Option.map_none, getElem?_map, getElem?_replicate]
|
||||
|
||||
open List in
|
||||
example : (replicate n a).map f = replicate n (f a) := by
|
||||
grind only [cases Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
|
||||
grind only [cases Exists, Option.map_some, Option.map_none, getElem?_map, getElem?_replicate]
|
||||
|
||||
open List in
|
||||
example : (replicate n a).map f = replicate n (f a) := by
|
||||
-- Should fail since extensionality is disabled
|
||||
fail_if_success grind -ext only [Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
|
||||
fail_if_success grind -ext only [Option.map_some, Option.map_none, getElem?_map, getElem?_replicate]
|
||||
sorry
|
||||
|
||||
@[ext] structure S where
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ attribute [grind =] List.getElem?_eq_none
|
|||
attribute [grind =] List.getElem?_eq_some_iff
|
||||
attribute [grind =] getElem!_pos
|
||||
|
||||
attribute [grind =] Option.map_some' Option.map_none'
|
||||
attribute [grind =] Option.map_some Option.map_none
|
||||
attribute [grind =] List.getElem?_map
|
||||
attribute [grind =] List.getElem?_replicate
|
||||
|
||||
|
|
@ -33,8 +33,8 @@ example : 0 < (x :: t).length := by
|
|||
grind?
|
||||
|
||||
/--
|
||||
info: Try this: grind only [= List.getElem?_replicate, = List.getElem?_eq_some_iff, = List.getElem?_map, =
|
||||
List.getElem_replicate, = List.getElem?_eq_none, = Option.map_some', = Option.map_none', = List.length_replicate, →
|
||||
info: Try this: grind only [= Option.map_some, = Option.map_none, = List.getElem?_replicate, = List.getElem?_eq_some_iff, =
|
||||
List.getElem?_map, = List.getElem_replicate, = List.getElem?_eq_none, = List.length_replicate, →
|
||||
List.getElem?_eq_getElem, cases Or]
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue