diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index f19aab2856..160ee46a22 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -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 diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 961e2a99fa..48604b6326 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -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₂) diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean index db30a57ef4..b9f5067eb4 100644 --- a/src/Init/Control/ExceptCps.lean +++ b/src/Init/Control/ExceptCps.lean @@ -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 diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean index 52250d894e..5ed26f1864 100644 --- a/src/Init/Control/Lawful/Basic.lean +++ b/src/Init/Control/Lawful/Basic.lean @@ -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]) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 41120e754b..7b3dbd9102 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -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 diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index aa50e66555..dc912e46d5 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -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 diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean index 7fc6afe3d5..ed973af9d0 100644 --- a/src/Init/Data/Array/Subarray/Split.lean +++ b/src/Init/Data/Array/Subarray/Split.lean @@ -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 diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index f9a7d7cd30..e0c478a508 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -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 diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index b612ff92cb..b6220fa06d 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -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ₙ diff --git a/src/Init/Data/Fin/Iterate.lean b/src/Init/Data/Fin/Iterate.lean index 3738eab0a8..6d55e44393 100644 --- a/src/Init/Data/Fin/Iterate.lean +++ b/src/Init/Data/Fin/Iterate.lean @@ -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 := diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 9884e0fc18..c121a06af3 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -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 := diff --git a/src/Init/Data/Fin/Log2.lean b/src/Init/Data/Fin/Log2.lean index 72efeeee50..d3f19d3635 100644 --- a/src/Init/Data/Fin/Log2.lean +++ b/src/Init/Data/Fin/Log2.lean @@ -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⟩ diff --git a/src/Init/Data/Format/Instances.lean b/src/Init/Data/Format/Instances.lean index 3d8b528d49..4003eba717 100644 --- a/src/Init/Data/Format/Instances.lean +++ b/src/Init/Data/Format/Instances.lean @@ -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 diff --git a/src/Init/Data/Function.lean b/src/Init/Data/Function.lean index 090fb1a6c8..c32291205d 100644 --- a/src/Init/Data/Function.lean +++ b/src/Init/Data/Function.lean @@ -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 diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean index 093c9256be..6594537955 100644 --- a/src/Init/Data/Hashable.lean +++ b/src/Init/Data/Hashable.lean @@ -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 diff --git a/src/Init/Data/Nat/Fold.lean b/src/Init/Data/Nat/Fold.lean index 2e5f85e7d8..6ba639457d 100644 --- a/src/Init/Data/Nat/Fold.lean +++ b/src/Init/Data/Nat/Fold.lean @@ -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)) diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index 6722cd98f5..234ccd7bef 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -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) diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 09858fb867..dc9f2f9d76 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -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 diff --git a/src/Init/Data/Option/BasicAux.lean b/src/Init/Data/Option/BasicAux.lean index 46298ca67e..770da08e1e 100644 --- a/src/Init/Data/Option/BasicAux.lean +++ b/src/Init/Data/Option/BasicAux.lean @@ -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" diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index d4ed9279c2..dee276944f 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -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 diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index aa322ba03d..dd65548ec4 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -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 diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean index 0696cd9ad3..540d7c90b6 100644 --- a/src/Init/Data/Ord.lean +++ b/src/Init/Data/Ord.lean @@ -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 := diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean index 2775984151..63d27a0499 100644 --- a/src/Init/Data/Prod.lean +++ b/src/Init/Data/Prod.lean @@ -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] diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 1d55efb2d8..4414279ef7 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -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 diff --git a/src/Init/Data/Sum/Basic.lean b/src/Init/Data/Sum/Basic.lean index d44e90eaeb..4eeb3bf5b7 100644 --- a/src/Init/Data/Sum/Basic.lean +++ b/src/Init/Data/Sum/Basic.lean @@ -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 diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index b89bcf53a4..04bb9bf61b 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -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 diff --git a/src/Init/WF.lean b/src/Init/WF.lean index ee457f3709..fe88f2016c 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -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 : α × β} :