diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index cfd1ba4fef..b289a12cc9 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3,11 +3,32 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -prelude +prelude -- Don't import Init, because we're in Init itself + +/-! +# Init.Prelude + +This is the first file in the lean import hierarchy. It is responsible for setting +up basic definitions, most of which lean already has "built in knowledge" about, +so it is important that they be set up in exactly this way. (For example, lean will +use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler.) + +-/ universe u v w -/-- Identity function -/ +/-- +The identity function. `id` takes an implicit argument `α : Sort u` +(a type in any universe), and an argument `a : α`, and returns `a`. + +Although this may look like a useless function, one application of the identity +function is to explicitly put a type on an expression. If `e` has type `T`, +and `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean +knows that this expression has type `T'` rather than `T`. This can make a +difference for typeclass inference, since `T` and `T'` may have different +typeclass instances on them. `show T' from e` is sugar for an `@id T' e` +expression. +-/ @[inline] def id {α : Sort u} (a : α) : α := a /-- @@ -31,7 +52,8 @@ and the representation is compact. fun x => f (g x) /-- -The constant function. +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 @@ -45,8 +67,11 @@ example (b : Bool) : Function.const Bool 10 b = 10 := set_option checkBinderAnnotations false in /-- -`inferInstance` is useful for triggering the type class resolution procedure when -the expected type is an instance. Example: +`inferInstance` synthesizes a value of any target type by typeclass +inference. This function has the same type signature as the identity +function, but the square brackets on the `[i : α]` argument means that it will +attempt to construct this argument by typeclass inference. (This will fail if +`α` is not a `class`.) Example: ``` #check (inferInstance : Inhabited Nat) -- Inhabited Nat @@ -58,10 +83,15 @@ example : foo.default = (default, default) := ``` -/ @[reducible] def inferInstance {α : Sort u} [i : α] : α := i + set_option checkBinderAnnotations false in -/-- -Similar to `inferInstance`, but the instance is explicitly provided. -Example: +/-- `inferInstanceAs α` synthesizes a value of any target type by typeclass +inference. This is just like `inferInstance` except that `α` is given +explicitly instead of being inferred from the target type. It is especially +useful when the target type is some `α'` which is definitionally equal to `α`, +but the instance we are looking for is only registered for `α` (because +typeclass search does not unfold most definitions, but definitional equality +does.) Example: ``` #check inferInstanceAs (Inhabited Nat) -- Inhabited Nat ``` @@ -70,14 +100,17 @@ Example: set_option bootstrap.inductiveCheckResultingUniverse false in /-- -The universe polymorphic `Unit` type. +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://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects) -/ inductive PUnit : Sort u where - | unit : PUnit + | /-- `PUnit.unit : PUnit` is the canonical element of the unit type. -/ + unit : PUnit /-- -`Unit` is a type with just one argumentless constructor, called `unit`. +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. @@ -85,18 +118,44 @@ The `Unit` type is similar to `void` in languages derived from C. `Unit` is actually defined as `PUnit.{0}` 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 `α`. -/ abbrev Unit : Type := PUnit /-- -Shorthand for `PUnit.unit`. +`Unit.unit : Unit` is the canonical element of the unit type. +It can also be written as `()`. -/ @[matchPattern] abbrev Unit.unit : Unit := PUnit.unit -/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/ +/-- +Auxiliary unsafe constant used by the Compiler when erasing proofs from code. + +It may look strange to have an axiom that says "every proposition is true", +since this is obviously unsound, but the `unsafe` marker ensures that the +kernel will not let this through into regular proofs. The lower levels of the +code generator don't need proofs in terms, so this is used to stub the proofs +out. +-/ unsafe axiom lcProof {α : Prop} : α -/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/ +/-- +Auxiliary unsafe constant used by the Compiler to mark unreachable code. + +Like `lcProof`, this is an `unsafe axiom`, which means that even though it is +not sound, the kernel will not let us use it for regular proofs. + +Executing this expression to actually synthesize a value of type `α` causes +**immediate undefined behavior**, and the compiler does take advantage of this +to optimize the code assuming that it is not called. If it is not optimized out, +it is likely to appear as a print message saying "unreachable code", but this +behavior is not guaranteed or stable in any way. +-/ unsafe axiom lcUnreachable {α : Sort u} : α /-- @@ -105,7 +164,8 @@ In other words, `True` is simply true, and has a canonical proof, `True.intro` For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic) -/ inductive True : Prop where - | /-- Introduction rule for `True`. -/ + | /-- `True` is true, and `True.intro` (or more commonly, `trivial`) + is the proof. -/ intro : True /-- @@ -126,21 +186,29 @@ inductive Empty : Type set_option bootstrap.inductiveCheckResultingUniverse false in /-- -The universe polymorphic empty type. -See `Empty`. +The universe-polymorphic empty type. Prefer `Empty` or `False` where +possible. -/ inductive PEmpty : Sort u where /-- -Negation, `Not p`, is actually defined to be `p → False`, so we obtain `Not p` by deriving a contradiction from `p`. -You can use `¬p` as a shorthand for `Not p`. +`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`, +so if your goal is `¬p` you can use `intro h` to turn the goal into +`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False` +and `(hn h).elim` will prove anything. For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic) -/ def Not (a : Prop) : Prop := a → False /-- -A simpler version of `False.rec` where the implicit argument has type `C : Sort u` instead of `C : False → Sort u`. -They both express the fact that anything follows from a contradiction. +`False.elim : False → C` says that from `False`, any desired proposition +`C` holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion. + +The target type is actually `C : Sort u` which means it works for both +propositions and types. When executed, this acts like an "unreachable" +instruction: it is **undefined behavior** to run, but it will probably print +"unreachable code". (You would need to construct a proof of false to run it +anyway, which you can only do using `sorry` or unsound axioms.) -/ @[macroInline] def False.elim {C : Sort u} (h : False) : C := h.rec @@ -183,63 +251,106 @@ The triangle in the second presentation is a macro built on top of `Eq.subst` an For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ inductive Eq : α → α → Prop where - | refl (a : α) : Eq a a + | /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the + equality type. See also `rfl`, which is usually used instead. -/ + refl (a : α) : Eq a a +/-- Non-dependent recursor for the equality type. -/ @[simp] abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b := h.rec m /-- -Short for `Eq.refl _` +`rfl : a = a` is the unique constructor of the equality type. This is the +same as `Eq.refl` except that it takes `a` implicitly instead of explicitly. + +This is a more powerful theorem than it may appear at first, because although +the statement of the theorem is `a = a`, lean will allow anything that is +definitionally equal to that type. So, for instance, `2 + 2 = 4` is proven in +lean by `rfl`, because both sides are the same up to definitional equality. -/ @[matchPattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a +/-- `id x = x`, as a `@[simp]` lemma. -/ @[simp] theorem id_eq (a : α) : Eq (id a) a := rfl /-- -Equality is much more than an equivalence relation, however. It has the important property that every assertion -respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. -That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. +The substitution principle for equality. If `a = b ` and `P a` holds, +then `P b` also holds. We conventionally use the name `motive` for `P` here, +so that you can specify it explicitly using e.g. +`Eq.subst (motive := fun x => x < 5)` if it is not otherwise inferred correctly. + +This theorem is the underlying mechanism behind the `rw` tactic, which is +essentially a fancy algorithm for finding good `motive` arguments to usefully +apply this theorem to replace occurrences of `a` with `b` in the goal or +hypotheses. + For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) (h₂ : motive a) : motive b := Eq.ndrec h₂ h₁ /-- -Equality is a symmetric relationship. +Equality is symmetric: if `a = b` then `b = a`. + +Because this is in the `Eq` namespace, if you have a variable `h : a = b`, +`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`. + For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a := h ▸ rfl /-- -Equality is a transitive relationship. +Equality is transitive: if `a = b` and `b = c` then `a = c`. + +Because this is in the `Eq` namespace, if you variables or expressions +`h₁ : a = b` and `h₂ : b = c`, you can use `h₁.trans h₂ : a = c` as shorthand +for `Eq.trans h₁ h₃`. + For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c := h₂ ▸ h₁ /-- -You can use an equality `α = β` to cast an value of type `α` into `β`. +Cast across a type equality. If `h : α = β` is an equality of types, and +`a : α`, then `a : β` will usually not typecheck directly, but this function +will allow you to work around this and embed `a` in type `β` as `cast h a : β`. + +It is best to avoid this function if you can, because it is more complicated +to reason about terms containing casts, but if the types don't match up +definitionally sometimes there isn't anything better you can do. + For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ @[macroInline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β := h.rec a /-- -Given a (nondependent) function `f` and a proof `h : a₁ = a₂`, `congrArg f h : f a₁ = f a₂`. +Congruence in the function argument: if `a₁ = a₂` then `f a₁ = f a₂` for +any (nondependent) function `f`. This is more powerful than it might look at first, because +you can also use a lambda expression for `f` to prove that +` = `. This function is used +internally by tactics like `congr` and `simp` to apply equalities inside +subterms. + For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) := h ▸ rfl /-- -`congr` is short for congruence. +Congruence in both function and argument. If `f₁ = f₂` and `a₁ = a₂` then +`f₁ a₁ = f₂ a₂`. This only works for nondependent functions; the theorem +statement is more complex in the dependent case. + For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) -/ theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : Eq f₁ f₂) (h₂ : Eq a₁ a₂) : Eq (f₁ a₁) (f₂ a₂) := h₁ ▸ h₂ ▸ rfl -theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) := +/-- Congruence in the function part of an application: If `f = g` then `f a = g a`. -/ +theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) := h ▸ rfl /-! @@ -260,15 +371,19 @@ 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. +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. -Given a type `α` and any binary relation `r` on `α`, `Quot r` is a type. Note that `r` is not required to be -an equilance relation. `Quot` is the basic building block used to construct later the type `Quotient`. +Given a type `α` and any binary relation `r` on `α`, `Quot r` is a type. Note +that `r` is not required to be an equivalance relation. `Quot` is the basic +building block used to construct later the type `Quotient`. -/ add_decl_doc Quot @@ -299,11 +414,22 @@ In fact, the computation principle is declared as a reduction rule. add_decl_doc Quot.lift /-- -Heterogeneous equality. That is, the elements may have different types. +Heterogeneous equality. `HEq a b` asserts that `a` and `b` have the same +type, and casting `a` across the equality yields `b`, and vice versa. + +You should avoid using this type if you can. Heterogeneous equality does not +have all the same properties as `Eq`, because the assumption that the types of +`a` and `b` are equal is often too weak to prove theorems of interest. One +important non-theorem is the analogue of `congr`: If `HEq f g` and `HEq x y` +and `f x` and `g y` are well typed it does not follow that `HEq (f x) (g y)`. +(This does follow if you have `f = g` instead.) However if `a` and `b` have +the same type then `a = b` and `HEq a b` ae equivalent. -/ inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where - | refl (a : α) : HEq a a + | /-- Reflexivity of heterogeneous equality. -/ + refl (a : α) : HEq a a +/-- A version of `HEq.refl` with an implicit argument. -/ @[matchPattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a := HEq.refl a @@ -323,7 +449,9 @@ and `Prod.snd p` respectively. You can also write `p.fst` and `p.snd`. For more information: [Constructors with Arguments](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html?highlight=Prod#constructors-with-arguments) -/ structure Prod (α : Type u) (β : Type v) where + /-- The first projection out of a pair. if `p : α × β` then `p.1 : α`. -/ fst : α + /-- The second projection out of a pair. if `p : α × β` then `p.2 : β`. -/ snd : β attribute [unbox] Prod @@ -333,7 +461,9 @@ Similar to `Prod`, but `α` and `β` can be propositions. We use this Type internally to automatically generate the `brecOn` recursor. -/ structure PProd (α : Sort u) (β : Sort v) where + /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/ fst : α + /-- The second projection out of a pair. if `p : PProd α β` then `p.2 : β`. -/ snd : β /-- @@ -341,50 +471,134 @@ Similar to `Prod`, but `α` and `β` are in the same universe. We say `MProd` is the universe monomorphic product type. -/ structure MProd (α β : Type u) where + /-- The first projection out of a pair. if `p : MProd α β` then `p.1 : α`. -/ fst : α + /-- The second projection out of a pair. if `p : MProd α β` then `p.2 : β`. -/ snd : β +/-- +`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be +constructed and destructed like a pair: if `ha : a` and `hb : b` then +`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`. +-/ structure And (a b : Prop) : Prop where - intro :: (left : a) (right : b) + /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/ + intro :: + /-- Extract the left conjunct from a conjunction. `h : a ∧ b` then + `h.left`, also notated as `h.1`, is a proof of `a`. -/ + left : a + /-- Extract the right conjunct from a conjunction. `h : a ∧ b` then + `h.right`, also notated as `h.2`, is a proof of `b`. -/ + right : b +/-- +`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two +constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`, +and you can use `match` or `cases` to destruct an `Or` assumption into the +two cases. +-/ inductive Or (a b : Prop) : Prop where - | inl (h : a) : Or a b - | inr (h : b) : Or a b + | /-- `Or.inl` is "left injection" into an `Or`. If `h : a` then `Or.inl h : a ∨ b`. -/ + inl (h : a) : Or a b + | /-- `Or.inr` is "right injection" into an `Or`. If `h : b` then `Or.inr h : a ∨ b`. -/ + inr (h : b) : Or a b +/-- Alias for `Or.inl`. -/ theorem Or.intro_left (b : Prop) (h : a) : Or a b := Or.inl h +/-- Alias for `Or.inr`. -/ theorem Or.intro_right (a : Prop) (h : b) : Or a b := Or.inr h +/-- +Proof by cases on an `Or`. If `a ∨ b`, and both `a` and `b` imply +proposition `c`, then `c` is true. +-/ theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c := match h with | Or.inl h => left h | Or.inr h => right h +/-- +`Bool` is the type of boolean values, `true` and `false`. Classically, +this is equivalent to `Prop` (the type of propositions), but the distinction +is important for programming, because values of type `Prop` are erased in the +code generator, while `Bool` corresponds to the type called `bool` or `boolean` +in most programming languages. +-/ inductive Bool : Type where - | false : Bool - | true : Bool + | /-- The boolean value `false`, not to be confused with the proposition `False`. -/ + false : Bool + | /-- The boolean value `true`, not to be confused with the proposition `True`. -/ + true : Bool export Bool (false true) -/-- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/ +/-- +`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`. +-/ 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. -/ 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. -/ property : p val set_option linter.unusedVariables.funArgs false in -/-- Gadget for optional parameter support. -/ +/-- +Gadget for optional parameter support. + +A binder like `(x : α := default)` in a declaration is syntax sugar for +`x : optParam α default`, and triggers the elaborator to attempt to use +`default` to supply the argument if it is not supplied. +-/ @[reducible] def optParam (α : Sort u) (default : α) : Sort u := α -/-- Gadget for marking output parameters in type classes. -/ +/-- +Gadget for marking output parameters in type classes. + +For example, the `Membership` class is defined as: +``` +class Membership (α : outParam (Type u)) (γ : Type v) +``` +This means that whenever a typeclass goal of the form `Membership ?α ?γ` comes +up, lean will wait to solve it until `?γ` is known, but then it will run +typeclass inference, and take the first solution it finds, for any value of `?α`, +which thereby determines what `?α` should be. + +This expresses that in a term like `a ∈ s`, `s` might be a `Set α` or +`List α` or some other type with a membership operation, and in each case +the "member" type `α` is determined by looking at the container type. +-/ @[reducible] def outParam (α : Sort u) : Sort u := α set_option linter.unusedVariables.funArgs false in -/-- Auxiliary Declaration used to implement the named patterns `x@h:p` -/ +/-- Auxiliary declaration used to implement named patterns like `x@h:p`. -/ @[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a -/-- Auxiliary axiom used to implement `sorry`. -/ +/-- +Auxiliary axiom used to implement `sorry`. + +The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`. This is a +proof of anything, which is intended for stubbing out incomplete parts of a +proof while still having a syntactically correct proof skeleton. Lean will give +a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but +you can double check if a theorem depends on `sorry` by using +`#print axioms my_thm` and looking for `sorryAx` in the axiom list. + +The `synthetic` flag is false when written explicitly by the user, but it is +set to `true` when a tactic fails to prove a goal, or if there is a type error +in the expression. A synthetic `sorry` acts like a regular one, except that it +suppresses follow-up errors in order to prevent one error from causing a cascade +of other errors because the desired term was not constructed. +-/ @[extern "lean_sorry", neverExtract] axiom sorryAx (α : Sort u) (synthetic := false) : α @@ -404,16 +618,67 @@ theorem ne_true_of_eq_false : {b : Bool} → Eq b false → Not (Eq b true) | true, h => Bool.noConfusion h | false, _ => fun h => Bool.noConfusion h +/-- +`Inhabited α` is a typeclass that says that `α` has a designated element, +called `(default : α)`. This is sometimes referred to as a "pointed type". + +This class is used by functions that need to return a value of the type +when called "out of domain". For example, `Array.get! arr i : α` returns +a value of type `α` when `arr : Array α`, but if `i` is not in range of +the array, it reports a panic message, but this does not halt the program, +so it must still return a value of type `α` (and in fact this is required +for logical consistency), so in this case it returns `default`. +-/ class Inhabited (α : Sort u) where + /-- `default` is a function that produces a "default" element of any + `Inhabited` type. This element does not have any particular specified + properties, but it is often an all-zeroes value. -/ default : α export Inhabited (default) +/-- +`Nonempty α` is a typeclass that says that `α` is not an empty type, +that is, there exists an element in the type. It differs from `Inhabited α` +in that `Nonempty α` is a `Prop`, which means that it does not actually carry +an element of `α`, only a proof that *there exists* such an element. +Given `Nonempty α`, you can construct an element of `α` *nonconstructively* +using `Classical.choice`. +-/ class inductive Nonempty (α : Sort u) : Prop where - | intro (val : α) : Nonempty α + | /-- If `val : α`, then `α` is nonempty. -/ + intro (val : α) : Nonempty α +/-- +**The axiom of choice**. `Nonempty α` is a proof that `α` has an element, +but the element itself is erased. The axiom `choice` supplies a particular +element of `α` given only this proof. + +The textbook axiom of choice normally makes a family of choices all at once, +but that is implied from this formulation, because if `α : ι → Type` is a +family of types and `h : ∀ i, Nonempty (α i)` is a proof that they are all +nonempty, then `fun i => Classical.choice (h i) : ∀ i, α i` is a family of +chosen elements. This is actually a bit stronger than the ZFC choice axiom; +this is sometimes called "[global choice](https://en.wikipedia.org/wiki/Axiom_of_global_choice)". + +In lean, we use the axiom of choice to derive the law of excluded middle +(see `Classical.em`), so it will often show up in axiom listings where you +may not expect. You can use `#print axioms my_thm` to find out if a given +theorem depends on this or other axioms. + +This axiom can be used to construct "data", but obviously there is no algorithm +to compute it, so lean will require you to mark any definition that would +involve executing `Classical.choice` or other axioms as `noncomputable`, and +will not produce any executable code for such definitions. +-/ axiom Classical.choice {α : Sort u} : Nonempty α → α +/-- +The elimination principle for `Nonempty α`. If `Nonempty α`, and we can +prove `p` given any element `x : α`, then `p` holds. Note that it is essential +that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent +to `Classical.choice`. +-/ protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p := match h₁ with | intro a => h₂ a @@ -421,6 +686,10 @@ protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ instance {α : Sort u} [Inhabited α] : Nonempty α := ⟨default⟩ +/-- +A variation on `Classical.choice` that uses typeclass inference to +infer the proof of `Nonempty α`. +-/ noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α := Classical.choice inferInstance @@ -441,55 +710,98 @@ instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : In deriving instance Inhabited for Bool -/-- Universe lifting operation from Sort to Type -/ +/-- Universe lifting operation from `Sort u` to `Type u`. -/ structure PLift (α : Sort u) : Type u where - up :: (down : α) + /-- Lift a value into `PLift α` -/ up :: + /-- Extract a value from `PLift α` -/ down : α -/-- Bijection between α and PLift α -/ -theorem PLift.up_down {α : Sort u} : ∀ (b : PLift α), Eq (up (down b)) b - | up _ => rfl +/-- Bijection between `α` and `PLift α` -/ +theorem PLift.up_down {α : Sort u} (b : PLift α) : Eq (up (down b)) b := rfl -theorem PLift.down_up {α : Sort u} (a : α) : Eq (down (up a)) a := - rfl +/-- Bijection between `α` and `PLift α` -/ +theorem PLift.down_up {α : Sort u} (a : α) : Eq (down (up a)) a := rfl -/-- Pointed types -/ +/-- +`NonemptyType.{u}` is the type of nonempty types in universe `u`. +It is mainly used in constant declarations where we wish to introduce a type +and simultaneously assert that it is nonempty, but otherwise make the type +opaque. +-/ def NonemptyType := Subtype fun α : Type u => Nonempty α +/-- The underlying type of a `NonemptyType`. -/ abbrev NonemptyType.type (type : NonemptyType.{u}) : Type u := type.val +/-- `NonemptyType` is inhabited, because `PUnit` is a nonempty type. -/ instance : Inhabited NonemptyType.{u} where - default := ⟨PUnit.{u+1}, Nonempty.intro ⟨⟩⟩ + default := ⟨PUnit, ⟨⟨⟩⟩⟩ -/-- Universe lifting operation -/ +/-- +Universe lifting operation from a lower `Type` universe to a higher one. +To express this using level variables, the input is `Type s` and the output is +`Type (max s r)`, so if `s ≤ r` then the latter is (definitionally) `Type r`. + +The universe variable `r` is written first so that `ULift.{r} α` can be used +when `s` can be inferred from the type of `α`. +-/ structure ULift.{r, s} (α : Type s) : Type (max s r) where - up :: (down : α) + /-- Lift a value into `ULift α` -/ up :: + /-- Extract a value from `ULift α` -/ down : α -/-- Bijection between α and ULift.{v} α -/ -theorem ULift.up_down {α : Type u} : ∀ (b : ULift.{v} α), Eq (up (down b)) b - | up _ => rfl +/-- Bijection between `α` and `ULift.{v} α` -/ +theorem ULift.up_down {α : Type u} (b : ULift.{v} α) : Eq (up (down b)) b := rfl -theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a := - rfl +/-- Bijection between `α` and `ULift.{v} α` -/ +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. + +`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). + +If a proposition `p` is `Decidable`, then `(by decide : p)` will prove it by +evaluating the decidability instance to `isTrue h` and returning `h`. +-/ class inductive Decidable (p : Prop) where - | isFalse (h : Not p) : Decidable p - | isTrue (h : p) : Decidable p + | /-- Prove 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` -/ + isTrue (h : p) : Decidable p +/-- +Convert a decidable proposition into a boolean value. + +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. +-/ @[inlineIfReduce, 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`. -/ abbrev DecidablePred {α : Sort u} (r : α → Prop) := (a : α) → Decidable (r a) +/-- A decidable relation. See `Decidable`. -/ abbrev DecidableRel {α : Sort u} (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`. +-/ abbrev DecidableEq (α : Sort u) := (a b : α) → Decidable (Eq a b) +/-- Proves that `a = b` is decidable given `DecidableEq α`. -/ def decEq {α : Sort u} [inst : DecidableEq α] (a b : α) : Decidable (Eq a b) := inst a b @@ -524,8 +836,16 @@ theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide | true, false => isFalse (fun h => Bool.noConfusion h) | true, true => isTrue rfl +/-- +`BEq α` is a typeclass for supplying a boolean-valued equality relation on +`α`, notated as `a == b`. Unlike `DecidableEq α` (which uses `a = b`), this +is `Bool` valued instead of `Prop` valued, and it also does not have any +axioms like being reflexive or agreeing with `=`. It is mainly intended for +programming applications. See `LawfulBEq` for a version that requires that +`==` and `=` coincide. +-/ class BEq (α : Type u) where - /-- Boolean equality. -/ + /-- Boolean equality, notated as `a == b`. -/ beq : α → α → Bool open BEq (beq) @@ -535,13 +855,41 @@ instance [DecidableEq α] : BEq α where /-- -We use "dependent" if-then-else to be able to communicate the if-then-else condition to the branches +"Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`, +is sugar for `dite c (fun h => t(h)) (fun h => e(h))`, and it is the same as +`if c then t else e` except that `t` is allowed to depend on a proof `h : c`, +and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypothesis, +even though it has different types in the two cases.) + +We use this to be able to communicate the if-then-else condition to the branches. +For example, `Array.get arr ⟨i, h⟩` expects a proof `h : i < arr.size` in order to +avoid a bounds check, so you can write `if h : i < arr.size then arr.get ⟨i, h⟩ else ...` +to avoid the bounds check inside the if branch. (Of course in this case we have only +lifted the check into an explicit `if`, but we could also use this proof multiple times +or derive `i < arr.size` from some other proposition that we are checking in the `if`.) -/ @[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α := h.casesOn e t /-! # if-then-else -/ +/-- +`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to +return `t` or `e` depending on whether `c` is true or false. The explicit argument +`c : Prop` does not have any actual computational content, but there is an additional +`[Decidable c]` argument synthesized by typeclass inference which actually +determines how to evaluate `c` to true or false. + +Because lean uses a strict (call-by-value) evaluation strategy, the signature of this +function is problematic in that it would require `t` and `e` to be evaluated before +calling the `ite` function, which would cause both sides of the `if` to be evaluated. +Even if the result is discarded, this would be a big performance problem, +and is undesirable for users in any case. To resolve this, `ite` is marked as +`@[macroInline]`, which means that it is unfolded during code generation, and +the definition of the function uses `fun _ => t` and `fun _ => e` so this recovers +the expected "lazy" behavior of `if`: the `t` and `e` arguments delay evaluation +until `c` is known. +-/ @[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α := h.casesOn (fun _ => e) (fun _ => t) @@ -572,6 +920,11 @@ instance [dp : Decidable p] : Decidable (Not p) := /-! # Boolean operators -/ +/-- +`cond b x y` is the same as `if b then x else y`, but optimized for a +boolean condition. This is `@[macroInline]` because `x` and `y` should not +be eagerly evaluated (see `ite`). +-/ @[macroInline] def cond {α : Type u} (c : Bool) (x y : α) : α := match c with | true => x diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index 832ed07969..1f6ee195a6 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -15,8 +15,8 @@ doc string for 'f' is not available "let rec documentation at f " doc string for 'g' is not available "let rec documentation at g " -"Gadget for optional parameter support. " -"Auxiliary Declaration used to implement the named patterns `x@h:p` " +"Gadget for optional parameter support.\n\nA binder like `(x : α := default)` in a declaration is syntax sugar for\n`x : optParam α default`, and triggers the elaborator to attempt to use\n`default` to supply the argument if it is not supplied.\n" +"Auxiliary declaration used to implement named patterns like `x@h:p`. " "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues bulding the telescope if it is a `forall`. " Foo := { range := { pos := { line := 4, column := 0 }, diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index 70685ca24d..bcee707917 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -48,7 +48,13 @@ {"label": "failure", "kind": 5, "detail": "[self : Alternative f] → {α : Type u} → f α"}, - {"label": "false", "kind": 4, "detail": "Bool"}, + {"label": "false", + "kind": 4, + "documentation": + {"value": + "The boolean value `false`, not to be confused with the proposition `False`. ", + "kind": "markdown"}, + "detail": "Bool"}, {"label": "false_and", "kind": 3, "detail": "∀ (p : Prop), (False ∧ p) = False"}, diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index 414115551d..5dcfbc8ee0 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/tests/lean/interactive/completion7.lean.expected.out @@ -1,7 +1,13 @@ {"textDocument": {"uri": "file://completion7.lean"}, "position": {"line": 0, "character": 10}} {"items": - [{"label": "And", "kind": 22, "detail": "Prop → Prop → Prop"}, + [{"label": "And", + "kind": 22, + "documentation": + {"value": + "`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be\nconstructed and destructed like a pair: if `ha : a` and `hb : b` then\n`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.\n", + "kind": "markdown"}, + "detail": "Prop → Prop → Prop"}, {"label": "AndOp", "kind": 7, "detail": "Type u → Type u"}, {"label": "AndThen", "kind": 7, "detail": "Type u → Type u"}, {"label": "and", "kind": 3, "detail": "Bool → Bool → Bool"}, @@ -53,7 +59,25 @@ "position": {"line": 2, "character": 11}} {"items": [{"label": "comm", "kind": 3, "detail": "a ∧ b ↔ b ∧ a"}, - {"label": "intro", "kind": 4, "detail": "a → b → a ∧ b"}, - {"label": "left", "kind": 5, "detail": "a ∧ b → a"}, - {"label": "right", "kind": 5, "detail": "a ∧ b → b"}], + {"label": "intro", + "kind": 4, + "documentation": + {"value": + "`And.intro : a → b → a ∧ b` is the constructor for the And operation. ", + "kind": "markdown"}, + "detail": "a → b → a ∧ b"}, + {"label": "left", + "kind": 5, + "documentation": + {"value": + "Extract the left conjunct from a conjunction. `h : a ∧ b` then\n`h.left`, also notated as `h.1`, is a proof of `a`. ", + "kind": "markdown"}, + "detail": "a ∧ b → a"}, + {"label": "right", + "kind": 5, + "documentation": + {"value": + "Extract the right conjunct from a conjunction. `h : a ∧ b` then\n`h.right`, also notated as `h.2`, is a proof of `b`. ", + "kind": "markdown"}, + "detail": "a ∧ b → b"}], "isIncomplete": true} diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index ad75a1f40d..4f31e07b68 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -4,7 +4,7 @@ {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 18}}, "contents": {"value": - "```lean\nTrue.intro : True\n```\n***\nIntroduction rule for `True`. ", + "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 7, "character": 8}} @@ -12,7 +12,7 @@ {"start": {"line": 7, "character": 8}, "end": {"line": 7, "character": 18}}, "contents": {"value": - "```lean\nTrue.intro : True\n```\n***\nIntroduction rule for `True`. ", + "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 12, "character": 4}} @@ -35,7 +35,7 @@ {"start": {"line": 21, "character": 13}, "end": {"line": 21, "character": 23}}, "contents": {"value": - "```lean\nTrue.intro : True\n```\n***\nIntroduction rule for `True`. ", + "```lean\nTrue.intro : True\n```\n***\n`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 31, "character": 2}} @@ -114,7 +114,7 @@ null {"start": {"line": 97, "character": 8}, "end": {"line": 97, "character": 10}}, "contents": {"value": - "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nIdentity function ", + "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 97, "character": 10}} diff --git a/tests/lean/interactive/lean3HoverIssue.lean.expected.out b/tests/lean/interactive/lean3HoverIssue.lean.expected.out index babbad6ca6..e3184a3192 100644 --- a/tests/lean/interactive/lean3HoverIssue.lean.expected.out +++ b/tests/lean/interactive/lean3HoverIssue.lean.expected.out @@ -4,7 +4,7 @@ {"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is a symmetric relationship.\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 0, "character": 52}} @@ -17,7 +17,7 @@ {"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is a symmetric relationship.\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 7, "character": 54}} @@ -25,7 +25,7 @@ {"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is a symmetric relationship.\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 7, "character": 65}} @@ -33,7 +33,7 @@ {"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is a symmetric relationship.\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", "kind": "markdown"}} {"textDocument": {"uri": "file://lean3HoverIssue.lean"}, "position": {"line": 7, "character": 70}} @@ -46,5 +46,5 @@ {"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}}, "contents": {"value": - "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is a symmetric relationship.\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", + "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n", "kind": "markdown"}}