max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: manual docstring review for smaller namespaces (#7365)

Browse source 
This PR updates docstrings and adds some that are missing.
This commit is contained in:
David Thrane Christiansen 2025-03-13 17:09:37 +01:00 • committed by GitHub
parent 044e3b1b56
commit 06c57826ae
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
27 changed files with 2089 additions and 632 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Control/Basic.lean
View file

@ -51,14 +51,28 @@ def ForInStep.value (x : ForInStep α) : α :=
@[simp] theorem ForInStep.value_done (b : β) : (ForInStep.done b).value = b := rfl
@[simp] theorem ForInStep.value_yield (b : β) : (ForInStep.yield b).value = b := rfl
/--
Maps a function over a functor, with parameters swapped so that the function comes last.
This function is `Functor.map` with the parameters reversed, typically used via the `<&>` operator.
-/
@[reducible]
def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β :=
fun a f => f <$> a
@[inherit_doc Functor.mapRev]
infixr:100 " <&> " => Functor.mapRev
recommended_spelling "mapRev" for "<&>" in [Functor.mapRev, «term_<&>_»]
/--
Discards the value in a functor, retaining the functor's structure.
Discarding values is especially useful when using `Applicative` functors or `Monad`s to implement
effects, and some operation should be carried out only for its effects. In `do`-notation, statements
whose values are discarded must return `Unit`, and `discard` can be used to explicitly discard their
values.
-/
@[always_inline, inline]
def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
Functor.mapConst PUnit.unit x

100
src/Init/Control/Except.lean
View file

@ -13,10 +13,20 @@ import Init.Coe
namespace Except
variable {ε : Type u}
/--
A successful computation in the `Except ε` monad: `a` is returned, and no exception is thrown.
-/
@[always_inline, inline]
protected def pure (a : α) : Except ε α :=
Except.ok a
/--
Transforms a successful result with a function, doing nothing when an exception is thrown.
Examples:
* `(pure 2 : Except String Nat).map toString = pure 2`
* `(throw "Error" : Except String Nat).map toString = throw "Error"`
-/
@[always_inline, inline]
protected def map (f : α → β) : Except ε α → Except ε β
| Except.error err => Except.error err
@ -27,36 +37,78 @@ protected def map (f : α → β) : Except ε α → Except ε β
intro e
simp [Except.map]; cases e <;> rfl
/--
Transforms exceptions with a function, doing nothing on successful results.
Examples:
* `(pure 2 : Except String Nat).mapError (·.length) = pure 2`
* `(throw "Error" : Except String Nat).mapError (·.length) = throw 5`
-/
@[always_inline, inline]
protected def mapError (f : ε → ε') : Except ε α → Except ε' α
| Except.error err => Except.error <| f err
| Except.ok v => Except.ok v
/--
Sequences two operations that may throw exceptions, allowing the second to depend on the value
returned by the first.
If the first operation throws an exception, then it is the result of the computation. If the first
succeeds but the second throws an exception, then that exception is the result. If both succeed,
then the result is the result of the second computation.
This is the implementation of the `>>=` operator for `Except ε`.
-/
@[always_inline, inline]
protected def bind (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
match ma with
| Except.error err => Except.error err
| Except.ok v => f v
/-- Returns true if the value is `Except.ok`, false otherwise. -/
/-- Returns `true` if the value is `Except.ok`, `false` otherwise. -/
@[always_inline, inline]
protected def toBool : Except ε α → Bool
| Except.ok _ => true
| Except.error _ => false
@[inherit_doc Except.toBool]
abbrev isOk : Except ε α → Bool := Except.toBool
/--
Returns `none` if an exception was thrown, or `some` around the value on success.
Examples:
* `(pure 10 : Except String Nat).toOption = some 10`
* `(throw "Failure" : Except String Nat).toOption = none`
-/
@[always_inline, inline]
protected def toOption : Except ε α → Option α
| Except.ok a => some a
| Except.error _ => none
/--
Handles exceptions thrown in the `Except ε` monad.
If `ma` is successful, its result is returned. If it throws an exception, then `handle` is invoked
on the exception's value.
Examples:
* `(pure 2 : Except String Nat).tryCatch (pure ·.length) = pure 2`
* `(throw "Error" : Except String Nat).tryCatch (pure ·.length) = pure 5`
* `(throw "Error" : Except String Nat).tryCatch (fun x => throw ("E: " ++ x)) = throw "E: Error"`
-/
@[always_inline, inline]
protected def tryCatch (ma : Except ε α) (handle : ε → Except ε α) : Except ε α :=
match ma with
| Except.ok a => Except.ok a
| Except.error e => handle e
/--
Recovers from exceptions thrown in the `Except ε` monad. Typically used via the `<|>` operator.
`Except.tryCatch` is a related operator that allows the recovery procedure to depend on _which_
exception was thrown.
-/
def orElseLazy (x : Except ε α) (y : Unit → Except ε α) : Except ε α :=
match x with
| Except.ok a => Except.ok a
@ -70,12 +122,26 @@ instance : Monad (Except ε) where
end Except
/--
Adds exceptions of type `ε` to a monad `m`.
-/
def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
m (Except ε α)
/--
Use a monadic action that may return an exception's value as an action in the transformed monad that
may throw the corresponding exception.
This is the inverse of `ExceptT.run`.
-/
@[always_inline, inline]
def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x
/--
Use a monadic action that may throw an exception as an action that may return an exception's value.
This is the inverse of `ExceptT.mk`.
-/
@[always_inline, inline]
def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
@ -83,25 +149,41 @@ namespace ExceptT
variable {ε : Type u} {m : Type u → Type v} [Monad m]
/--
Returns the value `a` without throwing exceptions or having any other effect.
-/
@[always_inline, inline]
protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
ExceptT.mk <| pure (Except.ok a)
/--
Handles exceptions thrown by an action that can have no effects _other_ than throwing exceptions.
-/
@[always_inline, inline]
protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
| Except.ok a => f a
| Except.error e => pure (Except.error e)
/--
Sequences two actions that may throw exceptions. Typically used via `do`-notation or the `>>=`
operator.
-/
@[always_inline, inline]
protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
ExceptT.mk <| ma >>= ExceptT.bindCont f
/--
Transforms a successful computation's value using `f`. Typically used via the `<$>` operator.
-/
@[always_inline, inline]
protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
ExceptT.mk <| x >>= fun a => match a with
| (Except.ok a) => pure <| Except.ok (f a)
| (Except.error e) => pure <| Except.error e
/--
Runs a computation from an underlying monad in the transformed monad with exceptions.
-/
@[always_inline, inline]
protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
ExceptT.mk <| Except.ok <$> t
@ -110,6 +192,9 @@ protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
instance : MonadLift (Except ε) (ExceptT ε m) := ⟨fun e => ExceptT.mk <| pure e⟩
instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
/--
Handles exceptions produced in the `ExceptT ε` transformer.
-/
@[always_inline, inline]
protected def tryCatch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
ExceptT.mk <| ma >>= fun res => match res with
@ -124,6 +209,11 @@ instance : Monad (ExceptT ε m) where
bind := ExceptT.bind
map := ExceptT.map
/--
Transforms exceptions using the function `f`.
This is the `ExceptT` version of `Except.mapError`.
-/
@[always_inline, inline]
protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α := fun x =>
ExceptT.mk <| Except.mapError f <$> x
@ -150,8 +240,12 @@ instance (ε) : MonadExceptOf ε (Except ε) where
namespace MonadExcept
variable {ε : Type u} {m : Type v → Type w}
/-- Alternative orelse operator that allows to select which exception should be used.
The default is to use the first exception since the standard `orelse` uses the second. -/
/--
An alternative unconditional error recovery operator that allows callers to specify which exception
to throw in cases where both operations throw exceptions.
By default, the first is thrown, because the `<|>` operator throws the second.
-/
@[always_inline, inline]
def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := true) : m α :=
tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx then e₁ else e₂)

21
src/Init/Control/ExceptCps.lean
View file

@ -10,19 +10,37 @@ import Init.Control.Lawful.Basic
The Exception monad transformer using CPS style.
-/
/--
Adds exceptions of type `ε` to a monad `m`.
Instead of using `Except ε` to model exceptions, this implementation uses continuation passing
style. This has different performance characteristics from `ExceptT ε`.
-/
def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
namespace ExceptCpsT
/--
Use a monadic action that may throw an exception as an action that may return an exception's value.
-/
@[always_inline, inline]
def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
set_option linter.unusedVariables false in -- `s` unused
/--
Use a monadic action that may throw an exception by providing explicit success and failure
continuations.
-/
@[always_inline, inline]
def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
x _ ok error
/--
Returns the value of a computation, forgetting whether it was an exception or a success.
This corresponds to early return.
-/
@[always_inline, inline]
def runCatch [Monad m] (x : ExceptCpsT α m α) : m α :=
x α pure pure
@ -40,6 +58,9 @@ instance : MonadExceptOf ε (ExceptCpsT ε m) where
throw e := fun _ _ k => k e
tryCatch x handle := fun _ k₁ k₂ => x _ k₁ (fun e => handle e _ k₁ k₂)
/--
Run an action from the transformed monad in the exception monad.
-/
@[always_inline, inline]
def lift [Monad m] (x : m α) : ExceptCpsT ε m α :=
fun _ k _ => x >>= k

99
src/Init/Control/Lawful/Basic.lean
View file

@ -13,17 +13,26 @@ open Function
rfl
/--
The `Functor` typeclass only contains the operations of a functor.
`LawfulFunctor` further asserts that these operations satisfy the laws of a functor,
including the preservation of the identity and composition laws:
```
id <$> x = x
(h ∘ g) <$> x = h <$> g <$> x
```
A functor satisfies the functor laws.
The `Functor` class contains the operations of a functor, but does not require that instances
prove they satisfy the laws of a functor. A `LawfulFunctor` instance includes proofs that the laws
are satisfied. Because `Functor` instances may provide optimized implementations of `mapConst`,
`LawfulFunctor` instances must also prove that the optimized implementation is equivalent to the
standard implementation.
-/
class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
/--
The `mapConst` implementation is equivalent to the default implementation.
-/
map_const : (Functor.mapConst : α → f β → f α) = Functor.map ∘ const β
/--
The `map` implementation preserves identity.
-/
id_map (x : f α) : id <$> x = x
/--
The `map` implementation preserves function composition.
-/
comp_map (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x
export LawfulFunctor (map_const id_map comp_map)
@ -38,21 +47,48 @@ attribute [simp] id_map
(comp_map _ _ _).symm
/--
The `Applicative` typeclass only contains the operations of an applicative functor.
`LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor:
```
pure id <*> v = v
pure (·∘·) <*> u <*> v <*> w = u <*> (v <*> w)
pure f <*> pure x = pure (f x)
u <*> pure y = pure (· y) <*> u
```
An applicative functor satisfies the laws of an applicative functor.
The `Applicative` class contains the operations of an applicative functor, but does not require that
instances prove they satisfy the laws of an applicative functor. A `LawfulApplicative` instance
includes proofs that the laws are satisfied.
Because `Applicative` instances may provide optimized implementations of `seqLeft` and `seqRight`,
`LawfulApplicative` instances must also prove that the optimized implementation is equivalent to the
standard implementation.
-/
class LawfulApplicative (f : Type u → Type v) [Applicative f] : Prop extends LawfulFunctor f where
/-- `seqLeft` is equivalent to the default implementation. -/
seqLeft_eq (x : f α) (y : f β) : x <* y = const β <$> x <*> y
/-- `seqRight` is equivalent to the default implementation. -/
seqRight_eq (x : f α) (y : f β) : x *> y = const α id <$> x <*> y
/--
`pure` before `seq` is equivalent to `Functor.map`.
This means that `pure` really is pure when occurring immediately prior to `seq`.
-/
pure_seq (g : α → β) (x : f α) : pure g <*> x = g <$> x
/--
Mapping a function over the result of `pure` is equivalent to applying the function under `pure`.
This means that `pure` really is pure with respect to `Functor.map`.
-/
map_pure (g : α → β) (x : α) : g <$> (pure x : f α) = pure (g x)
/--
`pure` after `seq` is equivalent to `Functor.map`.
This means that `pure` really is pure when occurring just after `seq`.
-/
seq_pure {α β : Type u} (g : f (α → β)) (x : α) : g <*> pure x = (fun h => h x) <$> g
/--
`seq` is associative.
Changing the nesting of `seq` calls while maintaining the order of computations results in an
equivalent computation. This means that `seq` is not doing any more than sequencing.
-/
seq_assoc {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = ((@comp α β γ) <$> h) <*> g <*> x
comp_map g h x := (by
repeat rw [← pure_seq]
@ -66,21 +102,36 @@ attribute [simp] map_pure seq_pure
simp [pure_seq]
/--
The `Monad` typeclass only contains the operations of a monad.
`LawfulMonad` further asserts that these operations satisfy the laws of a monad,
including associativity and identity laws for `bind`:
```
pure x >>= f = f x
x >>= pure = x
x >>= f >>= g = x >>= (fun x => f x >>= g)
```
Lawful monads are those that satisfy a certain behavioral specification. While all instances of
`Monad` should satisfy these laws, not all implementations are required to prove this.
`LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields.
`LawfulMonad.mk'` is an alternative constructor that contains useful defaults for many fields.
-/
class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplicative m where
/--
A `bind` followed by `pure` composed with a function is equivalent to a functorial map.
This means that `pure` really is pure after a `bind` and has no effects.
-/
bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
/--
A `bind` followed by a functorial map is equivalent to `Applicative` sequencing.
This means that the effect sequencing from `Monad` and `Applicative` are the same.
-/
bind_map {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = f <*> x
/--
`pure` followed by `bind` is equivalent to function application.
This means that `pure` really is pure before a `bind` and has no effects.
-/
pure_bind (x : α) (f : α → m β) : pure x >>= f = f x
/--
`bind` is associative.
Changing the nesting of `bind` calls while maintaining the order of computations results in an
equivalent computation. This means that `bind` is not doing more than data-dependent sequencing.
-/
bind_assoc (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun x => f x >>= g
map_pure g x := (by rw [← bind_pure_comp, pure_bind])
seq_pure g x := (by rw [← bind_map]; simp [map_pure, bind_pure_comp])

485
src/Init/Core.lean
View file

@ -52,8 +52,6 @@ attribute [simp] namedPattern
/--
`Empty.elim : Empty → C` says that a value of any type can be constructed from
`Empty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
This is a non-dependent variant of `Empty.rec`.
-/
@[macro_inline] def Empty.elim {C : Sort u} : Empty → C := Empty.rec
@ -63,8 +61,6 @@ instance : DecidableEq Empty := fun a => a.elim
/--
`PEmpty.elim : Empty → C` says that a value of any type can be constructed from
`PEmpty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
This is a non-dependent variant of `PEmpty.rec`.
-/
@[macro_inline] def PEmpty.elim {C : Sort _} : PEmpty → C := fun a => nomatch a
@ -138,46 +134,50 @@ recommended_spelling "iff" for "↔" in [Iff, «term_↔_»]
recommended_spelling "iff" for "<->" in [Iff, «term_<->_»]
/--
`Sum α β`, or `α ⊕ β`, is the disjoint union of types `α` and `β`.
An element of `α ⊕ β` is either of the form `.inl a` where `a : α`,
or `.inr b` where `b : β`.
The disjoint union of types `α` and `β`, ordinarily written `α ⊕ β`.
An element of `α ⊕ β` is either an `a : α` wrapped in `Sum.inl` or a `b : β` wrapped in `Sum.inr`.
`α ⊕ β` is not equivalent to the set-theoretic union of `α` and `β` because its values include an
indication of which of the two types was chosen. The union of a singleton set with itself contains
one element, while `Unit ⊕ Unit` contains distinct values `inl ()` and `inr ()`.
-/
inductive Sum (α : Type u) (β : Type v) where
/-- Left injection into the sum type `α ⊕ β`. If `a : α` then `.inl a : α ⊕ β`. -/
/-- Left injection into the sum type `α ⊕ β`. -/
| inl (val : α) : Sum α β
/-- Right injection into the sum type `α ⊕ β`. If `b : β` then `.inr b : α ⊕ β`. -/
/-- Right injection into the sum type `α ⊕ β`. -/
| inr (val : β) : Sum α β
@[inherit_doc] infixr:30 " ⊕ " => Sum
/--
`PSum α β`, or `α ⊕' β`, is the disjoint union of types `α` and `β`.
It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts
`Sort u` and `Sort v`, instead of restricting to `Type u` and `Type v`. This means
that it can be used in situations where one side is a proposition, like `True ⊕' Nat`.
The disjoint union of arbitrary sorts `α` `β`, or `α ⊕' β`.
The reason this is not the default is that this type lives in the universe `Sort (max 1 u v)`,
which can cause problems for universe level unification,
because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
`PSum` is usually only used in automation that constructs sums of arbitrary types.
It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts `Sort u` and `Sort v`,
instead of restricting them to `Type u` and `Type v`. This means that it can be used in situations
where one side is a proposition, like `True ⊕' Nat`. However, the resulting universe level
constraints are often more difficult to solve than those that result from `Sum`.
-/
inductive PSum (α : Sort u) (β : Sort v) where
/-- Left injection into the sum type `α ⊕' β`. If `a : α` then `.inl a : α ⊕' β`. -/
/-- Left injection into the sum type `α ⊕' β`.-/
| inl (val : α) : PSum α β
/-- Right injection into the sum type `α ⊕' β`. If `b : β` then `.inr b : α ⊕' β`. -/
/-- Right injection into the sum type `α ⊕' β`. -/
| inr (val : β) : PSum α β
@[inherit_doc] infixr:30 " ⊕' " => PSum
/--
`PSum α β` is inhabited if `α` is inhabited.
This is not an instance to avoid non-canonical instances.
If the left type in a sum is inhabited then the sum is inhabited.
This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
-/
@[reducible] def PSum.inhabitedLeft {α β} [Inhabited α] : Inhabited (PSum α β) := ⟨PSum.inl default⟩
@[reducible] def PSum.inhabitedLeft {α β} [Inhabited α] : Inhabited (PSum α β) := ⟨PSum.inl default⟩
/--
`PSum α β` is inhabited if `β` is inhabited.
This is not an instance to avoid non-canonical instances.
If the right type in a sum is inhabited then the sum is inhabited.
This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
-/
@[reducible] def PSum.inhabitedRight {α β} [Inhabited β] : Inhabited (PSum α β) := ⟨PSum.inr default⟩
@ -188,47 +188,58 @@ instance PSum.nonemptyRight [h : Nonempty β] : Nonempty (PSum α β) :=
Nonempty.elim h (fun b => ⟨PSum.inr b⟩)
/--
`Sigma β`, also denoted `Σ a : α, β a` or `(a : α) × β a`, is the type of dependent pairs
whose first component is `a : α` and whose second component is `b : β a`
(so the type of the second component can depend on the value of the first component).
It is sometimes known as the dependent sum type, since it is the type level version
of an indexed summation.
Dependent pairs, in which the second element's type depends on the value of the first element. The
type `Sigma β` is typically written `Σ a : α, β a` or `(a : α) × β a`.
Although its values are pairs, `Sigma` is sometimes known as the *dependent sum type*, since it is
the type level version of an indexed summation.
-/
@[pp_using_anonymous_constructor]
structure Sigma {α : Type u} (β : α → Type v) where
/-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : Sigma β`.
(This will usually require a type ascription to determine `β`
since it is not determined from `a` and `b` alone.) -/
/--
Constructs a dependent pair.
Using this constructor in a context in which the type is not known usually requires a type
ascription to determine `β`. This is because the desired relationship between the two values can't
generally be determined automatically.
-/
mk ::
/-- The first component of a dependent pair. If `p : @Sigma α β` then `p.1 : α`. -/
/--
The first component of a dependent pair.
-/
fst : α
/-- The second component of a dependent pair. If `p : Sigma β` then `p.2 : β p.1`. -/
/--
The second component of a dependent pair. Its type depends on the first component.
-/
snd : β fst
attribute [unbox] Sigma
/--
`PSigma β`, also denoted `Σ' a : α, β a` or `(a : α) ×' β a`, is the type of dependent pairs
whose first component is `a : α` and whose second component is `b : β a`
(so the type of the second component can depend on the value of the first component).
It differs from `Σ a : α, β a` in that it allows `α` and `β` to have arbitrary sorts
`Sort u` and `Sort v`, instead of restricting to `Type u` and `Type v`. This means
that it can be used in situations where one side is a proposition, like `(p : Nat) ×' p = p`.
Fully universe-polymorphic dependent pairs, in which the second element's type depends on the value
of the first element and both types are allowed to be propositions. The type `PSigma β` is typically
written `Σ' a : α, β a` or `(a : α) ×' β a`.
The reason this is not the default is that this type lives in the universe `Sort (max 1 u v)`,
which can cause problems for universe level unification,
because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
`PSigma` is usually only used in automation that constructs pairs of arbitrary types.
In practice, this generality leads to universe level constraints that are difficult to solve, so
`PSigma` is rarely used in manually-written code. It is usually only used in automation that
constructs pairs of arbitrary types.
To pair a value with a proof that a predicate holds for it, use `Subtype`. To demonstrate that a
value exists that satisfies a predicate, use `Exists`. A dependent pair with a proposition as its
first component is not typically useful due to proof irrelevance: there's no point in depending on a
specific proof because all proofs are equal anyway.
-/
@[pp_using_anonymous_constructor]
structure PSigma {α : Sort u} (β : α → Sort v) where
/-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : PSigma β`.
(This will usually require a type ascription to determine `β`
since it is not determined from `a` and `b` alone.) -/
/-- Constructs a fully universe-polymorphic dependent pair. -/
mk ::
/-- The first component of a dependent pair. If `p : @PSigma α β` then `p.1 : α`. -/
/--
The first component of a dependent pair.
-/
fst : α
/-- The second component of a dependent pair. If `p : PSigma β` then `p.2 : β p.1`. -/
/--
The second component of a dependent pair. Its type depends on the first component.
-/
snd : β fst
/--
@ -687,9 +698,11 @@ Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead
recommended_spelling "bne" for "!=" in [bne, «term_!=_»]
/--
`LawfulBEq α` is a typeclass which asserts that the `BEq α` implementation
(which supplies the `a == b` notation) coincides with logical equality `a = b`.
In other words, `a == b` implies `a = b`, and `a == a` is true.
A Boolean equality test coincides with propositional equality.
In other words:
* `a == b` implies `a = b`.
* `a == a` is true.
-/
class LawfulBEq (α : Type u) [BEq α] : Prop where
/-- If `a == b` evaluates to `true`, then `a` and `b` are equal in the logic. -/
@ -946,9 +959,10 @@ namespace Decidable
variable {p q : Prop}
/--
Synonym for `dite` (dependent if-then-else). We can construct an element `q`
(of any sort, not just a proposition) by cases on whether `p` is true or false,
provided `p` is decidable.
Construct a `q` if some proposition `p` is decidable, and both the truth and falsity of `p` are
sufficient to construct a `q`.
This is a synonym for `dite`, the dependent if-then-else operator.
-/
@[macro_inline] def byCases {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
match dec with
@ -1081,22 +1095,28 @@ theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p
/-! # Subsingleton -/
/--
A "subsingleton" is a type with at most one element.
In other words, it is either empty, or has a unique element.
All propositions are subsingletons because of proof irrelevance, but some other types
are subsingletons as well and they inherit many of the same properties as propositions.
`Subsingleton α` is a typeclass, so it is usually used as an implicit argument and
inferred by typeclass inference.
A _subsingleton_ is a type with at most one element. It is either empty or has a unique element.
All propositions are subsingletons because of proof irrelevance: false propositions are empty, and
all proofs of a true proposition are equal to one another. Some non-propositional types are also
subsingletons.
-/
class Subsingleton (α : Sort u) : Prop where
/-- Construct a proof that `α` is a subsingleton by showing that any two elements are equal. -/
/-- Prove that `α` is a subsingleton by showing that any two elements are equal. -/
intro ::
/-- Any two elements of a subsingleton are equal. -/
allEq : (a b : α) → a = b
/--
If a type is a subsingleton, then all of its elements are equal.
-/
protected theorem Subsingleton.elim {α : Sort u} [h : Subsingleton α] : (a b : α) → a = b :=
h.allEq
/--
If two types are equal and one of them is a subsingleton, then all of their elements are
[heterogeneously equal](lean-manual://section/HEq).
-/
protected theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : HEq a b := by
subst h₂
apply heq_of_eq
@ -1134,22 +1154,21 @@ theorem recSubsingleton
| isFalse h => h₄ h
/--
An equivalence relation `~ : α → α → Prop` is a relation that is:
An equivalence relation `r : α → α → Prop` is a relation that is
* reflexive: `x ~ x`
* symmetric: `x ~ y` implies `y ~ x`
* transitive: `x ~ y` and `y ~ z` implies `x ~ z`
* reflexive: `r x x`,
* symmetric: `r x y` implies `r y x`, and
* transitive: `r x y` and `r y z` implies `r x z`.
Equality is an equivalence relation, and equivalence relations share many of
the properties of equality. In particular, `Quot α r` is most well behaved
when `r` is an equivalence relation, and in this case we use `Quotient` instead.
Equality is an equivalence relation, and equivalence relations share many of the properties of
equality.
-/
structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
/-- An equivalence relation is reflexive: `x ~ x` -/
/-- An equivalence relation is reflexive: `r x x` -/
refl : ∀ x, r x x
/-- An equivalence relation is symmetric: `x ~ y` implies `y ~ x` -/
/-- An equivalence relation is symmetric: `r x y` implies `r y x` -/
symm : ∀ {x y}, r x y → r y x
/-- An equivalence relation is transitive: `x ~ y` and `y ~ z` implies `x ~ z` -/
/-- An equivalence relation is transitive: `r x y` and `r y z` implies `r x z` -/
trans : ∀ {x y z}, r x y → r y z → r x z
/-- The empty relation is the relation on `α` which is always `False`. -/
@ -1221,12 +1240,12 @@ end Subtype
section
variable {α : Type u} {β : Type v}
/-- This is not an instance to avoid non-canonical instances. -/
@[reducible] def Sum.inhabitedLeft [Inhabited α] : Inhabited (Sum α β) where
@[reducible, inherit_doc PSum.inhabitedLeft]
def Sum.inhabitedLeft [Inhabited α] : Inhabited (Sum α β) where
default := Sum.inl default
/-- This is not an instance to avoid non-canonical instances. -/
@[reducible] def Sum.inhabitedRight [Inhabited β] : Inhabited (Sum α β) where
@[reducible, inherit_doc PSum.inhabitedRight]
def Sum.inhabitedRight [Inhabited β] : Inhabited (Sum α β) where
default := Sum.inr default
instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
@ -1286,7 +1305,12 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
instance [BEq α] [BEq β] : BEq (α × β) where
beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂
/-- Lexicographical order for products -/
/--
Lexicographical order for products.
Two pairs are lexicographically ordered if their first elements are ordered or if their first
elements are equal and their second elements are ordered.
-/
def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
@ -1302,8 +1326,11 @@ theorem Prod.lexLt_def [LT α] [LT β] (s t : α × β) : (Prod.lexLt s t) = (s.
theorem Prod.eta (p : α × β) : (p.1, p.2) = p := rfl
/--
`Prod.map f g : α₁ × β₁ → α₂ × β₂` maps across a pair
by applying `f` to the first component and `g` to the second.
Transforms a pair by applying functions to both elements.
Examples:
* `(1, 2).map (· + 1) (· * 3) = (2, 6)`
* `(1, 2).map toString (· * 3) = ("1", 6)`
-/
def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
(f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
@ -1350,7 +1377,8 @@ instance : DecidableEq PUnit :=
/--
A setoid is a type with a distinguished equivalence relation, denoted `≈`.
This is mainly used as input to the `Quotient` type constructor.
The `Quotient` type constructor requires a `Setoid` instance.
-/
class Setoid (α : Sort u) where
/-- `x ≈ y` is the distinguished equivalence relation of a setoid. -/
@ -1365,12 +1393,15 @@ namespace Setoid
variable {α : Sort u} [Setoid α]
/-- A setoid's equivalence relation is reflexive. -/
theorem refl (a : α) : a ≈ a :=
iseqv.refl a
/-- A setoid's equivalence relation is symmetric. -/
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
iseqv.symm hab
/-- A setoid's equivalence relation is transitive. -/
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
iseqv.trans hab hbc
@ -1587,34 +1618,21 @@ theorem imp_iff_not (hb : ¬b) : a → b ↔ ¬a := imp_congr_right fun _ => iff
namespace Quot
/--
The **quotient axiom**, or at least the nontrivial part of the quotient
axiomatization. Quotient types are introduced by the `init_quot` command
in `Init.Prelude` which introduces the axioms:
The **quotient axiom**, which asserts the equality of elements related by the quotient's relation.
```
opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u
The relation `r` does not need to be an equivalence relation to use this axiom. When `r` is not an
equivalence relation, the quotient is with respect to the equivalence relation generated by `r`.
opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
`Quot.sound` is part of the built-in primitive quotient type:
* `Quot` is the built-in quotient type.
* `Quot.mk` places elements of the underlying type `α` into the quotient.
* `Quot.lift` allows the definition of functions from the quotient to some other type.
* `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
with `Quot.mk`; it is analogous to the [recursor](lean-manual://section/recursors) for a
structure.
opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → f a = f b) → Quot r → β
opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
```
All of these axioms are true if we assume `Quot α r = α` and `Quot.mk` and
`Quot.lift` are identity functions, so they do not add much. However this axiom
cannot be explained in that way (it is false for that interpretation), so the
real power of quotient types come from this axiom.
It says that the quotient by `r` maps elements which are related by `r` to equal
values in the quotient. Together with `Quot.lift` which says that functions
which respect `r` can be lifted to functions on the quotient, we can deduce that
`Quot α r` exactly consists of the equivalence classes with respect to `r`.
It is important to note that `r` need not be an equivalence relation in this axiom.
When `r` is not an equivalence relation, we are actually taking a quotient with
respect to the equivalence relation generated by `r`.
[Quotient types](lean-manual://section/quotients) are described in more detail in the Lean Language
Reference.
-/
axiom sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
@ -1632,8 +1650,17 @@ protected theorem indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot
rfl
/--
`Quot.liftOn q f h` is the same as `Quot.lift f h q`. It just reorders
the argument `q : Quot r` to be first.
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's relation.
Given a relation `r : α → α → Prop` and a quotient's value `q : Quot r`, applying a `f : α → β`
requires a proof `c` that `f` respects `r`. In this case, `Quot.liftOn q f h : β` evaluates
to the result of applying `f` to the underlying value in `α` from `q`.
`Quot.liftOn` is a version of the built-in primitive `Quot.lift` with its parameters re-ordered.
[Quotient types](lean-manual://section/quotients) are described in more detail in the Lean Language
Reference.
-/
protected abbrev liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop}
(q : Quot r) (f : α → β) (c : (a b : α) → r a b → f a = f b) : β :=
@ -1674,12 +1701,19 @@ protected theorem liftIndepPr1
exact rfl
/--
Dependent recursion principle for `Quot`. This constructor can be tricky to use,
so you should consider the simpler versions if they apply:
* `Quot.lift`, for nondependent functions
* `Quot.ind`, for theorems / proofs of propositions about quotients
* `Quot.recOnSubsingleton`, when the target type is a `Subsingleton`
* `Quot.hrecOn`, which uses `HEq (f a) (f b)` instead of a `sound p ▸ f a = f b` assummption
A dependent recursion principle for `Quot`. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
* `Quot.lift` is useful for defining non-dependent functions.
* `Quot.ind` is useful for proving theorems about quotients.
* `Quot.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
* `Quot.hrecOn` uses [heterogeneous equality](lean-manual://section/HEq) instead of rewriting with
`Quot.sound`.
`Quot.recOn` is a version of this recursor that takes the quotient parameter first.
-/
@[elab_as_elim] protected abbrev rec
(f : (a : α) → motive (Quot.mk r a))
@ -1687,7 +1721,22 @@ so you should consider the simpler versions if they apply:
(q : Quot r) : motive q :=
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
@[inherit_doc Quot.rec, elab_as_elim] protected abbrev recOn
/--
A dependent recursion principle for `Quot` that takes the quotient first. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
* `Quot.lift` is useful for defining non-dependent functions.
* `Quot.ind` is useful for proving theorems about quotients.
* `Quot.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
* `Quot.hrecOn` uses [heterogeneous equality](lean-manual://section/HEq) instead of rewriting with
`Quot.sound`.
`Quot.rec` is a version of this recursor that takes the quotient parameter last.
-/
@[elab_as_elim] protected abbrev recOn
(q : Quot r)
(f : (a : α) → motive (Quot.mk r a))
(h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
@ -1695,8 +1744,13 @@ so you should consider the simpler versions if they apply:
q.rec f h
/--
Dependent induction principle for a quotient, when the target type is a `Subsingleton`.
In this case the quotient's side condition is trivial so any function can be lifted.
An alternative induction principle for quotients that can be used when the target type is a
subsingleton, in which all elements are equal.
In these cases, the proof that the function respects the quotient's relation is trivial, so any
function can be lifted.
`Quot.rec` does not assume that the type is a subsingleton.
-/
@[elab_as_elim] protected abbrev recOnSubsingleton
[h : (a : α) → Subsingleton (motive (Quot.mk r a))]
@ -1708,9 +1762,11 @@ In this case the quotient's side condition is trivial so any function can be lif
apply Subsingleton.elim
/--
Heterogeneous dependent recursion principle for a quotient.
This may be easier to work with since it uses `HEq` instead of
an `Eq.ndrec` in the hypothesis.
A dependent recursion principle for `Quot` that uses [heterogeneous
equality](lean-manual://section/HEq), analogous to a [recursor](lean-manual://section/recursors) for
a structure.
`Quot.recOn` is a version of this recursor that uses `Eq` instead of `HEq`.
-/
protected abbrev hrecOn
(q : Quot r)
@ -1726,48 +1782,101 @@ end Quot
set_option linter.unusedVariables.funArgs false in
/--
`Quotient α s` is the same as `Quot α r`, but it is specialized to a setoid `s`
(that is, an equivalence relation) instead of an arbitrary relation.
Prefer `Quotient` over `Quot` if your relation is actually an equivalence relation.
Quotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
`Setoid`.
Set-theoretically, `Quotient s` can seen as the set of equivalence classes of `α` modulo the
`Setoid` instance's relation `s.r`. Functions from `Quotient s` must prove that they respect `s.r`:
to define a function `f : Quotient s → β`, it is necessary to provide `f' : α → β` and prove that
for all `x : α` and `y : α`, `s.r x y → f' x = f' y`. `Quotient.lift` implements this operation.
The key quotient operators are:
* `Quotient.mk` places elements of the underlying type `α` into the quotient.
* `Quotient.lift` allows the definition of functions from the quotient to some other type.
* `Quotient.sound` asserts the equality of elements related by `r`
* `Quotient.ind` is used to write proofs about quotients by assuming that all elements are
constructed with `Quotient.mk`.
`Quotient` is built on top of the primitive quotient type `Quot`, which does not require a proof
that the relation is an equivalence relation. `Quotient` should be used instead of `Quot` for
relations that actually are equivalence relations.
-/
def Quotient {α : Sort u} (s : Setoid α) :=
@Quot α Setoid.r
namespace Quotient
/-- The canonical quotient map into a `Quotient`. -/
/--
Places an element of a type into the quotient that equates terms according to an equivalence
relation.
The setoid instance is provided explicitly. `Quotient.mk'` uses instance synthesis instead.
Given `v : α`, `Quotient.mk s v : Quotient s` is like `v`, except all observations of `v`'s value
must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to other types, so long
as the mapping respects `s.r`.
-/
@[inline]
protected def mk {α : Sort u} (s : Setoid α) (a : α) : Quotient s :=
Quot.mk Setoid.r a
/--
The canonical quotient map into a `Quotient`.
(This synthesizes the setoid by typeclass inference.)
Places an element of a type into the quotient that equates terms according to an equivalence
relation.
The equivalence relation is found by synthesizing a `Setoid` instance. `Quotient.mk` instead expects
the instance to be provided explicitly.
Given `v : α`, `Quotient.mk' v : Quotient s` is like `v`, except all observations of `v`'s value
must respect `s.r`. `Quotient.lift` allows values in a quotient to be mapped to other types, so long
as the mapping respects `s.r`.
-/
protected def mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
Quotient.mk s a
/--
The analogue of `Quot.sound`: If `a` and `b` are related by the equivalence relation,
then they have equal equivalence classes.
The **quotient axiom**, which asserts the equality of elements related in the setoid.
Because `Quotient` is built on a lower-level type `Quot`, `Quotient.sound` is implemented as a
theorem. It is derived from `Quot.sound`, the soundness axiom for the lower-level quotient type
`Quot`.
-/
theorem sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b :=
Quot.sound
/--
The analogue of `Quot.lift`: if `f : α → β` respects the equivalence relation `≈`,
then it lifts to a function on `Quotient s` such that `lift f h (mk a) = f a`.
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.
Given `s : Setoid α` and a quotient `Quotient s`, applying a function `f : α → β` requires a proof
`h` that `f` respects the equivalence relation `s.r`. In this case, the function
`Quotient.lift f h : Quotient s → β` computes the same values as `f`.
`Quotient.liftOn` is a version of this operation that takes the quotient value as its first explicit
parameter.
-/
protected abbrev lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
Quot.lift f
/-- The analogue of `Quot.ind`: every element of `Quotient s` is of the form `Quotient.mk s a`. -/
/--
A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with `Quotient.mk`.
-/
protected theorem ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} : ((a : α) → motive (Quotient.mk s a)) → (q : Quotient s) → motive q :=
Quot.ind
/--
The analogue of `Quot.liftOn`: if `f : α → β` respects the equivalence relation `≈`,
then it lifts to a function on `Quotient s` such that `liftOn (mk a) f h = f a`.
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.
Given `s : Setoid α` and a quotient value `q : Quotient s`, applying a function `f : α → β` requires
a proof `c` that `f` respects the equivalence relation `s.r`. In this case, the term
`Quotient.liftOn q f h : β` reduces to the result of applying `f` to the underlying `α` value.
`Quotient.lift` is a version of this operation that takes the quotient value last, rather than
first.
-/
protected abbrev liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β :=
Quot.liftOn q f c
@ -1788,7 +1897,21 @@ variable {α : Sort u}
variable {s : Setoid α}
variable {motive : Quotient s → Sort v}
/-- The analogue of `Quot.rec` for `Quotient`. See `Quot.rec`. -/
/--
A dependent recursion principle for `Quotient`. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
* `Quotient.lift` is useful for defining non-dependent functions.
* `Quotient.ind` is useful for proving theorems about quotients.
* `Quotient.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
* `Quotient.hrecOn` uses heterogeneous equality instead of rewriting with `Quotient.sound`.
`Quotient.recOn` is a version of this recursor that takes the quotient parameter first.
-/
@[inline, elab_as_elim]
protected def rec
(f : (a : α) → motive (Quotient.mk s a))
@ -1797,7 +1920,21 @@ protected def rec
: motive q :=
Quot.rec f h q
/-- The analogue of `Quot.recOn` for `Quotient`. See `Quot.recOn`. -/
/--
A dependent recursion principle for `Quotient`. It is analogous to the
[recursor](lean-manual://section/recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
* `Quotient.lift` is useful for defining non-dependent functions.
* `Quotient.ind` is useful for proving theorems about quotients.
* `Quotient.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
* `Quotient.hrecOn` uses heterogeneous equality instead of rewriting with `Quotient.sound`.
`Quotient.rec` is a version of this recursor that takes the quotient parameter last.
-/
@[elab_as_elim]
protected abbrev recOn
(q : Quotient s)
@ -1806,7 +1943,15 @@ protected abbrev recOn
: motive q :=
Quot.recOn q f h
/-- The analogue of `Quot.recOnSubsingleton` for `Quotient`. See `Quot.recOnSubsingleton`. -/
/--
An alternative recursion or induction principle for quotients that can be used when the target type
is a subsingleton, in which all elements are equal.
In these cases, the proof that the function respects the quotient's equivalence relation is trivial,
so any function can be lifted.
`Quotient.rec` does not assume that the target type is a subsingleton.
-/
@[elab_as_elim]
protected abbrev recOnSubsingleton
[h : (a : α) → Subsingleton (motive (Quotient.mk s a))]
@ -1815,7 +1960,13 @@ protected abbrev recOnSubsingleton
: motive q :=
Quot.recOnSubsingleton (h := h) q f
/-- The analogue of `Quot.hrecOn` for `Quotient`. See `Quot.hrecOn`. -/
/--
A dependent recursion principle for `Quotient` that uses [heterogeneous
equality](lean-manual://section/HEq), analogous to a [recursor](lean-manual://section/recursors) for
a structure.
`Quotient.recOn` is a version of this recursor that uses `Eq` instead of `HEq`.
-/
@[elab_as_elim]
protected abbrev hrecOn
(q : Quotient s)
@ -1830,7 +1981,13 @@ universe uA uB uC
variable {α : Sort uA} {β : Sort uB} {φ : Sort uC}
variable {s₁ : Setoid α} {s₂ : Setoid β}
/-- Lift a binary function to a quotient on both arguments. -/
/--
Lifts a binary function from the underlying types to a binary function on quotients. The function
must respect both quotients' equivalence relations.
`Quotient.lift` is a version of this operation for unary functions. `Quotient.liftOn₂` is a version
that take the quotient parameters first.
-/
protected abbrev lift₂
(f : α → β → φ)
(c : (a₁ : α) → (b₁ : β) → (a₂ : α) → (b₂ : β) → a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
@ -1841,7 +1998,13 @@ protected abbrev lift₂
induction q₂ using Quotient.ind
apply c; assumption; apply Setoid.refl
/-- Lift a binary function to a quotient on both arguments. -/
/--
Lifts a binary function from the underlying types to a binary function on quotients. The function
must respect both quotients' equivalence relations.
`Quotient.liftOn` is a version of this operation for unary functions. `Quotient.lift₂` is a version
that take the quotient parameters last.
-/
protected abbrev liftOn₂
(q₁ : Quotient s₁)
(q₂ : Quotient s₂)
@ -1906,6 +2069,9 @@ private theorem rel.refl {s : Setoid α} (q : Quotient s) : rel q q :=
private theorem rel_of_eq {s : Setoid α} {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
fun h => Eq.ndrecOn h (rel.refl q₁)
/--
If two values are equal in a quotient, then they are related by its equivalence relation.
-/
theorem exact {s : Setoid α} {a b : α} : Quotient.mk s a = Quotient.mk s b → a ≈ b :=
fun h => rel_of_eq h
@ -1916,7 +2082,13 @@ universe uA uB uC
variable {α : Sort uA} {β : Sort uB}
variable {s₁ : Setoid α} {s₂ : Setoid β}
/-- Lift a binary function to a quotient on both arguments. -/
/--
An alternative induction or recursion operator for defining binary operations on quotients that can
be used when the target type is a subsingleton.
In these cases, the proof that the function respects the quotient's equivalence relation is trivial,
so any function can be lifted.
-/
@[elab_as_elim]
protected abbrev recOnSubsingleton₂
{motive : Quotient s₁ → Quotient s₂ → Sort uC}
@ -1976,28 +2148,39 @@ instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingl
/-! # Squash -/
/--
`Squash α` is the quotient of `α` by the always true relation.
It is empty if `α` is empty, otherwise it is a singleton.
(Thus it is unconditionally a `Subsingleton`.)
It is the "universal `Subsingleton`" mapped from `α`.
The quotient of `α` by the universal relation. The elements of `Squash α` are those of `α`, but all
of them are equal and cannot be distinguished.
It is similar to `Nonempty α`, which has the same properties, but unlike
`Nonempty` this is a `Type u`, that is, it is "data", and the compiler
represents an element of `Squash α` the same as `α` itself
(as compared to `Nonempty α`, whose elements are represented by a dummy value).
`Squash α` is a `Subsingleton`: it is empty if `α` is empty, otherwise it has just one element. It
is the “universal `Subsingleton`” mapped from `α`.
`Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
while `Nonempty.rec` can only do the same when `β` is a proposition.
`Nonempty α` also has these properties. It is a proposition, which means that its elements (i.e.
proofs) are erased from compiled code and represented by a dummy value. `Squash α` is a `Type u`,
and its representation in compiled code is identical to that of `α`.
Consequently, `Squash.lift` may extract an `α` value into any subsingleton type `β`, while
`Nonempty.rec` can only do the same when `β` is a proposition.
-/
def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
/-- The canonical quotient map into `Squash α`. -/
/--
Places a value into its squash type, in which it cannot be distinguished from any other.
-/
def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x
/--
A reasoning principle that allows proofs about squashed types to assume that all values are
constructed with `Squash.mk`.
-/
theorem Squash.ind {α : Sort u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
Quot.ind h
/-- If `β` is a subsingleton, then a function `α → β` lifts to `Squash α → β`. -/
/--
Extracts a squashed value into any subsingleton type.
If `β` is a subsingleton, a function `α → β` cannot distinguish between elements of `α` and thus
automatically respects the universal relation that `Squash` quotients with.
-/
@[inline] def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β :=
Quot.lift f (fun _ _ _ => Subsingleton.elim _ _) s

237
src/Init/Data/Array/Subarray.lean
View file

@ -10,15 +10,29 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
universe u v w
structure Subarray (α : Type u) where
/--
A region of some underlying array.
A subarray contains an array together with the start and end indices of a region of interest.
Subarrays can be used to avoid copying or allocating space, while being more convenient than
tracking the bounds by hand. The region of interest consists of every index that is both greater
than or equal to `start` and strictly less than `stop`.
-/
structure Subarray (α : Type u) where
/-- The underlying array. -/
array : Array α
/-- The starting index of the region of interest (inclusive). -/
start : Nat
/-- The ending index of the region of interest (exclusive). -/
stop : Nat
start_le_stop : start ≤ stop
stop_le_array_size : stop ≤ array.size
namespace Subarray
/--
Computes the size of the subarray.
-/
def size (s : Subarray α) : Nat :=
s.stop - s.start
@ -28,6 +42,11 @@ theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
apply Nat.le_trans (Nat.sub_le stop start)
assumption
/--
Extracts an element from the subarray.
The index is relative to the start of the subarray, rather than the underlying array.
-/
def get (s : Subarray α) (i : Fin s.size) : α :=
have : s.start + i.val < s.array.size := by
apply Nat.lt_of_lt_of_le _ s.stop_le_array_size
@ -40,12 +59,33 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
getElem xs i h := xs.get ⟨i, h⟩
/--
Extracts an element from the subarray, or returns a default value `v₀` when the index is out of
bounds.
The index is relative to the start and end of the subarray, rather than the underlying array.
-/
@[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
if h : i < s.size then s[i] else v₀
/--
Extracts an element from the subarray, or returns a default value when the index is out of bounds.
The index is relative to the start and end of the subarray, rather than the underlying array. The
default value is that provided by the `Inhabited α` instance.
-/
abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
getD s i default
/--
Shrinks the subarray by incrementing its starting index if possible, returning it unchanged if not.
Examples:
* `#[1,2,3].toSubarray.popFront.toArray = #[2, 3]`
* `#[1,2,3].toSubarray.popFront.popFront.toArray = #[3]`
* `#[1,2,3].toSubarray.popFront.popFront.popFront.toArray = #[]`
* `#[1,2,3].toSubarray.popFront.popFront.popFront.popFront.toArray = #[]`
-/
def popFront (s : Subarray α) : Subarray α :=
if h : s.start < s.stop then
{ s with start := s.start + 1, start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }
@ -54,6 +94,8 @@ def popFront (s : Subarray α) : Subarray α :=
/--
The empty subarray.
This empty subarray is backed by an empty array.
-/
protected def empty : Subarray α where
array := #[]
@ -88,46 +130,197 @@ protected opaque forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Mona
instance : ForIn m (Subarray α) α where
forIn := Subarray.forIn
/--
Folds a monadic operation from left to right over the elements in a subarray.
An accumulator of type `β` is constructed by starting with `init` and monadically combining each
element of the subarray with the current accumulator value in turn. The monad in question may permit
early termination or repetition.
Examples:
```lean example
#eval #["red", "green", "blue"].toSubarray.foldlM (init := "") fun acc x => do
let l ← Option.guard (· ≠ 0) x.length
return s!"{acc}({l}){x} "
```
```output
some "(3)red (5)green (4)blue "
```
```lean example
#eval #["red", "green", "blue"].toSubarray.foldlM (init := 0) fun acc x => do
let l ← Option.guard (· ≠ 5) x.length
return s!"{acc}({l}){x} "
```
```output
none
```
-/
@[inline]
def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β :=
as.array.foldlM f (init := init) (start := as.start) (stop := as.stop)
/--
Folds a monadic operation from right to left over the elements in a subarray.
An accumulator of type `β` is constructed by starting with `init` and monadically combining each
element of the subarray with the current accumulator value in turn, moving from the end to the
start. The monad in question may permit early termination or repetition.
Examples:
```lean example
#eval #["red", "green", "blue"].toSubarray.foldrM (init := "") fun x acc => do
let l ← Option.guard (· ≠ 0) x.length
return s!"{acc}({l}){x} "
```
```output
some "(4)blue (5)green (3)red "
```
```lean example
#eval #["red", "green", "blue"].toSubarray.foldrM (init := 0) fun x acc => do
let l ← Option.guard (· ≠ 5) x.length
return s!"{acc}({l}){x} "
```
```output
none
```
-/
@[inline]
def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m β :=
as.array.foldrM f (init := init) (start := as.stop) (stop := as.start)
/--
Checks whether any of the elements in a subarray satisfy a monadic Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that satisfies the predicate is found.
Example:
```lean example
#eval #["red", "green", "blue", "orange"].toSubarray.popFront.anyM fun x => do
IO.println x
pure (x == "blue")
```
```output
green
blue
```
```output
true
```
-/
@[inline]
def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool :=
as.array.anyM p (start := as.start) (stop := as.stop)
/--
Checks whether all of the elements in a subarray satisfy a monadic Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that does not satisfy the predicate is found.
Example:
```lean example
#eval #["red", "green", "blue", "orange"].toSubarray.popFront.allM fun x => do
IO.println x
pure (x.length == 5)
```
```output
green
blue
```
```output
false
```
-/
@[inline]
def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool :=
as.array.allM p (start := as.start) (stop := as.stop)
/--
Runs a monadic action on each element of a subarray.
The elements are processed starting at the lowest index and moving up.
-/
@[inline]
def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit :=
as.array.forM f (start := as.start) (stop := as.stop)
/--
Runs a monadic action on each element of a subarray, in reverse order.
The elements are processed starting at the highest index and moving down.
-/
@[inline]
def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit :=
as.array.forRevM f (start := as.stop) (stop := as.start)
/--
Folds an operation from left to right over the elements in a subarray.
An accumulator of type `β` is constructed by starting with `init` and combining each
element of the subarray with the current accumulator value in turn.
Examples:
* `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
* `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
-/
@[inline]
def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
Id.run <| as.foldlM f (init := init)
/--
Folds an operation from right to left over the elements in a subarray.
An accumulator of type `β` is constructed by starting with `init` and combining each element of the
subarray with the current accumulator value in turn, moving from the end to the start.
Examples:
* `#eval #["red", "green", "blue"].toSubarray.foldr (·.length + ·) 0 = 12`
* `#["red", "green", "blue"].toSubarray.popFront.foldlr (·.length + ·) 0 = 9`
-/
@[inline]
def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) : β :=
Id.run <| as.foldrM f (init := init)
/--
Checks whether any of the elements in a subarray satisfy a Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that satisfies the predicate is found.
-/
@[inline]
def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
Id.run <| as.anyM p
/--
Checks whether all of the elements in a subarray satisfy a Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that does not satisfy the predicate is found.
-/
@[inline]
def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
Id.run <| as.allM p
/--
Applies a monadic function to each element in a subarray in reverse order, stopping at the first
element for which the function succeeds by returning a value other than `none`. The succeeding value
is returned, or `none` if there is no success.
Example:
```lean example
#eval #["red", "green", "blue"].toSubarray.findSomeRevM? fun x => do
IO.println x
return Option.guard (· = 5) x.length
```
```output
blue
green
```
```output
some 5
```
-/
@[inline]
def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β) :=
let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
@ -142,10 +335,39 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
find i this
find as.size (Nat.le_refl _)
/--
Applies a monadic Boolean predicate to each element in a subarray in reverse order, stopping at the
first element that satisfies the predicate. The element that satisfies the predicate is returned, or
`none` if no element satisfies it.
Example:
```lean example
#eval #["red", "green", "blue"].toSubarray.findRevM? fun x => do
IO.println x
return (x.length = 5)
```
```output
blue
green
```
```output
some 5
```
-/
@[inline]
def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) : m (Option α) :=
as.findSomeRevM? fun a => return if (← p a) then some a else none
/--
Tests each element in a subarray with a Boolean predicate in reverse order, stopping at the first
element that satisfies the predicate. The element that satisfies the predicate is returned, or
`none` if no element satisfies the predicate.
Examples:
* `#["red", "green", "blue"].toSubarray.findRev? (·.length ≠ 4) = some "green"`
* `#["red", "green", "blue"].toSubarray.findRev? (fun _ => true) = some "blue"`
* `#["red", "green", "blue"].toSubarray 0 0 |>.findRev? (fun _ => true) = none`
-/
@[inline]
def findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α :=
Id.run <| as.findRevM? p
@ -155,6 +377,12 @@ end Subarray
namespace Array
variable {α : Type u}
/--
Returns a subarray of an array, with the given bounds.
If `start` or `stop` are not valid bounds for a subarray, then they are clamped to array's size.
Additionally, the starting index is clamped to the ending index.
-/
def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Subarray α :=
if h₂ : stop ≤ as.size then
if h₁ : start ≤ stop then
@ -177,6 +405,9 @@ def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Suba
start_le_stop := Nat.le_refl _,
stop_le_array_size := Nat.le_refl _ }
/--
Allocates a new array that contains the contents of the subarray.
-/
@[coe]
def ofSubarray (s : Subarray α) : Array α := Id.run do
let mut as := mkEmpty (s.stop - s.start)
@ -186,8 +417,11 @@ def ofSubarray (s : Subarray α) : Array α := Id.run do
instance : Coe (Subarray α) (Array α) := ⟨ofSubarray⟩
/-- A subarray with the provided bounds.-/
syntax:max term noWs "[" withoutPosition(term ":" term) "]" : term
/-- A subarray with the provided lower bound that extends to the rest of the array. -/
syntax:max term noWs "[" withoutPosition(term ":") "]" : term
/-- A subarray with the provided upper bound, starting at the index 0. -/
syntax:max term noWs "[" withoutPosition(":" term) "]" : term
macro_rules
@ -197,6 +431,7 @@ macro_rules
end Array
@[inherit_doc Array.ofSubarray]
def Subarray.toArray (s : Subarray α) : Array α :=
Array.ofSubarray s

3
src/Init/Data/Array/Subarray/Split.lean
View file

@ -20,7 +20,8 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
namespace Subarray
/--
Splits a subarray into two parts.
Splits a subarray into two parts, the first of which contains the first `i` elements and the second
of which contains the remainder.
-/
def split (s : Subarray α) (i : Fin s.size.succ) : (Subarray α × Subarray α) :=
let ⟨i', isLt⟩ := i

211
src/Init/Data/Fin/Basic.lean
View file

@ -14,22 +14,23 @@ instance coeToNat : CoeOut (Fin n) Nat :=
⟨fun v => v.val⟩
/--
From the empty type `Fin 0`, any desired result `α` can be derived. This is similar to `Empty.elim`.
The type `Fin 0` is uninhabited, so it can be used to derive any result whatsoever.
This is similar to `Empty.elim`. It can be thought of as a compiler-checked assertion that a code
path is unreachable, or a logical contradiction from which `False` and thus anything else could be
derived.
-/
def elim0.{u} {α : Sort u} : Fin 0 → α
| ⟨_, h⟩ => absurd h (not_lt_zero _)
/--
Returns the successor of the argument.
The successor, with an increased bound.
The bound in the result type is increased:
```
(2 : Fin 3).succ = (3 : Fin 4)
```
This differs from addition, which wraps around:
```
(2 : Fin 3) + 1 = (0 : Fin 3)
```
This differs from adding `1`, which instead wraps around.
Examples:
* `(2 : Fin 3).succ = (3 : Fin 4)`
* `(2 : Fin 3) + 1 = (0 : Fin 3)`
-/
def succ : Fin n → Fin (n + 1)
| ⟨i, h⟩ => ⟨i+1, Nat.succ_lt_succ h⟩
@ -53,7 +54,13 @@ protected def ofNat {n : Nat} (a : Nat) : Fin (n + 1) :=
-- We provide this because other similar types have a `toNat` function, but `simp` rewrites
-- `i.toNat` to `i.val`.
@[inline, inherit_doc val]
/--
Extracts the underlying `Nat` value.
This function is a synonym for `Fin.val`, which is the simp normal form. `Fin.val` is also a
coercion, so values of type `Fin n` are automatically converted to `Nat`s as needed.
-/
@[inline]
protected def toNat (i : Fin n) : Nat :=
i.val
@ -65,15 +72,34 @@ private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
have : n > 0 := Nat.lt_trans (Nat.zero_lt_succ _) h;
Nat.mod_lt _ this
/-- Addition modulo `n` -/
/--
Addition modulo `n`, usually invoked via the `+` operator.
Examples:
* `(2 : Fin 8) + (2 : Fin 8) = (4 : Fin 8)`
* `(2 : Fin 3) + (2 : Fin 3) = (1 : Fin 3)`
-/
protected def add : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, mlt h⟩
/-- Multiplication modulo `n` -/
/--
Multiplication modulo `n`, usually invoked via the `*` operator.
Examples:
* `(2 : Fin 10) * (2 : Fin 10) = (4 : Fin 10)`
* `(2 : Fin 10) * (7 : Fin 10) = (4 : Fin 10)`
* `(3 : Fin 10) * (7 : Fin 10) = (1 : Fin 10)`
-/
protected def mul : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, mlt h⟩
/-- Subtraction modulo `n` -/
/--
Subtraction modulo `n`, usually invoked via the `-` operator.
Examples:
* `(5 : Fin 11) - (3 : Fin 11) = (2 : Fin 11)`
* `(3 : Fin 11) - (5 : Fin 11) = (9 : Fin 11)`
-/
protected def sub : Fin n → Fin n → Fin n
/-
The definition of `Fin.sub` has been updated to improve performance.
@ -100,27 +126,76 @@ we are trying to minimize the number of Nat theorems
needed to bootstrap Lean.
-/
/--
Modulus of bounded numbers, usually invoked via the `%` operator.
The resulting value is that computed by the `%` operator on `Nat`.
-/
protected def mod : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
/--
Division of bounded numbers, usually invoked via the `/` operator.
The resulting value is that computed by the `/` operator on `Nat`. In particular, the result of
division by `0` is `0`.
Examples:
* `(5 : Fin 10) / (2 : Fin 10) = (2 : Fin 10)`
* `(5 : Fin 10) / (0 : Fin 10) = (0 : Fin 10)`
* `(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)`
-/
protected def div : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
/--
Modulus of bounded numbers with respect to a `Nat`.
The resulting value is that computed by the `%` operator on `Nat`.
-/
def modn : Fin n → Nat → Fin n
| ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
/--
Bitwise and.
-/
def land : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
/--
Bitwise or.
-/
def lor : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
/--
Bitwise xor (“exclusive or”).
-/
def xor : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, mlt h⟩
/--
Bitwise left shift of bounded numbers, with wraparound on overflow.
Examples:
* `(1 : Fin 10) <<< (1 : Fin 10) = (2 : Fin 10)`
* `(1 : Fin 10) <<< (3 : Fin 10) = (8 : Fin 10)`
* `(1 : Fin 10) <<< (4 : Fin 10) = (6 : Fin 10)`
-/
def shiftLeft : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, mlt h⟩
/--
Bitwise right shift of bounded numbers.
This operator corresponds to logical rather than arithmetic bit shifting. The new bits are always
`0`.
Examples:
* `(15 : Fin 16) >>> (1 : Fin 16) = (7 : Fin 16)`
* `(15 : Fin 16) >>> (2 : Fin 16) = (3 : Fin 16)`
* `(15 : Fin 17) >>> (2 : Fin 17) = (3 : Fin 17)`
-/
def shiftRight : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, mlt h⟩
@ -174,39 +249,125 @@ theorem val_lt_of_le (i : Fin b) (h : b ≤ n) : i.val < n :=
protected theorem pos (i : Fin n) : 0 < n :=
Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
/-- The greatest value of `Fin (n+1)`. -/
/--
The greatest value of `Fin (n+1)`, namely `n`.
Examples:
* `Fin.last 4 = (4 : Fin 5)`
* `(Fin.last 0).val = (0 : Nat)`
-/
@[inline] def last (n : Nat) : Fin (n + 1) := ⟨n, n.lt_succ_self⟩
/-- `castLT i h` embeds `i` into a `Fin` where `h` proves it belongs into. -/
/--
Replaces the bound with another that is suitable for the value.
The proof embedded in `i` can be used to cast to a larger bound even if the concrete value is not
known.
Examples:
```lean example
example : Fin 12 := (7 : Fin 10).castLT (by decide : 7 < 12)
```
```lean example
example (i : Fin 10) : Fin 12 :=
i.castLT <| by
cases i; simp; omega
```
-/
@[inline] def castLT (i : Fin m) (h : i.1 < n) : Fin n := ⟨i.1, h⟩
/-- `castLE h i` embeds `i` into a larger `Fin` type. -/
/--
Coarsens a bound to one at least as large.
See also `Fin.castAdd` for a version that represents the larger bound with addition rather than an
explicit inequality proof.
-/
@[inline] def castLE (h : n ≤ m) (i : Fin n) : Fin m := ⟨i, Nat.lt_of_lt_of_le i.2 h⟩
/-- `cast eq i` embeds `i` into an equal `Fin` type. -/
/--
Uses a proof that two bounds are equal to allow a value bounded by one to be used with the other.
In other words, when `eq : n = m`, `Fin.cast eq i` converts `i : Fin n` into a `Fin m`.
-/
@[inline] protected def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩
/-- `castAdd m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAdd` and `Fin.addNat`. -/
/--
Coarsens a bound to one at least as large.
See also `Fin.natAdd` and `Fin.addNat` for addition functions that increase the bound, and
`Fin.castLE` for a version that uses an explicit inequality proof.
-/
@[inline] def castAdd (m) : Fin n → Fin (n + m) :=
castLE <| Nat.le_add_right n m
/-- `castSucc i` embeds `i : Fin n` in `Fin (n+1)`. -/
/--
Coarsens a bound by one.
-/
@[inline] def castSucc : Fin n → Fin (n + 1) := castAdd 1
/-- `addNat m i` adds `m` to `i`, generalizes `Fin.succ`. -/
/--
Adds a natural number to a `Fin`, increasing the bound.
This is a generalization of `Fin.succ`.
`Fin.natAdd` is a version of this function that takes its `Nat` parameter first.
Examples:
* `Fin.addNat (5 : Fin 8) 3 = (8 : Fin 11)`
* `Fin.addNat (0 : Fin 8) 1 = (1 : Fin 9)`
* `Fin.addNat (1 : Fin 8) 2 = (3 : Fin 10)`
-/
def addNat (i : Fin n) (m) : Fin (n + m) := ⟨i + m, Nat.add_lt_add_right i.2 _⟩
/-- `natAdd n i` adds `n` to `i` "on the left". -/
/--
Adds a natural number to a `Fin`, increasing the bound.
This is a generalization of `Fin.succ`.
`Fin.addNat` is a version of this function that takes its `Nat` parameter second.
Examples:
* `Fin.natAdd 3 (5 : Fin 8) = (8 : Fin 11)`
* `Fin.natAdd 1 (0 : Fin 8) = (1 : Fin 9)`
* `Fin.natAdd 1 (2 : Fin 8) = (3 : Fin 9)`
-/
def natAdd (n) (i : Fin m) : Fin (n + m) := ⟨n + i, Nat.add_lt_add_left i.2 _⟩
/-- Maps `0` to `n-1`, `1` to `n-2`, ..., `n-1` to `0`. -/
/--
Replaces a value with its difference from the largest value in the type.
Considering the values of `Fin n` as a sequence `0`, `1`, …, `n-2`, `n-1`, `Fin.rev` finds the
corresponding element of the reversed sequence. In other words, it maps `0` to `n-1`, `1` to `n-2`,
..., and `n-1` to `0`.
Examples:
* `(5 : Fin 6).rev = (0 : Fin 6)`
* `(0 : Fin 6).rev = (5 : Fin 6)`
* `(2 : Fin 5).rev = (2 : Fin 5)`
-/
@[inline] def rev (i : Fin n) : Fin n := ⟨n - (i + 1), Nat.sub_lt i.pos (Nat.succ_pos _)⟩
/-- `subNat i h` subtracts `m` from `i`, generalizes `Fin.pred`. -/
/--
Subtraction of a natural number from a `Fin`, with the bound narrowed.
This is a generalization of `Fin.pred`. It is guaranteed to not underflow or wrap around.
Examples:
* `(5 : Fin 9).subNat 2 (by decide) = (3 : Fin 7)`
* `(5 : Fin 9).subNat 0 (by decide) = (5 : Fin 9)`
* `(3 : Fin 9).subNat 3 (by decide) = (0 : Fin 6)`
-/
@[inline] def subNat (m) (i : Fin (n + m)) (h : m ≤ i) : Fin n :=
⟨i - m, Nat.sub_lt_right_of_lt_add h i.2⟩
/-- Predecessor of a nonzero element of `Fin (n+1)`. -/
/--
The predecessor of a non-zero element of `Fin (n+1)`, with the bound decreased.
Examples:
* `(4 : Fin 8).pred (by decide) = (3 : Fin 7)`
* `(1 : Fin 2).pred (by decide) = (0 : Fin 1)`
-/
@[inline] def pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n :=
subNat 1 i <| Nat.pos_of_ne_zero <| mt (Fin.eq_of_val_eq (j := 0)) h

24
src/Init/Data/Fin/Fold.lean
View file

@ -10,14 +10,26 @@ import Init.Data.Fin.Lemmas
namespace Fin
/-- Folds over `Fin n` from the left: `foldl 3 f x = f (f (f x 0) 1) 2`. -/
/--
Combine all the values that can be represented by `Fin n` with an initial value, starting at `0` and
nesting to the left.
Example:
* `Fin.foldl 3 (· + ·.val) (0 : Nat) = ((0 + (0 : Fin 3).val) + (1 : Fin 3).val) + (2 : Fin 3).val`
-/
@[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
/-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)` -/
@[semireducible, specialize] loop (x : α) (i : Nat) : α :=
if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
termination_by n - i
/-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
/--
Combine all the values that can be represented by `Fin n` with an initial value, starting at `n - 1`
and nesting to the right.
Example:
* `Fin.foldr 3 (·.val + ·) (0 : Nat) = (0 : Fin 3).val + ((1 : Fin 3).val + ((2 : Fin 3).val + 0))`
-/
@[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop n (Nat.le_refl n) init where
/-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))` -/
@[specialize] loop : (i : _) → i ≤ n → α → α
@ -26,7 +38,9 @@ namespace Fin
termination_by structural i => i
/--
Folds a monadic function over `Fin n` from left to right:
Folds a monadic function over all the values in `Fin n` from left to right, starting with `0`.
It is the sequence of steps:
```
Fin.foldlM n f x₀ = do
let x₁ ← f x₀ 0
@ -53,7 +67,9 @@ Fin.foldlM n f x₀ = do
decreasing_by decreasing_trivial_pre_omega
/--
Folds a monadic function over `Fin n` from right to left:
Folds a monadic function over `Fin n` from right to left, starting with `n-1`.
It is the sequence of steps:
```
Fin.foldrM n f xₙ = do
let xₙ₋₁ ← f (n-1) xₙ

30
src/Init/Data/Fin/Iterate.lean
View file

@ -10,10 +10,18 @@ import Init.Data.Fin.Basic
namespace Fin
/--
`hIterateFrom f i bnd a` applies `f` over indices `[i:n]` to compute `P n`
from `P i`.
Applies an index-dependent function `f` to all of the values in `[i:n]`, starting at `i` with an
initial accumulator `a`.
See `hIterate` below for more details.
Concretely, `Fin.hIterateFrom P f i a` is equal to
```lean
a |> f i |> f (i + 1) |> ... |> f (n - 1)
```
Theorems about `Fin.hIterateFrom` can be proven using the general theorem `Fin.hIterateFrom_elim` or
other more specialized theorems.
`Fin.hIterate` is a variant that always starts at `0`.
-/
def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.val+1))
(i : Nat) (ubnd : i ≤ n) (a : P i) : P n :=
@ -26,20 +34,18 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
decreasing_by decreasing_trivial_pre_omega
/--
`hIterate` is a heterogeneous iterative operation that applies a
index-dependent function `f` to a value `init : P start` a total of
`stop - start` times to produce a value of type `P stop`.
Applies an index-dependent function to all the values less than the given bound `n`, starting at
`0` with an accumulator.
Concretely, `hIterate start stop f init` is equal to
Concretely, `Fin.hIterate P init f` is equal to
```lean
init |> f start _ |> f (start+1) _ ... |> f (end-1) _
init |> f 0 |> f 1 |> ... |> f (n-1)
```
Because it is heterogeneous and must return a value of type `P stop`,
`hIterate` requires proof that `start ≤ stop`.
Theorems about `Fin.hIterate` can be proven using the general theorem `Fin.hIterate_elim` or other more
specialized theorems.
One can prove properties of `hIterate` using the general theorem
`hIterate_elim` or other more specialized theorems.
`Fin.hIterateFrom` is a variant that takes a custom starting value instead of `0`.
-/
def hIterate (P : Nat → Sort _) {n : Nat} (init : P 0) (f : ∀(i : Fin n), P i.val → P (i.val+1)) :
P n :=

108
src/Init/Data/Fin/Lemmas.lean
View file

@ -670,12 +670,20 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
@[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
natAdd n (subNat n (i.cast (Nat.add_comm ..)) h) = i := by simp [← cast_addNat]
/-! ### recursion and induction principles -/
/-! ### Recursion and induction principles -/
/-- Define `motive n i` by induction on `i : Fin n` interpreted as `(0 : Fin (n - i)).succ.succ…`.
This function has two arguments: `zero n` defines `0`-th element `motive (n+1) 0` of an
`(n+1)`-tuple, and `succ n i` defines `(i+1)`-st element of `(n+1)`-tuple based on `n`, `i`, and
`i`-th element of `n`-tuple. -/
/--
An induction principle for `Fin` that considers a given `i : Fin n` as given by a sequence of `i`
applications of `Fin.succ`.
The cases in the induction are:
* `zero` demonstrates the motive for `(0 : Fin (n + 1))` for all bounds `n`
* `succ` demonstrates the motive for `Fin.succ` applied to an arbitrary `Fin` for an arbitrary
bound `n`
Unlike `Fin.induction`, the motive quantifies over the bound, and the bound varies at each inductive
step. `Fin.succRecOn` is a version of this induction principle that takes the `Fin` argument first.
-/
-- FIXME: Performance review
@[elab_as_elim] def succRec {motive : ∀ n, Fin n → Sort _}
(zero : ∀ n, motive n.succ (0 : Fin (n + 1)))
@ -684,13 +692,18 @@ This function has two arguments: `zero n` defines `0`-th element `motive (n+1) 0
| Nat.succ n, ⟨0, _⟩ => by rw [mk_zero]; exact zero n
| Nat.succ _, ⟨Nat.succ i, h⟩ => succ _ _ (succRec zero succ ⟨i, Nat.lt_of_succ_lt_succ h⟩)
/-- Define `motive n i` by induction on `i : Fin n` interpreted as `(0 : Fin (n - i)).succ.succ…`.
This function has two arguments:
`zero n` defines the `0`-th element `motive (n+1) 0` of an `(n+1)`-tuple, and
`succ n i` defines the `(i+1)`-st element of an `(n+1)`-tuple based on `n`, `i`,
and the `i`-th element of an `n`-tuple.
/--
An induction principle for `Fin` that considers a given `i : Fin n` as given by a sequence of `i`
applications of `Fin.succ`.
A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
The cases in the induction are:
* `zero` demonstrates the motive for `(0 : Fin (n + 1))` for all bounds `n`
* `succ` demonstrates the motive for `Fin.succ` applied to an arbitrary `Fin` for an arbitrary
bound `n`
Unlike `Fin.induction`, the motive quantifies over the bound, and the bound varies at each inductive
step. `Fin.succRec` is a version of this induction principle that takes the `Fin` argument last.
-/
-- FIXME: Performance review
@[elab_as_elim] def succRecOn {n : Nat} (i : Fin n) {motive : ∀ n, Fin n → Sort _}
(zero : ∀ n, motive (n + 1) 0) (succ : ∀ n i, motive n i → motive (Nat.succ n) i.succ) :
@ -705,9 +718,17 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
cases i; rfl
/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
This function has two arguments: `zero` handles the base case on `motive 0`,
and `succ` defines the inductive step using `motive i.castSucc`.
/--
Proves a statement by induction on the underlying `Nat` value in a `Fin (n + 1)`.
For the induction:
* `zero` is the base case, demonstrating `motive 0`.
* `succ` is the inductive step, assuming the motive for `i : Fin n` (lifted to `Fin (n + 1)` with
`Fin.castSucc`) and demonstrating it for `i.succ`.
`Fin.inductionOn` is a version of this induction principle that takes the `Fin` as its first
parameter, `Fin.cases` is the corresponding case analysis operator, and `Fin.reverseInduction` is a
version that starts at the greatest value instead of `0`.
-/
-- FIXME: Performance review
@[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
@ -728,18 +749,30 @@ where
(succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := rfl
/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
This function has two arguments: `zero` handles the base case on `motive 0`,
and `succ` defines the inductive step using `motive i.castSucc`.
/--
Proves a statement by induction on the underlying `Nat` value in a `Fin (n + 1)`.
A version of `Fin.induction` taking `i : Fin (n + 1)` as the first argument.
For the induction:
* `zero` is the base case, demonstrating `motive 0`.
* `succ` is the inductive step, assuming the motive for `i : Fin n` (lifted to `Fin (n + 1)` with
`Fin.castSucc`) and demonstrating it for `i.succ`.
`Fin.induction` is a version of this induction principle that takes the `Fin` as its last
parameter.
-/
-- FIXME: Performance review
@[elab_as_elim] def inductionOn (i : Fin (n + 1)) {motive : Fin (n + 1) → Sort _} (zero : motive 0)
(succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) : motive i := induction zero succ i
/-- Define `f : Π i : Fin n.succ, motive i` by separately handling the cases `i = 0` and
`i = j.succ`, `j : Fin n`. -/
/--
Proves a statement by cases on the underlying `Nat` value in a `Fin (n + 1)`.
The two cases are:
* `zero`, used when the value is of the form `(0 : Fin (n + 1))`
* `succ`, used when the value is of the form `(j : Fin n).succ`
The corresponding induction principle is `Fin.induction`.
-/
@[elab_as_elim] def cases {motive : Fin (n + 1) → Sort _}
(zero : motive 0) (succ : ∀ i : Fin n, motive i.succ) :
∀ i : Fin (n + 1), motive i := induction zero fun i _ => succ i
@ -777,9 +810,14 @@ theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a =
simp only [forall_fin_two]; decide
/--
Define `motive i` by reverse induction on `i : Fin (n + 1)` via induction on the underlying `Nat`
value. This function has two arguments: `last` handles the base case on `motive (Fin.last n)`,
and `cast` defines the inductive step using `motive i.succ`, inducting downwards.
Proves a statement by reverse induction on the underlying `Nat` value in a `Fin (n + 1)`.
For the induction:
* `last` is the base case, demonstrating `motive (Fin.last n)`.
* `cast` is the inductive step, assuming the motive for `(j : Fin n).succ` and demonstrating it for
the predecessor `j.castSucc`.
`Fin.induction` is the non-reverse induction principle.
-/
@[elab_as_elim] def reverseInduction {motive : Fin (n + 1) → Sort _} (last : motive (Fin.last n))
(cast : ∀ i : Fin n, motive i.succ → motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
@ -802,8 +840,16 @@ decreasing_by decreasing_with
succ i (reverseInduction zero succ i.succ) := by
rw [reverseInduction, dif_neg (Fin.ne_of_lt (Fin.castSucc_lt_last i))]; rfl
/-- Define `f : Π i : Fin n.succ, motive i` by separately handling the cases `i = Fin.last n` and
`i = j.castSucc`, `j : Fin n`. -/
/--
Proves a statement by cases on the underlying `Nat` value in a `Fin (n + 1)`, checking whether the
value is the greatest representable or a predecessor of some other.
The two cases are:
* `last`, used when the value is `Fin.last n`
* `cast`, used when the value is of the form `(j : Fin n).succ`
The corresponding induction principle is `Fin.reverseInduction`.
-/
@[elab_as_elim] def lastCases {n : Nat} {motive : Fin (n + 1) → Sort _} (last : motive (Fin.last n))
(cast : ∀ i : Fin n, motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
reverseInduction last (fun i _ => cast i) i
@ -816,8 +862,16 @@ decreasing_by decreasing_with
(i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i :=
reverseInduction_castSucc ..
/-- Define `f : Π i : Fin (m + n), motive i` by separately handling the cases `i = castAdd n i`,
`j : Fin m` and `i = natAdd m j`, `j : Fin n`. -/
/--
A case analysis operator for `i : Fin (m + n)` that separately handles the cases where `i < m` and
where `m ≤ i < m + n`.
The first case, where `i < m`, is handled by `left`. In this case, `i` can be represented as
`Fin.castAdd n (j : Fin m)`.
The second case, where `m ≤ i < m + n`, is handled by `right`. In this case, `i` can be represented
as `Fin.natAdd m (j : Fin n)`.
-/
@[elab_as_elim] def addCases {m n : Nat} {motive : Fin (m + n) → Sort u}
(left : ∀ i, motive (castAdd n i)) (right : ∀ i, motive (natAdd m i))
(i : Fin (m + n)) : motive i :=

16
src/Init/Data/Fin/Log2.lean
View file

@ -6,4 +6,20 @@ Authors: Henrik Böving
prelude
import Init.Data.Nat.Log2
set_option linter.missingDocs true
/--
Logarithm base 2 for bounded numbers.
The resulting value is the same as that computed by `Nat.log2`. In particular, the result for `0` is
`0`.
Examples:
* `(8 : Fin 10).log2 = (3 : Fin 10)`
* `(7 : Fin 10).log2 = (2 : Fin 10)`
* `(4 : Fin 10).log2 = (2 : Fin 10)`
* `(3 : Fin 10).log2 = (1 : Fin 10)`
* `(1 : Fin 10).log2 = (0 : Fin 10)`
* `(0 : Fin 10).log2 = (0 : Fin 10)`
-/
def Fin.log2 (n : Fin m) : Fin m := ⟨Nat.log2 n.val, Nat.lt_of_le_of_lt (Nat.log2_le_self n.val) n.isLt⟩

6
src/Init/Data/Format/Instances.lean
View file

@ -23,6 +23,12 @@ instance [ToFormat α] : ToFormat (List α) where
instance [ToFormat α] : ToFormat (Array α) where
format a := "#" ++ format a.toList
/--
Formats an optional value, with no expectation that the Lean parser should be able to parse the
result.
This function is usually accessed through the `ToFormat (Option α)` instance.
-/
def Option.format {α : Type u} [ToFormat α] : Option α → Format
| none => "none"
| some a => "some " ++ Std.format a

15
src/Init/Data/Function.lean
View file

@ -9,10 +9,23 @@ import Init.Core
namespace Function
/--
Transforms a function from pairs into an equivalent two-parameter function.
Examples:
* `Function.curry (fun (x, y) => x + y) 3 5 = 8`
* `Function.curry Prod.swap 3 "five" = ("five", 3)`
-/
@[inline]
def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
/-- Interpret a function with two arguments as a function on `α × β` -/
/--
Transforms a two-parameter function into an equivalent function from pairs.
Examples:
* `Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]`
* `[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]`
-/
@[inline]
def uncurry : (α → β → φ) → α × β → φ := fun f a => f a.1 a.2

10
src/Init/Data/Hashable.lean
View file

@ -75,13 +75,19 @@ instance (P : Prop) : Hashable P where
@[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
mixHash u 11
/-- `LawfulHashable α` says that the `BEq α` and `Hashable α` instances on `α` are compatible, i.e.,
that `a == b` implies `hash a = hash b`. This is automatic if the `BEq` instance is lawful.
/--
The `BEq α` and `Hashable α` instances on `α` are compatible. This means that that `a == b` implies
`hash a = hash b`.
This is automatic if the `BEq` instance is lawful.
-/
class LawfulHashable (α : Type u) [BEq α] [Hashable α] where
/-- If `a == b`, then `hash a = hash b`. -/
hash_eq (a b : α) : a == b → hash a = hash b
/--
A lawful hash function respects its Boolean equality test.
-/
theorem hash_eq [BEq α] [Hashable α] [LawfulHashable α] {a b : α} : a == b → hash a = hash b :=
LawfulHashable.hash_eq a b

38
src/Init/Data/Nat/Fold.lean
View file

@ -191,25 +191,43 @@ end Nat
namespace Prod
/--
`(start, stop).foldI f a` evaluates `f` on all the numbers
Combines an initial value with each natural number from in a range, in increasing order.
In particular, `(start, stop).foldI f init` applies `f`on all the numbers
from `start` (inclusive) to `stop` (exclusive) in increasing order:
* `(5, 8).foldI f init = init |> f 5 |> f 6 |> f 7`
Examples:
* `(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = (#[] |>.push 5 |>.push 6 |>.push 7)`
* `(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]`
* `(5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]`
-/
@[inline] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → α → α) (a : α) : α :=
(i.2 - i.1).fold (fun j _ => f (i.1 + j) (by omega) (by omega)) a
@[inline] def foldI {α : Type u} (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → α → α) (init : α) : α :=
(i.2 - i.1).fold (fun j _ => f (i.1 + j) (by omega) (by omega)) init
/--
`(start, stop).anyI f a` returns true if `f` is true for some natural number
from `start` (inclusive) to `stop` (exclusive):
* `(5, 8).anyI f = f 5 || f 6 || f 7`
Checks whether a predicate holds for any natural number in a range.
In particular, `(start, stop).allI f` returns true if `f` is true for any natural number from
`start` (inclusive) to `stop` (exclusive).
Examples:
* `(5, 8).anyI (fun j _ _ => j == 6) = (5 == 6) || (6 == 6) || (7 == 6)`
* `(5, 8).anyI (fun j _ _ => j % 2 = 0) = true`
* `(6, 6).anyI (fun j _ _ => j % 2 = 0) = false`
-/
@[inline] def anyI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
(i.2 - i.1).any (fun j _ => f (i.1 + j) (by omega) (by omega))
/--
`(start, stop).allI f a` returns true if `f` is true for all natural numbers
from `start` (inclusive) to `stop` (exclusive):
* `(5, 8).anyI f = f 5 && f 6 && f 7`
Checks whether a predicate holds for all natural numbers in a range.
In particular, `(start, stop).allI f` returns true if `f` is true for all natural numbers from
`start` (inclusive) to `stop` (exclusive).
Examples:
* `(5, 8).allI (fun j _ _ => j < 10) = (5 < 10) && (6 < 10) && (7 < 10)`
* `(5, 8).allI (fun j _ _ => j % 2 = 0) = false`
* `(6, 7).allI (fun j _ _ => j % 2 = 0) = true`
-/
@[inline] def allI (i : Nat × Nat) (f : (j : Nat) → i.1 ≤ j → j < i.2 → Bool) : Bool :=
(i.2 - i.1).all (fun j _ => f (i.1 + j) (by omega) (by omega))

34
src/Init/Data/Option/Attach.lean
View file

@ -18,16 +18,30 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
@[inline] private unsafe def attachWithImpl
(o : Option α) (P : α → Prop) (_ : ∀ x ∈ o, P x) : Option {x // P x} := unsafeCast o
/-- "Attach" a proof `P x` that holds for the element of `o`, if present,
to produce a new option with the same element but in the type `{x // P x}`. -/
/--
“Attaches” a proof that some predicate holds for an optional value, if present, returning a subtype
that expresses this fact.
This function is primarily used to implement `Option.attach`, which allows definitions by
well-founded recursion that use iteration operators (such as `Option.map`) to prove that an optional
value drawn from a parameter is smaller than the parameter. This allows the well-founded recursion
mechanism to prove that the function terminates.
-/
@[implemented_by attachWithImpl] def attachWith
(xs : Option α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Option {x // P x} :=
match xs with
| none => none
| some x => some ⟨x, H x (mem_some_self x)⟩
/-- "Attach" the proof that the element of `xs`, if present, is in `xs`
to produce a new option with the same elements but in the type `{x // x ∈ xs}`. -/
/--
“Attaches” a proof that an optional value, if present, is indeed this value, returning a subtype
that expresses this fact.
This function is primarily used to allow definitions by well-founded recursion that use iteration
operators (such as `Option.map`) to prove that an optional value drawn from a parameter is smaller
than the parameter. This allows the well-founded recursion mechanism to prove that the function
terminates.
-/
@[inline] def attach (xs : Option α) : Option {x // x ∈ xs} := xs.attachWith _ fun _ => id
@[simp] theorem attach_none : (none : Option α).attach = none := rfl
@ -200,11 +214,15 @@ Further, we provide simp lemmas that push `unattach` inwards.
-/
/--
A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
It is introduced as an intermediate step by lemmas such as `map_subtype`,
and is ideally subsequently simplified away by `unattach_attach`.
Remove an attached proof that the value in an `Option` is indeed that value.
If not, usually the right approach is `simp [Option.unattach, -Option.map_subtype]` to unfold.
This function is usually inserted automatically by Lean, rather than explicitly in code. It is
introduced as an intermediate step during the elaboration of definitions by well-founded recursion.
If this function is encountered in a proof state, the right approach is usually the tactic
`simp [Option.unattach, -Option.map_subtype]`.
It is a synonym for `Option.map Subtype.val`.
-/
def unattach {α : Type _} {p : α → Prop} (o : Option { x // p x }) := o.map (·.val)

281
src/Init/Data/Option/Basic.lean
View file

@ -24,7 +24,15 @@ def getM [Alternative m] : Option α → m α
@[simp] theorem isSome_none : @isSome α none = false := rfl
@[simp] theorem isSome_some : isSome (some a) = true := rfl
/-- Returns `true` on `none` and `false` on `some x`. -/
/--
Returns `true` on `none` and `false` on `some x`.
This function is more flexible than `(· == none)` because it does not require a `BEq α` instance.
Examples:
* `(none : Option Nat).isNone = true`
* `(some Nat.add).isNone = false`
-/
@[inline] def isNone : Option α → Bool
| some _ => false
| none => true
@ -33,17 +41,46 @@ def getM [Alternative m] : Option α → m α
@[simp] theorem isNone_some : isNone (some a) = false := rfl
/--
`x?.isEqSome y` is equivalent to `x? == some y`, but avoids an allocation.
Checks whether an optional value is both present and equal to some other value.
Given `x? : Option α` and `y : α`, `x?.isEqSome y` is equivalent to `x? == some y`. It is more
efficient because it avoids an allocation.
-/
@[inline] def isEqSome [BEq α] : Option α → α → Bool
| some a, b => a == b
| none, _ => false
/--
Sequencing of `Option` computations.
From the perspective of `Option` as computations that might fail, this function sequences
potentially-failing computations, failing if either fails. From the perspective of `Option` as a
collection with at most one element, the function is applied to the element if present, and the
final result is empty if either the initial or the resulting collections are empty.
This function is often accessed via the `>>=` operator from the `Bind (Option α)` instance, or
implicitly via `do`-notation, but it is also idiomatic to call it using [generalized field
notation](lean-manual://section/generalized-field-notation).
Examples:
* `none.bind (fun x => some x) = none`
* `(some 4).bind (fun x => some x) = some 4`
* `none.bind (Option.guard (· > 2)) = none`
* `(some 2).bind (Option.guard (· > 2)) = none`
* `(some 4).bind (Option.guard (· > 2)) = some 4`
-/
@[inline] protected def bind : Option α → (α → Option β) → Option β
| none, _ => none
| some a, f => f a
/-- Runs `f` on `o`'s value, if any, and returns its result, or else returns `none`. -/
/--
Runs the monadic action `f` on `o`'s value, if any, and returns the result, or `none` if there is
no value.
From the perspective of `Option` as a collection with at most one element, the monadic the function
is applied to the element if present, and the final result is empty if either the initial or the
resulting collections are empty.
-/
@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
if let some a := o then
return (← f a)
@ -51,8 +88,13 @@ def getM [Alternative m] : Option α → m α
return none
/--
Runs a monadic function `f` on an optional value.
If the optional value is `none` the function is not called.
Runs a monadic function `f` on an optional value, returning the result. If the optional value is
`none`, the function is not called and the result is also `none`.
From the perspective of `Option` as a container with at most one element, this is analogous to
`List.mapM`, returning the result of running the monadic function on all elements of the container.
`Option.mapA` is the corresponding operation for applicative functors.
-/
@[inline] protected def mapM [Monad m] (f : α → m β) (o : Option α) : m (Option β) := do
if let some a := o then
@ -63,25 +105,51 @@ If the optional value is `none` the function is not called.
theorem map_id : (Option.map id : Option α → Option α) = id :=
funext (fun o => match o with | none => rfl | some _ => rfl)
/-- Keeps an optional value only if it satisfies the predicate `p`. -/
/--
Keeps an optional value only if it satisfies a Boolean predicate.
If `Option` is thought of as a collection that contains at most one element, then `Option.filter` is
analogous to `List.filter` or `Array.filter`.
Examples:
* `(some 5).filter (· % 2 == 0) = none`
* `(some 4).filter (· % 2 == 0) = some 4`
* `none.filter (fun x : Nat => x % 2 == 0) = none`
* `none.filter (fun x : Nat => true) = none`
-/
@[always_inline, inline] protected def filter (p : α → Bool) : Option α → Option α
| some a => if p a then some a else none
| none => none
/-- Checks that an optional value satisfies a predicate `p` or is `none`. -/
/--
Checks whether an optional value either satisfies a Boolean predicate or is `none`.
Examples:
* `(some 33).all (· % 2 == 0) = false
* `(some 22).all (· % 2 == 0) = true
* `none.all (fun x : Nat => x % 2 == 0) = true
-/
@[always_inline, inline] protected def all (p : α → Bool) : Option α → Bool
| some a => p a
| none => true
/-- Checks that an optional value is not `none` and the value satisfies a predicate `p`. -/
/--
Checks whether an optional value is not `none` and satisfies a Boolean predicate.
Examples:
* `(some 33).any (· % 2 == 0) = false
* `(some 22).any (· % 2 == 0) = true
* `none.any (fun x : Nat => true) = false
-/
@[always_inline, inline] protected def any (p : α → Bool) : Option α → Bool
| some a => p a
| none => false
/--
Implementation of `OrElse`'s `<|>` syntax for `Option`. If the first argument is `some a`, returns
`some a`, otherwise evaluates and returns the second argument. See also `or` for a version that is
strict in the second argument.
`some a`, otherwise evaluates and returns the second argument.
See also `or` for a version that is strict in the second argument.
-/
@[always_inline, macro_inline] protected def orElse : Option α → (Unit → Option α) → Option α
| some a, _ => some a
@ -90,16 +158,36 @@ strict in the second argument.
instance : OrElse (Option α) where
orElse := Option.orElse
/-- If the first argument is `some a`, returns `some a`, otherwise returns the second argument.
This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
/--
Returns the first of its arguments that is `some`, or `none` if neither is `some`.
This is similar to the `<|>` operator, also known as `OrElse.orElse`, but both arguments are always
evaluated without short-circuiting.
-/
@[always_inline, macro_inline] def or : Option α → Option α → Option α
| some a, _ => some a
| none, b => b
/--
Lifts an ordering relation to `Option`, such that `none` is the least element.
It can be understood as adding a distinguished least element, represented by `none`, to both `α` and
`β`.
This definition is part of the implementation of the `LT (Option α)` instance. However, because it
can be used with heterogeneous relations, it is sometimes useful on its own.
Examples:
* `Option.lt (fun n k : Nat => n < k) none none = False`
* `Option.lt (fun n k : Nat => n < k) none (some 3) = True`
* `Option.lt (fun n k : Nat => n < k) (some 3) none = False`
* `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
* `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
-/
@[inline] protected def lt (r : α → β → Prop) : Option α → Option β → Prop
| none, some _ => True
| some x, some y => r x y
| _, _ => False
| none, some _ => True
| some x, some y => r x y
| _, _ => False
@[inline] protected def le (r : α → β → Prop) : Option α → Option β → Prop
| none, some _ => True
@ -113,8 +201,20 @@ instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
| some _, none => isFalse not_false
| none, none => isFalse not_false
/-- Take a pair of options and if they are both `some`, apply the given fn to produce an output.
Otherwise act like `orElse`. -/
/--
Applies a function to a two optional values if both are present. Otherwise, if one value is present,
it is returned and the function is not used.
The value is `some (fn a b)` if the inputs are `some a` and `some b`. Otherwise, the behavior is
equivalent to `Option.orElse`: if only one input is `some x`, then the value is `some x`, and if
both are `none`, then the value is `none`.
Examples:
* `Option.merge (· + ·) none (some 3) = some 3`
* `Option.merge (· + ·) (some 2) (some 3) = some 5`
* `Option.merge (· + ·) (some 2) none = some 2`
* `Option.merge (· + ·) none none = none`
-/
def merge (fn : α → α → α) : Option α → Option α → Option α
| none , none => none
| some x, none => some x
@ -131,12 +231,26 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
@[simp] theorem some_bind (a) (f : α → Option β) : (some a).bind f = f a := rfl
/-- An elimination principle for `Option`. It is a nondependent version of `Option.recOn`. -/
/--
A case analysis function for `Option`.
Given a value for `none` and a function to apply to the contents of `some`, `Option.elim` checks
which constructor a given `Option` consists of, and uses the appropriate argument.
`Option.elim` is an elimination principle for `Option`. In particular, it is a non-dependent version
of `Option.recOn`. It can also be seen as a combination of `Option.map` and `Option.getD`.
Examples:
* `(some "hello").elim 0 String.length = 5`
* `none.elim 0 String.length = 0`
-/
@[inline] protected def elim : Option α → β → (α → β) → β
| some x, _, f => f x
| none, y, _ => y
/-- Extracts the value `a` from an option that is known to be `some a` for some `a`. -/
/--
Extracts the value from an option that can be proven to be `some`.
-/
@[inline] def get {α : Type u} : (o : Option α) → isSome o → α
| some x, _ => x
@ -144,27 +258,54 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
| some _, _ => rfl
@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
/-- `guard p a` returns `some a` if `p a` holds, otherwise `none`. -/
/--
Returns `none` if a value doesn't satisfy a predicate, or the value itself otherwise.
From the perspective of `Option` as computations that might fail, this function is a run-time
assertion operator in the `Option` monad.
Examples:
* `Option.guard (· > 2) 1 = none`
* `Option.guard (· > 2) 5 = some 5`
-/
@[inline] def guard (p : α → Prop) [DecidablePred p] (a : α) : Option α :=
if p a then some a else none
/--
Cast of `Option` to `List`. Returns `[a]` if the input is `some a`, and `[]` if it is `none`.
Converts an optional value to a list with zero or one element.
Examples:
* `(some "value").toList = ["value"]`
* `none.toList = []`
-/
@[inline] def toList : Option α → List α
| none => .nil
| some a => .cons a .nil
/--
Cast of `Option` to `Array`. Returns `#[a]` if the input is `some a`, and `#[]` if it is `none`.
Converts an optional value to an array with zero or one element.
Examples:
* `(some "value").toArray = #["value"]`
* `none.toArray = #[]`
-/
@[inline] def toArray : Option α → Array α
| none => List.toArray .nil
| some a => List.toArray (.cons a .nil)
/--
Two arguments failsafe function. Returns `f a b` if the inputs are `some a` and `some b`, and
"does nothing" otherwise.
Applies a function to a two optional values if both are present. Otherwise, if one value is present,
it is returned and the function is not used.
The value is `some (f a b)` if the inputs are `some a` and `some b`. Otherwise, the behavior is
equivalent to `Option.orElse`. If only one input is `some x`, then the value is `some x`. If both
are `none`, then the value is `none`.
Examples:
* `Option.liftOrGet (· + ·) none (some 3) = some 3`
* `Option.liftOrGet (· + ·) (some 2) (some 3) = some 5`
* `Option.liftOrGet (· + ·) (some 2) none = some 2`
* `Option.liftOrGet (· + ·) none none = none`
-/
def liftOrGet (f : α → α → α) : Option α → Option α → Option α
| none, none => none
@ -180,28 +321,69 @@ inductive Rel (r : α → β → Prop) : Option α → Option β → Prop
/-- `none ~ none` -/
| none : Rel r none none
/-- Flatten an `Option` of `Option`, a specialization of `joinM`. -/
/--
Flattens nested optional values, preserving any value found.
This is analogous to `List.flatten`.
Examples:
* `none.join = none`
* `(some none).join = none`
* `(some (some v)).join = some v`
-/
@[simp, inline] def join (x : Option (Option α)) : Option α := x.bind id
/-- Like `Option.mapM` but for applicative functors. -/
/--
Applies a function in some applicative functor to an optional value, returning `none` with no
effects if the value is missing.
This is analogous to `Option.mapM` for monads.
-/
@[inline] protected def mapA [Applicative m] {α β} (f : α → m β) : Option α → m (Option β)
| none => pure none
| some x => some <$> f x
/--
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.
Converts an optional monadic computation into a monadic computation of an optional value.
Example:
```lean example
#eval show IO (Option String) from
Option.sequence <| some do
IO.println "hello"
return "world"
```
```output
hello
```
```output
some "world"
```
-/
@[inline] def sequence [Monad m] {α : Type u} : Option (m α) → m (Option α)
| none => pure none
| some fn => some <$> fn
/-- A monadic analogue of `Option.elim`. -/
/--
A monadic case analysis function for `Option`.
Given a fallback computation for `none` and a monadic operation to apply to the contents of `some`,
`Option.elimM` checks which constructor a given `Option` consists of, and uses the appropriate
argument.
`Option.elimM` can also be seen as a combination of `Option.mapM` and `Option.getDM`. It is a
monadic analogue of `Option.elim`.
-/
@[inline] def elimM [Monad m] (x : m (Option α)) (y : m β) (z : α → m β) : m β :=
do (← x).elim y z
/-- A monadic analogue of `Option.getD`. -/
/--
Gets the value in an option, monadically computing a default value on `none`.
This is the monadic analogue of `Option.getD`.
-/
@[inline] def getDM [Monad m] (x : Option α) (y : m α) : m α :=
match x with
| some a => pure a
@ -224,11 +406,18 @@ instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
@[simp] theorem any_some : Option.any p (some x) = p x := rfl
/--
The minimum of two optional values.
The minimum of two optional values, with `none` treated as the least element. This function is
usually accessed through the `Min (Option α)` instance, rather than directly.
Note this treats `none` as the least element,
so `min none x = min x none = none` for all `x : Option α`.
Prior to nightly-2025-02-27, we instead had `min none (some x) = min (some x) none = some x`.
Prior to `nightly-2025-02-27`, `none` was treated as the greatest element, so
`min none (some x) = min (some x) none = some x`.
Examples:
* `Option.min (some 2) (some 5) = some 2`
* `Option.min (some 5) (some 2) = some 2`
* `Option.min (some 2) none = none`
* `Option.min none (some 5) = none`
* `Option.min none none = none`
-/
protected def min [Min α] : Option α → Option α → Option α
| some x, some y => some (Min.min x y)
@ -243,7 +432,18 @@ instance [Min α] : Min (Option α) where min := Option.min
@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = none := rfl
@[simp] theorem min_none_none [Min α] : min (none : Option α) none = none := rfl
/-- The maximum of two optional values. -/
/--
The maximum of two optional values.
This function is usually accessed through the `Max (Option α)` instance, rather than directly.
Examples:
* `Option.max (some 2) (some 5) = some 5`
* `Option.max (some 5) (some 2) = some 5`
* `Option.max (some 2) none = some 2`
* `Option.max none (some 5) = some 5`
* `Option.max none none = none`
-/
protected def max [Max α] : Option α → Option α → Option α
| some x, some y => some (Max.max x y)
| some x, none => some x
@ -284,6 +484,15 @@ def liftOption [Alternative m] : Option α → m α
| some a => pure a
| none => failure
/--
Recover from failing `Option` computations with a handler function.
This function is usually accessed through the `MonadExceptOf Unit Option` instance.
Examples:
* `Option.tryCatch none (fun () => some "handled") = some "handled"`
* `Option.tryCatch (some "succeeded") (fun () => some "handled") = some "succeeded"`
-/
@[always_inline, inline] protected def Option.tryCatch (x : Option α) (handle : Unit → Option α) : Option α :=
match x with
| some _ => x

3
src/Init/Data/Option/BasicAux.lean
View file

@ -11,6 +11,9 @@ universe u
namespace Option
/--
Extracts the value from an `Option`, panicking on `none`.
-/
@[inline] def get! {α : Type u} [Inhabited α] : Option α → α
| some x => x
| none => panic! "value is none"

116
src/Init/Data/Option/Instances.lean
View file

@ -32,9 +32,12 @@ instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp; rfl
/--
`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 `instance : DecidableEq Option`.
Try to use `o.isNone` or `o.isSome` instead.
Equality with `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 the standard instance of
`DecidableEq (Option α)`, which can cause problems. It can be locally bound if needed.
Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead.
-/
@[inline] def decidable_eq_none {o : Option α} : Decidable (o = none) :=
decidable_of_decidable_of_iff isNone_iff_eq_none
@ -50,34 +53,115 @@ instance {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (Exi
| some a => if h : p a then isTrue ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ => h hn
/--
Partial bind. If for some `x : Option α`, `f : Π (a : α), a ∈ x → Option β` is a
partial function defined on `a : α` giving an `Option β`, where `some a = x`,
then `pbind x f h` is essentially the same as `bind x f`
but is defined only when all `x = some a`, using the proof to apply `f`.
Given an optional value and a function that can be applied when the value is `some`, returns the
result of applying the function if this is possible.
The function `f` is _partial_ because it is only defined for the values `a : α` such `a ∈ o`, which
is equivalent to `o = some a`. This restriction allows the function to use the fact that it can only
be called when `o` is not `none`: it can relate its argument to the optional value `o`. Its runtime
behavior is equivalent to that of `Option.bind`.
Examples:
```lean example
def attach (v : Option α) : Option { y : α // y ∈ v } :=
v.pbind fun x h => some ⟨x, h⟩
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
-/
@[inline]
def pbind : ∀ x : Option α, (∀ a : α, a ∈ x → Option β) → Option β
def pbind : (o : Option α) → (f : (a : α) → a ∈ o → Option β) → Option β
| none, _ => none
| some a, f => f a rfl
/--
Partial map. If `f : Π a, p a → β` is a partial function defined on `a : α` satisfying `p`,
then `pmap f x h` is essentially the same as `map f x` but is defined only when all members of `x`
satisfy `p`, using the proof to apply `f`.
Given a function from the elements of `α` that satisfy `p` to `β` and a proof that an optional value
satisfies `p` if it's present, applies the function to the value.
Examples:
```lean example
def attach (v : Option α) : Option { y : α // y ∈ v } :=
v.pmap (fun a (h : a ∈ v) => ⟨_, h⟩) (fun _ h => h)
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
-/
@[inline] def pmap {p : α → Prop} (f : ∀ a : α, p a → β) :
∀ x : Option α, (∀ a, a ∈ x → p a) → Option β
@[inline] def pmap {p : α → Prop}
(f : ∀ a : α, p a → β) :
(o : Option α) → (∀ a, a ∈ o → p a) → Option β
| none, _ => none
| some a, H => f a (H a rfl)
/-- Partial elimination. If `o : Option α` and `f : (a : α) → a ∈ o → β`, then `o.pelim b f` is
the same as `o.elim b f` but `f` is passed the proof that `a ∈ o`. -/
/--
Given an optional value and a function that can be applied when the value is `some`, returns the
result of applying the function if this is possible, or a fallback value otherwise.
The function `f` is _partial_ because it is only defined for the values `a : α` such `a ∈ o`, which
is equivalent to `o = some a`. This restriction allows the function to use the fact that it can only
be called when `o` is not `none`: it can relate its argument to the optional value `o`. Its runtime
behavior is equivalent to that of `Option.elim`.
Examples:
```lean example
def attach (v : Option α) : Option { y : α // y ∈ v } :=
v.pelim none fun x h => some ⟨x, h⟩
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
-/
@[inline] def pelim (o : Option α) (b : β) (f : (a : α) → a ∈ o → β) : β :=
match o with
| none => b
| some a => f a rfl
/-- Map a monadic function which returns `Unit` over an `Option`. -/
/--
Executes a monadic action on an optional value if it is present, or does nothing if there is no
value.
Examples:
```lean example
#eval ((some 5).forM set : StateM Nat Unit).run 0
```
```output
((), 5)
```
```lean example
#eval (none.forM (fun x : Nat => set x) : StateM Nat Unit).run 0
```
```output
((), 0)
```
-/
@[inline] protected def forM [Pure m] : Option α → (α → m PUnit) → m PUnit
| none , _ => pure ⟨⟩
| some a, f => f a

7
src/Init/Data/Option/Lemmas.lean
View file

@ -352,7 +352,12 @@ section choice
attribute [local instance] Classical.propDecidable
/-- An arbitrary `some a` with `a : α` if `α` is nonempty, and otherwise `none`. -/
/--
An optional arbitrary element of a given type.
If `α` is non-empty, then there exists some `v : α` and this arbitrary element is `some v`.
Otherwise, it is `none`.
-/
noncomputable def choice (α : Type _) : Option α :=
if h : Nonempty α then some (Classical.choice h) else none

156
src/Init/Data/Ord.lean
View file

@ -8,35 +8,81 @@ prelude
import Init.Data.String
import Init.Data.Array.Basic
/--
The result of a comparison according to a total order.
The relationship between the compared items may be:
* `Ordering.lt`: less than
* `Ordering.eq`: equal
* `Ordering.gt`: greater than
-/
inductive Ordering where
| lt | eq | gt
| /-- Less than. -/
lt
| /-- Equal. -/
eq
| /-- Greater than. -/
gt
deriving Inhabited, DecidableEq
namespace Ordering
/-- Swaps less and greater ordering results -/
/--
Swaps less-than and greater-than ordering results.
Examples:
* `Ordering.lt.swap = Ordering.gt`
* `Ordering.eq.swap = Ordering.eq`
* `Ordering.gt.swap = Ordering.lt`
-/
def swap : Ordering → Ordering
| .lt => .gt
| .eq => .eq
| .gt => .lt
/--
If `o₁` and `o₂` are `Ordering`, then `o₁.then o₂` returns `o₁` unless it is `.eq`,
in which case it returns `o₂`. Additionally, it has "short-circuiting" semantics similar to
boolean `x && y`: if `o₁` is not `.eq` then the expression for `o₂` is not evaluated.
This is a useful primitive for constructing lexicographic comparator functions:
```
If `a` and `b` are `Ordering`, then `a.then b` returns `a` unless it is `.eq`, in which case it
returns `b`. Additionally, it has “short-circuiting” behavior similar to boolean `&&`: if `a` is not
`.eq` then the expression for `b` is not evaluated.
This is a useful primitive for constructing lexicographic comparator functions. The `deriving Ord`
syntax on a structure uses the `Ord` instance to compare each field in order, combining the results
equivalently to `Ordering.then`.
Use `compareLex` to lexicographically combine two comparison functions.
Examples:
```lean example
structure Person where
name : String
age : Nat
-- Sort people first by name (in ascending order), and people with the same name by age (in
-- descending order)
instance : Ord Person where
compare a b := (compare a.name b.name).then (compare b.age a.age)
```
This example will sort people first by name (in ascending order) and will sort people with
the same name by age (in descending order). (If all fields are sorted ascending and in the same
order as they are listed in the structure, you can also use `deriving Ord` on the structure
definition for the same effect.)
```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Dana", 50⟩
```
```output
Ordering.gt
```
```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 50⟩
```
```output
Ordering.gt
```
```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 20⟩
```
```output
Ordering.lt
```
-/
@[macro_inline] def «then» (a b : Ordering) : Ordering :=
match a with
@ -44,42 +90,42 @@ definition for the same effect.)
| a => a
/--
Check whether the ordering is 'equal'.
Checks whether the ordering is `eq`.
-/
def isEq : Ordering → Bool
| eq => true
| _ => false
/--
Check whether the ordering is 'not equal'.
Checks whether the ordering is not `eq`.
-/
def isNe : Ordering → Bool
| eq => false
| _ => true
/--
Check whether the ordering is 'less than or equal to'.
Checks whether the ordering is `lt` or `eq`.
-/
def isLE : Ordering → Bool
| gt => false
| _ => true
/--
Check whether the ordering is 'less than'.
Checks whether the ordering is `lt`.
-/
def isLT : Ordering → Bool
| lt => true
| _ => false
/--
Check whether the ordering is 'greater than'.
Checks whether the ordering is `gt`.
-/
def isGT : Ordering → Bool
| gt => true
| _ => false
/--
Check whether the ordering is 'greater than or equal'.
Checks whether the ordering is `gt` or `eq`.
-/
def isGE : Ordering → Bool
| lt => false
@ -263,8 +309,12 @@ end Lemmas
end Ordering
/--
Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
`x = y` corresponds to `Ordering.eq`.
Uses decidable less-than and equality relations to find an `Ordering`.
In particular, if `x < y` then the result is `Ordering.lt`. If `x = y` then the result is
`Ordering.eq`. Otherwise, it is `Ordering.gt`.
`compareOfLessAndBEq` uses `BEq` instead of `DecidableEq`.
-/
@[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
if x < y then Ordering.lt
@ -272,8 +322,12 @@ Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` a
else Ordering.gt
/--
Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` and
`x == y` corresponds to `Ordering.eq`.
Uses a decidable less-than relation and Boolean equality to find an `Ordering`.
In particular, if `x < y` then the result is `Ordering.lt`. If `x == y` then the result is
`Ordering.eq`. Otherwise, it is `Ordering.gt`.
`compareOfLessAndEq` uses `DecidableEq` instead of `BEq`.
-/
@[inline] def compareOfLessAndBEq {α} (x y : α) [LT α] [Decidable (x < y)] [BEq α] : Ordering :=
if x < y then .lt
@ -281,9 +335,12 @@ Yields an `Ordering` s.t. `x < y` corresponds to `Ordering.lt` / `Ordering.gt` a
else .gt
/--
Compare `a` and `b` lexicographically by `cmp₁` and `cmp₂`. `a` and `b` are
first compared by `cmp₁`. If this returns 'equal', `a` and `b` are compared
Compares `a` and `b` lexicographically by `cmp₁` and `cmp₂`.
`a` and `b` are first compared by `cmp₁`. If this returns `Ordering.eq`, `a` and `b` are compared
by `cmp₂` to break the tie.
To lexicographically combine two `Ordering`s, use `Ordering.then`.
-/
@[inline] def compareLex (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering :=
(cmp₁ a b).then (cmp₂ a b)
@ -306,7 +363,14 @@ export Ord (compare)
set_option linter.unusedVariables false in -- allow specifying `ord` explicitly
/--
Compare `x` and `y` by comparing `f x` and `f y`.
Compares two values by comparing the results of applying a function.
In particular, `x` is compared to `y` by comparing `f x` and `f y`.
Examples:
* `compareOn (·.length) "apple" "banana" = .lt`
* `compareOn (· % 3) 5 6 = .gt`
* `compareOn (·.foldl max 0) [1, 2, 3] [3, 2, 1] = .eq`
-/
@[inline] def compareOn [ord : Ord β] (f : α → β) (x y : α) : Ordering :=
compare (f x) (f y)
@ -358,12 +422,20 @@ instance [Ord α] : Ord (Option α) where
def lexOrd [Ord α] [Ord β] : Ord (α × β) where
compare := compareLex (compareOn (·.1)) (compareOn (·.2))
/--
Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
`Ordering.lt`.
-/
def ltOfOrd [Ord α] : LT α where
lt a b := compare a b = Ordering.lt
instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
/--
Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
satisfies `Ordering.isLE`.
-/
def leOfOrd [Ord α] : LE α where
le a b := (compare a b).isLE
@ -373,56 +445,70 @@ instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
namespace Ord
/--
Derive a `BEq` instance from an `Ord` instance.
Constructs a `BEq` instance from an `Ord` instance.
-/
protected def toBEq (ord : Ord α) : BEq α where
beq x y := ord.compare x y == .eq
/--
Derive an `LT` instance from an `Ord` instance.
Constructs an `LT` instance from an `Ord` instance.
-/
protected def toLT (_ : Ord α) : LT α :=
protected def toLT (ord : Ord α) : LT α :=
ltOfOrd
instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
/--
Derive an `LE` instance from an `Ord` instance.
Constructs an `LE` instance from an `Ord` instance.
-/
protected def toLE (_ : Ord α) : LE α :=
protected def toLE (ord : Ord α) : LE α :=
leOfOrd
instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
/--
Invert the order of an `Ord` instance.
Inverts the order of an `Ord` instance.
The result is an `Ord α` instance that returns `Ordering.lt` when `ord` would return `Ordering.gt`
and that returns `Ordering.gt` when `ord` would return `Ordering.lt`.
-/
protected def opposite (ord : Ord α) : Ord α where
compare x y := ord.compare y x
/--
`ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.
Constructs an `Ord` instance that compares values according to the results of `f`.
In particular, `ord.on f` compares `x` and `y` by comparing `f x` and `f y` according to `ord`.
The function `compareOn` can be used to perform this comparison without constructing an intermediate
`Ord` instance.
-/
protected def on (_ : Ord β) (f : α → β) : Ord α where
compare := compareOn f
/--
Derive the lexicographic order on products `α × β` from orders for `α` and `β`.
Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
-/
protected def lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
lexOrd
/--
Create an order which compares elements first by `ord₁` and then, if this
returns 'equal', by `ord₂`.
Constructs an `Ord` instance from two existing instances by combining them lexicographically.
The resulting instance compares elements first by `ord₁` and then, if this returns `Ordering.eq`, by
`ord₂`.
The function `compareLex` can be used to perform this comparison without constructing an
intermediate `Ord` instance. `Ordering.then` can be used to lexicographically combine the results of
comparisons.
-/
protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
compare := compareLex ord₁.compare ord₂.compare
/--
Creates an order which compares elements of an `Array` in lexicographic order.
Constructs an order which compares elements of an `Array` in lexicographic order.
-/
protected def arrayOrd [a : Ord α] : Ord (Array α) where
compare x y :=

8
src/Init/Data/Prod.lean
View file

@ -43,7 +43,13 @@ theorem map_map (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ
Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x :=
rfl
/-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
/--
Swaps the elements in a pair.
Examples:
* `(1, 2).swap = (2, 1)`
* `("orange", -87).swap = (-87, "orange")`
-/
def swap : α × β → β × α := fun p => (p.2, p.1)
@[simp]

6
src/Init/Data/Repr.lean
View file

@ -79,6 +79,12 @@ instance [Repr α] : Repr (ULift.{v} α) where
instance : Repr Unit where
reprPrec _ _ := "()"
/--
Returns a representation of an optional value that should be able to be parsed as an equivalent
optional value.
This function is typically accessed through the `Repr (Option α)` instance.
-/
protected def Option.repr [Repr α] : Option α → Nat → Format
| none, _ => "none"
| some a, prec => Repr.addAppParen ("some " ++ reprArg a) prec

29
src/Init/Data/Sum/Basic.lean
View file

@ -47,30 +47,30 @@ deriving instance BEq for Sum
section get
/-- Check if a sum is `inl`. -/
/-- Checks whether a sum is the left injection `inl`. -/
def isLeft : α ⊕ β → Bool
| inl _ => true
| inr _ => false
/-- Check if a sum is `inr`. -/
/-- Checks whether a sum is the right injection `inr`. -/
def isRight : α ⊕ β → Bool
| inl _ => false
| inr _ => true
/-- Retrieve the contents from a sum known to be `inl`.-/
/-- Retrieves the contents from a sum known to be `inl`.-/
def getLeft : (ab : α ⊕ β) → ab.isLeft → α
| inl a, _ => a
/-- Retrieve the contents from a sum known to be `inr`.-/
/-- Retrieves the contents from a sum known to be `inr`.-/
def getRight : (ab : α ⊕ β) → ab.isRight → β
| inr b, _ => b
/-- Check if a sum is `inl` and if so, retrieve its contents. -/
/-- Checks whether a sum is the left injection `inl` and, if so, retrieves its contents. -/
def getLeft? : α ⊕ β → Option α
| inl a => some a
| inr _ => none
/-- Check if a sum is `inr` and if so, retrieve its contents. -/
/-- Checks whether a sum is the right injection `inr` and, if so, retrieves its contents. -/
def getRight? : α ⊕ β → Option β
| inr b => some b
| inl _ => none
@ -90,7 +90,10 @@ def getRight? : α ⊕ β → Option β
end get
/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
/--
Case analysis for sums that applies the appropriate function `f` or `g` after checking which
constructor is present.
-/
protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
fun x => Sum.casesOn x f g
@ -100,7 +103,11 @@ protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ
@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
Sum.elim f g (inr x) = g x := rfl
/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
/--
Transforms a sum according to functions on each type.
This function maps `α ⊕ β` to `α' ⊕ β'`, sending `α` to `α'` and `β` to `β'`.
-/
protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
Sum.elim (inl ∘ f) (inr ∘ g)
@ -108,7 +115,11 @@ protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β'
@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
/-- Swap the factors of a sum type -/
/--
Swaps the factors of a sum type.
The constructor `Sum.inl` is replaced with `Sum.inr`, and vice versa.
-/
def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl
@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl

653
src/Init/Prelude.lean
View file

@ -33,35 +33,26 @@ expression.
@[inline] def id {α : Sort u} (a : α) : α := a
/--
Function composition is the act of pipelining the result of one function, to the input of another, creating an entirely new function.
Example:
```
#eval Function.comp List.reverse (List.drop 2) [3, 2, 4, 1]
-- [1, 4]
```
You can use the notation `f ∘ g` as shorthand for `Function.comp f g`.
```
#eval (List.reverse ∘ List.drop 2) [3, 2, 4, 1]
-- [1, 4]
```
A simpler way of thinking about it, is that `List.reverse ∘ List.drop 2`
is equivalent to `fun xs => List.reverse (List.drop 2 xs)`,
the benefit is that the meaning of composition is obvious,
and the representation is compact.
Function composition, usually written with the infix operator `∘`. A new function is created from
two existing functions, where one function's output is used as input to the other.
Examples:
* `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`
* `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`
-/
@[inline] def Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ :=
fun x => f (g x)
/--
The constant function. If `a : α`, then `Function.const β a : β → α` is the
"constant function with value `a`", that is, `Function.const β a b = a`.
```
example (b : Bool) : Function.const Bool 10 b = 10 :=
rfl
The constant function that ignores its argument.
#check Function.const Bool 10
-- Bool → Nat
```
If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
arguments `b : β`, `Function.const β a b = a`.
Examples:
* `Function.const Bool 10 true = 10`
* `Function.const Bool 10 false = 10`
* `Function.const String 10 "any string" = 10`
-/
@[inline] def Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
fun _ => a
@ -114,36 +105,31 @@ abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
set_option bootstrap.inductiveCheckResultingUniverse false in
/--
The unit type, the canonical type with one element, named `unit` or `()`.
This is the universe-polymorphic version of `Unit`; it is preferred to use
`Unit` instead where applicable.
For more information about universe levels: [Types as objects](https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects)
The canonical universe-polymorphic type with just one element.
It should be used in contexts that require a type to be universe polymorphic, thus disallowing
`Unit`.
-/
inductive PUnit : Sort u where
/-- `PUnit.unit : PUnit` is the canonical element of the unit type. -/
/-- The only element of the universe-polymorphic unit type. -/
| unit : PUnit
/--
The unit type, the canonical type with one element, named `unit` or `()`.
In other words, it describes only a single value, which consists of said constructor applied
to no arguments whatsoever.
The `Unit` type is similar to `void` in languages derived from C.
The canonical type with one element. This element is written `()`.
`Unit` is actually defined as `PUnit.{1}` where `PUnit` is the universe
polymorphic version. The `Unit` should be preferred over `PUnit` where possible to avoid
unnecessary universe parameters.
In functional programming, `Unit` is the return type of things that "return
nothing", since a type with one element conveys no additional information.
When programming with monads, the type `m Unit` represents an action that has
some side effects but does not return a value, while `m α` would be an action
that has side effects and returns a value of type `α`.
`Unit` has a number of uses:
* It can be used to model control flow that returns from a function call without providing other
information.
* Monadic actions that return `Unit` have side effects without computing values.
* In polymorphic types, it can be used to indicate that no data is to be stored in a particular
field.
-/
abbrev Unit : Type := PUnit
/--
`Unit.unit : Unit` is the canonical element of the unit type.
It can also be written as `()`.
The only element of the unit type.
It can be written as an empty tuple: `()`.
-/
@[match_pattern] abbrev Unit.unit : Unit := PUnit.unit
@ -205,14 +191,18 @@ For more information: [Propositional Logic](https://lean-lang.org/theorem_provin
inductive False : Prop
/--
The empty type. It has no constructors. The `Empty.rec`
eliminator expresses the fact that anything follows from the empty type.
The empty type. It has no constructors.
Use `Empty.elim` in contexts where a value of type `Empty` is in scope.
-/
inductive Empty : Type
set_option bootstrap.inductiveCheckResultingUniverse false in
/--
The universe-polymorphic empty type. Prefer `Empty` or `False` where
The universe-polymorphic empty type, with no constructors.
`PEmpty` can be used in any universe, but this flexibility can lead to worse error messages and more
challenges with universe level unification. Prefer the type `Empty` or the proposition `False` when
possible.
-/
inductive PEmpty : Sort u where
@ -396,46 +386,75 @@ opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
init_quot
/--
Let `α` be any type, and let `r` be an equivalence relation on `α`.
It is mathematically common to form the "quotient" `α / r`, that is, the type of
elements of `α` "modulo" `r`. Set theoretically, one can view `α / r` as the set
of equivalence classes of `α` modulo `r`. If `f : α → β` is any function that
respects the equivalence relation in the sense that for every `x y : α`,
`r x y` implies `f x = f y`, then f "lifts" to a function `f' : α / r → β`
defined on each equivalence class `⟦x⟧` by `f' ⟦x⟧ = f x`.
Lean extends the Calculus of Constructions with additional constants that
perform exactly these constructions, and installs this last equation as a
definitional reduction rule.
Low-level quotient types. Quotient types coarsen the propositional equality for a type `α`, so that
terms related by some relation `r` are considered equal in `Quot r`.
Given a type `α` and any binary relation `r` on `α`, `Quot r` is a type. Note
that `r` is not required to be an equivalence relation. `Quot` is the basic
building block used to construct later the type `Quotient`.
Set-theoretically, `Quot r` can seen as the set of equivalence classes of `α` modulo `r`. Functions
from `Quot r` must prove that they respect `r`: to define a function `f : Quot r → β`, it is
necessary to provide `f' : α → β` and prove that for all `x : α` and `y : α`, `r x y → f' x = f' y`.
`Quot` is a built-in primitive:
* `Quot.mk` places elements of the underlying type `α` into the quotient.
* `Quot.lift` allows the definition of functions from the quotient to some other type.
* `Quot.sound` asserts the equality of elements related by `r`.
* `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
with `Quot.mk`.
The relation `r` is not required to be an equivalence relation; the resulting quotient type's
equality extends `r` to an equivalence as a consequence of the rules for equality and quotients.
When `r` is an equivalence relation, it can be more convenient to use the higher-level type
`Quotient`.
-/
add_decl_doc Quot
/--
Given a type `α` and any binary relation `r` on `α`, `Quot.mk` maps `α` to `Quot r`.
So that if `r : α → α → Prop` and `a : α`, then `Quot.mk r a` is an element of `Quot r`.
Places an element of a type into the quotient that equates terms according to the provided relation.
See `Quot`.
Given `v : α` and relation `r : α → α → Prop`, `Quot.mk r v : Quot r` is like `v`, except all
observations of `v`'s value must respect `r`.
`Quot.mk` is a built-in primitive:
* `Quot` is the built-in quotient type.
* `Quot.lift` allows the definition of functions from the quotient to some other type.
* `Quot.sound` asserts the equality of elements related by `r`.
* `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
with `Quot.mk`.
-/
add_decl_doc Quot.mk
/--
Given a type `α` and any binary relation `r` on `α`,
`Quot.ind` says that every element of `Quot r` is of the form `Quot.mk r a`.
A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with `Quot.mk`.
See `Quot` and `Quot.lift`.
`Quot.rec` is analogous to the [recursor](lean-manual://section/recursors) for a structure, and can
be used when the resulting type is not necessarily a proposition.
`Quot.ind` is a built-in primitive:
* `Quot` is the built-in quotient type.
* `Quot.mk` places elements of the underlying type `α` into the quotient.
* `Quot.lift` allows the definition of functions from the quotient to some other type.
* `Quot.sound` asserts the equality of elements related by `r`.
-/
add_decl_doc Quot.ind
/--
Given a type `α`, any binary relation `r` on `α`, a function `f : α → β`, and a proof `h`
that `f` respects the relation `r`, then `Quot.lift f h` is the corresponding function on `Quot r`.
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's relation.
The idea is that for each element `a` in `α`, the function `Quot.lift f h` maps `Quot.mk r a`
(the `r`-class containing `a`) to `f a`, wherein `h` shows that this function is well defined.
In fact, the computation principle is declared as a reduction rule.
Given a relation `r : α → α → Prop` and a quotient `Quot r`, applying a function `f : α → β`
requires a proof `a` that `f` respects `r`. In this case, `Quot.lift f a : Quot r → β` computes the
same values as `f`.
Lean's type theory includes a [definitional reduction](lean-manual://section/type-theory) from
`Quot.lift f h (Quot.mk r v)` to `f v`.
`Quot.lift` is a built-in primitive:
* `Quot` is the built-in quotient type.
* `Quot.mk` places elements of the underlying type `α` into the quotient.
* `Quot.sound` asserts the equality of elements related by `r`
* `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
with `Quot.mk`; it is analogous to the [recursor](lean-manual://section/recursors) for a
structure.
-/
add_decl_doc Quot.lift
@ -471,43 +490,45 @@ theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=
this α α a a' h rfl
/--
Product type (aka pair). You can use `α × β` as notation for `Prod α β`.
Given `a : α` and `b : β`, `Prod.mk a b : Prod α β`. You can use `(a, b)`
as notation for `Prod.mk a b`. Moreover, `(a, b, c)` is notation for
`Prod.mk a (Prod.mk b c)`.
Given `p : Prod α β`, `p.1 : α` and `p.2 : β`. They are short for `Prod.fst p`
and `Prod.snd p` respectively. You can also write `p.fst` and `p.snd`.
For more information: [Constructors with Arguments](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html?highlight=Prod#constructors-with-arguments)
The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.
Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.
-/
structure Prod (α : Type u) (β : Type v) where
/-- Constructs a pair from two terms. -/
/--
Constructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.
-/
mk ::
/-- The first projection out of a pair. if `p : α × β` then `p.1 : α`. -/
/-- The first element of a pair. -/
fst : α
/-- The second projection out of a pair. if `p : α × β` then `p.2 : β`. -/
/-- The second element of a pair. -/
snd : β
attribute [unbox] Prod
/--
Similar to `Prod`, but `α` and `β` can be propositions.
You can use `α ×' β` as notation for `PProd α β`.
We use this type internally to automatically generate the `brecOn` recursor.
A product type in which the types may be propositions, usually written `α ×' β`.
This type is primarily used internally and as an implementation detail of proof automation. It is
rarely useful in hand-written code.
-/
structure PProd (α : Sort u) (β : Sort v) where
/-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
/-- The first element of a pair. -/
fst : α
/-- The second projection out of a pair. if `p : PProd α β` then `p.2 : β`. -/
/-- The second element of a pair. -/
snd : β
/--
Similar to `Prod`, but `α` and `β` are in the same universe.
We say `MProd` is the universe monomorphic product type.
A product type in which both `α` and `β` are in the same universe.
It is called `MProd` is because it is the *universe-monomorphic* product type.
-/
structure MProd (α β : Type u) where
/-- The first projection out of a pair. if `p : MProd α β` then `p.1 : α`. -/
/-- The first element of a pair. -/
fst : α
/-- The second projection out of a pair. if `p : MProd α β` then `p.2 : β`. -/
/-- The second element of a pair. -/
snd : β
/--
@ -577,20 +598,30 @@ inductive Bool : Type where
export Bool (false true)
/--
`Subtype p`, usually written as `{x : α // p x}`, is a type which
represents all the elements `x : α` for which `p x` is true. It is structurally
a pair-like type, so if you have `x : α` and `h : p x` then
`⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
you can also make it explicit using `s.1` or `s.val`.
All the elements of a type that satisfy a predicate.
`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.
There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.
Examples:
* `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
* `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
* Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
contained in `xs`.
-/
@[pp_using_anonymous_constructor]
structure Subtype {α : Sort u} (p : α → Prop) where
/-- If `s : {x // p x}` then `s.val : α` is the underlying element in the base
type. You can also write this as `s.1`, or simply as `s` when the type is
known from context. -/
/--
The value in the underlying type that satisfies the predicate.
-/
val : α
/-- If `s : {x // p x}` then `s.2` or `s.property` is the assertion that
`p s.1`, that is, that `s` is in fact an element for which `p` holds. -/
/--
The proof that `val` satisfies the predicate `p`.
-/
property : p val
set_option linter.unusedVariables.funArgs false in
@ -822,58 +853,64 @@ theorem ULift.up_down {α : Type u} (b : ULift.{v} α) : Eq (up (down b)) b := r
theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a := rfl
/--
`Decidable p` is a data-carrying class that supplies a proof that `p` is
either `true` or `false`. It is equivalent to `Bool` (and in fact it has the
same code generation as `Bool`) together with a proof that the `Bool` is
true iff `p` is.
Either a proof that `p` is true or a proof that `p` is false. This is equivalent to a `Bool` paired
with a proof that the `Bool` is `true` if and only if `p` is true.
`Decidable` instances are used to infer "computation strategies" for
propositions, so that you can have the convenience of writing propositions
inside `if` statements and executing them (which actually executes the inferred
decidability instance instead of the proposition, which has no code).
`Decidable` instances are primarily used via `if`-expressions and the tactic `decide`. In
conditional expressions, the `Decidable` instance for the proposition is used to select a branch. At
run time, this case distinction code is identical to that which would be generated for a
`Bool`-based conditional. In proofs, the tactic `decide` synthesizes an instance of `Decidable p`,
attempts to reduce it to `isTrue h`, and then succeeds with the proof `h` if it can.
If a proposition `p` is `Decidable`, then `(by decide : p)` will prove it by
evaluating the decidability instance to `isTrue h` and returning `h`.
Because `Decidable` carries data,
when writing `@[simp]` lemmas which include a `Decidable` instance on the LHS,
it is best to use `{_ : Decidable p}` rather than `[Decidable p]`
so that non-canonical instances can be found via unification rather than
typeclass search.
Because `Decidable` carries data, when writing `@[simp]` lemmas which include a `Decidable` instance
on the LHS, it is best to use `{_ : Decidable p}` rather than `[Decidable p]` so that non-canonical
instances can be found via unification rather than instance synthesis.
-/
class inductive Decidable (p : Prop) where
/-- Prove that `p` is decidable by supplying a proof of `¬p` -/
/-- Proves that `p` is decidable by supplying a proof of `¬p` -/
| isFalse (h : Not p) : Decidable p
/-- Prove that `p` is decidable by supplying a proof of `p` -/
/-- Proves that `p` is decidable by supplying a proof of `p` -/
| isTrue (h : p) : Decidable p
/--
Convert a decidable proposition into a boolean value.
Converts a decidable proposition into a `Bool`.
If `p : Prop` is decidable, then `decide p : Bool` is the boolean value
which is `true` if `p` is true and `false` if `p` is false.
If `p : Prop` is decidable, then `decide p : Bool` is the Boolean value
that is `true` if `p` is true and `false` if `p` is false.
-/
@[inline_if_reduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
h.casesOn (fun _ => false) (fun _ => true)
export Decidable (isTrue isFalse decide)
/-- A decidable predicate. See `Decidable`. -/
/--
A decidable predicate.
A predicate is decidable if the corresponding proposition is `Decidable` for each possible argument.
-/
abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
(a : α) → Decidable (r a)
/-- A decidable relation. See `Decidable`. -/
/--
A decidable relation.
A relation is decidable if the corresponding proposition is `Decidable` for all possible arguments.
-/
abbrev DecidableRel {α : Sort u} {β : Sort v} (r : α → β → Prop) :=
(a : α) → (b : β) → Decidable (r a b)
/--
Asserts that `α` has decidable equality, that is, `a = b` is decidable
for all `a b : α`. See `Decidable`.
Propositional equality is `Decidable` for all elements of a type.
In other words, an instance of `DecidableEq α` is a means of deciding the proposition `a = b` is
for all `a b : α`.
-/
abbrev DecidableEq (α : Sort u) :=
(a b : α) → Decidable (Eq a b)
/-- Proves that `a = b` is decidable given `DecidableEq α`. -/
/--
Checks whether two terms of a type are equal using the type's `DecidableEq` instance.
-/
def decEq {α : Sort u} [inst : DecidableEq α] (a b : α) : Decidable (Eq a b) :=
inst a b
@ -1173,27 +1210,35 @@ abbrev DecidableLT (α : Type u) [LT α] := DecidableRel (LT.lt : α → α →
/-- Abbreviation for `DecidableRel (· ≤ · : α → α → Prop)`. -/
abbrev DecidableLE (α : Type u) [LE α] := DecidableRel (LE.le : α → α → Prop)
/-- `Max α` is the typeclass which supports the operation `max x y` where `x y : α`.-/
/--
An overloaded operation to find the greater of two values of type `α`.
-/
class Max (α : Type u) where
/-- The maximum operation: `max x y`. -/
/-- Returns the greater of its two arguments. -/
max : α → α → α
export Max (max)
/-- Implementation of the `max` operation using `≤`. -/
/--
Constructs a `Max` instance from a decidable `≤` operation.
-/
-- Marked inline so that `min x y + max x y` can be optimized to a single branch.
@[inline]
def maxOfLe [LE α] [DecidableRel (@LE.le α _)] : Max α where
max x y := ite (LE.le x y) y x
/-- `Min α` is the typeclass which supports the operation `min x y` where `x y : α`.-/
/--
An overloaded operation to find the lesser of two values of type `α`.
-/
class Min (α : Type u) where
/-- The minimum operation: `min x y`. -/
/-- Returns the lesser of its two arguments. -/
min : α → α → α
export Min (min)
/-- Implementation of the `min` operation using `≤`. -/
/--
Constructs a `Min` instance from a decidable `≤` operation.
-/
-- Marked inline so that `min x y + max x y` can be optimized to a single branch.
@[inline]
def minOfLe [LE α] [DecidableRel (@LE.le α _)] : Min α where
@ -1876,17 +1921,24 @@ theorem System.Platform.numBits_eq : Or (Eq numBits 32) (Eq numBits 64) :=
(getNumBits ()).property
/--
`Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.
It is the "canonical type with `n` elements".
Natural numbers less than some upper bound.
In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
-/
@[pp_using_anonymous_constructor]
structure Fin (n : Nat) where
/-- Creates a `Fin n` from `i : Nat` and a proof that `i < n`. -/
mk ::
/-- If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be
written as `i.1` or just `i` when the target type is known. -/
/--
The number that is strictly less than `n`.
`Fin.val` is a coercion, so any `Fin n` can be used in a position where a `Nat` is expected.
-/
val : Nat
/-- If `i : Fin n`, then `i.2` is a proof that `i.1 < n`. -/
/--
The number `val` is strictly less than the bound `n`.
-/
isLt : LT.lt val n
attribute [coe] Fin.val
@ -2307,37 +2359,10 @@ def Char.utf8Size (c : Char) : Nat :=
(ite (LE.le v (UInt32.ofNatLT 0xFFFF (of_decide_eq_true rfl))) 3 4))
/--
`Option α` is the type of values which are either `some a` for some `a : α`,
or `none`. In functional programming languages, this type is used to represent
the possibility of failure, or sometimes nullability.
Optional values, which are either `some` around a value from the underlying type or `none`.
For example, the function `HashMap.get? : HashMap α β → α → Option β` looks up
a specified key `a : α` inside the map. Because we do not know in advance
whether the key is actually in the map, the return type is `Option β`, where
`none` means the value was not in the map, and `some b` means that the value
was found and `b` is the value retrieved.
The `xs[i]` syntax, which is used to index into collections, has a variant
`xs[i]?` that returns an optional value depending on whether the given index
is valid. For example, if `m : HashMap α β` and `a : α`, then `m[a]?` is
equivalent to `HashMap.get? m a`.
To extract a value from an `Option α`, we use pattern matching:
```
def map (f : α → β) (x : Option α) : Option β :=
match x with
| some a => some (f a)
| none => none
```
We can also use `if let` to pattern match on `Option` and get the value
in the branch:
```
def map (f : α → β) (x : Option α) : Option β :=
if let some a := x then
some (f a)
else
none
```
`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
-/
inductive Option (α : Type u) where
/-- No value. -/
@ -2353,11 +2378,14 @@ instance {α} : Inhabited (Option α) where
default := none
/--
Get with default. If `opt : Option α` and `dflt : α`, then `opt.getD dflt`
returns `a` if `opt = some a` and `dflt` otherwise.
Gets an optional value, returning a given default on `none`.
This function is `@[macro_inline]`, so `dflt` will not be evaluated unless
`opt` turns out to be `none`.
This function is `@[macro_inline]`, so `dflt` will not be evaluated unless `opt` turns out to be
`none`.
Examples:
* `(some "hello").getD "goodbye" = "hello"`
* `none.getD "goodbye" = "hello"`
-/
@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α :=
match opt with
@ -2365,8 +2393,14 @@ This function is `@[macro_inline]`, so `dflt` will not be evaluated unless
| none => dflt
/--
Map a function over an `Option` by applying the function to the contained
value if present.
Apply a function to an optional value, if present.
From the perspective of `Option` as a container with at most one value, this is analogous to
`List.map`. It can also be accessed via the `Functor Option` instance.
Examples:
* `(none : Option Nat).map (· + 1) = none`
* `(some 3).map (· + 1) = some 4`
-/
@[inline] protected def Option.map (f : α → β) : Option α → Option β
| some x => some (f x)
@ -2812,77 +2846,151 @@ def Array.extract (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : A
let sz' := Nat.sub (min stop as.size) start
loop sz' start (emptyWithCapacity sz')
/-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/
/--
The `>>=` operator is overloaded via instances of `bind`.
`Bind` is typically used via `Monad`, which extends it.
-/
class Bind (m : Type u → Type v) where
/-- If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the
result of executing `x` to get a value of type `α` and then passing it to `f`. -/
/--
Sequences two computations, allowing the second to depend on the value computed by the first.
If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the result of executing `x` to get
a value of type `α` and then passing it to `f`.
-/
bind : {α β : Type u} → m α → (α → m β) → m β
export Bind (bind)
/-- The typeclass which supplies the `pure` function. See `Monad`. -/
/--
The `pure` function is overloaded via `Pure` instances.
`Pure` is typically accessed via `Monad` or `Applicative` instances.
-/
class Pure (f : Type u → Type v) where
/-- If `a : α`, then `pure a : f α` represents a monadic action that does
nothing and returns `a`. -/
/--
Given `a : α`, then `pure a : f α` represents an action that does nothing and returns `a`.
Examples:
* `(pure "hello" : Option String) = some "hello"`
* `(pure "hello" : Except (Array String) String) = Except.ok "hello"`
* `(pure "hello" : StateM Nat String).run 105 = ("hello", 105)`
-/
pure {α : Type u} : α → f α
export Pure (pure)
/--
In functional programming, a "functor" is a function on types `F : Type u → Type v`
equipped with an operator called `map` or `<$>` such that if `f : α → β` then
`map f : F α → F β`, so `f <$> x : F β` if `x : F α`. This corresponds to the
category-theory notion of [functor](https://en.wikipedia.org/wiki/Functor) in
the special case where the category is the category of types and functions
between them, except that this class supplies only the operations and not the
laws (see `LawfulFunctor`).
A functor in the sense used in functional programming, which means a function `f : Type u → Type v`
has a way of mapping a function over its contents. This `map` operator is written `<$>`, and
overloaded via `Functor` instances.
This `map` function should respect identity and function composition. In other words, for all terms
`v : f α`, it should be the case that:
* `id <$> v = v`
* For all functions `h : β → γ` and `g : α → β`, `(h ∘ g) <$> v = h <$> g <$> v`
While all `Functor` instances should live up to these requirements, they are not required to _prove_
that they do. Proofs may be required or provided via the `LawfulFunctor` class.
Assuming that instances are lawful, this definition corresponds to the category-theoretic notion of
[functor](https://en.wikipedia.org/wiki/Functor) in the special case where the category is the
category of types and functions between them.
-/
class Functor (f : Type u → Type v) : Type (max (u+1) v) where
/-- If `f : α → β` and `x : F α` then `f <$> x : F β`. -/
/--
Applies a function inside a functor. This is used to overload the `<$>` operator.
When mapping a constant function, use `Functor.mapConst` instead, because it may be more
efficient.
-/
map : {α β : Type u} → (α → β) → f α → f β
/-- The special case `const a <$> x`, which can sometimes be implemented more
efficiently. -/
/--
Mapping a constant function.
Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some
functors, this can be implemented more efficiently; for all other functors, the default
implementation may be used.
-/
mapConst : {α β : Type u} → α → f β → f α := Function.comp map (Function.const _)
/-- The typeclass which supplies the `<*>` "seq" function. See `Applicative`. -/
class Seq (f : Type u → Type v) : Type (max (u+1) v) where
/-- If `mf : F (α → β)` and `mx : F α`, then `mf <*> mx : F β`.
In a monad this is the same as `do let f ← mf; x ← mx; pure (f x)`:
it evaluates first the function, then the argument, and applies one to the other.
/--
The `<*>` operator is overloaded using the function `Seq.seq`.
To avoid surprising evaluation semantics, `mx` is taken "lazily", using a
`Unit → f α` function. -/
While `<$>` from the class `Functor` allows an ordinary function to be mapped over its contents,
`<*>` allows a function that's “inside” the functor to be applied. When thinking about `f` as
possible side effects, this captures evaluation order: `seq` arranges for the effects that produce
the function to occur prior to those that produce the argument value.
For most applications, `Applicative` or `Monad` should be used rather than `Seq` itself.
-/
class Seq (f : Type u → Type v) : Type (max (u+1) v) where
/--
The implementation of the `<*>` operator.
In a monad, `mf <*> mx` is the same as `do let f ← mf; x ← mx; pure (f x)`: it evaluates the
function first, then the argument, and applies one to the other.
To avoid surprising evaluation semantics, `mx` is taken "lazily", using a `Unit → f α` function.
-/
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
/-- The typeclass which supplies the `<*` "seqLeft" function. See `Applicative`. -/
class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where
/-- If `x : F α` and `y : F β`, then `x <* y` evaluates `x`, then `y`,
and returns the result of `x`.
/--
The `<*` operator is overloaded using `seqLeft`.
To avoid surprising evaluation semantics, `y` is taken "lazily", using a
`Unit → f β` function. -/
When thinking about `f` as potential side effects, `<*` evaluates first the left and then the right
argument for their side effects, discarding the value of the right argument and returning the value
of the left argument.
For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself.
-/
class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where
/--
Sequences the effects of two terms, discarding the value of the second. This function is usually
invoked via the `<*` operator.
Given `x : f α` and `y : f β`, `x <* y` runs `x`, then runs `y`, and finally returns the result of
`x`.
The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.
-/
seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
/-- The typeclass which supplies the `*>` "seqRight" function. See `Applicative`. -/
class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where
/-- If `x : F α` and `y : F β`, then `x *> y` evaluates `x`, then `y`,
and returns the result of `y`.
/--
The `*>` operator is overloaded using `seqRight`.
To avoid surprising evaluation semantics, `y` is taken "lazily", using a
`Unit → f β` function. -/
When thinking about `f` as potential side effects, `*>` evaluates first the left and then the right
argument for their side effects, discarding the value of the left argument and returning the value
of the right argument.
For most applications, `Applicative` or `Monad` should be used rather than `SeqLeft` itself.
-/
class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where
/--
Sequences the effects of two terms, discarding the value of the first. This function is usually
invoked via the `*>` operator.
Given `x : f α` and `y : f β`, `x *> y` runs `x`, then runs `y`, and finally returns the result of
`y`.
The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.
-/
seqRight : {α β : Type u} → f α → (Unit → f β) → f β
/--
An [applicative functor](https://en.wikipedia.org/wiki/Applicative_functor) is
an intermediate structure between `Functor` and `Monad`. It mainly consists of
two operations:
An [applicative functor](lean-manual://section/monads-and-do) is more powerful than a `Functor`, but
less powerful than a `Monad`.
* `pure : α → F α`
* `seq : F (α → β) → F α → F β` (written as `<*>`)
Applicative functors capture sequencing of effects with the `<*>` operator, overloaded as `seq`, but
not data-dependent effects. The results of earlier computations cannot be used to control later
effects.
The `seq` operator gives a notion of evaluation order to the effects, where
the first argument is executed before the second, but unlike a monad the results
of earlier computations cannot be used to define later actions.
Applicative functors should satisfy four laws. Instances of `Applicative` are not required to prove
that they satisfy these laws, which are part of the `LawfulApplicative` class.
-/
class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where
map := fun x y => Seq.seq (pure x) fun _ => y
@ -2890,19 +2998,18 @@ class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqL
seqRight := fun a b => Seq.seq (Functor.map (Function.const _ id) a) b
/--
A [monad](https://en.wikipedia.org/wiki/Monad_(functional_programming)) is a
structure which abstracts the concept of sequential control flow.
It mainly consists of two operations:
[Monads](https://en.wikipedia.org/wiki/Monad_(functional_programming)) are an abstraction of
sequential control flow and side effects used in functional programming. Monads allow both
sequencing of effects and data-dependent effects: the values that result from an early step may
influence the effects carried out in a later step.
* `pure : α → F α`
* `bind : F α → (α → F β) → F β` (written as `>>=`)
The `Monad` API may be used directly. However, it is most commonly accessed through
[`do`-notation](lean-manual://section/do-notation).
Like many functional programming languages, Lean makes extensive use of monads
for structuring programs. In particular, the `do` notation is a very powerful
syntax over monad operations, and it depends on a `Monad` instance.
See [the `do` notation](https://lean-lang.org/lean4/doc/do.html)
chapter of the manual for details.
Most `Monad` instances provide implementations of `pure` and `bind`, and use default implementations
for the other methods inherited from `Applicative`. Monads should satisfy certain laws, but
instances are not required to prove this. An instance of `LawfulMonad` expresses that a given
monad's operations are lawful.
-/
class Monad (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind m where
map f x := bind x (Function.comp pure f)
@ -3010,10 +3117,12 @@ instance monadFunctorRefl (m) : MonadFunctorT m m where
monadMap f := f
/--
`Except ε α` is a type which represents either an error of type `ε`, or an "ok"
value of type `α`. The error type is listed first because
`Except ε : Type → Type` is a `Monad`: the pure operation is `ok` and the bind
operation returns the first encountered `error`.
`Except ε α` is a type which represents either an error of type `ε` or a successful result with a
value of type `α`.
`Except ε : Type u → Type v` is a `Monad` that represents computations that may throw exceptions:
the `pure` operation is `Except.ok` and the `bind` operation returns the first encountered
`Except.error`.
-/
inductive Except (ε : Type u) (α : Type v) where
/-- A failure value of type `ε` -/
@ -3027,54 +3136,65 @@ instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) w
default := Except.error default
/--
An implementation of Haskell's [`MonadError`] class. A `MonadError ε m` is a
monad `m` with two operations:
Exception monads provide the ability to throw errors and handle errors.
* `throw : ε → m α` "throws an error" of type `ε` to the nearest enclosing
catch block
* `tryCatch (body : m α) (handler : ε → m α) : m α` will catch any errors in
`body` and pass the resulting error to `handler`.
Errors in `handler` will not be caught.
In this class, `ε` is a `semiOutParam`, which means that it can influence the choice of instance.
`MonadExcept ε` provides the same operations, but requires that `ε` be inferrable from `m`.
The `try ... catch e => ...` syntax inside `do` blocks is sugar for the
`tryCatch` operation.
[`MonadError`]: https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError
`tryCatchThe`, which takes an explicit exception type, is used to desugar `try ... catch ...` steps
inside `do`-blocks when the handlers have type annotations.
-/
class MonadExceptOf (ε : semiOutParam (Type u)) (m : Type v → Type w) where
/-- `throw : ε → m α` "throws an error" of type `ε` to the nearest enclosing
catch block. -/
/--
Throws an exception of type `ε` to the nearest enclosing `catch`.
-/
throw {α : Type v} : ε → m α
/-- `tryCatch (body : m α) (handler : ε → m α) : m α` will catch any errors in
`body` and pass the resulting error to `handler`.
Errors in `handler` will not be caught. -/
/--
Catches errors thrown in `body`, passing them to `handler`. Errors in `handler` are not caught.
-/
tryCatch {α : Type v} (body : m α) (handler : ε → m α) : m α
/--
This is the same as `throw`, but allows specifying the particular error type
in case the monad supports throwing more than one type of error.
Throws an exception, with the exception type specified explicitly. This is useful when a monad
supports throwing more than one type of exception.
Use `throw` for a version that expects the exception type to be inferred from `m`.
-/
abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m α :=
MonadExceptOf.throw e
/--
This is the same as `tryCatch`, but allows specifying the particular error type
in case the monad supports throwing more than one type of error.
Catches errors, recovering using `handle`. The exception type is specified explicitly. This is useful when a monad
supports throwing or handling more than one type of exception.
Use `tryCatch`, for a version that expects the exception type to be inferred from `m`.
-/
abbrev tryCatchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
MonadExceptOf.tryCatch x handle
/-- Similar to `MonadExceptOf`, but `ε` is an `outParam` for convenience. -/
class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) where
/-- `throw : ε → m α` "throws an error" of type `ε` to the nearest enclosing
catch block. -/
throw {α : Type v} : ε → m α
/-- `tryCatch (body : m α) (handler : ε → m α) : m α` will catch any errors in
`body` and pass the resulting error to `handler`.
Errors in `handler` will not be caught. -/
tryCatch {α : Type v} : m α → (ε → m α) → m α
/--
Exception monads provide the ability to throw errors and handle errors.
/-- "Unwraps" an `Except ε α` to get the `α`, or throws the exception otherwise. -/
In this class, `ε` is an `outParam`, which means that it is inferred from `m`. `MonadExceptOf ε`
provides the same operations, but allows `ε` to influence instance synthesis.
`MonadExcept.tryCatch` is used to desugar `try ... catch ...` steps inside `do`-blocks when the
handlers do not have exception type annotations.
-/
class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) where
/--
Throws an exception of type `ε` to the nearest enclosing `catch`.
-/
throw {α : Type v} : ε → m α
/--
Catches errors thrown in `body`, passing them to `handler`. Errors in `handler` are not caught.
-/
tryCatch {α : Type v} : (body : m α) → (handler : ε → m α) → m α
/--
Re-interprets an `Except ε` action in an exception monad `m`, succeeding if it succeeds and throwing
an exception if it throws an exception.
-/
def MonadExcept.ofExcept [Monad m] [MonadExcept ε m] : Except ε α → m α
| .ok a => pure a
| .error e => throw e
@ -3088,7 +3208,12 @@ instance (ε : Type u) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcep
namespace MonadExcept
variable {ε : Type u} {m : Type v → Type w}
/-- A `MonadExcept` can implement `t₁ <|> t₂` as `try t₁ catch _ => t₂`. -/
/--
Unconditional error recovery that ignores which exception was thrown. Usually used via the `<|>`
operator.
If both computations throw exceptions, then the result is the second exception.
-/
@[inline] protected def orElse [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α) : m α :=
tryCatch t₁ fun _ => t₂ ()
@ -3515,14 +3640,14 @@ instance nonBacktrackable : Backtrackable PUnit σ where
end EStateM
/-- A class for types that can be hashed into a `UInt64`. -/
/-- Types that can be hashed into a `UInt64`. -/
class Hashable (α : Sort u) where
/-- Hashes the value `a : α` into a `UInt64`. -/
/-- Hashes a value into a `UInt64`. -/
hash : α → UInt64
export Hashable (hash)
/-- An opaque hash mixing operation, used to implement hashing for tuples. -/
/-- An opaque hash mixing operation, used to implement hashing for products. -/
@[extern "lean_uint64_mix_hash"]
opaque mixHash (u₁ u₂ : UInt64) : UInt64

11
src/Init/WF.lean
View file

@ -241,9 +241,18 @@ variable {α : Type u} {β : Type v}
variable (ra : α → α → Prop)
variable (rb : β → β → Prop)
-- Lexicographical order based on ra and rb
/--
A lexicographical order based on the orders `ra` and `rb` for the elements of pairs.
-/
protected inductive Lex : α × β → α × β → Prop where
/--
If the first projections of two pairs are ordered, then they are lexicographically ordered.
-/
| left {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Prod.Lex (a₁, b₁) (a₂, b₂)
/--
If the first projections of two pairs are equal, then they are lexicographically ordered if the
second projections are ordered.
-/
| right (a) {b₁ b₂} (h : rb b₁ b₂) : Prod.Lex (a, b₁) (a, b₂)
theorem lex_def {r : α → α → Prop} {s : β → β → Prop} {p q : α × β} :