feat: review of grind annotations for Option (#9863)
This PR reviews `grind` annotations for `Option`, preferring to use `@[grind =]` instead of `@[grind]` (and fixing a few problems revealed by this), and making sure `@[grind =]` theorems are "fully applied".
This commit is contained in:
Kim Morrison
GitHub
parent
49cd03bc29
commit
c8dae31ba5
3 changed files with 99 additions and 76 deletions
|
|
@ -58,9 +58,9 @@ theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.get
|
|||
theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b ↔ (o = some b ∨ o = none ∧ a = b) := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp, grind] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
|
||||
@[simp, grind =] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
|
||||
|
||||
@[simp, grind] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
|
||||
@[simp, grind =] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
|
||||
|
||||
theorem get_eq_get! [Inhabited α] : (o : Option α) → {h : o.isSome} → o.get h = o.get!
|
||||
| some _, _ => rfl
|
||||
|
|
@ -120,7 +120,7 @@ theorem isSome_of_eq_some {x : Option α} {y : α} (h : x = some y) : x.isSome :
|
|||
@[simp] theorem isNone_eq_false_iff : isNone a = false ↔ a.isSome = true := by
|
||||
cases a <;> simp
|
||||
|
||||
@[simp, grind]
|
||||
@[simp, grind =]
|
||||
theorem not_isSome (a : Option α) : (!a.isSome) = a.isNone := by
|
||||
cases a <;> simp
|
||||
|
||||
|
|
@ -129,7 +129,7 @@ theorem not_comp_isSome : (! ·) ∘ @Option.isSome α = Option.isNone := by
|
|||
funext
|
||||
simp
|
||||
|
||||
@[simp, grind]
|
||||
@[simp, grind =]
|
||||
theorem not_isNone (a : Option α) : (!a.isNone) = a.isSome := by
|
||||
cases a <;> simp
|
||||
|
||||
|
|
@ -191,11 +191,15 @@ theorem forall_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x)
|
|||
@[deprecated forall_ne_none (since := "2025-04-04")]
|
||||
abbrev ball_ne_none := @forall_ne_none
|
||||
|
||||
@[simp, grind] theorem pure_def : pure = @some α := rfl
|
||||
@[simp] theorem pure_def : pure = @some α := rfl
|
||||
|
||||
@[simp, grind] theorem bind_eq_bind : bind = @Option.bind α β := rfl
|
||||
@[grind =] theorem pure_apply : pure x = some x := rfl
|
||||
|
||||
@[simp, grind] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
|
||||
@[simp] theorem bind_eq_bind : bind = @Option.bind α β := rfl
|
||||
|
||||
@[grind =] theorem bind_apply : bind x f = Option.bind x f := rfl
|
||||
|
||||
@[simp, grind =] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
|
||||
|
||||
@[simp] theorem bind_fun_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
|
||||
cases x <;> rfl
|
||||
|
|
@ -216,7 +220,7 @@ 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]
|
||||
|
||||
@[grind] theorem mem_bind_iff {o : Option α} {f : α → Option β} :
|
||||
@[grind =] theorem mem_bind_iff {o : Option α} {f : α → Option β} :
|
||||
b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a := by
|
||||
cases o <;> simp
|
||||
|
||||
|
|
@ -224,7 +228,7 @@ theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β)
|
|||
(a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
|
||||
cases a <;> cases b <;> rfl
|
||||
|
||||
@[grind]
|
||||
@[grind =]
|
||||
theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) :
|
||||
(x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
|
||||
|
||||
|
|
@ -232,12 +236,12 @@ theorem bind_congr {α β} {o : Option α} {f g : α → Option β} :
|
|||
(h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by
|
||||
cases o <;> simp
|
||||
|
||||
@[grind]
|
||||
@[grind =]
|
||||
theorem isSome_bind {α β : Type _} (x : Option α) (f : α → Option β) :
|
||||
(x.bind f).isSome = x.any (fun x => (f x).isSome) := by
|
||||
cases x <;> rfl
|
||||
|
||||
@[grind]
|
||||
@[grind =]
|
||||
theorem isNone_bind {α β : Type _} (x : Option α) (f : α → Option β) :
|
||||
(x.bind f).isNone = x.all (fun x => (f x).isNone) := by
|
||||
cases x <;> rfl
|
||||
|
|
@ -250,7 +254,7 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α →
|
|||
(h : (x.bind f).isSome) : (f (x.get (isSome_of_isSome_bind h))).isSome := by
|
||||
cases x <;> trivial
|
||||
|
||||
@[simp, grind] theorem get_bind {α β : Type _} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome) :
|
||||
@[simp, grind =] theorem get_bind {α β : Type _} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome) :
|
||||
(x.bind f).get h = (f (x.get (isSome_of_isSome_bind h))).get
|
||||
(isSome_apply_of_isSome_bind h) := by
|
||||
cases x <;> trivial
|
||||
|
|
@ -263,7 +267,7 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α →
|
|||
(o.bind f).all p = o.all (Option.all p ∘ f) := by
|
||||
cases o <;> simp
|
||||
|
||||
@[grind] theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
|
||||
@[grind =] theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
|
||||
|
||||
theorem join_eq_some_iff : x.join = some a ↔ x = some (some a) := by
|
||||
simp [← bind_id_eq_join, bind_eq_some_iff]
|
||||
|
|
@ -287,7 +291,9 @@ theorem bind_join {f : α → Option β} {o : Option (Option α)} :
|
|||
o.join.bind f = o.bind (·.bind f) := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp, grind] theorem map_eq_map : Functor.map f = Option.map f := rfl
|
||||
@[simp] theorem map_eq_map : Functor.map f = Option.map f := rfl
|
||||
|
||||
@[grind =] theorem map_apply : Functor.map f x = Option.map f x := rfl
|
||||
|
||||
@[deprecated map_none (since := "2025-04-10")]
|
||||
abbrev map_none' := @map_none
|
||||
|
|
@ -313,13 +319,13 @@ 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, grind] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
|
||||
@[simp, grind =] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
|
||||
cases x <;> simp
|
||||
|
||||
@[deprecated isSome_map (since := "2025-04-10")]
|
||||
abbrev isSome_map' := @isSome_map
|
||||
|
||||
@[simp, grind] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by
|
||||
@[simp, grind =] 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
|
||||
|
|
@ -329,28 +335,32 @@ 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]
|
||||
|
||||
@[simp, grind] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
|
||||
@[simp] theorem map_id_fun {α : Type u} : Option.map (id : α → α) = id := by
|
||||
funext; simp [map_id]
|
||||
|
||||
@[grind =] theorem map_id_apply {α : Type u} {x : Option α} : Option.map (id : α → α) x = x := by simp
|
||||
|
||||
theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
|
||||
|
||||
@[simp, grind] theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id := by
|
||||
@[simp] theorem map_id_fun' {α : Type u} : Option.map (fun (a : α) => a) = id := by
|
||||
funext; simp [map_id']
|
||||
|
||||
@[simp, grind] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
|
||||
@[grind =] theorem map_id_apply' {α : Type u} {x : Option α} : Option.map (fun (a : α) => a) x = x := by simp
|
||||
|
||||
@[simp, grind =] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
|
||||
(o.map f).get h = f (o.get (by simpa using h)) := by
|
||||
cases o with
|
||||
| none => simp at h
|
||||
| some a => simp
|
||||
|
||||
@[simp, grind _=_] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
|
||||
@[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, ·∘·]
|
||||
|
||||
theorem comp_map (h : β → γ) (g : α → β) (x : Option α) : x.map (h ∘ g) = (x.map g).map h :=
|
||||
(map_map ..).symm
|
||||
|
||||
@[simp, grind _=_] theorem map_comp_map (f : α → β) (g : β → γ) :
|
||||
@[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 ..
|
||||
|
|
@ -372,9 +382,9 @@ theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y
|
|||
(if h : c then some (a h) else none).map f = if h : c then some (f (a h)) else none := by
|
||||
split <;> rfl
|
||||
|
||||
@[simp, grind] theorem filter_none (p : α → Bool) : none.filter p = none := rfl
|
||||
@[simp, grind =] theorem filter_none (p : α → Bool) : none.filter p = none := rfl
|
||||
|
||||
@[grind] theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
|
||||
@[grind =] theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
|
||||
|
||||
theorem filter_some_pos (h : p a) : Option.filter p (some a) = some a := by
|
||||
rw [filter_some, if_pos h]
|
||||
|
|
@ -417,12 +427,12 @@ theorem filter_some_eq_some : Option.filter p (some a) = some a ↔ p a := by si
|
|||
|
||||
theorem filter_some_eq_none : Option.filter p (some a) = none ↔ ¬p a := by simp
|
||||
|
||||
@[grind]
|
||||
@[grind =]
|
||||
theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
|
||||
a ∈ o.filter p ↔ a ∈ o ∧ p a := by
|
||||
simp
|
||||
|
||||
@[grind]
|
||||
@[grind =]
|
||||
theorem bind_guard (x : Option α) (p : α → Bool) :
|
||||
x.bind (Option.guard p) = x.filter p := by
|
||||
cases x <;> rfl
|
||||
|
|
@ -457,7 +467,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
|
|||
| false => by simp [filter_some_neg h, h]
|
||||
| true => by simp [filter_some_pos h, h]
|
||||
|
||||
@[simp, grind] theorem isSome_filter : Option.isSome (Option.filter p o) = Option.any p o :=
|
||||
@[simp, grind =] theorem isSome_filter : Option.isSome (Option.filter p o) = Option.any p o :=
|
||||
match o with
|
||||
| none => rfl
|
||||
| some a =>
|
||||
|
|
@ -536,12 +546,12 @@ theorem get_of_any_eq_true (p : α → Bool) (x : Option α) (h : x.any p = true
|
|||
p (x.get (isSome_of_any h)) :=
|
||||
any_eq_true_iff_get p x |>.1 h |>.2
|
||||
|
||||
@[grind]
|
||||
@[grind =]
|
||||
theorem any_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Bool} :
|
||||
(x.map f).any p = x.any (fun a => p (f a)) := by
|
||||
cases x <;> rfl
|
||||
|
||||
@[grind]
|
||||
@[grind =]
|
||||
theorem all_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Bool} :
|
||||
(x.map f).all p = x.all (fun a => p (f a)) := by
|
||||
cases x <;> rfl
|
||||
|
|
@ -549,13 +559,13 @@ theorem all_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Boo
|
|||
theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
|
||||
x.bind (Option.map f) = (x.map (Option.map f)).bind id := by cases x <;> simp
|
||||
|
||||
@[grind] theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
|
||||
@[grind =] theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
|
||||
(x.map f).bind g = x.bind (g ∘ f) := by cases x <;> simp
|
||||
|
||||
@[simp, grind] theorem map_bind {f : α → Option β} {g : β → γ} {x : Option α} :
|
||||
@[simp, grind =] theorem map_bind {f : α → Option β} {g : β → γ} {x : Option α} :
|
||||
(x.bind f).map g = x.bind (Option.map g ∘ f) := by cases x <;> simp
|
||||
|
||||
@[grind] theorem join_map_eq_map_join {f : α → β} {x : Option (Option α)} :
|
||||
@[grind =] theorem join_map_eq_map_join {f : α → β} {x : Option (Option α)} :
|
||||
(x.map (Option.map f)).join = x.join.map f := by cases x <;> simp
|
||||
|
||||
@[grind _=_] theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join).join := by
|
||||
|
|
@ -652,10 +662,11 @@ theorem get_none_eq_iff_true {h} : (none : Option α).get h = a ↔ True := by
|
|||
simp only [guard]
|
||||
split <;> simp
|
||||
|
||||
@[grind]
|
||||
theorem guard_def (p : α → Bool) :
|
||||
Option.guard p = fun x => if p x then some x else none := rfl
|
||||
|
||||
@[grind =] theorem guard_apply : Option.guard p x = if p x then some x else none := rfl
|
||||
|
||||
@[deprecated guard_def (since := "2025-05-15")]
|
||||
theorem guard_eq_map (p : α → Bool) :
|
||||
Option.guard p = fun x => Option.map (fun _ => x) (if p x then some x else none) := by
|
||||
|
|
@ -704,13 +715,13 @@ theorem merge_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b
|
|||
| none, some _ => .inr rfl
|
||||
| some a, some b => by have := h a b; simp [merge] at this ⊢; exact this
|
||||
|
||||
@[simp, grind] theorem merge_none_left {f} {b : Option α} : merge f none b = b := by
|
||||
@[simp, grind =] theorem merge_none_left {f} {b : Option α} : merge f none b = b := by
|
||||
cases b <;> rfl
|
||||
|
||||
@[simp, grind] theorem merge_none_right {f} {a : Option α} : merge f a none = a := by
|
||||
@[simp, grind =] theorem merge_none_right {f} {a : Option α} : merge f a none = a := by
|
||||
cases a <;> rfl
|
||||
|
||||
@[simp, grind] theorem merge_some_some {f} {a b : α} :
|
||||
@[simp, grind =] theorem merge_some_some {f} {a b : α} :
|
||||
merge f (some a) (some b) = some (f a b) := rfl
|
||||
|
||||
@[deprecated merge_eq_or_eq (since := "2025-04-04")]
|
||||
|
|
@ -784,9 +795,9 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
|
|||
(o.merge f o').get h = f (o.getD i) (o'.getD i) := by
|
||||
cases o <;> cases o' <;> simp [Std.LawfulLeftIdentity.left_id, Std.LawfulRightIdentity.right_id]
|
||||
|
||||
@[simp, grind] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
|
||||
@[simp, grind =] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
|
||||
|
||||
@[simp, grind] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
|
||||
@[simp, grind =] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
|
||||
|
||||
@[grind =] theorem elim_filter {o : Option α} {b : β} :
|
||||
Option.elim (Option.filter p o) b f = Option.elim o b (fun a => if p a then f a else b) :=
|
||||
|
|
@ -804,7 +815,8 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
|
|||
theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
|
||||
cases h : p a <;> simp [*, guard]
|
||||
|
||||
@[simp, grind] theorem getD_map (f : α → β) (x : α) (o : Option α) :
|
||||
-- I don't see how to construct a good grind pattern to instantiate this.
|
||||
@[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
|
||||
(o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
|
||||
|
||||
section choice
|
||||
|
|
@ -867,37 +879,37 @@ theorem get!_choice [Inhabited α] : (choice α).get! = (choice α).get isSome_c
|
|||
|
||||
end choice
|
||||
|
||||
@[simp, grind] theorem toList_some (a : α) : (some a).toList = [a] := rfl
|
||||
@[simp, grind] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
|
||||
@[simp, grind =] theorem toList_some (a : α) : (some a).toList = [a] := rfl
|
||||
@[simp, grind =] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
|
||||
|
||||
@[simp, grind] theorem toArray_some (a : α) : (some a).toArray = #[a] := rfl
|
||||
@[simp, grind] theorem toArray_none (α : Type _) : (none : Option α).toArray = #[] := rfl
|
||||
@[simp, grind =] theorem toArray_some (a : α) : (some a).toArray = #[a] := rfl
|
||||
@[simp, grind =] theorem toArray_none (α : Type _) : (none : Option α).toArray = #[] := rfl
|
||||
|
||||
-- See `Init.Data.Option.List` for lemmas about `toList`.
|
||||
|
||||
@[simp, grind] theorem some_or : (some a).or o = some a := rfl
|
||||
@[simp, grind] theorem none_or : none.or o = o := rfl
|
||||
@[simp, grind =] theorem some_or : (some a).or o = some a := rfl
|
||||
@[simp, grind =] theorem none_or : none.or o = o := rfl
|
||||
|
||||
theorem or_eq_right_of_none {o o' : Option α} (h : o = none) : o.or o' = o' := by
|
||||
cases h; simp
|
||||
|
||||
@[simp, grind] theorem or_some {o : Option α} : o.or (some a) = some (o.getD a) := by
|
||||
@[simp, grind =] theorem or_some {o : Option α} : o.or (some a) = some (o.getD a) := by
|
||||
cases o <;> rfl
|
||||
|
||||
@[deprecated or_some (since := "2025-05-03")]
|
||||
abbrev or_some' := @or_some
|
||||
|
||||
@[simp, grind]
|
||||
@[simp, grind =]
|
||||
theorem or_none : or o none = o := by
|
||||
cases o <;> rfl
|
||||
|
||||
theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
|
||||
cases o <;> rfl
|
||||
|
||||
@[simp, grind] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
|
||||
@[simp, grind =] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
|
||||
cases o <;> rfl
|
||||
|
||||
@[simp, grind] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
|
||||
@[simp, grind =] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
|
||||
cases o <;> rfl
|
||||
|
||||
@[simp] theorem or_eq_none_iff : or o o' = none ↔ o = none ∧ o' = none := by
|
||||
|
|
@ -912,7 +924,7 @@ abbrev or_eq_none := @or_eq_none_iff
|
|||
@[deprecated or_eq_some_iff (since := "2025-04-10")]
|
||||
abbrev or_eq_some := @or_eq_some_iff
|
||||
|
||||
@[grind] theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
|
||||
@[grind _=_] 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 _⟩
|
||||
|
||||
|
|
@ -923,7 +935,7 @@ instance : Std.LawfulIdentity (or (α := α)) none where
|
|||
left_id := @none_or _
|
||||
right_id := @or_none _
|
||||
|
||||
@[simp, grind]
|
||||
@[simp, grind =]
|
||||
theorem or_self : or o o = o := by
|
||||
cases o <;> rfl
|
||||
instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
|
||||
|
|
@ -962,13 +974,15 @@ theorem guard_or_guard : (guard p a).or (guard q a) = guard (fun x => p x || q x
|
|||
/-! ### `orElse` -/
|
||||
|
||||
/-- The `simp` normal form of `o <|> o'` is `o.or o'` via `orElse_eq_orElse` and `orElse_eq_or`. -/
|
||||
@[simp, grind] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
|
||||
@[simp] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
|
||||
|
||||
@[grind =] theorem orElse_apply : HOrElse.hOrElse o o' = Option.orElse o o' := rfl
|
||||
|
||||
theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
|
||||
cases o <;> rfl
|
||||
|
||||
/-- The `simp` normal form of `o.orElse f` is o.or (f ())`. -/
|
||||
@[simp, grind] theorem orElse_eq_or {o : Option α} {f} : o.orElse f = o.or (f ()) := by
|
||||
@[simp, grind =] theorem orElse_eq_or {o : Option α} {f} : o.orElse f = o.or (f ()) := by
|
||||
simp [or_eq_orElse]
|
||||
|
||||
@[deprecated or_some (since := "2025-05-03")]
|
||||
|
|
@ -1001,13 +1015,13 @@ section beq
|
|||
|
||||
variable [BEq α]
|
||||
|
||||
@[simp, grind] theorem none_beq_none : ((none : Option α) == none) = true := rfl
|
||||
@[simp, grind] theorem none_beq_some (a : α) : ((none : Option α) == some a) = false := rfl
|
||||
@[simp, grind] theorem some_beq_none (a : α) : ((some a : Option α) == none) = false := rfl
|
||||
@[simp, grind] theorem some_beq_some {a b : α} : (some a == some b) = (a == b) := rfl
|
||||
@[simp, grind =] theorem none_beq_none : ((none : Option α) == none) = true := rfl
|
||||
@[simp, grind =] theorem none_beq_some (a : α) : ((none : Option α) == some a) = false := rfl
|
||||
@[simp, grind =] theorem some_beq_none (a : α) : ((some a : Option α) == none) = false := rfl
|
||||
@[simp, grind =] theorem some_beq_some {a b : α} : (some a == some b) = (a == b) := rfl
|
||||
|
||||
/-- We simplify away `isEqSome` in terms of `==`. -/
|
||||
@[simp, grind] theorem isEqSome_eq_beq_some {o : Option α} : isEqSome o y = (o == some y) := by
|
||||
@[simp, grind =] theorem isEqSome_eq_beq_some {o : Option α} : isEqSome o y = (o == some y) := by
|
||||
cases o <;> simp [isEqSome]
|
||||
|
||||
@[simp] theorem reflBEq_iff : ReflBEq (Option α) ↔ ReflBEq α := by
|
||||
|
|
@ -1128,12 +1142,15 @@ theorem mem_ite_none_right {x : α} {_ : Decidable p} {l : Option α} :
|
|||
@[simp] theorem isSome_dite {p : Prop} {_ : Decidable p} {b : p → β} :
|
||||
(if h : p then some (b h) else none).isSome = true ↔ p := by
|
||||
split <;> simpa
|
||||
|
||||
@[simp] theorem isSome_ite {p : Prop} {_ : Decidable p} :
|
||||
(if p then some b else none).isSome = true ↔ p := by
|
||||
split <;> simpa
|
||||
|
||||
@[simp] theorem isSome_dite' {p : Prop} {_ : Decidable p} {b : ¬ p → β} :
|
||||
(if h : p then none else some (b h)).isSome = true ↔ ¬ p := by
|
||||
split <;> simpa
|
||||
|
||||
@[simp] theorem isSome_ite' {p : Prop} {_ : Decidable p} :
|
||||
(if p then none else some b).isSome = true ↔ ¬ p := by
|
||||
split <;> simpa
|
||||
|
|
@ -1145,9 +1162,11 @@ theorem mem_ite_none_right {x : α} {_ : Decidable p} {l : Option α} :
|
|||
· exfalso
|
||||
simp at w
|
||||
contradiction
|
||||
|
||||
@[simp] theorem get_ite {p : Prop} {_ : Decidable p} (h) :
|
||||
(if p then some b else none).get h = b := by
|
||||
simpa using get_dite (p := p) (fun _ => b) (by simpa using h)
|
||||
|
||||
@[simp] theorem get_dite' {p : Prop} {_ : Decidable p} (b : ¬ p → β) (w) :
|
||||
(if h : p then none else some (b h)).get w = b (by simpa using w) := by
|
||||
split
|
||||
|
|
@ -1155,13 +1174,14 @@ theorem mem_ite_none_right {x : α} {_ : Decidable p} {l : Option α} :
|
|||
simp at w
|
||||
contradiction
|
||||
· simp
|
||||
|
||||
@[simp] theorem get_ite' {p : Prop} {_ : Decidable p} (h) :
|
||||
(if p then none else some b).get h = b := by
|
||||
simpa using get_dite' (p := p) (fun _ => b) (by simpa using h)
|
||||
|
||||
end ite
|
||||
|
||||
@[simp, grind] theorem get_filter {α : Type _} {x : Option α} {f : α → Bool} (h : (x.filter f).isSome) :
|
||||
@[simp, grind =] theorem get_filter {α : Type _} {x : Option α} {f : α → Bool} (h : (x.filter f).isSome) :
|
||||
(x.filter f).get h = x.get (isSome_of_isSome_filter f x h) := by
|
||||
cases x
|
||||
· contradiction
|
||||
|
|
@ -1176,16 +1196,16 @@ end ite
|
|||
@[grind = gen] theorem pbind_none' (h : x = none) : pbind x f = none := by subst h; rfl
|
||||
@[grind = gen] theorem pbind_some' (h : x = some a) : pbind x f = f a h := by subst h; rfl
|
||||
|
||||
@[simp, grind] theorem map_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
|
||||
@[simp, grind =] theorem map_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
|
||||
{g : β → γ} : (o.pbind f).map g = o.pbind (fun a h => (f a h).map g) := by
|
||||
cases o <;> rfl
|
||||
|
||||
@[simp, grind] theorem pbind_map {α β γ : Type _} (o : Option α)
|
||||
@[simp, grind =] theorem pbind_map {α β γ : Type _} (o : Option α)
|
||||
(f : α → β) (g : (x : β) → o.map f = some x → Option γ) :
|
||||
(o.map f).pbind g = o.pbind (fun x h => g (f x) (h ▸ rfl)) := by
|
||||
cases o <;> rfl
|
||||
|
||||
@[simp, grind] theorem pbind_eq_bind {α β : Type _} (o : Option α)
|
||||
@[simp] theorem pbind_eq_bind {α β : Type _} (o : Option α)
|
||||
(f : α → Option β) : o.pbind (fun x _ => f x) = o.bind f := by
|
||||
cases o <;> rfl
|
||||
|
||||
|
|
@ -1253,11 +1273,11 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
|
|||
pmap f o h = none ↔ o = none := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp, grind] theorem isSome_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
|
||||
@[simp, grind =] theorem isSome_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
|
||||
(pmap f o h).isSome = o.isSome := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp, grind] theorem isNone_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
|
||||
@[simp, grind =] theorem isNone_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
|
||||
(pmap f o h).isNone = o.isNone := by
|
||||
cases o <;> simp
|
||||
|
||||
|
|
@ -1279,11 +1299,11 @@ theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
|
|||
@pmap _ _ p (fun a _ => f a) o H = Option.map f o := by
|
||||
cases o <;> simp
|
||||
|
||||
@[grind] theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) :
|
||||
@[grind =] theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) :
|
||||
Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H := by
|
||||
cases o <;> simp
|
||||
|
||||
@[grind] theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) :
|
||||
@[grind =] 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_iff.2 ⟨_, m, rfl⟩)) := by
|
||||
cases o <;> simp
|
||||
|
|
@ -1340,7 +1360,7 @@ theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
|
|||
@[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
|
||||
cases o <;> simp
|
||||
|
||||
@[simp, grind] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
|
||||
@[simp, grind =] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
|
||||
(H : ∀ (a : α), o = some a → p a) (g : γ) (g' : β → γ) :
|
||||
(o.pmap f H).elim g g' =
|
||||
o.pelim g (fun a h => g' (f a (H a h))) := by
|
||||
|
|
@ -1387,11 +1407,11 @@ theorem pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o')
|
|||
congr; funext a ha
|
||||
exact hf a ha
|
||||
|
||||
@[simp, grind] theorem pfilter_none {α : Type _} {p : (a : α) → none = some a → Bool} :
|
||||
@[simp, grind =] theorem pfilter_none {α : Type _} {p : (a : α) → none = some a → Bool} :
|
||||
none.pfilter p = none := by
|
||||
rfl
|
||||
|
||||
@[simp, grind] theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
|
||||
@[simp, grind =] theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
|
||||
(some x).pfilter p = if p x rfl then some x else none := by
|
||||
simp only [pfilter, cond_eq_if]
|
||||
|
||||
|
|
@ -1416,7 +1436,7 @@ theorem isNone_pfilter_iff {o : Option α} {p : (a : α) → o = some a → Bool
|
|||
Bool.not_eq_true, some.injEq]
|
||||
exact ⟨fun h _ h' => h' ▸ h, fun h => h _ rfl⟩
|
||||
|
||||
@[simp, grind] theorem get_pfilter {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool}
|
||||
@[simp, grind =] theorem get_pfilter {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool}
|
||||
(h : (o.pfilter p).isSome) :
|
||||
(o.pfilter p).get h = o.get (isSome_of_isSome_pfilter h) := by
|
||||
cases o <;> simp
|
||||
|
|
|
|||
|
|
@ -468,9 +468,10 @@ theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f := by
|
|||
theorem map_eq_foldr {f : α → β} {l : List α} : map f l = foldr (fun a bs => f a :: bs) [] l := by
|
||||
induction l <;> grind
|
||||
|
||||
attribute [local ext, local grind ext] List.ext_getElem in
|
||||
theorem map_set {f : α → β} {l : List α} {i : Nat} {a : α} :
|
||||
(l.set i a).map f = (l.map f).set i (f a) := by
|
||||
grind +extAll
|
||||
grind
|
||||
|
||||
theorem head_map {f : α → β} {l : List α} (w) :
|
||||
(map f l).head w = f (l.head (by grind)) := by
|
||||
|
|
@ -489,8 +490,8 @@ theorem map_tail {f : α → β} {l : List α} :
|
|||
theorem headD_map {f : α → β} {l : List α} {a : α} : (map f l).headD (f a) = f (l.headD a) := by
|
||||
cases l with grind
|
||||
|
||||
theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
|
||||
grind
|
||||
-- theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
|
||||
-- grind
|
||||
|
||||
theorem map_map {g : β → γ} {f : α → β} {l : List α} :
|
||||
map g (map f l) = map (g ∘ f) l := by induction l with grind
|
||||
|
|
@ -850,8 +851,9 @@ theorem replicate_eq_append_iff {l₁ l₂ : List α} {a : α} :
|
|||
l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a := by
|
||||
grind [append_eq_replicate_iff]
|
||||
|
||||
attribute [local ext, local grind ext] List.ext_getElem in
|
||||
theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
|
||||
grind +extAll
|
||||
grind
|
||||
|
||||
theorem filter_replicate_of_pos (h : p a) : (replicate n a).filter p = replicate n a := by grind
|
||||
|
||||
|
|
|
|||
|
|
@ -7,7 +7,8 @@ section
|
|||
variable [BEq α] {o₁ o₂ o₃ o₄ o₅ : Option α}
|
||||
|
||||
/--
|
||||
info: Try this: grind only [Option.some_or, Option.or_assoc, Option.some_beq_none, Option.or_some]
|
||||
info: Try this: grind only [=_ Option.or_assoc, = Option.getD_or, = Option.or_some, = Option.some_beq_none, = Option.or_assoc,
|
||||
= Option.some_or]
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by grind?
|
||||
|
|
@ -16,11 +17,11 @@ example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by
|
|||
#guard_msgs in
|
||||
example : max (some 7) none = min (some 13) (some 7) := by grind?
|
||||
|
||||
/-- info: Try this: grind only [Option.guard_def] -/
|
||||
/-- info: Try this: grind only [= Option.guard_apply] -/
|
||||
#guard_msgs in
|
||||
example : Option.guard (· ≤ 7) 3 = some 3 := by grind?
|
||||
|
||||
/-- info: Try this: grind only [Option.mem_bind_iff] -/
|
||||
/-- info: Try this: grind only [= Option.mem_bind_iff] -/
|
||||
#guard_msgs in
|
||||
example {x : β} {o : Option α} {f : α → Option β} (h : a ∈ o) (h' : x ∈ f a) : x ∈ o.bind f := by grind?
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue