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
! This file was ported from Lean 3 source module data.option.defs
! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Init.Algebra.Classes
/-!
# Extra definitions on `Option`
This file defines more operations involving `Option α`. Lemmas about them are located in other
files under `Mathlib.Data.Option`.
Other basic operations on `Option` are defined in the core library.
-/
namespace Option
#align option.lift_or_get Option.liftOrGet
/-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
`none ~ none`. -/
inductive rel ( r : α → β → Prop ) : Option α → Option β → Prop
| /-- If `a ~ b`, then `some a ~ some b` -/
some { a b } : r a b → rel r ( some a ) ( some b )
| /-- `none ~ none` -/
none : rel r none none
#align option.rel Option.rel
/-- Traverse an object of `Option α` with a function `f : α → F β` for an applicative `F`. -/
protected def traverse .{u, v} { F : Type u → Type v } [ Applicative : (Type ?u.124 → Type ?u.123Type (max(?u.124+1)?u.123) F ] { α β : Type _ } ( f : α → F β ) :
Option α → F ( Option β )
| none => pure : {f : Type ?u.164 → Type ?u.163[self : Pure f {α : Type ?u.164} → α → f α none
| some x => some <$> f x
#align option.traverse Option.traverse
/-- If you maybe have a monadic computation in a `[Monad m]` which produces a term of type `α`,
then there is a naturally associated way to always perform a computation in `m` which maybe
produces a result. -/
def maybe .{u, v} { m : Type u → Type v } [ Monad : (Type ?u.542 → Type ?u.541Type (max(?u.542+1)?u.541) m ] { α : Type u } : Option ( m α ) → m ( Option α )
| none => pure : {f : Type ?u.572 → Type ?u.571[self : Pure f {α : Type ?u.572} → α → f α none
| some fn => some <$> fn
#align option.maybe Option.maybe
#align option.mmap Option.mapM
#align option.melim Option.elimM : {m : Type u_1 → Type u_2{α β : Type u_1} → [inst : Monad m m (Option α m β (α → m β m β
@[ deprecated getDM ]
protected def getDM' [ Monad : (Type ?u.919 → Type ?u.918Type (max(?u.919+1)?u.918) m ] ( x : m ( Option α )) ( y : m α ) : m α := do
(← x ) . getDM y
#align option.mget_or_else Option.getDM'
variable { α : Type _ } { β : Type _ }
-- Porting note: Would need to add the attribute directly in `Init.Prelude`.
-- attribute [inline] Option.isSome Option.isNone
/-- An elimination principle for `Option`. It is a nondependent version of `Option.rec`. -/
protected def elim' : β → (α → β Option α β elim' ( b : β ) ( f : α → β ) : Option α → β
| some a => f a
| none => b
#align option.elim Option.elim' : {α : Type u_1} → {β : Type u_2} → β → (α → β Option α β
@[ simp ]
theorem elim'_none ( b : β ) ( f : α → β ) : Option.elim' : {α : Type ?u.1399} → {β : Type ?u.1398} → β → (α → β Option α β b f none = b := rfl : ∀ {α : Sort ?u.1412} {a : α }, a = a
@[ simp ]
theorem elim'_some ( b : β ) ( f : α → β ) : Option.elim' : {α : Type ?u.1483} → {β : Type ?u.1482} → β → (α → β Option α β b f ( some a ) = f a := rfl : ∀ {α : Sort ?u.1496} {a : α }, a = a
theorem mem_some_iff : ∀ {α : Type u_1} {a b : α }, a ∈ some b ↔ b = a mem_some_iff { α : Type _ } { a b : α } : a ∈ some b ↔ b = a := by simp
#align option.mem_some_iff Option.mem_some_iff : ∀ {α : Type u_1} {a b : α }, a ∈ some b ↔ b = a
/-- `o = none` is decidable even if the wrapped type does not have decidable equality.
This is not an instance because it is not definitionally equal to `Option.decidableEq`.
Try to use `o.isNone` or `o.isSome` instead.
-/
@[inline]
def decidableEqNone { o : Option α } : Decidable ( o = none ) :=
decidable_of_decidable_of_iff isNone_iff_eq_none
#align option.decidable_eq_none Option.decidableEqNone
instance decidableForallMem { p : α → Prop } [ DecidablePred : {α : Sort ?u.1827} → (α → Prop Sort (max1?u.1827) p ] :
∀ o : Option α , Decidable (∀ a ∈ o , p a )
| none => isTrue ( by ∀ (a : α ), a ∈ none p a simp [ false_imp_iff ] )
| some a =>
if h : p a then isTrue fun o e ↦ some_inj . 1 : ∀ {a b : Prop }, (a ↔ b a → b e ▸ h
else isFalse <| mt : ∀ {a b : Prop }, (a → b ¬ b ¬ a ( fun H ↦ H _ rfl : ∀ {α : Sort ?u.1987} {a : α }, a = a ) h
instance decidableExistsMem { p : α → Prop } [ DecidablePred : {α : Sort ?u.2436} → (α → Prop Sort (max1?u.2436) p ] :
∀ o : Option α , Decidable (∃ a ∈ o , p a )
| none => isFalse fun ⟨ a , ⟨ h , _⟩⟩ ↦ by cases h
| some a => if h : p a then isTrue <| ⟨ _ , rfl : ∀ {α : Sort ?u.2700} {a : α }, a = a , h ⟩ else isFalse fun ⟨ _ , ⟨ rfl : ∀ {α : Sort ?u.2719} {a : α }, a = a , hn ⟩⟩ ↦ h hn
/-- Inhabited `get` function. Returns `a` if the input is `some a`, otherwise returns `default`. -/
@[reducible]
def iget [ Inhabited : Sort ?u.3243 → Sort (max1?u.3243) α ] : Option α → α
| some x => x
| none => default
#align option.iget Option.iget
theorem iget_some [ Inhabited : Sort ?u.3530 → Sort (max1?u.3530) α ] { a : α } : ( some a ). iget = a :=
rfl : ∀ {α : Sort ?u.3554} {a : α }, a = a
#align option.iget_some Option.iget_some
@[ simp ]
theorem mem_toList { a : α } { o : Option α } : a ∈ toList o ↔ a ∈ o := by
cases o <;> simp [ toList , eq_comm : ∀ {α : Sort ?u.3821} {a b : α }, a = b ↔ b = a ]
#align option.mem_to_list Option.mem_toList
instance liftOrGet_isCommutative ( f : α → α → α ) [ IsCommutative : (α : Type ?u.3981) → (α → α → α Prop α f ] :
IsCommutative : (α : Type ?u.3986) → (α → α → α Prop ( Option α ) ( liftOrGet f ) :=
⟨ fun a b ↦ by cases a <;> cases b <;> none.none none.some some.none some.some simp [ liftOrGet , IsCommutative.comm : ∀ {α : Type ?u.4395} {op : α → α → α self : IsCommutative α op a b : α ), op a b = op b a ] ⟩
instance liftOrGet_isAssociative ( f : α → α → α ) [ IsAssociative : (α : Type ?u.4699) → (α → α → α Prop α f ] :
IsAssociative : (α : Type ?u.4704) → (α → α → α Prop ( Option α ) ( liftOrGet f ) :=
⟨ fun a b c ↦ by cases a <;> cases b <;> none.none none.some some.none some.some cases c some.none.none some.none.some <;> none.none.none none.none.some none.some.none none.some.some some.none.none some.none.some some.some.none some.some.some simp [ liftOrGet , IsAssociative.assoc : ∀ {α : Type ?u.8987} {op : α → α → α self : IsAssociative α op a b c : α ), op (op a b c = op a (op b c ] ⟩
instance liftOrGet_isIdempotent ( f : α → α → α ) [ IsIdempotent : (α : Type ?u.11269) → (α → α → α Prop α f ] :
IsIdempotent : (α : Type ?u.11274) → (α → α → α Prop ( Option α ) ( liftOrGet f ) :=
⟨ fun a ↦ by cases a <;> simp [ liftOrGet , IsIdempotent.idempotent : ∀ {α : Type ?u.11458} {op : α → α → α self : IsIdempotent α op a : α ), op a a = a ] ⟩
instance liftOrGet_isLeftId ( f : α → α → α ) : IsLeftId ( Option α ) ( liftOrGet f ) none :=
⟨ fun a ↦ by cases a α : Type ?u.11597β : Type ?u.11600f : α → α → α none α : Type ?u.11597β : Type ?u.11600f : α → α → α val✝ : α some <;> α : Type ?u.11597β : Type ?u.11600f : α → α → α none α : Type ?u.11597β : Type ?u.11600f : α → α → α val✝ : α some simp [ liftOrGet ] ⟩
instance liftOrGet_isRightId ( f : α → α → α ) : IsRightId ( Option α ) ( liftOrGet f ) none :=
⟨ fun a ↦ by cases a α : Type ?u.11807β : Type ?u.11810f : α → α → α none α : Type ?u.11807β : Type ?u.11810f : α → α → α val✝ : α some <;> α : Type ?u.11807β : Type ?u.11810f : α → α → α none α : Type ?u.11807β : Type ?u.11810f : α → α → α val✝ : α some simp [ liftOrGet ] ⟩
#align option.lift_or_get_comm Option.liftOrGet_isCommutative
#align option.lift_or_get_assoc Option.liftOrGet_isAssociative
#align option.lift_or_get_idem Option.liftOrGet_isIdempotent
#align option.lift_or_get_is_left_id Option.liftOrGet_isLeftId
#align option.lift_or_get_is_right_id Option.liftOrGet_isRightId