Lean core references

Every Lean core declaration referred to directly by this project’s own code, grouped by the module it comes from.

definition abbreviation theorem

legend

`BinderNameHint`

binderNameHint

The expression binderNameHint v binder e defined to be e.

If it is used on the right-hand side of an equation that is used for rewriting by rw or simp, and v is a local variable, and binder is an expression that (after beta-reduction) is a binder (fun w => … or ∀ w, …), then it will rename v to the name used in that binder, and remove the binderNameHint.

A typical use of this gadget would be as follows; the gadget ensures that after rewriting, the local variable is still name, and not x:

theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
    l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry

example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
  rw [all_eq_not_any_not]
  -- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true

If binder is not a binder, then the name of v attains a macro scope. This only matters when the resulting term is used in a non-hygienic way, e.g. in termination proofs for well-founded recursion.

This gadget is supported by * simp, dsimp and rw in the right-hand-side of an equation * simp in the assumptions of congruence rules

It is ineffective in other positions (hypotheses of rewrite rules) or when used by other tactics (e.g. apply).

def binderNameHint.{u, v, w} {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ

Used by: BitFunction.exists_settle

`ByCases`

if_true

theorem if_true.{u_1} {α : Sort u_1} {x✝ : Decidable True} (t e : α) : (if True then t else e) = t

Used by: Frame.crcStep_poly, Frame.toPoly_ne_zero_of_any, Logic.PropositionalLogic.Formula.kalmar

`Classical`

Classical.byContradiction

theorem Classical.byContradiction {p : Prop} (h : ¬p → False) : p

Used by: Frame.crcStep_poly, arithZero_unique

Classical.choose

Given that there exists an element satisfying p, returns one such element.

This is a straightforward consequence of, and equivalent to, Classical.choice.

See also choose_spec, which asserts that the returned value has property p.

def Classical.choose.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α

Used by: Structure.Arithmetic.pred, Structure.Arithmetic.the

Classical.choose_spec

theorem Classical.choose_spec.{u} {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (Classical.choose h)

Used by: Structure.Arithmetic.S_pred, Structure.Arithmetic.the_spec

Classical.not_forall

theorem Classical.not_forall.{u_1} {α : Sort u_1} {p : α → Prop} : (¬∀ (x : α), p x) ↔ ∃ x, ¬p x

Used by: SeqColimit.exists_not_mem_range, Structure.Arithmetic.exists_S_of_not_Z, Structure.Arithmetic.instDefS

Classical.or_iff_not_imp_left

theorem Classical.or_iff_not_imp_left {a b : Prop} : a ∨ b ↔ ¬a → b

Used by: Logic.Popper.Basis1.contract, Logic.Popper.Basis1.exchange

Exists.choose

Extract an element from an existential statement, using Classical.choose.

def Exists.choose.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : α

Used by: Discrete.size, Discrete.size_eq, HeapCover.whole, HeapCover.whole_at, Layer.toFun, SeqColimit.fresh, Tower.heapBot, Tower.heapTop

Exists.choose_spec

Show that an element extracted from P : ∃ a, p a using P.choose satisfies p.

theorem Exists.choose_spec.{u_1} {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : p P.choose

Used by: Discrete.size_eq, HeapCover.whole, HeapCover.whole_at, Layer.toFun_spec, SeqColimit.fresh_spec, Tower.heapBot, Tower.heapTop

`Control.Id`

Id

The identity function on types, used primarily for its Monad instance.

The identity monad is useful together with monad transformers to construct monads for particular purposes. Additionally, it can be used with do-notation in order to use control structures such as local mutability, for-loops, and early returns in code that does not otherwise use monads.

Examples: lean example def containsFive (xs : List Nat) : Bool := Id.run do for x in xs do if x == 5 then return true return false

lean example #eval containsFive [1, 3, 5, 7]

true

def Id.{u} (type : Type u) : Type u

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations

Id.run

Runs a computation in the identity monad.

This function is the identity function. Because its parameter has type Id α, it causes do-notation in its arguments to use the Monad Id instance.

def Id.run.{u_1} {α : Type u_1} (x : Id α) : α

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations

`Core`

Bool.of_not_eq_true

theorem Bool.of_not_eq_true {b : Bool} : ¬b = true → b = false

Used by: Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.semantic_iff_provable

Decidable.byContradiction

theorem Decidable.byContradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) : p

Empty.elim

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.

def Empty.elim.{u} {C : Sort u} : Empty → C

Used by: InterfaceOld.unit, arithStruct, arithStruct_congr, arithTower, instIsEmptyPortsUnit_computerChips, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

Eq.mp

If h : α = β is a proof of type equality, then h.mp : α → β is the induced “cast” operation, mapping elements of α to elements of β.

You can prove theorems about the resulting element by induction on h, since rfl.mp is definitionally the identity function.

def Eq.mp.{u} {α β : Sort u} (h : α = β) (a : α) : β

Eq.mpr

If h : α = β is a proof of type equality, then h.mpr : β → α is the induced “cast” operation in the reverse direction, mapping elements of β to elements of α.

You can prove theorems about the resulting element by induction on h, since rfl.mpr is definitionally the identity function.

def Eq.mpr.{u} {α β : Sort u} (h : α = β) (b : β) : α

Exists

Existential quantification. If p : α → Prop is a predicate, then ∃ x : α, p x asserts that there is some x of type α such that p x holds. To create an existential proof, use the exists tactic, or the anonymous constructor notation ⟨x, h⟩. To unpack an existential, use cases h where h is a proof of ∃ x : α, p x, or let ⟨x, hx⟩ := h where `.

Because Lean has proof irrelevance, any two proofs of an existential are definitionally equal. One consequence of this is that it is impossible to recover the witness of an existential from the mere fact of its existence. For example, the following does not compile:

example (h : ∃ x : Nat, x = x) : Nat :=
  let ⟨x, _⟩ := h  -- fail, because the goal is `Nat : Type`
  x

The error message recursor 'Exists.casesOn' can only eliminate into Prop means that this only works when the current goal is another proposition:

example (h : ∃ x : Nat, x = x) : True :=
  let ⟨x, _⟩ := h  -- ok, because the goal is `True : Prop`
  trivial

inductive Exists.{u} {α : Sort u} (p : α → Prop) : Prop

ForInStep

An indication of whether a loop’s body terminated early that’s used to compile the for x in xs notation.

A collection’s ForIn or ForIn' instance describes how to iterate over its elements. The monadic action that represents the body of the loop returns a ForInStep α, where α is the local state used to implement features such as let mut.

inductive ForInStep.{u} (α : Type u) : Type u

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations

Iff

If and only if, or logical bi-implication. a ↔︎ b means that a implies b and vice versa. By propext, this implies that a and b are equal and hence any expression involving a is equivalent to the corresponding expression with b instead.

Conventions for notations in identifiers:

The recommended spelling of ↔︎ in identifiers is iff.
The recommended spelling of <-> in identifiers is iff (prefer ↔︎ over <->).

structure Iff (a b : Prop) : Prop

Iff.of_eq

theorem Iff.of_eq {a b : Prop} (h : a = b) : a ↔ b

Used by: arithTower

Iff.rfl

theorem Iff.rfl {a : Prop} : a ↔ a

Used by: InterfaceOld.Value.ext_of_fired_eq, Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset, Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons, Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons, Logic.PropositionalLogic.Formula.syntactic_iff_provable, SimpleGraph.induceComplSingletonEquiv, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.stepTo_le_iff, arithStruct_congr

Iff.symm

theorem Iff.symm {a b : Prop} (h : a ↔ b) : b ↔ a

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic, Specification.galoisConnection

Iff.trans

theorem Iff.trans {a b c : Prop} (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c

Used by: Logic.Popper.Basis1.isClassicalNegation_congr, Logic.Popper.Basis1.isConjunction_congr, Logic.Popper.Basis1.isDisjunction_congr, Logic.Popper.Basis1.isImplication_congr, Logic.Popper.Basis1.isIntuitionisticNegation_congr, Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons, Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons, Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

InvImage

The inverse image of r : β → β → Prop by a function α → β is the relation s : α → α → Prop defined by s a b = r (f a) (f b).

def InvImage.{u, v} {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) : α → α → Prop

Used by: Logic.ProofTheory.Derivation.toCutFree

Nat.add_zero

theorem Nat.add_zero (n : ℕ) : n + 0 = n

Used by: Component.monoidalCategory, Component.monoidalCategoryStruct, Component.parallel_empty

Ne

a ≠ b, or Ne a b is defined as ¬ (a = b) or a = b → False, and asserts that a and b are not equal.

Conventions for notations in identifiers:

The recommended spelling of ≠ in identifiers is ne.

def Ne.{u} {α : Sort u} (a b : α) : Prop

Ne.symm

theorem Ne.symm.{u} {α : Sort u} {a b : α} (h : a ≠ b) : b ≠ a

Used by: BitFunction.exists_settle, Frame.ofFn_update, Logic.FirstOrderLogic.basis3ext, Logic.FirstOrderLogic.hasExistential, Logic.FirstOrderLogic.hasUniversal

Not.intro

theorem Not.intro {a : Prop} (h : a → False) : ¬a

Used by: Channel.lossless_stationary, Component.Simplex.toInformationSystem, Component.parallel, Component.sequential, InformationSystem.Environment.universe, InformationSystem.Step.delta_alt, InformationSystem.eval_delta, InformationSystem.roundtrip_neutral, InformationSystem.toSimplex, irrational_logb_two_five, irrational_logb_two_three

PSigma

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.

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.

structure PSigma.{u, v} {α : Sort u} (β : α → Sort v) : Sort (max (max 1 u) v)

Used by: Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.DerivationsOf.forall_toCutFree, Topology.runArrows'

PSum

The disjoint union of arbitrary sorts α β, or α ⊕' β.

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.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

Used by: Logic.ProofTheory.Derivation.toCutFree

Quotient

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.{u} {α : Sort u} (s : Setoid α) : Sort u

Used by: Component.Hom, Component.Hom.recast_recast, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, SeqColimit, Structure.Arithmetic.Tower.Colimit

Quotient.exact

If two values are equal in a quotient, then they are related by its equivalence relation.

theorem Quotient.exact.{u} {α : Sort u} {s : Setoid α} {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b

Used by: SeqColimit.freshSeq_lt_ne, SeqColimit.mk_injective, arithPlus_iff, arithSucc_iff

Quotient.ind

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with Quotient.mk.

theorem Quotient.ind.{u} {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} :
  (∀ (a : α), motive ⟦a⟧) → ∀ (q : Quotient s), motive q

Used by: Component.Hom.comp_assoc, Component.Hom.comp_eqToHom, Component.Hom.comp_id, Component.Hom.eqToHom_comp, Component.Hom.id_comp, Component.Hom.recast_recast, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.monoidalCategory, Structure.Arithmetic.Tower.exists_of_le_ι, arithFromNat_toNat

Quotient.lift

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.

abbrev Quotient.lift.{u, v} {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) :
  (∀ (a b : α), a ≈ b → f a = f b) → Quotient s → β

Used by: arithSucc_iff, arithToNat

Quotient.lift₂

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.

abbrev Quotient.lift₂.{uA, uB, uC} {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α}
  {s₂ : Setoid β} (f : α → β → φ)
  (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
  (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instPeanoStandard

Quotient.mk

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.

def Quotient.mk.{u} {α : Sort u} (s : Setoid α) (a : α) : Quotient s

Used by: Component.Hom.comp_assoc, Component.Hom.comp_eqToHom, Component.Hom.eqToHom_comp, Component.Hom.id, Component.Hom.recast_recast, Component.Hom.symmetry, Component.Hom.tensorUnit, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, SeqColimit.mk, Structure.Arithmetic.Tower.exists_of_le_ι, Structure.Arithmetic.Tower.ι, arithFromNat_toNat

Quotient.sound

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 Quotient.sound.{u} {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧

Used by: Component.Hom.comp_assoc, Component.Hom.comp_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id_comp, Component.Hom.symmetry_symmetry, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.monoidalCategory, SeqColimit.mk_stepTo, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.ι_stepTo, arithFromNat_toNat

Relation.TransGen

The transitive closure TransGen r of a relation r is the smallest relation which is transitive and contains r. TransGen r a z if and only if there exists a sequence a r b r ... r z of length at least 1 connecting a to z.

inductive Relation.TransGen.{u} {α : Sort u} (r : α → α → Prop) : α → α → Prop

Used by: Mereology.ProperPart

Setoid

A setoid is a type with a distinguished equivalence relation, denoted ≈.

The Quotient type constructor requires a Setoid instance.

structure Setoid.{u} (α : Sort u) : Sort (max 1 u)

Used by: Component.Arrow.setoid, SeqColimit.setoid, Structure.Arithmetic.Tower.setoid

Sigma

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.

structure Sigma.{u, v} {α : Type u} (β : α → Type v) : Type (max u v)

Subsingleton

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.

structure Subsingleton.{u} (α : Sort u) : Prop

Used by: InterfaceOld.unit.Value.subsingleton

Subsingleton.elim

If a type is a subsingleton, then all of its elements are equal.

theorem Subsingleton.elim.{u} {α : Sort u} [h : Subsingleton α] (a b : α) : a = b

Used by: Specification.closed, Topology.nerveCoverage

Subtype.ext

theorem Subtype.ext.{u} {α : Sort u} {p : α → Prop} {a1 a2 : { x // p x }} : ↑a1 = ↑a2 → a1 = a2

Used by: InterfaceOld.Value.ext_of_fired_eq, SimpleGraph.induceComplSingletonEquiv

Sum

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.{u, v} (α : Type u) (β : Type v) : Type (max u v)

Used by: Finset.sum_preimage_map_disjUnion, Interface.combine, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor, Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex

bne

x != y is boolean not-equal. It is the negation of x == y which is supplied by the BEq typeclass.

Unlike x ≠ y (which is notation for Ne x y), this is Bool valued instead of Prop valued. It is mainly intended for programming applications.

Conventions for notations in identifiers:

The recommended spelling of != in identifiers is bne.

def bne.{u} {α : Type u} [BEq α] (a b : α) : Bool

Used by: Frame.toPoly_xor

decide_true

theorem decide_true (h : Decidable True) : decide True = true

Used by: Frame.crc32Ethernet_detects_single_bit_flip

dif_neg

theorem dif_neg.{u} {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} :
  dite c t e = e hnc

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Heap.combine_at_right, Structure.Arithmetic.iter_step

dif_pos

theorem dif_pos.{u} {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} :
  dite c t e = t hc

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Heap.combine_at_left, Heap.combine_at_right, Structure.Arithmetic.iter_base

funext

Function extensionality. If two functions return equal results for all possible arguments, then they are equal.

It is called “extensionality” because it provides a way to prove two objects equal based on the properties of the underlying mathematical functions, rather than based on the syntax used to denote them. Function extensionality is a theorem that can be proved using quotient types.

theorem funext.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) : f = g

Used by: BitSequence.trueCount_strict, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.interchange, Component.monoidalCategory, Component.parallel_assoc, Component.parallel_comm, Component.symmetry_symmetry, Finset.sum_preimage_map_disjUnion, Frame.crc32Ethernet_detects_single_bit_flip, Frame.toPoly_xor, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, Layer.eq_toFun_of_univalent, Layer.id_sequential, Layer.sequential_assoc, Layer.sequential_id, Layer.sequential_rel, Layer.trace_naturality_left, Layer.trace_naturality_right, Layer.trace_sliding, Layer.trace_superposing, Layer.trace_vanishing, Layer.trace_yanking, Logic.FirstOrderLogic.realize_SUB, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset, Logic.PropositionalLogic.Formula.bigOr_val, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.minterm_val, Structure.Arithmetic.exists_S_of_not_Z, Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.instDefS, Structure.Arithmetic.rec_base, Topology.isNerveCover_inter

if_neg

theorem if_neg.{u} {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (if c then t else e) = e

Used by: Frame.crcStep_length, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Structure.Arithmetic.S_iff_add_one, Topology.step_conserves

if_pos

theorem if_pos.{u} {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (if c then t else e) = t

Used by: Frame.crcStep_length, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Logic.PropositionalLogic.Formula.completeness, Structure.Arithmetic.S_iff_add_one, Topology.step_conserves

le_of_le_of_eq

theorem le_of_le_of_eq.{u_1} {α : Type u_1} {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c

noConfusionEnum

Auxiliary definition for generating compact noConfusion for enumeration types

abbrev noConfusionEnum.{u, v, w} {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w}
  {x y : α} (h : x = y) : noConfusionTypeEnum f P x y

Used by: ApplicationLayer.Op, Difficulty, DoorState, Icmp, Kind, NetworkLayer.Protocol, Quality, Topology.Signal, TrafficLightColor

noConfusionTypeEnum

Auxiliary definition for generating compact noConfusion for enumeration types

abbrev noConfusionTypeEnum.{u, v, w} {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β)
  (P : Sort w) (x y : α) : Sort w

Used by: ApplicationLayer.Op, Difficulty, DoorState, Icmp, Kind, NetworkLayer.Protocol, Quality, Topology.Signal, TrafficLightColor

not_false_iff

theorem not_false_iff : ¬False ↔ True

Used by: Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent

trivial

True is true, and True.intro (or more commonly, trivial) is the proof.

theorem trivial : True

Used by: InterfaceOld.homogeneous, InterfaceOld.unit, Layer.trace_vanishing, Logic.Popper.Basis1.instHasExistentialNatUnitTotalBasis1InferInstanceHasSubstitutionMutual, Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1, Logic.Popper.Basis1.instHasUniversalNatUnitTotalBasis1InferInstanceHasSubstitutionMutual, Logic.Popper.Basis1.totalBasis1, doorHeap.closed_reachable, doorHeap.opened_reachable, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass

`Data.Array.Basic`

Array.append

Appends two arrays. Normally used via the ++ operator.

Appending arrays takes time proportional to the length of the second array.

Examples: * #[1, 2, 3] ++ #[4, 5] = #[1, 2, 3, 4, 5]. * #[] ++ #[4, 5] = #[4, 5]. * #[1, 2, 3] ++ #[] = #[1, 2, 3].

def Array.append.{u} {α : Type u} (as bs : Array α) : Array α

Used by: unexpandSeqAppend

Array.contains

Checks whether a is an element of as, using == to compare elements.

Array.elem is a synonym that takes the element before the array.

Examples: * #[1, 4, 2, 3, 3, 7].contains 3 = true * Array.contains #[1, 4, 2, 3, 3, 7] 5 = false

def Array.contains.{u} {α : Type u} [BEq α] (as : Array α) (a : α) : Bool

Used by: isExample, isIgnored, isLemma

`Data.Bool`

Bool.and_eq_true_iff

theorem Bool.and_eq_true_iff {x y : Bool} : (x && y) = true ↔ x = true ∧ y = true

Used by: Logic.PropositionalLogic.Formula.and_entails_left, Logic.PropositionalLogic.Formula.and_entails_right, Logic.PropositionalLogic.Formula.entails_and_iff

Bool.and_not_self

theorem Bool.and_not_self (x : Bool) : (x && !x) = false

Used by: Logic.PropositionalLogic.Formula.val_falsum'

Bool.bne_false

theorem Bool.bne_false (b : Bool) : (b != false) = b

Used by: Frame.toPoly_xor

Bool.bne_true

theorem Bool.bne_true (b : Bool) : (b != true) = !b

Used by: Frame.toPoly_xor

Bool.eq_iff_iff

theorem Bool.eq_iff_iff {a b : Bool} : a = b ↔ (a = true ↔ b = true)

Used by: Logic.PropositionalLogic.Formula.exists_andOrNot_of_boolFun

Bool.false_eq_true

These two rules follow trivially by simp, but are needed to avoid non-termination in false_eq and true_eq.

theorem Bool.false_eq_true : (false = true) = False

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.crcStep_poly, Frame.pos_length_of_any, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any, Frame.toPoly_replicate_false, Frame.toPoly_set_flip, Frame.toPoly_xor, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Logic.PropositionalLogic.Formula.bigOr_val, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.literal_val

Bool.not_and

De Morgan’s law for boolean and

theorem Bool.not_and (x y : Bool) : (!(x && y)) = (!x || !y)

Used by: Logic.PropositionalLogic.NandFormula.toFormula_val

Bool.not_or_self

theorem Bool.not_or_self (x : Bool) : (!x || x) = true

Used by: Logic.PropositionalLogic.Formula.val_verum'

Bool.or_eq_true_iff

theorem Bool.or_eq_true_iff {x y : Bool} : (x || y) = true ↔ x = true ∨ y = true

Used by: Logic.PropositionalLogic.semanticConnectives

Bool.true_eq_false

theorem Bool.true_eq_false : (true = false) = False

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Logic.PropositionalLogic.Formula.literal_val

Bool.xor

Boolean “exclusive or”. xor x y can be written x ^^ y.

x ^^ y is true when precisely one of x or y is true. Unlike and and or, it does not have short-circuiting behavior, because one argument’s value never determines the final value. Also unlike and and or, there is no commonly-used corresponding propositional connective.

Examples: * false ^^ false = false * true ^^ false = true * false ^^ true = true * true ^^ true = false

Conventions for notations in identifiers:

The recommended spelling of ^^ in identifiers is xor.

abbrev Bool.xor : Bool → Bool → Bool

Used by: Frame.crcStep, Frame.crcStep_length, Frame.crcStep_poly, Frame.toPoly_xor

`Data.Cast`

Nat.cast

The canonical homomorphism Nat → R. In most use cases, the target type will have a (semi)ring structure, and this homomorphism should be a (semi)ring homomorphism.

NatCast and IntCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with NatCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus a NatCast R instance) whenever R is an additive monoid with a 1.

The prototypical example is Int.ofNat.

def Nat.cast.{u} {R : Type u} [NatCast R] : ℕ → R

`Data.Fin.Basic`

Fin.cast

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.

def Fin.cast {n m : ℕ} (eq : n = m) (i : Fin n) : Fin m

Used by: Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_assoc, Component.parallel_empty, Component.recast, Frame.crc32Ethernet_detects_single_bit_flip, arithStepNeg, arithStepNeg_injective, arithStepNeg_not_surjective

Fin.castAdd

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.

def Fin.castAdd {n : ℕ} (m : ℕ) : Fin n → Fin (n + m)

Used by: Component.Hom.tensor_id_id, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.interchange, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.parallel_empty, Component.symmetry, Component.symmetry_symmetry, Fin.append_eval, InformationSystem.parallel_delta

Fin.castSucc

Coarsens a bound by one.

def Fin.castSucc {n : ℕ} : Fin n → Fin (n + 1)

Used by: Structure.Arithmetic.finTower, arithStepNeg, arithStepNeg_injective, arithStepNeg_not_surjective, arithStepPos, castSucc_not_surjective

Fin.elim0

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 Fin.elim0.{u} {α : Sort u} : Fin 0 → α

Used by: Component.empty, Component.empty_parallel, Component.monoidalCategory, Component.parallel_empty

Fin.last

The greatest value of Fin (n+1), namely n.

Examples: * Fin.last 4 = (4 : Fin 5) * (Fin.last 0).val = (0 : Nat)

def Fin.last (n : ℕ) : Fin (n + 1)

Used by: Structure.Arithmetic.finTower, arithFromNat, arithFromNat_toNat, arithPlus_iff, arithStepNeg_not_surjective, arithSucc_iff, castSucc_not_surjective

Fin.natAdd

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 Fin.natAdd {m : ℕ} (n : ℕ) (i : Fin m) : Fin (n + m)

Used by: Component.Hom.tensor_id_id, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.interchange, Component.parallel, Component.parallel_assoc, Component.parallel_comm, Component.parallel_congr, Component.symmetry, Component.symmetry_symmetry, Fin.append_eval, InformationSystem.parallel_delta

Fin.succ

The successor, with an increased bound.

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 Fin.succ {n : ℕ} : Fin n → Fin (n + 1)

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.toPoly_set_flip

Fin.val_congr

theorem Fin.val_congr {n : ℕ} {a b : Fin n} (h : a = b) : ↑a = ↑b

Used by: Fin.append_eval

Fin.val_lt_of_le

theorem Fin.val_lt_of_le {n b : ℕ} (i : Fin b) (h : b ≤ n) : ↑i < n

Used by: Frame.toPoly_set_flip

`Data.Fin.Lemmas`

Fin.cases

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.

def Fin.cases.{u_1} {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0)
  (succ : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) : motive i

Used by: Frame.toPoly_set_flip

Fin.castSucc_lt_last

theorem Fin.castSucc_lt_last {n : ℕ} (a : Fin n) : a.castSucc < Fin.last n

Used by: arithStepNeg_not_surjective, castSucc_not_surjective

Fin.cast_refl

theorem Fin.cast_refl (n : ℕ) (h : n = n) : Fin.cast h = id

Used by: Component.parallel_empty, Component.recast

Fin.ext

theorem Fin.ext {n : ℕ} {a b : Fin n} (h : ↑a = ↑b) : a = b

Used by: Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_assoc, Fin.append_eval, Frame.reflectIndex_involutive, InformationSystem.exists_repeat_state, Structure.Arithmetic.finTower, arithFromNat_toNat

Fin.ext_iff

theorem Fin.ext_iff {n : ℕ} {a b : Fin n} : a = b ↔ ↑a = ↑b

Used by: Frame.ofFn_update, Structure.Arithmetic.instArithFin

Fin.le_def

theorem Fin.le_def {n : ℕ} {a b : Fin n} : a ≤ b ↔ ↑a ≤ ↑b

Used by: Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.finTower

Fin.lt_def

theorem Fin.lt_def {n : ℕ} {a b : Fin n} : a < b ↔ ↑a < ↑b

Used by: Structure.Arithmetic.S_iff_add_one

Fin.val_add

theorem Fin.val_add {n : ℕ} (a b : Fin n) : ↑(a + b) = (↑a + ↑b) % n

Used by: Structure.Arithmetic.S_iff_add_one

Fin.val_castSucc

theorem Fin.val_castSucc {n : ℕ} (i : Fin n) : ↑i.castSucc = ↑i

Used by: Structure.Arithmetic.finTower

Fin.val_eq_zero

theorem Fin.val_eq_zero (a : Fin 1) : ↑a = 0

Used by: Frame.crc32Ethernet_detects_single_bit_flip

Fin.val_last

theorem Fin.val_last (n : ℕ) : ↑(Fin.last n) = n

Used by: Structure.Arithmetic.finTower, arithFromNat_toNat, arithPlus_iff, arithSucc_iff, arithToNat_fromNat

Fin.zero_le

theorem Fin.zero_le {n : ℕ} [NeZero n] (a : Fin n) : 0 ≤ a

Used by: Structure.Arithmetic.Z_iff_zero_fin

`Data.Function`

Function.Injective

A function f : α → β is called injective if f x = f y implies x = y.

def Function.Injective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

Used by: Cell.erase_not_injective, Cell.erase_not_surjective, FiniteStateMachine.Reversible, Frame.crc32Ethernet_detects_single_bit_flip, InformationSystem.reversible, SeqColimit.freshSeq_injective, SeqColimit.freshSeq_lt_ne, SeqColimit.infinite, SeqColimit.mk_injective, Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.ι_injective, Tower, arithStepNeg_injective, arithSuccFun_injective, arithToNat_injective

Function.Surjective

A function f : α → β is called surjective if every b : β is equal to f a for some a : α.

def Function.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

Used by: Cell.erase_not_surjective, SeqColimit.exists_not_mem_range, SeqColimit.fresh, SeqColimit.freshSeq, SeqColimit.freshSeq_injective, SeqColimit.freshSeq_lt_ne, SeqColimit.fresh_spec, SeqColimit.infinite, Structure.Arithmetic.Tower, Structure.Arithmetic.count_surjective, Structure.Arithmetic.finTower, Tower, arithStepNeg_not_surjective, castSucc_not_surjective

`Data.Int.Basic`

Int

The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for Int that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually GMP). A “small number” is an integer that can be encoded with one fewer bits than the platform’s pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).

inductive Int : Type

Int.cast

The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure, and this homomorphism should be a ring homomorphism.

IntCast and NatCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an IntCast R instance) whenever R is an additive group with a 1.

def Int.cast.{u} {R : Type u} [IntCast R] : ℤ → R

Used by: irrational_logb_two_five, irrational_logb_two_three

Int.natAbs

The absolute value of an integer is its distance from 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples: * (7 : Int).natAbs = 7 * (0 : Int).natAbs = 0 * (-11 : Int).natAbs = 11

def Int.natAbs (m : ℤ) : ℕ

Used by: arithFromNat_toNat, arithLevel, arithLevel_negNatAbs, arithPlus_iff, arithStepNeg, arithStepNeg_injective, arithStepNeg_not_surjective, arithStepNeg_val, arithStepPos, arithStepPos_val, arithStepTo_val, arithSucc_iff, arithToNat, arithTower

Int.negOfNat

Negation of natural numbers.

Examples: * Int.negOfNat 6 = -6 * Int.negOfNat 0 = 0

def Int.negOfNat : ℕ → ℤ

Int.toNat

Converts an integer into a natural number. Negative numbers are converted to 0.

Examples: * (7 : Int).toNat = 7 * (0 : Int).toNat = 0 * (-7 : Int).toNat = 0

def Int.toNat : ℤ → ℕ

Used by: irrational_logb_two_five, irrational_logb_two_three

`Data.Int.DivMod.Basic`

Int.natCast_ediv

theorem Int.natCast_ediv (m n : ℕ) : ↑(m / n) = ↑m / ↑n

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive

`Data.Int.DivMod.Bootstrap`

Int.emod_def

theorem Int.emod_def (a b : ℤ) : a % b = a - b * (a / b)

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Int.lt_mul_ediv_self_add

theorem Int.lt_mul_ediv_self_add {x k : ℤ} (h : 0 < k) : x < k * (x / k) + k

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Int.mul_ediv_self_le

theorem Int.mul_ediv_self_le {x k : ℤ} (h : k ≠ 0) : k * (x / k) ≤ x

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Int.natCast_emod

theorem Int.natCast_emod (m n : ℕ) : ↑(m % n) = ↑m % ↑n

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

`Data.Int.Lemmas`

Int.natCast_mul

theorem Int.natCast_mul (n m : ℕ) : ↑(n * m) = ↑n * ↑m

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Int.sub_eq_zero_of_eq

theorem Int.sub_eq_zero_of_eq {a b : ℤ} (h : a = b) : a - b = 0

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Frame.crc32Ethernet_detects_single_bit_flip, Frame.crcStep_length, Frame.crcStep_poly, Frame.reflectIndex, Frame.reflectIndex_involutive, Frame.toPoly_set_flip, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Z_iff_zero, Structure.Arithmetic.finTower, Structure.Arithmetic.instNeZeroNat_structure, Structure.Arithmetic.instPeanoNat, arithPlus_succ, arithSucc_no_fixed_point, arithZero_not_succ, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

`Data.Int.Order`

Int.natAbs_neg

theorem Int.natAbs_neg (a : ℤ) : (-a).natAbs = a.natAbs

Used by: arithLevel_negNatAbs

Int.natCast_nonneg

theorem Int.natCast_nonneg (n : ℕ) : 0 ≤ ↑n

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Frame.toPoly_set_flip, Logic.ProofTheory.Derivation.toCutFree, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Z_iff_zero, Structure.Arithmetic.instPeanoNat, arithZero_not_succ

Int.sub_nonneg_of_le

theorem Int.sub_nonneg_of_le {a b : ℤ} (h : b ≤ a) : 0 ≤ a - b

Int.toNat_of_nonneg

theorem Int.toNat_of_nonneg {a : ℤ} (h : 0 ≤ a) : ↑a.toNat = a

Used by: irrational_logb_two_five, irrational_logb_two_three

`Data.List.Basic`

List.Mem

List membership, typically accessed via the ∈ operator.

a ∈ l means that a is an element of the list l. Elements are compared according to Lean’s logical equality.

The related function List.elem is a Boolean membership test that uses a BEq α instance.

Examples: * a ∈ [x, y, z] ↔︎ a = x ∨ a = y ∨ a = z

inductive List.Mem.{u} {α : Type u} (a : α) : List α → Prop

Used by: Logic.Popper.Basis1.substitutivity, Ontology.empty_wellFormed, arithPlus_iff, arithSucc_iff

List.Nodup

The list has no duplicates: it contains every element at most once.

It is defined as Pairwise (· ≠ ·): each element is unequal to all other elements.

def List.Nodup.{u} {α : Type u} : List α → Prop

Used by: Logic.PropositionalLogic.Formula.eliminate

List.any

Returns true if p returns true for any element of l.

O(|l|). Short-circuits upon encountering the first true.

Examples: * [2, 4, 6].any (· % 2 = 0) = true * [2, 4, 6].any (· % 2 = 1) = false * [2, 4, 5, 6].any (· % 2 = 0) = true * [2, 4, 5, 6].any (· % 2 = 1) = true

def List.any.{u} {α : Type u} (l : List α) (p : α → Bool) : Bool

Used by: Frame.crc32EthernetPoly_any, Frame.crcFrom_detects_single_bit_flip, Frame.crc_detects_single_bit_flip, Frame.generator_not_dvd_pow, Frame.pos_length_of_any, Frame.toPoly_ne_zero_of_any

List.append_assoc

theorem List.append_assoc.{u} {α : Type u} (as bs cs : List α) : as ++ bs ++ cs = as ++ (bs ++ cs)

Used by: Logic.Popper.Basis1.demonstrate_congr_premise

List.append_nil

theorem List.append_nil.{u} {α : Type u} (as : List α) : as ++ [] = as

Used by: Logic.Popper.Basis1.demonstrate_singleton

List.cons_append

theorem List.cons_append.{u} {α : Type u} {a : α} {as bs : List α} : a :: as ++ bs = a :: (as ++ bs)

Used by: Logic.Popper.Basis1.demonstrate_congr_premise

List.filter

Returns the list of elements in l for which p returns true.

O(|l|).

Examples: * [1, 2, 5, 2, 7, 7].filter (· > 2) = [5, 7, 7] * [1, 2, 5, 2, 7, 7].filter (fun _ => false) = [] * [1, 2, 5, 2, 7, 7].filter (fun _ => true) = [1, 2, 5, 2, 7, 7]

def List.filter.{u} {α : Type u} (p : α → Bool) (l : List α) : List α

Used by: Logic.PropositionalLogic.Formula.dnf, Logic.PropositionalLogic.Formula.dnf_val, qualityOf

List.filterMap

Applies a function that returns an Option to each element of a list, collecting the non-none values.

O(|l|).

Example: lean example #eval [1, 2, 5, 2, 7, 7].filterMap fun x => if x > 2 then some (2 * x) else none

[10, 14, 14]

def List.filterMap.{u, v} {α : Type u} {β : Type v} (f : α → Option β) : List α → List β

Used by: getConceptsOf

List.find?

Returns the first element of the list for which the predicate p returns true, or none if no such element is found.

O(|l|).

Examples: * [7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1 * [7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none

def List.find?.{u} {α : Type u} (p : α → Bool) : List α → Option α

Used by: resolveRelation

List.foldr

Folds a function over a list from the right, accumulating a value starting with init. The accumulated value is combined with the each element of the list in reverse order, using f.

O(|l|). Replaced at runtime with List.foldrTR.

Examples: * [a, b, c].foldr f init = f a (f b (f c init)) * [1, 2, 3].foldr (toString · ++ ·) "" = "123" * [1, 2, 3].foldr (s!"({·} {·})") "!" = "(1 (2 (3 !)))"

def List.foldr.{u, v} {α : Type u} {β : Type v} (f : α → β → β) (init : β) (l : List α) : β

Used by: Logic.PropositionalLogic.Formula.bigAnd, Logic.PropositionalLogic.Formula.bigAnd_val, Logic.PropositionalLogic.Formula.bigOr, Logic.PropositionalLogic.Formula.bigOr_val

List.getLast

Returns the last element of a non-empty list.

Examples: * ["circle", "rectangle"].getLast (by decide) = "rectangle" * ["circle"].getLast (by decide) = "circle"

def List.getLast.{u} {α : Type u} (as : List α) : as ≠ [] → α

Used by: InformationSystem.Run.final, InformationSystem.Run.toChain

List.getLast?

Returns the last element in the list, or none if the list is empty.

Alternatives include List.getLastD, which takes a fallback value for empty lists, and List.getLast!, which panics on empty lists.

Examples: * ["circle", "rectangle"].getLast? = some "rectangle" * ["circle"].getLast? = some "circle" * ([] : List String).getLast? = none

def List.getLast?.{u} {α : Type u} : List α → Option α

Used by: InformationSystem.Chain.ofIsChain

List.head

Returns the first element of a non-empty list.

def List.head.{u} {α : Type u} (as : List α) : as ≠ [] → α

Used by: InformationSystem.Run.initial, InformationSystem.Run.toChain

List.head?

Returns the first element in the list, if there is one. Returns none if the list is empty.

Use List.headD to provide a fallback value for empty lists, or List.head! to panic on empty lists.

Examples: * ([] : List Nat).head? = none * [3, 2, 1].head? = some 3

def List.head?.{u} {α : Type u} : List α → Option α

Used by: InformationSystem.Chain.ofIsChain, InformationSystem.Run.trajectory_head

List.head?_cons

theorem List.head?_cons.{u} {α : Type u} {a : α} {l : List α} : (a :: l).head? = some a

Used by: InformationSystem.Chain.ofIsChain

List.headD

Returns the first element in the list if there is one, or fallback if the list is empty.

Use List.head? to return an Option, and List.head! to panic on empty lists.

Examples: * [].headD "empty" = "empty" * [].headD 2 = 2 * ["head", "shoulders", "knees"].headD "toes" = "head"

def List.headD.{u} {α : Type u} (as : List α) (fallback : α) : α

Used by: Frame.crcStep, Frame.crcStep_length, Frame.crcStep_poly

List.length_append

theorem List.length_append.{u} {α : Type u} {as bs : List α} : (as ++ bs).length = as.length + bs.length

Used by: Frame.crcStep_length, Frame.crcStep_poly, Frame.toPoly_append

List.length_replicate

theorem List.length_replicate.{u} {α : Type u} {n : ℕ} {a : α} : (List.replicate n a).length = n

Used by: Frame.crc_detects_single_bit_flip, Frame.toPoly_replicate_false

List.length_set

theorem List.length_set.{u} {α : Type u} {as : List α} {i : ℕ} {a : α} : (as.set i a).length = as.length

Used by: Frame.crcFrom_detects_single_bit_flip, Frame.ofFn_update, Frame.toPoly_set_flip

List.replicate

Creates a list that contains n copies of a.

List.replicate 5 "five" = ["five", "five", "five", "five", "five"]
List.replicate 0 "zero" = []
List.replicate 2 ' ' = [' ', ' ']

def List.replicate.{u} {α : Type u} (n : ℕ) (a : α) : List α

Used by: Frame.crc, Frame.crc32Ethernet, Frame.crc32Ethernet_detects_single_bit_flip, Frame.crc_detects_single_bit_flip, Frame.toPoly_replicate_false

List.reverse

Reverses a list.

O(|as|).

Because of the “functional but in place” optimization implemented by Lean’s compiler, this function does not allocate a new list when its reference to the input list is unshared: it simply walks the linked list and reverses all the node pointers.

Examples: * [1, 2, 3, 4].reverse = [4, 3, 2, 1] * [].reverse = []

def List.reverse.{u} {α : Type u} (as : List α) : List α

Used by: Frame.crc32Ethernet, Frame.crc32Ethernet_detects_single_bit_flip

List.sum

Computes the sum of the elements of a list.

Examples: * [a, b, c].sum = a + (b + (c + 0)) * [1, 2, 5].sum = 8

def List.sum.{u_1} {α : Type u_1} [Add α] [Zero α] : List α → α

Used by: Channel.lossy_loses_overall, List.totalSize

List.tail

Drops the first element of a nonempty list, returning the tail. Returns [] when the argument is empty.

Examples: * ["apple", "banana", "grape"].tail = ["banana", "grape"] * ["apple"].tail = [] * ([] : List String).tail = []

def List.tail.{u} {α : Type u} : List α → List α

Used by: Frame.crcStep, Frame.crcStep_length, Frame.crcStep_poly

List.take

Extracts the first n elements of xs, or the whole list if n is greater than xs.length.

O(min n |xs|).

Examples: * [a, b, c, d, e].take 0 = [] * [a, b, c, d, e].take 3 = [a, b, c] * [a, b, c, d, e].take 6 = [a, b, c, d, e]

def List.take.{u} {α : Type u} (n : ℕ) (xs : List α) : List α

Used by: InformationSystem.exists_repeat_equivalent, InformationSystem.exists_repeat_state

List.zipWith

Applies a function to the corresponding elements of two lists, stopping at the end of the shorter list.

O(min |xs| |ys|).

Examples: * [1, 2].zipWith (· + ·) [5, 6] = [6, 8] * [1, 2, 3].zipWith (· + ·) [5, 6, 10] = [6, 8, 13] * [].zipWith (· + ·) [5, 6] = [] * [x₁, x₂, x₃].zipWith f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]

def List.zipWith.{u, v, w} {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (xs : List α)
  (ys : List β) : List γ

Used by: Frame.crcStep, Frame.crcStep_length, Frame.crcStep_poly, Frame.toPoly_xor

`Data.List.BasicAux`

List.getLast!

Returns the last element in the list. Panics and returns default if the list is empty.

Safer alternatives include: * getLast?, which returns an Option, * getLastD, which takes a fallback value for empty lists, and * getLast, which requires a proof that the list is non-empty.

Examples: * ["circle", "rectangle"].getLast! = "rectangle" * ["circle"].getLast! = "circle"

def List.getLast!.{u_1} {α : Type u_1} [Inhabited α] : List α → α

Used by: qualityOf

`Data.List.Control`

List.mapM

Applies the monadic action f to every element in the list, left-to-right, and returns the list of results.

This implementation is tail recursive. List.mapM' is a non-tail-recursive variant that may be more convenient to reason about. List.forM is the variant that discards the results and List.mapA is the variant that works with Applicative.

def List.mapM.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β)
  (as : List α) : m (List β)

Used by: Ontology.readFile

`Data.List.FinRange`

List.finRange

Lists all elements of Fin n in order, starting at 0.

Examples: * List.finRange 0 = ([] : List (Fin 0)) * List.finRange 2 = ([0, 1] : List (Fin 2))

def List.finRange (n : ℕ) : List (Fin n)

Used by: Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.minterm, Logic.PropositionalLogic.Formula.minterm_val, arithPlus_iff, arithSucc_iff

List.mem_finRange

theorem List.mem_finRange {n : ℕ} (x : Fin n) : x ∈ List.finRange n

Used by: Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.minterm_val

`Data.List.Lemmas`

List.eq_or_mem_of_mem_cons

theorem List.eq_or_mem_of_mem_cons.{u_1} {α : Type u_1} {a b : α} {l : List α} : a ∈ b :: l → a = b ∨ a ∈ l

Used by: InformationSystem.not_spontaneous_and_perpetuous

List.ext_getElem

theorem List.ext_getElem.{u_1} {α : Type u_1} {l₁ l₂ : List α} (hl : l₁.length = l₂.length)
  (h : ∀ (i : ℕ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]) : l₁ = l₂

Used by: Frame.ofFn_update

List.forall_mem_map

theorem List.forall_mem_map.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}
  {P : β → Prop} : (∀ i ∈ List.map f l, P i) ↔ ∀ j ∈ l, P (f j)

Used by: Logic.PropositionalLogic.Formula.minterm_val

List.getElem_set_ne

theorem List.getElem_set_ne.{u_1} {α : Type u_1} {l : List α} {i j : ℕ} (h : i ≠ j) {a : α}
  (hj : j < (l.set i a).length) : (l.set i a)[j] = l[j]

Used by: Frame.ofFn_update

List.getElem_set_self

theorem List.getElem_set_self.{u_1} {α : Type u_1} {l : List α} {i : ℕ} {a : α}
  (h : i < (l.set i a).length) : (l.set i a)[i] = a

Used by: Frame.ofFn_update

List.getLast?_cons_cons

theorem List.getLast?_cons_cons.{u_1} {α✝ : Type u_1} {a b : α✝} {l : List α✝} :
  (a :: b :: l).getLast? = (b :: l).getLast?

Used by: InformationSystem.Chain.ofIsChain

List.getLast_mem_getLast?

theorem List.getLast_mem_getLast?.{u_1} {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h ∈ l.getLast?

Used by: InformationSystem.Run.toChain

List.headD_eq_head?_getD

simp unfolds headD in terms of head? and Option.getD.

theorem List.headD_eq_head?_getD.{u_1} {α : Type u_1} {a : α} {l : List α} : l.headD a = l.head?.getD a

Used by: Frame.crcStep_poly

List.head_mem_head?

theorem List.head_mem_head?.{u_1} {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h ∈ l.head?

Used by: InformationSystem.Run.toChain

List.length_tail

theorem List.length_tail.{u_1} {α : Type u_1} {l : List α} : l.tail.length = l.length - 1

Used by: Frame.crcStep_length

List.map_congr_left

theorem List.map_congr_left.{u_1, u_2} {α✝ : Type u_1} {l : List α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹}
  (h : ∀ a ∈ l, f a = g a) : List.map f l = List.map g l

Used by: Logic.PropositionalLogic.Formula.eliminate

List.mem_append

theorem List.mem_append.{u_1} {α : Type u_1} {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Used by: InformationSystem.spontaneous_no_self_return, Logic.Popper.Basis1.contract, Logic.Popper.Basis1.cut, Logic.Popper.Basis1.demonstrate_congr_conclusion, Logic.Popper.Basis1.demonstrate_mono, Logic.Popper.Basis1.demonstrate_of_mem, Logic.Popper.Basis1.exchange, Logic.Popper.Basis1.weaken, Logic.ProofTheory.CutFree.DerivationsOf.graft, Logic.ProofTheory.CutFree.DerivationsOf.mono

List.mem_cons

theorem List.mem_cons.{u_1} {α✝ : Type u_1} {b : α✝} {l : List α✝} {a : α✝} : a ∈ b :: l ↔ a = b ∨ a ∈ l

List.mem_cons_of_mem

theorem List.mem_cons_of_mem.{u_1} {α : Type u_1} (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l

Used by: InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le

List.mem_cons_self

theorem List.mem_cons_self.{u_1} {α : Type u_1} {a : α} {l : List α} : a ∈ a :: l

Used by: InformationSystem.spontaneous_no_self_return, InformationSystem.zero_run_le, Logic.Popper.Basis1.contradictory_of_isClassicalNegation, Logic.Popper.Basis1.demonstrate_congr_conclusion, Logic.Popper.Basis1.demonstrate_cons_of_isConjunction, Logic.Popper.Basis1.demonstrate_cons_of_isDisjunction, Logic.Popper.Basis1.substitutivity, Logic.PropositionalLogic.semanticConnectives, Logic.PropositionalLogic.syntacticConnectives

List.mem_filter

theorem List.mem_filter.{u_1} {α✝ : Type u_1} {p : α✝ → Bool} {as : List α✝} {x : α✝} :
  x ∈ List.filter p as ↔ x ∈ as ∧ p x = true

Used by: Logic.PropositionalLogic.Formula.dnf_val

List.mem_map

theorem List.mem_map.{u_1, u_2} {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α} :
  b ∈ List.map f l ↔ ∃ a ∈ l, f a = b

Used by: Logic.PropositionalLogic.Formula.dnf_val, Logic.PropositionalLogic.Formula.kalmar

List.mem_map_of_mem

theorem List.mem_map_of_mem.{u_1, u_2} {α : Type u_1} {β : Type u_2} {l : List α} {a : α} {f : α → β}
  (h : a ∈ l) : f a ∈ List.map f l

Used by: Logic.ProofTheory.Derivation.toCutFree

List.mem_singleton

theorem List.mem_singleton.{u_1} {α : Type u_1} {a b : α} : a ∈ [b] ↔ a = b

List.mem_singleton_self

theorem List.mem_singleton_self.{u_1} {α : Type u_1} (a : α) : a ∈ [a]

List.not_mem_nil

theorem List.not_mem_nil.{u_1} {α : Type u_1} {a : α} : a ∉ []

Used by: Logic.PropositionalLogic.Formula.soundness

List.reverse_reverse

theorem List.reverse_reverse.{u_1} {α : Type u_1} (as : List α) : as.reverse.reverse = as

Used by: Frame.crc32Ethernet_detects_single_bit_flip

`Data.List.Nat.TakeDrop`

List.length_zipWith

theorem List.length_zipWith.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ}
  {l₁ : List α} {l₂ : List β} : (List.zipWith f l₁ l₂).length = min l₁.length l₂.length

Used by: Frame.crcStep_length, Frame.toPoly_xor

`Data.List.OfFn`

List.getElem_ofFn

theorem List.getElem_ofFn.{u_1} {n : ℕ} {α : Type u_1} {i : ℕ} {f : Fin n → α}
  (h : i < (List.ofFn f).length) : (List.ofFn f)[i] = f ⟨i, ⋯⟩

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.ofFn_update

List.length_ofFn

theorem List.length_ofFn.{u_1} {n : ℕ} {α : Type u_1} {f : Fin n → α} : (List.ofFn f).length = n

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.ofFn_update

List.ofFn

Creates a list by applying f to each potential index in order, starting at 0.

Examples: * List.ofFn (n := 3) toString = ["0", "1", "2"] * List.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = ["red", "green", "blue"]

def List.ofFn.{u_1} {α : Type u_1} {n : ℕ} (f : Fin n → α) : List α

Used by: Frame.crc32Ethernet, Frame.crc32EthernetPoly, Frame.crc32Ethernet_detects_single_bit_flip, Frame.make, Frame.ofFn_update, Frame.valid, Receiver.step, Receiver.step_correct

List.ofFn_succ

theorem List.ofFn_succ.{u_1} {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α} :
  List.ofFn f = f 0 :: List.ofFn fun i => f i.succ

Used by: Frame.crc32Ethernet_detects_single_bit_flip

List.ofFn_zero

ofFn on an empty domain is the empty list.

theorem List.ofFn_zero.{u_1} {α : Type u_1} {f : Fin 0 → α} : List.ofFn f = []

Used by: Frame.crc32Ethernet_detects_single_bit_flip

`Data.List.Pairwise`

List.nodup_cons

theorem List.nodup_cons.{u_1} {α : Type u_1} {a : α} {l : List α} : (a :: l).Nodup ↔ a ∉ l ∧ l.Nodup

Used by: Logic.PropositionalLogic.Formula.eliminate

`Data.List.Sublist`

List.nil_subset

theorem List.nil_subset.{u_1} {α : Type u_1} (l : List α) : [] ⊆ l

Used by: Logic.PropositionalLogic.Formula.Derivable.ax

List.subset_cons_self

theorem List.subset_cons_self.{u_1} {α : Type u_1} (a : α) (l : List α) : l ⊆ a :: l

Used by: Logic.PropositionalLogic.Formula.kalmar

`Data.List.Zip`

List.zipWith_self

theorem List.zipWith_self.{u_1, u_2} {α : Type u_1} {δ : Type u_2} {f : α → α → δ} {l : List α} :
  List.zipWith f l l = List.map (fun a => f a a) l

Used by: Frame.toPoly_xor

`Data.Nat.Basic`

Nat.add_assoc

theorem Nat.add_assoc (n m k : ℕ) : n + m + k = n + (m + k)

Used by: Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.tensor_assoc, Component.braidedCategory, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.monoidalCategory, Component.monoidalCategoryStruct, Component.parallel_assoc

Nat.add_lt_add_left

theorem Nat.add_lt_add_left {n m : ℕ} (h : n < m) (k : ℕ) : k + n < k + m

Used by: Component.hexagon_reverse_arrow

Nat.add_sub_cancel

theorem Nat.add_sub_cancel (n m : ℕ) : n + m - m = n

Used by: Frame.toPoly_set_flip

Nat.eq_zero_or_pos

theorem Nat.eq_zero_or_pos (n : ℕ) : n = 0 ∨ n > 0

Used by: no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Nat.exists_eq_succ_of_ne_zero

theorem Nat.exists_eq_succ_of_ne_zero {n : ℕ} : n ≠ 0 → ∃ k, n = k.succ

Used by: arithZero_unique

Nat.le_of_lt

theorem Nat.le_of_lt {n m : ℕ} : n < m → n ≤ m

Used by: arithPlus_iff, arithSucc_iff

Nat.le_of_not_lt

theorem Nat.le_of_not_lt {a b : ℕ} : ¬a < b → b ≤ a

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Frame.crc32Ethernet_detects_single_bit_flip, Frame.crcFrom_detects_single_bit_flip, Frame.reflectIndex, Frame.toPoly_set_flip, Logic.ProofTheory.Derivation.toCutFree, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.S_iff_succ, Structure.Arithmetic.Tower.lt_card_level, Structure.Arithmetic.finTower

Nat.le_of_succ_le

theorem Nat.le_of_succ_le {n m : ℕ} (h : n.succ ≤ m) : n ≤ m

Used by: BitFunction.exists_settle

Nat.le_zero

theorem Nat.le_zero {i : ℕ} : i ≤ 0 ↔ i = 0

Used by: Structure.Arithmetic.Z_iff_zero, Structure.Arithmetic.instPeanoNat

Nat.lt_add_right

theorem Nat.lt_add_right {a b : ℕ} (c : ℕ) (h : a < b) : a < b + c

Used by: Component.hexagon_forward_arrow

Nat.lt_of_succ_lt_succ

theorem Nat.lt_of_succ_lt_succ {n m : ℕ} : n.succ < m.succ → n < m

Used by: Frame.toPoly_set_flip

Nat.lt_or_gt_of_ne

theorem Nat.lt_or_gt_of_ne {a b : ℕ} (ne : a ≠ b) : a < b ∨ a > b

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_assoc, Fin.append_eval, Frame.crcStep_length, Frame.reflectIndex_involutive, Frame.toPoly_set_flip, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.S_iff_succ, arithPlus_succ, arithPlus_zero, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Nat.mul_assoc

theorem Nat.mul_assoc (n m k : ℕ) : n * m * k = n * (m * k)

Used by: BitFunction.cardinality_input_growth

Nat.mul_comm

theorem Nat.mul_comm (n m : ℕ) : n * m = m * n

Used by: BitFunction.cardinality

Nat.recAux

A recursor for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

It is otherwise identical to the default recursor Nat.rec. It is used by the induction tactic by default for Nat.

abbrev Nat.recAux.{u} {motive : ℕ → Sort u} (zero : motive 0) (succ : (n : ℕ) → motive n → motive (n + 1))
  (t : ℕ) : motive t

Used by: BitFunction.exists_settle, BitFunction.iterate_dominates_succ, Frame.toPoly_replicate_false, Structure.Arithmetic.Tower.lt_card_level, Structure.Arithmetic.Tower.stepTo_bot, Tower.card_zero_le_neg, Tower.card_zero_le_pos

Nat.zero_add

theorem Nat.zero_add (n : ℕ) : 0 + n = n

Used by: Component.Hom.tensor_empty, Component.empty_parallel, Component.monoidalCategory, Component.monoidalCategoryStruct

Nat.zero_lt_one

theorem Nat.zero_lt_one : 0 < 1

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations

`Data.Nat.Bitwise.Basic`

Nat.hasNotBit

Asserts that the (n+1)th least significant bit of m is not set.

(This definition is used by Lean internally for compact bitmaps.)

def Nat.hasNotBit (m n : ℕ) : Prop

Used by: DataLinkLayer.network, DataLinkLayer.physical, NetworkLayer.forwards, NetworkLayer.transport, qualityOf

Nat.land

Bitwise and. Usually accessed via the &&& operator.

Each bit of the resulting value is set if the corresponding bit is set in both of the inputs.

def Nat.land : ℕ → ℕ → ℕ

Used by: DataLinkLayer.network, DataLinkLayer.physical, NetworkLayer.transport, qualityOf

Nat.shiftRight

Shifts the binary representation of a value right by the specified number of bits. Usually accessed via the >>> operator.

Examples: * 4 >>> 2 = 1 * 8 >>> 2 = 2 * 8 >>> 3 = 1 * 0 >>> 3 = 0 * 0xf13a >>> 8 = 0xf1

def Nat.shiftRight : ℕ → ℕ → ℕ

Used by: DataLinkLayer.network, DataLinkLayer.physical, NetworkLayer.transport, qualityOf

Nat.testBit

Returns true if the (n+1)th least significant bit is 1, or false if it is 0.

def Nat.testBit (m n : ℕ) : Bool

Used by: Frame.crc32EthernetPoly, Frame.crc32Ethernet_detects_single_bit_flip

`Data.Nat.Bitwise.Lemmas`

Nat.testBit_zero

theorem Nat.testBit_zero (x : ℕ) : x.testBit 0 = decide (x % 2 = 1)

Used by: Frame.crc32Ethernet_detects_single_bit_flip

`Data.Nat.Div.Basic`

Nat.mod_eq_of_lt

theorem Nat.mod_eq_of_lt {a b : ℕ} (h : a < b) : a % b = a

Used by: Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.instArithFin

Nat.mod_self

theorem Nat.mod_self (n : ℕ) : n % n = 0

Used by: Structure.Arithmetic.S_iff_add_one

`Data.Nat.Lemmas`

Nat.add_right_cancel_iff

theorem Nat.add_right_cancel_iff {m k n : ℕ} : m + n = k + n ↔ m = k

Used by: arithSuccFun_injective

Nat.le_self_pow

theorem Nat.le_self_pow {n : ℕ} (hn : n ≠ 0) (a : ℕ) : a ≤ a ^ n

Used by: no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Nat.min_self

theorem Nat.min_self (a : ℕ) : min a a = a

Used by: Frame.toPoly_xor

Nat.mod_succ

theorem Nat.mod_succ (n : ℕ) : n % n.succ = n

Used by: no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Nat.pow_mod

theorem Nat.pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n

Used by: no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

`Data.Nat.Simproc`

Nat.Simproc.sub_add_eq_comm

theorem Nat.Simproc.sub_add_eq_comm (a b c : ℕ) : a - (b + c) = a - c - b

Used by: Frame.crc32Ethernet_detects_single_bit_flip

`Data.NeZero`

NeZero

A type-class version of n ≠ 0.

structure NeZero.{u_1} {R : Type u_1} [Zero R] (n : R) : Prop

Used by: Structure.Arithmetic.instNeZeroNat_structure

`Data.Option.Basic`

Option.isSome

Returns true on some x and false on none.

def Option.isSome.{u_1} {α : Type u_1} : Option α → Bool

Used by: NormalBehavior

`Data.Option.Instances`

Option.mem_def

theorem Option.mem_def.{u_1} {α : Type u_1} {a : α} {b : Option α} : a ∈ b ↔ b = some a

Used by: InformationSystem.Chain.ofIsChain

`Data.Ord.Basic`

Ordering

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 : Type

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit

compareOfLessAndEq

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.

def compareOfLessAndEq.{u_1} {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] :
  Ordering

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instPeanoStandard

`Data.Range.Basic`

Std.Legacy.Range

structure Std.Legacy.Range : Type

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations

`Data.Rat.Basic`

Rat

Rational numbers, implemented as a pair of integers num / den such that the denominator is positive and the numerator and denominator are coprime.

structure Rat : Type

Used by: irrational_logb_two_five, irrational_logb_two_three

`Data.Sum.Basic`

Sum.elim

Case analysis for sums that applies the appropriate function f or g after checking which constructor is present.

def Sum.elim.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) :
  α ⊕ β → γ

Used by: Interface.combine, InterfaceOld.tensor, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex

`Meta.Defs`

Lean.Syntax.TSepArray.getElems

Extracts the non-separator elements of a separated array.

def Lean.Syntax.TSepArray.getElems {k : SyntaxNodeKinds} {sep : String} (sa : Syntax.TSepArray k sep) :
  TSyntaxArray k

Used by: unexpandSeqAppend

Lean.Syntax.TSepArray.ofElems

Constructs a typed separated array from elements by adding suitable separators. The provided array should not include the separators.

Like Syntax.SepArray.ofElems but for typed syntax.

def Lean.Syntax.TSepArray.ofElems {k : SyntaxNodeKinds} {sep : String} (elems : Array (TSyntax k)) :
  Syntax.TSepArray k sep

Used by: unexpandSeqAppend

`Omega.Coeffs`

Lean.Omega.Coeffs.isZero

Are the coefficients all zero?

abbrev Lean.Omega.Coeffs.isZero (xs : Omega.Coeffs) : Prop

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.Coeffs.ofList

Identity, turning List Int into Coeffs.

abbrev Lean.Omega.Coeffs.ofList (xs : List ℤ) : Omega.Coeffs

`Omega.Constraint`

Lean.Omega.Constraint.addEquality_sat

theorem Lean.Omega.Constraint.addEquality_sat {c : ℤ} {x y : Omega.Coeffs} (w : c + x.dot y = 0) :
  { lowerBound := some (-c), upperBound := some (-c) }.sat' x y = true

Lean.Omega.Constraint.addInequality_sat

theorem Lean.Omega.Constraint.addInequality_sat {c : ℤ} {x y : Omega.Coeffs} (w : c + x.dot y ≥ 0) :
  { lowerBound := some (-c), upperBound := none }.sat' x y = true

Lean.Omega.Constraint.combine_sat'

theorem Lean.Omega.Constraint.combine_sat' {s t : Omega.Constraint} {x y : Omega.Coeffs}
  (ws : s.sat' x y = true) (wt : t.sat' x y = true) : (s.combine t).sat' x y = true

Lean.Omega.Constraint.isImpossible

Check if a constraint is unsatisfiable.

def Lean.Omega.Constraint.isImpossible : Omega.Constraint → Bool

Lean.Omega.Constraint.not_sat'_of_isImpossible

theorem Lean.Omega.Constraint.not_sat'_of_isImpossible {c : Omega.Constraint} (h : c.isImpossible = true)
  {x y : Omega.Coeffs} : ¬c.sat' x y = true

Lean.Omega.combo_sat'

theorem Lean.Omega.combo_sat' (s t : Omega.Constraint) (a : ℤ) (x : Omega.Coeffs) (b : ℤ)
  (y v : Omega.Coeffs) (wx : s.sat' x v = true) (wy : t.sat' y v = true) :
  (Omega.Constraint.combo a s b t).sat' (Omega.Coeffs.combo a x b y) v = true

Lean.Omega.tidy_sat

theorem Lean.Omega.tidy_sat {s : Omega.Constraint} {x v : Omega.Coeffs} (w : s.sat' x v = true) :
  (Omega.tidyConstraint s x).sat' (Omega.tidyCoeffs s x) v = true

`Omega.Int`

Lean.Omega.Int.add_congr

theorem Lean.Omega.Int.add_congr {a b c d : ℤ} (h₁ : a = b) (h₂ : c = d) : a + c = b + d

Lean.Omega.Int.mul_congr

theorem Lean.Omega.Int.mul_congr {a b c d : ℤ} (h₁ : a = b) (h₂ : c = d) : a * c = b * d

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_congr

theorem Lean.Omega.Int.ofNat_congr {a b : ℕ} (h : a = b) : ↑a = ↑b

Used by: Fin.append_eval, Frame.crc32Ethernet_detects_single_bit_flip, Frame.crcStep_length, Frame.crcStep_poly, Frame.reflectIndex, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Z_iff_zero, Structure.Arithmetic.finTower, Structure.Arithmetic.instNeZeroNat_structure, Structure.Arithmetic.instPeanoNat, arithPlus_succ, arithSucc_no_fixed_point, arithZero_not_succ, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_le_of_le

theorem Lean.Omega.Int.ofNat_le_of_le {x y : ℕ} (h : x ≤ y) : ↑x ≤ ↑y

Used by: BitFunction.exists_settle, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Frame.crc32Ethernet_detects_single_bit_flip, Frame.crcFrom_detects_single_bit_flip, Frame.reflectIndex, Frame.toPoly_set_flip, Logic.ProofTheory.Derivation.toCutFree, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.S_iff_succ, Structure.Arithmetic.Tower.instInfiniteColimit, Structure.Arithmetic.Tower.lt_card_level, Structure.Arithmetic.finTower, Structure.Arithmetic.instNeZeroNat_structure, Structure.Arithmetic.instPeanoNat, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_lt_of_lt

theorem Lean.Omega.Int.ofNat_lt_of_lt {x y : ℕ} (h : x < y) : ↑x < ↑y

Lean.Omega.Int.ofNat_pow

theorem Lean.Omega.Int.ofNat_pow (a b : ℕ) : ↑(a ^ b) = ↑a ^ b

Used by: no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_sub_dichotomy

theorem Lean.Omega.Int.ofNat_sub_dichotomy {a b : ℕ} : b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Frame.crcStep_length, Frame.reflectIndex, Frame.reflectIndex_involutive, Frame.toPoly_set_flip, Structure.Arithmetic.S_iff_add_one, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.Int.ofNat_sub_sub

theorem Lean.Omega.Int.ofNat_sub_sub {a b c : ℕ} : ↑(a - b - c) = ↑(a - (b + c))

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Frame.toPoly_set_flip

Lean.Omega.Int.sub_congr

theorem Lean.Omega.Int.sub_congr {a b c d : ℤ} (h₁ : a = b) (h₂ : c = d) : a - c = b - d

`Omega.LinearCombo`

Lean.Omega.LinearCombo

Internal representation of a linear combination of atoms, and a constant term.

structure Lean.Omega.LinearCombo : Type

Lean.Omega.LinearCombo.add_eval

theorem Lean.Omega.LinearCombo.add_eval (l₁ l₂ : Omega.LinearCombo) (v : Omega.Coeffs) :
  (l₁ + l₂).eval v = l₁.eval v + l₂.eval v

Lean.Omega.LinearCombo.coordinate

The i-th coordinate function.

def Lean.Omega.LinearCombo.coordinate (i : ℕ) : Omega.LinearCombo

Lean.Omega.LinearCombo.coordinate_eval_0

theorem Lean.Omega.LinearCombo.coordinate_eval_0 {a0 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 0).eval (Omega.Coeffs.ofList (a0 :: t)) = a0

Lean.Omega.LinearCombo.coordinate_eval_1

theorem Lean.Omega.LinearCombo.coordinate_eval_1 {a0 a1 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 1).eval (Omega.Coeffs.ofList (a0 :: a1 :: t)) = a1

Lean.Omega.LinearCombo.coordinate_eval_2

theorem Lean.Omega.LinearCombo.coordinate_eval_2 {a0 a1 a2 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 2).eval (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2

Used by: BitFunction.exists_settle, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_assoc, Fin.append_eval, Frame.crcFrom_detects_single_bit_flip, Frame.crcStep_length, Frame.reflectIndex, Frame.reflectIndex_involutive, Frame.toPoly_set_flip, Logic.ProofTheory.Derivation.toCutFree, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Tower.lt_card_level, Structure.Arithmetic.finTower, arithPlus_succ, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.coordinate_eval_3

theorem Lean.Omega.LinearCombo.coordinate_eval_3 {a0 a1 a2 a3 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 3).eval (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3

Used by: BitFunction.exists_settle, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Frame.crc32Ethernet_detects_single_bit_flip, Frame.crcFrom_detects_single_bit_flip, Frame.reflectIndex, Frame.reflectIndex_involutive, Frame.toPoly_set_flip, InformationSystem.exists_repeat_state, Logic.ProofTheory.Derivation.toCutFree, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.finTower, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.coordinate_eval_4

theorem Lean.Omega.LinearCombo.coordinate_eval_4 {a0 a1 a2 a3 a4 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 4).eval (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Fin.append_eval, Frame.crc32Ethernet_detects_single_bit_flip, Frame.reflectIndex, Frame.reflectIndex_involutive, Frame.toPoly_set_flip, InformationSystem.exists_repeat_state, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.coordinate_eval_5

theorem Lean.Omega.LinearCombo.coordinate_eval_5 {a0 a1 a2 a3 a4 a5 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 5).eval
      (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) =
    a5

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Frame.crc32Ethernet_detects_single_bit_flip, Frame.reflectIndex_involutive, Structure.Arithmetic.S_iff_add_one, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.coordinate_eval_6

theorem Lean.Omega.LinearCombo.coordinate_eval_6 {a0 a1 a2 a3 a4 a5 a6 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 6).eval
      (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) =
    a6

Used by: Component.hexagon_reverse_arrow, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.coordinate_eval_7

theorem Lean.Omega.LinearCombo.coordinate_eval_7 {a0 a1 a2 a3 a4 a5 a6 a7 : ℤ} {t : List ℤ} :
  (Omega.LinearCombo.coordinate 7).eval
      (Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) =
    a7

Used by: Component.hexagon_reverse_arrow

Lean.Omega.LinearCombo.eval

Evaluate a linear combination ⟨r, [c_1, …, c_k]⟩ at values [v_1, …, v_k] to obtain r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0)))).

def Lean.Omega.LinearCombo.eval (lc : Omega.LinearCombo) (values : Omega.Coeffs) : ℤ

Lean.Omega.LinearCombo.mul

Multiplication of two linear combinations. This is useful only if at least one of the linear combinations is constant, and otherwise should be considered as a junk value.

def Lean.Omega.LinearCombo.mul (l₁ l₂ : Omega.LinearCombo) : Omega.LinearCombo

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.mul_eval

theorem Lean.Omega.LinearCombo.mul_eval (l₁ l₂ : Omega.LinearCombo) (v : Omega.Coeffs)
  (w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero) : (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Used by: Frame.reflectIndex, Frame.reflectIndex_involutive, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Lean.Omega.LinearCombo.sub_eval

theorem Lean.Omega.LinearCombo.sub_eval (l₁ l₂ : Omega.LinearCombo) (v : Omega.Coeffs) :
  (l₁ - l₂).eval v = l₁.eval v - l₂.eval v

`Omega.Logic`

Lean.Omega.Decidable.and_not_or_not_and_of_not_iff

theorem Lean.Omega.Decidable.and_not_or_not_and_of_not_iff {a b : Prop} [Decidable a] [Decidable b]
  (h : ¬(a ↔ b)) : a ∧ ¬b ∨ ¬a ∧ b

Used by: arithPlus_succ

`Prelude`

And

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.

Conventions for notations in identifiers:

The recommended spelling of ∧ in identifiers is and.

structure And (a b : Prop) : Prop

Array

Array α is the type of dynamic arrays with elements from α. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array, all updates will be performed destructively. This results in performance comparable to mutable arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while the capacity is the amount of memory currently allocated for elements. The size is accessible via Array.size, but the capacity is not observable from Lean code. Array.emptyWithCapacity n creates an array which is equal to #[], but internally allocates an array of capacity n. When the size exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, Array α is just a wrapper around List α.

structure Array.{u} (α : Type u) : Type u

Used by: Ontology.readFile, allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations, instDecodeTomlConcept, instDecodeTomlRawRelation, moduleOf

Array.mkArray0

Create array #[]

def Array.mkArray0.{u} {α : Type u} : Array α

Used by: unexpandSeqAppend

Array.size

Gets the number of elements stored in an array.

This is a cached value, so it is O(1) to access. The space allocated for an array, referred to as its capacity, is at least as large as its size, but may be larger. The capacity of an array is an internal detail that’s not observable by Lean code.

def Array.size.{u} {α : Type u} (a : Array α) : ℕ

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations, moduleOf

Bool

The Boolean values, true and false.

Logically speaking, this is equivalent to Prop (the type of propositions). The distinction is public important for programming: both propositions and their proofs are erased in the code generator, while Bool corresponds to the Boolean type in most programming languages and carries precisely one bit of run-time information.

inductive Bool : Type

Bool.and

Boolean “and”, also known as conjunction. and x y can be written x && y.

The corresponding propositional connective is And : Prop → Prop → Prop, written with the ∧ operator.

The Boolean and is a @[macro_inline] function in order to give it short-circuiting evaluation: if x is false then y is not evaluated at runtime.

Conventions for notations in identifiers:

The recommended spelling of && in identifiers is and.
The recommended spelling of || in identifiers is or.

def Bool.and (x y : Bool) : Bool

Bool.not

Boolean negation, also known as Boolean complement. not x can be written !x.

This is a function that maps the value true to false and the value false to true. The propositional connective is Not : Prop → Prop.

Conventions for notations in identifiers:

The recommended spelling of ! in identifiers is not.

def Bool.not : Bool → Bool

Bool.or

Boolean “or”, also known as disjunction. or x y can be written x || y.

The corresponding propositional connective is Or : Prop → Prop → Prop, written with the ∨ operator.

The Boolean or is a @[macro_inline] function in order to give it short-circuiting evaluation: if x is true then y is not evaluated at runtime.

def Bool.or (x y : Bool) : Bool

Decidable

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 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.

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.

inductive Decidable (p : Prop) : Type

Used by: Frame.crcStep_length, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Ontology.decidableWellFormed, Structure.Arithmetic.S_iff_add_one

Decidable.decide

Converts a decidable proposition into a Bool.

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.

def Decidable.decide (p : Prop) [h : Decidable p] : Bool

DecidableEq

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.{u} (α : Sort u) : Sort (max 1 u)

DecidablePred

A decidable predicate.

A predicate is decidable if the corresponding proposition is Decidable for each possible argument.

abbrev DecidablePred.{u} {α : Sort u} (r : α → Prop) : Sort (max 1 u)

Used by: BitSequence.trueCount_strict

EStateM

A combined state and exception monad in which exceptions do not automatically roll back the state.

Instances of EStateM.Backtrackable provide a way to roll back some part of the state if needed.

EStateM ε σ is equivalent to ExceptT ε (StateM σ), but it is more efficient.

def EStateM.{u} (ε σ α : Type u) : Type u

Used by: unexpandSeqAppend, unexpandToSeq

EStateM.Result

The value returned from a combined state and exception monad in which exceptions do not automatically roll back the state.

Result ε σ α is equivalent to Except ε α × σ, but using a single combined inductive type yields a more efficient data representation.

inductive EStateM.Result.{u} (ε σ α : Type u) : Type u

Used by: Ontology.readFile

EStateM.run

Executes an EStateM action with the initial state s. The returned value includes the final state and indicates whether an exception was thrown or a value was returned.

def EStateM.run.{u} {ε σ α : Type u} (x : EStateM ε σ α) (s : σ) : EStateM.Result ε σ α

Used by: Ontology.readFile

Empty

The empty type. It has no constructors.

Use Empty.elim in contexts where a value of type Empty is in scope.

inductive Empty : Type

Used by: InterfaceOld.unit, arithLang, doorLanguage

Eq

The equality relation. It has one introduction rule, Eq.refl. We use a = b as notation for Eq a b. A fundamental property of equality is that it is an equivalence relation.

variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd

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. Example:

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2

The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t. For more information: Equality

Conventions for notations in identifiers:

The recommended spelling of = in identifiers is eq.

inductive Eq.{u_1} {α : Sort u_1} : α → α → Prop

Eq.ndrec_symm

Non-dependent recursor for the equality type (symmetric variant)

abbrev Eq.ndrec_symm.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α}
  (h : b = a) : motive b

Used by: Difficulty.ofString?, Quality.ofString?, arithLang, doorLanguage

Eq.symm

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

theorem Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

Eq.trans

Equality is transitive: if a = b and b = c then a = c.

Because this is in the Eq namespace, if you have 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

theorem Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

Except

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.{u, v} (ε : Type u) (α : Type v) : Type (max u v)

Used by: Ontology.readFile, resolveRelation

False

False is the empty proposition. Thus, it has no introduction rules. It represents a contradiction. False elimination rule, False.rec, expresses the fact that anything follows from a contradiction. This rule is sometimes called ex falso (short for ex falso sequitur quodlibet), or the principle of explosion. For more information: Propositional Logic

inductive False : Prop

False.elim

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.)

def False.elim.{u} {C : Sort u} (h : False) : C

Fin

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.

structure Fin (n : ℕ) : Type

Function.comp

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]

Conventions for notations in identifiers:

The recommended spelling of ∘ in identifiers is comp.

def Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ

Used by: BitFunction.comp, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_assoc, Component.parallel_empty, Component.recast, Frame.crc32Ethernet, Frame.crc32Ethernet_detects_single_bit_flip, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset, Tower, arithTower

GE.ge

a ≥ b is an abbreviation for b ≤ a.

Conventions for notations in identifiers:

The recommended spelling of ≥ in identifiers is ge.

def GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop

Used by: Fin.append_eval

GT.gt

a > b is an abbreviation for b < a.

Conventions for notations in identifiers:

The recommended spelling of > in identifiers is gt.

def GT.gt.{u} {α : Type u} [LT α] (a b : α) : Prop

HEq

Heterogeneous equality. 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 public important non-theorem is the analogue of congr: If f ≍ g and x ≍ y and f x and g y are well typed it does not follow that 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 a ≍ b are equivalent.

Conventions for notations in identifiers:

The recommended spelling of ≍ in identifiers is heq.

inductive HEq.{u} {α : Sort u} : α → {β : Sort u} → β → Prop

Lean.MacroScope

A macro scope identifier is just a Nat that gets bumped every time we enter a new macro scope. Within a macro scope, all occurrences of identifier x parse to the same thing, but x parsed from different macro scopes will produce different identifiers.

abbrev Lean.MacroScope : Type

Used by: unexpandSeqAppend, unexpandToSeq

Lean.MonadRef.mkInfoFromRefPos

Construct a synthetic SourceInfo from the ref in the monad state.

def Lean.MonadRef.mkInfoFromRefPos {m : Type → Type} [Monad m] [MonadRef m] : m SourceInfo

Used by: unexpandSeqAppend, unexpandToSeq

Lean.Name

Hierarchical names consist of a sequence of components, each of which is either a string or numeric, that are written separated by dots (.).

Hierarchical names are used to name declarations and for creating unique identifiers for free variables and metavariables.

You can create hierarchical names using a backtick:

`Lean.Meta.whnf

It is short for .str (.str (.str .anonymous "Lean") "Meta") "whnf".

You can use double backticks to request Lean to statically check whether the name corresponds to a Lean declaration in scope.

``Lean.Meta.whnf

If the name is not in scope, Lean will report an error.

There are two ways to convert a String to a Name:

Name.mkSimple creates a name with a single string component.
String.toName first splits the string into its dot-separated components, and then creates a hierarchical name.

inductive Lean.Name : Type

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations, getConceptsOf, isExample, isIgnored, isLemma, moduleOf, qualityOf, unexpandSeqAppend, unexpandToSeq

Lean.Name.mkStr1

Make name s₁

def Lean.Name.mkStr1 (s₁ : String) : Name

Used by: Logic.PropositionalLogic.Notation.«term⊢_», Logic.PropositionalLogic.Notation.«term⊨_», Ontology.readFile, concept, difficultyTag, exampleTag, forwardReferencingTag, ignoreTag, instDecodeTomlConcept, instDecodeTomlRawRelation, lemmaTag, qualityTag, unexpandSeqAppend, unexpandToSeq, «term⟪_⟫»

Lean.Name.mkStr4

Make name s₁.s₂.s₃.s₄

def Lean.Name.mkStr4 (s₁ s₂ s₃ s₄ : String) : Name

Used by: Logic.PropositionalLogic.Notation.«term⊢_», Logic.PropositionalLogic.Notation.«term⊨_», unexpandSeqAppend, unexpandToSeq

Lean.ParserDescr

A ParserDescr is a grammar for parsers. This is used by the syntax command to produce parsers without having to import Lean.

inductive Lean.ParserDescr : Type

Used by: Logic.PropositionalLogic.Notation.«term⊢_», Logic.PropositionalLogic.Notation.«term⊨_», concept, difficultyTag, exampleTag, forwardReferencingTag, ignoreTag, lemmaTag, qualityTag, «term⟪_⟫»

Lean.PrettyPrinter.UnexpandM

The unexpander monad, essentially Syntax → Option α. The Syntax is the ref, and it has the possibility of failure without an error message.

abbrev Lean.PrettyPrinter.UnexpandM (α : Type) : Type

Used by: unexpandSeqAppend, unexpandToSeq

Lean.PrettyPrinter.Unexpander

Function that tries to reverse macro expansions as a post-processing step of delaboration. While less general than an arbitrary delaborator, it can be declared without importing Lean. Used by the [app_unexpander] attribute.

abbrev Lean.PrettyPrinter.Unexpander : Type

Used by: unexpandSeqAppend, unexpandToSeq

Lean.SourceInfo

Source information that relates syntax to the context that it came from.

The primary purpose of SourceInfo is to relate the output of the parser and the macro expander to the original source file. When produced by the parser, Syntax.node does not carry source info; the parser associates it only with atoms and identifiers. If a Syntax.node is introduced by a quotation, then it has synthetic source info that both associates it with an original reference position and indicates that the original atoms in it may not originate from the Lean file under elaboration.

Source info is also used to relate Lean’s output to the internal data that it represents; this is the basis for many interactive features. When used this way, it can occur on Syntax.node as well.

inductive Lean.SourceInfo : Type

Used by: unexpandSeqAppend, unexpandToSeq

Lean.Syntax

Lean syntax trees.

Syntax trees are used pervasively throughout Lean: they are produced by the parser, transformed by the macro expander, and elaborated. They are also produced by the delaborator and presented to users.

inductive Lean.Syntax : Type

Used by: unexpandSeqAppend, unexpandToSeq

Lean.Syntax.TSepArray

An array of syntax elements that alternate with the given separator. Each syntax element has a kind drawn from ks.

Separator arrays result from repetition operators such as ,*. Coercions to and from Array (TSyntax ks) insert or remove separators as required. The untyped equivalent is Lean.Syntax.SepArray.

structure Lean.Syntax.TSepArray (ks : SyntaxNodeKinds) (sep : String) : Type

Used by: unexpandSeqAppend

Lean.Syntax.getArg

Gets the i’th argument of the syntax node. This can also be written stx[i]. Returns missing if i is out of range.

def Lean.Syntax.getArg (stx : Syntax) (i : ℕ) : Syntax

Used by: unexpandSeqAppend, unexpandToSeq

Lean.Syntax.getArgs

Gets the list of arguments of the syntax node, or #[] if it’s not a node.

def Lean.Syntax.getArgs (stx : Syntax) : Array Syntax

Used by: unexpandSeqAppend

Lean.Syntax.isOfKind

Checks whether syntax has the given kind or pseudo-kind.

“Pseudo-kinds” are kinds that are assigned by convention to non-Syntax.node values: identKind for Syntax.ident, `missing for Syntax.missing, and the atom’s string literal for atoms.

def Lean.Syntax.isOfKind (stx : Syntax) (k : SyntaxNodeKind) : Bool

Used by: unexpandSeqAppend, unexpandToSeq

Lean.Syntax.matchesNull

Is this syntax a null node?

def Lean.Syntax.matchesNull (stx : Syntax) (n : ℕ) : Bool

Used by: unexpandSeqAppend, unexpandToSeq

Lean.Syntax.node1

Create syntax node with 1 child

def Lean.Syntax.node1 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ : Syntax) : Syntax

Used by: unexpandToSeq

Lean.Syntax.node3

Create syntax node with 3 children

def Lean.Syntax.node3 (info : SourceInfo) (kind : SyntaxNodeKind) (a₁ a₂ a₃ : Syntax) : Syntax

Used by: unexpandSeqAppend, unexpandToSeq

Lean.SyntaxNodeKind

Specifies the interpretation of a Syntax.node value. An abbreviation for Name.

Node kinds may be any name, and do not need to refer to declarations in the environment. Conventionally, however, a node’s kind corresponds to the Parser or ParserDesc declaration that produces it. There are also a number of built-in node kinds that are used by the parsing infrastructure, such as nullKind and choiceKind; these do not correspond to parser declarations.

abbrev Lean.SyntaxNodeKind : Type

Used by: unexpandSeqAppend, unexpandToSeq

Lean.TSyntax

Typed syntax, which tracks the potential kinds of the Syntax it contains.

While syntax quotations produce or expect TSyntax values of the correct kinds, this is not otherwise enforced; it can easily be circumvented by direct use of the constructor.

structure Lean.TSyntax (ks : SyntaxNodeKinds) : Type

Used by: unexpandSeqAppend, unexpandToSeq

Lean.TSyntaxArray

An array of syntaxes of kind ks.

abbrev Lean.TSyntaxArray (ks : SyntaxNodeKinds) : Type

Used by: unexpandSeqAppend

List

Linked lists: ordered lists, in which each element has a reference to the next element.

Most operations on linked lists take time proportional to the length of the list, because each element must be traversed to find the next element.

List α is isomorphic to Array α, but they are useful for different things: * List α is easier for reasoning, and Array α is modeled as a wrapper around List α. * List α works well as a persistent data structure, when many copies of the tail are shared. When the value is not shared, Array α will have better performance because it can do destructive updates.

inductive List.{u} (α : Type u) : Type u

List.append

Appends two lists. Normally used via the ++ operator.

Appending lists takes time proportional to the length of the first list: O(|xs|).

Examples: * [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]. * [] ++ [4, 5] = [4, 5]. * [1, 2, 3] ++ [] = [1, 2, 3].

def List.append.{u_1} {α : Type u_1} (xs ys : List α) : List α

List.foldl

Folds a function over a list from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

Examples: * [a, b, c].foldl f z = f (f (f z a) b) c * [1, 2, 3].foldl (· ++ toString ·) "" = "123" * [1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"

def List.foldl.{u, v} {α : Type u} {β : Type v} (f : α → β → α) (init : α) : List β → α

Used by: Frame.crcFrom, Frame.crc_poly_dvd, Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons, Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons, Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

List.length

The length of a list.

This function is overridden in the compiler to lengthTR, which uses constant stack space.

Examples: * ([] : List String).length = 0 * ["green", "brown"].length = 2

def List.length.{u_1} {α : Type u_1} : List α → ℕ

List.map

Applies a function to each element of the list, returning the resulting list of values.

O(|l|).

Examples: * [a, b, c].map f = [f a, f b, f c] * [].map Nat.succ = [] * ["one", "two", "three"].map (·.length) = [3, 3, 5] * ["one", "two", "three"].map (·.reverse) = ["eno", "owt", "eerht"]

def List.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List β

List.set

Replaces the value at (zero-based) index n in l with a. If the index is out of bounds, then the list is returned unmodified.

Examples: * ["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"] * ["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]

def List.set.{u_1} {α : Type u_1} (l : List α) (n : ℕ) (a : α) : List α

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.crcFrom_detects_single_bit_flip, Frame.crc_detects_single_bit_flip, Frame.ofFn_update, Frame.toPoly_set_flip

List.toArray

Converts a List α into an Array α.

O(|xs|). At runtime, this operation is implemented by List.toArrayImpl and takes time linear in the length of the list. List.toArray should be used instead of Array.mk.

Examples: * [1, 2, 3].toArray = #[1, 2, 3] * ["monday", "wednesday", friday"].toArray = #["monday", "wednesday", friday"].

abbrev List.toArray.{u_1} {α : Type u_1} (xs : List α) : Array α

Used by: Ontology.readFile

Membership

The typeclass behind the notation a ∈ s : Prop where a : α, s : γ. Because α is an outParam, the “container type” γ determines the type of the elements of the container.

structure Membership.{u, v} (α : outParam (Type u)) (γ : Type v) : Type (max u v)

Used by: allConceptAnnotations, allDifficultyAnnotations, allExampleTags, allForwardReferencingTags, allIgnoreTags, allLemmaTags, allQualityAnnotations

Nat

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually GMP); at runtime, Nat values that are sufficiently small are unboxed.

inductive Nat : Type

Nat.add

Addition of natural numbers, typically used via the + operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

def Nat.add : ℕ → ℕ → ℕ

Used by: Frame.toPoly_xor

Nat.ble

The Boolean less-than-or-equal-to comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples: * Nat.ble 2 5 = true * Nat.ble 5 2 = false * Nat.ble 5 5 = true

def Nat.ble : ℕ → ℕ → Bool

Used by: ApplicationLayer.Op, Difficulty, DoorState, Icmp, InformationSystem.Chain, Kind, Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.Derivation, Logic.ProofTheory.DerivationsOf, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.NandFormula, NetworkLayer.Protocol, Quality, Topology.Event, Topology.Signal, TrafficLightColor, phoneNumberInformation_eq

Nat.decEq

A decision procedure for equality of natural numbers, usually accessed via the DecidableEq Nat instance.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples: * Nat.decEq 5 5 = isTrue rfl * (if 3 = 4 then "yes" else "no") = "no" * show 12 = 12 by decide

def Nat.decEq (n m : ℕ) : Decidable (n = m)

Used by: Logic.ProofTheory.Derivation, Logic.PropositionalLogic.Formula, Topology.Event

Nat.le

Non-strict, or weak, inequality of natural numbers, usually accessed via the ≤ operator.

inductive Nat.le (n : ℕ) : ℕ → Prop

Used by: arithStepTo_val, arithTranslatePos_stepTo_eq

Nat.le_refl

theorem Nat.le_refl (n : ℕ) : n ≤ n

Used by: Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff, arithPlus_iff, arithStepTo_val, arithSucc_iff

Nat.le_succ

theorem Nat.le_succ (n : ℕ) : n ≤ n.succ

Used by: SeqColimit.freshSeq_lt_ne, SeqColimit.stepTo_succ, Structure.Arithmetic.Tower.stepTo_bot, Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff, Structure.Arithmetic.Tower.stepTo_succ, arithStepTo_val, arithTranslatePos_stepTo_eq

Nat.le_succ_of_le

theorem Nat.le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ m.succ

Used by: BitFunction.iterate_settles, Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff

Nat.lt_of_not_le

theorem Nat.lt_of_not_le {a b : ℕ} (h : ¬a ≤ b) : b < a

Used by: BitFunction.exists_settle, Frame.crcStep_length, InformationSystem.exists_repeat_state, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.S_iff_succ, Structure.Arithmetic.Z_iff_zero

Nat.lt_or_ge

theorem Nat.lt_or_ge (n m : ℕ) : n < m ∨ n ≥ m

Used by: Fin.append_eval

Nat.lt_succ_self

theorem Nat.lt_succ_self (n : ℕ) : n < n.succ

Used by: Frame.toPoly_degree_lt

Nat.ne_of_beq_eq_false

theorem Nat.ne_of_beq_eq_false {n m : ℕ} : n.beq m = false → ¬n = m

Used by: DataLinkLayer.network, DataLinkLayer.physical, NetworkLayer.transport, qualityOf

Nat.pow

The power operation on natural numbers, usually accessed via the ^ operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

def Nat.pow (m : ℕ) : ℕ → ℕ

Used by: phoneNumberInformation_eq, phoneNumber_bits_needed

Nat.succ_pos

theorem Nat.succ_pos (n : ℕ) : 0 < n.succ

Used by: Logic.PropositionalLogic.Formula.witness

Nat.zero_le

theorem Nat.zero_le (n : ℕ) : 0 ≤ n

Used by: BitFunction.exists_settle, Structure.Arithmetic.Tower.instOrderBotColimit, Structure.Arithmetic.Tower.stepTo_bot, arithPlus_mk_eq, arithSucc_mk_eq

Nonempty

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.

inductive Nonempty.{u} (α : Sort u) : Prop

Nonempty.elim

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.

theorem Nonempty.elim.{u} {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : ∀ (a : α), p) : p

Used by: Logic.ProofTheory.CutFree.DerivationsOf.graft, Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.DerivableCutFree.graft, Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.DerivationsOf.of_forall, Logic.ProofTheory.toBasis1

Not

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

Conventions for notations in identifiers:

The recommended spelling of ¬ in identifiers is not.

def Not (a : Prop) : Prop

Option

Optional values, which are either some around a value from the underlying type or 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.{u} (α : Type u) : Type u

Option.getD

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.

Examples: * (some "hello").getD "goodbye" = "hello" * none.getD "goodbye" = "goodbye"

def Option.getD.{u_1} {α : Type u_1} (opt : Option α) (dflt : α) : α

Used by: Frame.make, Frame.valid, Receiver.step, Receiver.step_correct, qualityOf

Or

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.

Conventions for notations in identifiers:

The recommended spelling of ∨ in identifiers is or.

inductive Or (a b : Prop) : Prop

Or.elim

Proof by cases on an Or. If a ∨ b, and both a and b imply proposition c, then c is true.

theorem Or.elim {a b c : Prop} (h : a ∨ b) (left : a → c) (right : b → c) : c

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.parallel_assoc, Fin.append_eval, Frame.crcStep_length, Frame.reflectIndex, Frame.reflectIndex_involutive, Frame.toPoly_set_flip, Logic.ProofTheory.CutFree.DerivationsOf.graft, Logic.ProofTheory.CutFree.DerivationsOf.mono, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.S_iff_succ, arithPlus_succ, arithPlus_zero, no_pow_two_eq_pow_five, no_pow_two_eq_pow_three

Or.resolve_left

theorem Or.resolve_left {a b : Prop} (h : a ∨ b) (na : ¬a) : b

Used by: Heap.combine, Heap.create

PEmpty

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.{u} : Sort u

Used by: Specification.terminalCone

PProd

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.

Conventions for notations in identifiers:

The recommended spelling of ×' in identifiers is PProd.

structure PProd.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

Used by: Frame.toPoly, InformationSystem.Chain, InformationSystem.eval, Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.Derivation, Logic.ProofTheory.DerivationsOf, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.NandFormula, Logic.PropositionalLogic.NandFormula.ofFormula, Logic.PropositionalLogic.NandFormula.toFormula, Logic.PropositionalLogic.NandFormula.val

PULift

Lifts a type or proposition to a higher universe level.

PULift α wraps a value of type α. It is a generalization of PLift that allows lifting values whose type may live in Sort s. It also subsumes PLift.

structure PULift.{r, s} (α : Sort s) : Sort (max s r 1)

PUnit

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.{u} : Sort u

Used by: Frame.toPoly, InformationSystem.Chain, InformationSystem.eval, Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.Derivation, Logic.ProofTheory.DerivationsOf, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.NandFormula, Logic.PropositionalLogic.NandFormula.ofFormula, Logic.PropositionalLogic.NandFormula.toFormula, Logic.PropositionalLogic.NandFormula.val, unexpandSeqAppend, unexpandToSeq

Prod

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)) : α × (β × γ).

Conventions for notations in identifiers:

The recommended spelling of × in identifiers is Prod.

structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)

String

A string is a sequence of Unicode scalar values.

At runtime, strings are represented by dynamic arrays of bytes using the UTF-8 encoding. Both the size in bytes (String.utf8ByteSize) and in characters (String.length) are cached and take constant time. Many operations on strings perform in-place modifications when the reference to the string is unique.

structure String : Type

Used by: Concept, Difficulty.ofString?, Ontology.readFile, Quality.ofString?, RawRelation, Relation, allConceptAnnotations, allDifficultyAnnotations, allQualityAnnotations, getConceptsOf, instDecodeTomlConcept, instDecodeTomlRawRelation, qualityOf, resolveRelation

String.Pos.Raw

A byte position in a String, according to its UTF-8 encoding.

Character positions (counting the Unicode code points rather than bytes) are represented by plain Nats. Indexing a String by a String.Pos.Raw takes constant time, while character positions need to be translated internally to byte positions, which takes linear time.

A byte position p is valid for a string s if 0 ≤ p ≤ s.rawEndPos and p lies on a UTF-8 character boundary, see String.Pos.IsValid.

There is another type, String.Pos, which bundles the validity predicate. Using String.Pos instead of String.Pos.Raw is recommended because it will lead to less error handling and fewer edge cases.

structure String.Pos.Raw : Type

Used by: Ontology.readFile

String.rawEndPos

A UTF-8 byte position that points at the end of a string, just after the last character.

"abc".rawEndPos = ⟨3⟩
"L∃∀N".rawEndPos = ⟨8⟩

def String.rawEndPos (s : String) : String.Pos.Raw

Used by: Ontology.readFile

Subtype

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 Strings. * Given xs : List α, List { x : α // x ∈ xs } is the type of lists in which all elements are contained in xs.

Conventions for notations in identifiers:

The recommended spelling of { x // p x } in identifiers is subtype.

structure Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)

Used by: InterfaceOld.Value, InterfaceOld.Value.eq_of_heq, InterfaceOld.Value.ext_of_fired_eq, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.unit.Value.subsingleton, Logic.FirstOrderLogic.realize_update_of_not_mem_freeVarFinset, Object, SimpleGraph.induceComplSingletonEquiv, Topology, Topology.leaveCoverage, Topology.whole, Topology.whole_adj_of_internal, Topology.whole_adj_of_link, Topology.whole_reachable_of_external, instNonemptyValue, instNormValue

True

True is a proposition and has only an introduction rule, True.intro : True. In other words, True is simply true, and has a canonical proof, True.intro For more information: Propositional Logic

inductive True : Prop

Unit

The canonical type with one element. This element is written ().

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

Used by: ApplicationLayer.Value, Cell.eraseSecondBit, Cell.erase_not_injective, Cell.erase_not_surjective, Component.Hom.comp_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensorUnit, Component.Hom.tensor_comm, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.empty, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id, Component.id_sequential, Component.monoidalCategory, Component.parallel_comm, Component.parallel_empty, Component.sequential_id, Component.symmetry, Component.symmetry_symmetry, DataLinkLayer.network, DataLinkLayer.physical, Difficulty.ofString?, Frame.toPoly, InformationSystem.Environment.universe, InformationSystem.Environment.universe_isolated, Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.Popper.Basis1.instHasExistentialNatUnitTotalBasis1InferInstanceHasSubstitutionMutual, Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1, Logic.Popper.Basis1.instHasUniversalNatUnitTotalBasis1InferInstanceHasSubstitutionMutual, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, Ontology.readFile, Quality.ofString?, Receiver.step, Receiver.step_correct, Topology.joinHistory, Topology.step, Unit.discrete, arithLang, doorInterface, doorLanguage, instDecodeTomlConcept, instDecodeTomlRawRelation, instNormEvent, instNormNonnegUnit, instNormSignal, instNormUnit_computerNetworks, qualityOf, unexpandSeqAppend, unexpandToSeq

Unit.unit

The only element of the unit type.

It can be written as an empty tuple: ().

abbrev Unit.unit : Unit

Used by: ApplicationLayer.Value, Cell.eraseSecondBit, Cell.erase_not_injective, Cell.erase_not_surjective, Component.Hom.comp_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensorUnit, Component.Hom.tensor_comm, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.empty, Component.empty_parallel, Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow, Component.id, Component.id_sequential, Component.monoidalCategory, Component.parallel_comm, Component.parallel_empty, Component.sequential_id, Component.symmetry, Component.symmetry_symmetry, DataLinkLayer.network, DataLinkLayer.physical, Difficulty.ofString?, Frame.toPoly, InformationSystem.Environment.universe, Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.Popper.Basis1.instHasExistentialNatUnitTotalBasis1InferInstanceHasSubstitutionMutual, Logic.Popper.Basis1.instHasSubstitutionNatUnitMutualTotalBasis1, Logic.Popper.Basis1.instHasUniversalNatUnitTotalBasis1InferInstanceHasSubstitutionMutual, NetworkLayer.forwards, NetworkLayer.resolves, NetworkLayer.transport, Quality.ofString?, Receiver.step, Receiver.step_correct, Topology.joinHistory, arithLang, arithPlus, arithPlus_iff, arithPlus_mk_eq, arithStruct_congr, doorLanguage, instNormEvent, instNormSignal, qualityOf, unexpandSeqAppend, unexpandToSeq

absurd

Anything follows from two contradictory hypotheses. Example:

example (hp : p) (hnp : ¬p) : q := absurd hp hnp

For more information: Propositional Logic

def absurd.{v} {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b

cast

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

def cast.{u} {α β : Sort u} (h : α = β) (a : α) : β

Used by: Frame.generator_not_dvd_pow, Frame.toPoly_degree_lt, irrational_logb_two_five, irrational_logb_two_three, phoneNumberInformation_eq, trafficLightInformation_eq

cond

The conditional function.

cond c x y is the same as if c then x else y, but optimized for a Boolean condition rather than a decidable proposition. It can also be written using the notation bif c then x else y.

Just like ite, cond is declared @[macro_inline], which causes applications of cond to be unfolded. As a result, x and y are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated.

def cond.{u} {α : Sort u} (c : Bool) (x y : α) : α

congr

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

theorem congr.{u, v} {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) :
  f₁ a₁ = f₂ a₂

congrArg

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 <something containing a₁> = <something containing a₂>. This function is used internally by tactics like congr and simp to apply equalities inside subterms.

For more information: Equality

theorem congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂

congrFun

Congruence in the function part of an application: If f = g then f a = g a.

theorem congrFun.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) : f a = g a

Used by: Structure.Arithmetic.rec_base, Structure.Arithmetic.rec_step, notRule_no_fixedPoint

congrFun'

Similar to congrFun but β does not depend on α.

theorem congrFun'.{u, v} {α : Sort u} {β : Sort v} {f g : α → β} (h : f = g) (a : α) : f a = g a

dite

“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.)

def dite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : ¬c → α) : α

eq_of_heq

If two heterogeneously equal terms have the same type, then they are propositionally equal.

theorem eq_of_heq.{u} {α : Sort u} {a a' : α} (h : a ≍ a') : a = a'

heq_of_eq

Propositionally equal terms are also heterogeneously equal.

theorem heq_of_eq.{u_1} {α✝ : Sort u_1} {a a' : α✝} (h : a = a') : a ≍ a'

Used by: InterfaceOld.Value.ext_of_fired_eq

id

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.

def id.{u} {α : Sort u} (a : α) : α

inferInstance

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

def foo : Inhabited (Nat × Nat) :=
  inferInstance

example : foo.default = (default, default) :=
  rfl

abbrev inferInstance.{u} {α : Sort u} [i : α] : α

ite

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. Write if h : c then t else e instead for a “dependent if-then-else” dite, which allows t/e to use the fact that c is true/false.

def ite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α

Used by: Frame.crcStep, Frame.crcStep_length, Frame.crcStep_poly, Frame.crc_poly_dvd, Frame.toPoly, Frame.toPoly_append, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any, Frame.toPoly_replicate_false, Frame.toPoly_set_flip, Frame.toPoly_xor, InformationSystem.gatedFlow, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Logic.FirstOrderLogic.all, Logic.FirstOrderLogic.ex, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.literal, Logic.PropositionalLogic.Formula.literal_val, Logic.PropositionalLogic.Formula.starred, NetworkLayer.forwards, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instPeanoStandard, Topology.step, Topology.step_conserves, getConceptsOf, unexpandSeqAppend, unexpandToSeq

liftM

Translates an action from monad m into monad n.

abbrev liftM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n]
  {α : Type u_1} : m α → n α

Used by: Ontology.readFile

noConfusion_of_Nat

A helper theorem to deduce False from a = b when f a ≠ f b for some function f : α → Nat (typically .ctorIdx). Used as a simpler alternative to the no-confusion theorems.

theorem noConfusion_of_Nat.{u} {α : Sort u} (f : α → ℕ) {a b : α} (h : a = b) :
  Bool.rec False True ((f a).beq (f b))

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_strict, Finset.sum_preimage_map_disjUnion, Frame.toPoly_xor, InformationSystem.Chain.ofIsChain, InformationSystem.not_spontaneous_and_perpetuous, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.tensor, Logic.Popper.Basis1.substitutivity, Ontology.empty_wellFormed, arithPlus_iff, arithSucc_iff

of_decide_eq_true

theorem of_decide_eq_true {p : Prop} [inst : Decidable p] : decide p = true → p

optParam

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.

def optParam.{u} (α : Sort u) (default : α) : Sort u

Used by: Ontology.readFile

rfl

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.

def rfl.{u} {α : Sort u} {a : α} : a = a

`PropLemmas`

decide_eq_true_iff

theorem decide_eq_true_iff {p : Prop} [Decidable p] : decide p = true ↔ p

Used by: Receiver.step_correct

exists_eq_right

theorem exists_eq_right.{u_1} {α : Sort u_1} {p : α → Prop} {a' : α} : (∃ a, p a ∧ a = a') ↔ p a'

Used by: InterfaceOld.Value.join

exists_false

theorem exists_false.{u_1} {α : Sort u_1} : ¬∃ _a, False

Used by: InterfaceOld.Value.join

exists_prop_congr

theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') :
  Exists q ↔ ∃ (h : p'), q' ⋯

Used by: arithTower

`SimpLemmas`

Bool.and_eq_true

theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

Bool.and_false

theorem Bool.and_false (b : Bool) : (b && false) = false

Used by: Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.NandFormula.ofFormula_val

Bool.and_self

theorem Bool.and_self (b : Bool) : (b && b) = b

Used by: Logic.PropositionalLogic.NandFormula.ofFormula_val, Logic.PropositionalLogic.semanticConnectives

Bool.and_true

theorem Bool.and_true (b : Bool) : (b && true) = b

Used by: Logic.PropositionalLogic.NandFormula.ofFormula_val

Bool.false_and

theorem Bool.false_and (b : Bool) : (false && b) = false

Used by: Logic.PropositionalLogic.Formula.kalmar

Bool.false_or

theorem Bool.false_or (b : Bool) : (false || b) = b

Used by: Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.Formula.soundness

Bool.not_false

theorem Bool.not_false : (!false) = true

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.toPoly_set_flip, Frame.toPoly_xor, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.literal_val, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.NandFormula.ofFormula_val, Logic.PropositionalLogic.semanticConnectives

Bool.not_true

theorem Bool.not_true : (!true) = false

Used by: Frame.crc32Ethernet_detects_single_bit_flip, Frame.toPoly_set_flip, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.literal_val, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.Formula.soundness, Logic.PropositionalLogic.NandFormula.ofFormula_val

Bool.or_eq_true

theorem Bool.or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true)

Used by: Frame.toPoly_ne_zero_of_any, Logic.PropositionalLogic.Formula.bigOr_val, Logic.PropositionalLogic.semanticConnectives

Bool.or_false

theorem Bool.or_false (b : Bool) : (b || false) = b

Used by: Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.NandFormula.ofFormula_val

Bool.or_self

theorem Bool.or_self (b : Bool) : (b || b) = b

Used by: Logic.PropositionalLogic.NandFormula.ofFormula_val

Bool.or_true

theorem Bool.or_true (b : Bool) : (b || true) = true

Used by: Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.or_entails_right, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.NandFormula.ofFormula_val

Bool.true_and

theorem Bool.true_and (b : Bool) : (true && b) = b

Used by: Logic.PropositionalLogic.Formula.kalmar

Bool.true_or

theorem Bool.true_or (b : Bool) : (true || b) = true

Used by: Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.or_entails_left, Logic.PropositionalLogic.Formula.semantic_iff_provable

Eq.mpr_not

theorem Eq.mpr_not {p q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow

Eq.mpr_prop

theorem Eq.mpr_prop {p q : Prop} (h₁ : p = q) (h₂ : q) : p

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow

and_false

theorem and_false (p : Prop) : (p ∧ False) = False

Used by: Finset.sum_preimage_map_disjUnion, InformationSystem.spontaneous_no_self_return, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr

and_self

theorem and_self (p : Prop) : (p ∧ p) = p

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

bne_self_eq_false

theorem bne_self_eq_false.{u_1} {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) : (a != a) = false

Used by: Frame.toPoly_xor

dite_cond_eq_false

theorem dite_cond_eq_false.{u} {α : Sort u} {c : Prop} {x✝ : Decidable c} {t : c → α} {e : ¬c → α}
  (h : c = False) : dite c t e = e ⋯

Used by: Frame.ofFn_update, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex

dite_cond_eq_true

theorem dite_cond_eq_true.{u} {α : Sort u} {c : Prop} {x✝ : Decidable c} {t : c → α} {e : ¬c → α}
  (h : c = True) : dite c t e = t ⋯

Used by: Frame.ofFn_update, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex

dite_congr

theorem dite_congr.{u_1} {b c : Prop} {α : Sort u_1} {x✝ : Decidable b} [Decidable c] {x : b → α}
  {u : c → α} {y : ¬b → α} {v : ¬c → α} (h₁ : b = c) (h₂ : ∀ (h : c), x ⋯ = u h)
  (h₃ : ∀ (h : ¬c), y ⋯ = v h) : dite b x y = dite c u v

Used by: Component.hexagon_forward_arrow, Component.hexagon_reverse_arrow

eq_false

theorem eq_false {p : Prop} (h : ¬p) : p = False

Used by: Frame.ofFn_update, InterfaceOld.Value.join, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Structure.Arithmetic.S_iff_add_one, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_step, Topology.Step.coverageFunctor

eq_false'

theorem eq_false' {p : Prop} (h : p → False) : p = False

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_strict, Finset.sum_preimage_map_disjUnion, InformationSystem.Chain.ofIsChain, InformationSystem.not_spontaneous_and_perpetuous, InterfaceOld.Value.join, InterfaceOld.Value.join_disjoint, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.tensor

eq_self

theorem eq_self.{u_1} {α : Sort u_1} (a : α) : (a = a) = True

eq_true

theorem eq_true {p : Prop} (h : p) : p = True

Used by: BitSequence.trueCount_strict, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.DerivationsOf.of_forall, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_base, Topology.Step.coverageFunctor

false_and

theorem false_and (p : Prop) : (False ∧ p) = False

Used by: Logic.PropositionalLogic.Formula.bigOr_val, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_base, Structure.Arithmetic.rec_step

false_iff

theorem false_iff (p : Prop) : (False ↔ p) = ¬p

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

false_or

theorem false_or (p : Prop) : (False ∨ p) = p

Used by: Finset.sum_preimage_map_disjUnion, Frame.toPoly_ne_zero_of_any, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inr, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_step

forall_congr

theorem forall_congr.{u} {α : Sort u} {p q : α → Prop} (h : ∀ (a : α), p a = q a) :
  (∀ (a : α), p a) = ∀ (a : α), q a

Used by: BitFunction.exists_settle, InformationSystem.spontaneous_no_self_return, Logic.PropositionalLogic.Formula.bigAnd_val, Specification.terminalCone, Structure.Arithmetic.S_iff_add_one, Topology.isNerveCover_inter

heq_eq_eq

theorem heq_eq_eq.{u_1} {α : Sort u_1} (a b : α) : (a ≍ b) = (a = b)

Used by: Topology.whole_adj_of_internal

iff_false

theorem iff_false (p : Prop) : (p ↔ False) = ¬p

Used by: BitSequence.trueCount_strict

iff_self

theorem iff_self (p : Prop) : (p ↔ p) = True

Used by: Finset.sum_preimage_map_disjUnion, InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, InterfaceOld.Value.join, InterfaceOld.Value.join_fired_inl, InterfaceOld.Value.join_fired_inr, InterfaceOld.tensor, Layer.id_rel, Layer.parallel_rel, Layer.sequential_rel, Logic.PropositionalLogic.Formula.bigAnd_val, Logic.PropositionalLogic.Formula.bigOr_val, Logic.PropositionalLogic.Formula.literal_val, Structure.Arithmetic.Tower.stepTo_le_iff, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_base, arithTower

iff_true

theorem iff_true (p : Prop) : (p ↔ True) = p

Used by: BitSequence.trueCount_strict

implies_congr

theorem implies_congr.{u, v} {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) :
  (p₁ → q₁) = (p₂ → q₂)

Used by: Frame.crc32Ethernet_detects_single_bit_flip, InformationSystem.spontaneous_no_self_return, Logic.PropositionalLogic.Formula.bigAnd_val, Structure.Arithmetic.S_iff_add_one

implies_congr_ctx

theorem implies_congr_ctx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA

implies_true

theorem implies_true.{u} (α : Sort u) : (∀ (a : α), True) = True

Used by: InformationSystem.gatedFlow_success_AB, InformationSystem.gatedFlow_success_BA, Logic.PropositionalLogic.Formula.bigAnd_val, Specification.terminalCone

ite_cond_eq_false

theorem ite_cond_eq_false.{u} {α : Sort u} {c : Prop} {x✝ : Decidable c} (a b : α) (h : c = False) :
  (if c then a else b) = b

Used by: Frame.crcStep_poly, Frame.toPoly_degree_lt, Frame.toPoly_ne_zero_of_any, Frame.toPoly_replicate_false, Frame.toPoly_set_flip, Frame.toPoly_xor, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.literal_val, Structure.Arithmetic.S_iff_add_one, Topology.Step.coverageFunctor

ite_cond_eq_true

theorem ite_cond_eq_true.{u} {α : Sort u} {c : Prop} {x✝ : Decidable c} (a b : α) (h : c = True) :
  (if c then a else b) = a

Used by: Frame.crcStep_poly, Frame.toPoly_degree_lt, Frame.toPoly_set_flip, Frame.toPoly_xor, Logic.FirstOrderLogic.realize_all, Logic.FirstOrderLogic.realize_ex, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.literal_val, Structure.Arithmetic.S_iff_add_one, Topology.Step.coverageFunctor

ite_congr

theorem ite_congr.{u_1} {α : Sort u_1} {b c : Prop} {x y u v : α} {s : Decidable b} [Decidable c]
  (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬c → y = v) : (if b then x else y) = if c then u else v

Used by: Frame.crcStep_poly, Frame.toPoly_ne_zero_of_any, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.kalmar

not_false_eq_true

theorem not_false_eq_true : (¬False) = True

Used by: BitSequence.Dominates.bot, Frame.ofFn_update, Frame.toPoly_set_flip, InformationSystem.not_spontaneous_and_perpetuous, InformationSystem.spontaneous_no_self_return, InterfaceOld.Value.join_disjoint, InterfaceOld.unit.Value.subsingleton, Logic.Popper.Basis1.demonstrate_of_contradictory, Logic.ProofTheory.Derivation.toCutFree, Logic.ProofTheory.Schema.IsSimpleRule.of_isAxiom, Logic.PropositionalLogic.HilbertSchema.mp_isSimple, Structure.Arithmetic.instArithFin

not_true_eq_false

theorem not_true_eq_false : (¬True) = False

Used by: BitSequence.trueCount_strict, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_base

of_eq_true

theorem of_eq_true {p : Prop} (h : p = True) : p

or_false

theorem or_false (p : Prop) : (p ∨ False) = p

or_true

theorem or_true (p : Prop) : (p ∨ True) = True

Used by: Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.DerivationsOf.of_forall, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.provable_lem, Logic.PropositionalLogic.semanticConnectives, Logic.PropositionalLogic.syntacticConnectives, Topology.join_preserves_connected

true_and

theorem true_and (p : Prop) : (True ∧ p) = p

Used by: BitSequence.trueCount_strict, Logic.PropositionalLogic.Formula.kalmar, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.rec_base, Structure.Arithmetic.rec_step, Topology.whole_adj_of_internal

true_or

theorem true_or (p : Prop) : (True ∨ p) = True

Used by: Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.DerivationsOf.of_forall, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.semanticConnectives, Logic.PropositionalLogic.syntacticConnectives

`SizeOf`

SizeOf

SizeOf is a typeclass automatically derived for every inductive type, which equips the type with a “size” function to Nat. The default instance defines each constructor to be 1 plus the sum of the sizes of all the constructor fields.

This is used for proofs by well-founded induction, since every field of the constructor has a smaller size than the constructor itself, and in many cases this will suffice to do the proof that a recursive function is only called on smaller values. If the default proof strategy fails, it is recommended to supply a custom size measure using the termination_by argument on the function definition.

structure SizeOf.{u} (α : Sort u) : Sort (max 1 u)

`System.FilePath`

System.FilePath

A path on the file system.

Paths consist of a sequence of directories followed by the name of a file or directory. They are delimited by a platform-dependent separator character (see System.FilePath.pathSeparator).

structure System.FilePath : Type

Used by: Ontology.readFile

`System.IO`

BaseIO

An IO monad that cannot throw exceptions.

def BaseIO (α : Type) : Type

Used by: Ontology.readFile

EIO

A monad that can have side effects on the external world or throw exceptions of type ε.

BaseIO is a version of this monad that cannot throw exceptions. IO sets the exception type to IO.Error.

def EIO (ε α : Type) : Type

Used by: Ontology.readFile

EIO.toBaseIO

Converts an EIO ε action that might throw an exception of type ε into an exception-free BaseIO action that returns an Except value.

def EIO.toBaseIO {ε α : Type} (act : EIO ε α) : BaseIO (Except ε α)

Used by: Ontology.readFile

IO

A monad that supports arbitrary side effects and throwing exceptions of type IO.Error.

abbrev IO : Type → Type

Used by: Ontology.readFile

IO.FS.readFile

Reads the entire contents of the UTF-8-encoded file at the given path as a String.

An exception is thrown if the contents of the file are not valid UTF-8. This is in addition to exceptions that may always be thrown as a result of failing to read files.

def IO.FS.readFile (fname : System.FilePath) : IO String

Used by: Ontology.readFile

`System.IOError`

IO.Error

Exceptions that may be thrown in the IO monad.

Many of the constructors of IO.Error correspond to POSIX error numbers. In these cases, the documentation string lists POSIX standard error macros that correspond to the error. This list is not necessarily exhaustive, and these constructor includes a field for the underlying error number.

inductive IO.Error : Type

Used by: Ontology.readFile

IO.userError

Constructs an IO.Error from a string.

IO.Error is the type of exceptions thrown by the IO monad.

def IO.userError (s : String) : IO.Error

Used by: Ontology.readFile

`WF`

Acc

Acc is the accessibility predicate. Given some relation r (e.g. <) and a value x, Acc r x means that x is accessible through r:

x is accessible if there exists no infinite sequence ... < y₂ < y₁ < y₀ < x.

inductive Acc.{u} {α : Sort u} (r : α → α → Prop) : α → Prop

Used by: Structure.Arithmetic.Halts, Structure.Arithmetic.terminates_of_halts

InvImage.wf

theorem InvImage.wf.{u, v} {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) (h : WellFounded r) :
  WellFounded (InvImage r f)

Used by: Structure.Arithmetic.halts_of_measure

Subrelation.wf

theorem Subrelation.wf.{u} {α : Sort u} {r q : α → α → Prop} (h₁ : Subrelation q r) (h₂ : WellFounded r) :
  WellFounded q

Used by: Structure.Arithmetic.halts_of_measure

WellFounded

A relation r is WellFounded if all elements of α are accessible within r. If a relation is WellFounded, it does not allow for an infinite descent along the relation.

If the arguments of the recursive calls in a function definition decrease according to a well founded relation, then the function terminates. Well-founded relations are sometimes called Artinian or said to satisfy the “descending chain condition”.

inductive WellFounded.{u} {α : Sort u} (r : α → α → Prop) : Prop

Used by: Structure.Arithmetic.lt_wf

WellFounded.Nat.fix

A well-founded fixpoint operator specialized for Nat-valued measures. Given a measure h, it expects its higher order function argument F to invoke its argument only on values y that are smaller than x with regard to h.

In contrast to WellFounded.fix, this fixpoint operator reduces on closed terms. (More precisely: when h x evaluates to a ground value)

def WellFounded.Nat.fix.{u, v} {α : Sort u} {motive : α → Sort v} (h : α → ℕ)
  (F : (x : α) → ((y : α) → InvImage (fun x1 x2 => x1 < x2) h y x → motive y) → motive x) (x : α) :
  motive x

Used by: Logic.ProofTheory.Derivation.toCutFree

WellFounded.apply

theorem WellFounded.apply.{u} {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a

Used by: Structure.Arithmetic.halts_of_measure

WellFounded.fix

A well-founded fixpoint. If satisfying the motive C for all values that are smaller according to a well-founded relation allows it to be satisfied for the current value, then it is satisfied for all values.

This function is used as part of the elaboration of well-founded recursion.

def WellFounded.fix.{u, v} {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r)
  (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x

Used by: Structure.Arithmetic.iter

WellFounded.fix_eq

theorem WellFounded.fix_eq.{u, v} {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r)
  (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : hwf.fix F x = F x fun y x => hwf.fix F y

Used by: Structure.Arithmetic.iter_eq

WellFounded.induction

theorem WellFounded.induction.{u} {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Prop}
  (a : α) (h : ∀ (x : α), (∀ (y : α), r y x → C y) → C x) : C a

Used by: Structure.Arithmetic.count_surjective, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent