Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt

Use this file to discover all available pages before exploring further.

LeanSpec.lib.Util provides the generic types and functions that underpin the tutorial examples throughout lean-spec. The definitions here are foundational building blocks — range-constrained strings and numbers, ordering predicates for lists, finite sets with the standard set algebra, and finite maps supporting key-based lookup. Items are included only when needed by the examples, and most instances requiring a proof obligation are left as sorry to keep the focus squarely on specification rather than proof or implementation detail.

​
Restricted Basic Types

These subtypes carve out well-behaved subsets of String, Nat, and Int and equip them with the typeclass instances — equality, ordering — needed for use in specifications.

​
Str m n

A length-constrained string whose character count lies in the closed interval [m, n]. 
def Str (m n : Nat) := { s : String // m ≤ s.length ∧ s.length ≤ n }
Both bounds are inclusive. A value s : Str m n carries the proof m ≤ s.val.length ∧ s.val.length ≤ n as part of its type, so any attempt to construct an out-of-range string is rejected at the type level. DecidableEq instance — equality on Str m n is decidable: 
instance : DecidableEq (Str m n) :=
  sorry
LT instance — the strict order on Str m n is inherited from the underlying String order: 
instance (m n : Nat) : LT (Str m n) where
  lt s₀ s₁ := s₀.val < s₁.val
Decidable < — the decision procedure delegates to the underlying string comparison: 
instance (m n : Nat) (x y : Str m n) : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.val < y.val))

​
NatMN m n

A natural number constrained to the half-open interval [m, n). The lower bound is inclusive and the upper bound is exclusive. 
def NatMN (m n : Nat) := { x : Nat // m ≤ x ∧ x < n }
DecidableEq instance: 
instance : DecidableEq (NatMN m n) :=
  sorry
NatMN is used extensively in Geo to represent degree values — for example, bearings in [0°, 360°).

​
IntMN m n

A signed integer constrained to the half-open interval [m, n). The lower bound is inclusive and the upper bound is exclusive. 
def IntMN (m n : Int) := { x : Int // m ≤ x ∧ x < n }
DecidableEq instance: 
instance : DecidableEq (IntMN m n) :=
  sorry
IntMN is used in Geo to represent latitude and longitude expressed in arc-seconds, where negative values are South or West respectively.

​
List Utilities

The List namespace is extended with aggregation functions and order-checking predicates. Each function is polymorphic over the element type and requires only the minimal typeclass constraint.

​
List.add

The sum of the elements of a list. An identity value must be supplied for the empty case. 
def add [Add α] (as : List α) : α → α :=
  as.foldr (· + ·)

​
List.mul

The product of the elements of a list. An identity value must be supplied for the empty case. 
def mul [Mul α] (as : List α) : α → α :=
  as.foldr (· * ·)

​
List.max

The maximum of the elements of a list. A default value is supplied for the empty case. 
def max [Max α] (as : List α) : α → α :=
  as.foldr Max.max

​
List.min

The minimum of the elements of a list. A default value is supplied for the empty case. 
def min [Min α] (as : List α) : α → α :=
  as.foldr Min.min

​
List.minimumD

The minimum element of a list, returning a caller-supplied default for the empty list. Delegates to List.minimum? internally. 
def minimumD [Min α] (as : List α) (a : α) : α :=
  match as.minimum? with
  | none   => a
  | some a => a

​
List.ascending

A proposition stating that the elements of a list are in non-strictly ascending (i.e. non-decreasing) order. 
def ascending [LE α] : List α → Prop
 | [] | [_] => True
 | a::b::as => a ≤ b ∧ ascending (b::as)
Empty and singleton lists vacuously satisfy ascending.

​
List.ascendingStrict

A proposition stating that the elements of a list are in strictly ascending order (no two adjacent elements are equal). 
def ascendingStrict [LT α] : List α → Prop
 | [] | [_] => True
 | a::b::as => a < b ∧ ascendingStrict (b::as)

​
List.descending

A proposition stating that the elements of a list are in non-strictly descending (i.e. non-increasing) order. 
def descending [LE α] : List α → Prop
 | [] | [_] => True
 | a::b::as => a ≥ b ∧ descending (b::as)

​
List.descendingStrict

A proposition stating that the elements of a list are in strictly descending order. 
def descendingStrict [LT α] : List α → Prop
 | [] | [_] => True
 | a::b::as => a > b ∧ descendingStrict (b::as)

​
List.toSet

Converts a list to a Set by removing duplicate elements using eraseDup. 
def List.toSet [DecidableEq α] (as : List α) : Set α :=
  ⟨as.eraseDup, sorry⟩

​
Finite Sets

Set A is the type of finite sets of elements drawn from A. Sets are represented internally as duplicate-free lists; all operations must be order-agnostic so that two sets with the same elements are considered equal regardless of the order in which their backing lists happen to be stored.

​
Type definition

def Set (α : Type) [DecidableEq α] := { as : List α // as.Nodup }
The Nodup predicate guarantees no element appears more than once.

​
Standard typeclass instances

InstanceNotationMeaning
EmptyCollection∅The empty set
Membershipa ∈ sElement membership
HasSubsets₁ ⊆ s₂Every element of s₁ is in s₂
HasSSubsets₁ ⊊ s₂s₁ ⊆ s₂ and some element of s₁ is absent from s₂
Unions₁ ∪ s₂Elements in either set (deduped)
Inters₁ ∩ s₂Elements in both sets
SDiffs₁ \ s₂Elements in s₁ not in s₂
Insertinsert a sAdd an element, preserving Nodup
Singleton{a}A one-element set
DecidableEq—Equality is decidable
Sep{ a ∈ A | P a }Set comprehension via filterp

​
Set.card

The cardinality (number of elements) of a set. 
def card [DecidableEq α] (s : Set α) : Nat :=
  s.val.length

​
Set.map

Apply a function to every element, deduplicating the image. The result may have fewer elements than the input if the function is not injective. 
def map [DecidableEq α] [DecidableEq β] (f : α → β) (as : Set α) : Set β :=
  ⟨(as.val.map f).eraseDup, sorry⟩

​
Set.filter

Retain elements satisfying a boolean predicate. 
def filter [DecidableEq α] (p : α → Bool) (as : Set α) : Set α :=
  ⟨as.val.filter p, sorry⟩

​
Set.filterp

Retain elements satisfying a propositional predicate. This is the backing function for the Sep instance, enabling { a ∈ A | P a } notation. 
def filterp [DecidableEq α] (p : α → Prop) (as : Set α) : Set α :=
  sorry

​
Set.foldr

Fold a binary function over the elements of a set. Because sets are unordered, the supplied function should be commutative and associative for the result to be well-defined. 
def foldr [DecidableEq α] (f : α → β → β) (init : β) (as : Set α) : β :=
  as.val.foldr f init

​
Set.select

Extract the unique element from a singleton set. Requires a proof that card s = 1. 
def select [DecidableEq α] : (as : Set α) → (as.card = 1) → α :=
  sorry

​
Set.minimumD

The minimum element of a set, with a caller-supplied default for the empty set. Delegates to List.minimumD on the backing list. 
def minimumD [DecidableEq α] [Min α] (as : Set α) (a : α) : α :=
  as.val.minimumD a

​
Set.add

The sum of all elements in the set. An identity value must be provided for the empty case. 
def add [DecidableEq α] [Add α] (as : Set α) : α → α :=
  as.foldr (· + ·)

​
Set.add'

The sum of the images of elements under a function f. An identity value is provided for the empty case. 
def add' [DecidableEq α] [Add β] (as : Set α) (f : α → β) : β → β :=
  as.foldr (f · + ·)

​
Finite Maps

α ⟹ β is the type of finite maps from keys of type α to values of type β. It uses the infix operator ⟹ (precedence 34, just below ×) and is defined within the Std namespace.

​
Type definition

A Map.Entry pairs a key with a value: 
structure Map.Entry (α β : Type) where
  key   : α
  value : β
deriving DecidableEq
A Map is a Set of entries in which all keys are distinct — enforced by requiring the cardinality of the entry set equals the cardinality of the set of projected keys: 
def Map α β [DecidableEq α] [DecidableEq β] :=
  { s : Set (Map.Entry α β) // s.card = (s.map (·.key)).card }

infixr:34 " ⟹ " => Map

​
Standard typeclass instances

InstanceNotationMeaning
DecidableEq—Equality is decidable
EmptyCollection∅The empty map
Unionm₁ ∪ m₂Merge; m₁ takes precedence on duplicate keys
Interm₁ ∩ m₂Keys present in both; values drawn from m₁
Membershipentry ∈ mFull entry membership (key and value must match)

​
Map.contains

Test whether a map contains a given key (regardless of value). 
def contains [DecidableEq α] [DecidableEq β] (a : α) (m : α ⟹ β) : Prop :=
  ∃ x ∈ m, x.key = a

​
Map.erase

Remove the entry with the given key from a map. 
def erase [DecidableEq α] [DecidableEq β] (m : α ⟹ β) (a : α) : α ⟹ β :=
  sorry

​
Map.insert

Add a key-value pair to a map. 
def insert [DecidableEq α] [DecidableEq β] (m : α ⟹ β) (a : α) (b : β) : α ⟹ β :=
  sorry

​
Map.findEntry?

Find the full entry (key + value) for a given key, returning none if the key is absent. 
def findEntry? [DecidableEq α] [DecidableEq β] (a : α) (m : α ⟹ β) : Option (Entry α β) :=
  sorry

​
Map.findEntry

Find the full entry for a given key, given a proof h : m.contains a that the key is present. 
def findEntry [DecidableEq α] [DecidableEq β] (a : α) (m : α ⟹ β) (h : m.contains a) : Entry α β :=
  sorry

​
Map.find?

Look up the value associated with a key, returning none if the key is absent. 
def find? [DecidableEq α] [DecidableEq β] (a : α) (m : α ⟹ β) : Option β :=
  sorry

​
Map.find

Look up the value associated with a key, given a proof that the key is present. Implemented via findEntry. 
def find [DecidableEq α] [DecidableEq β] (a : α) (m : α ⟹ β) (h : m.contains a) : β :=
  (m.findEntry a h).value

​
Map.isEmpty

Test whether a map has no entries. 
def isEmpty [DecidableEq α] [DecidableEq β] (m : α ⟹ β) : Prop :=
  m = ∅

​
Map.filter

Retain only those entries whose key satisfies a boolean predicate. 
def filter [DecidableEq α] [DecidableEq β] (p : α → Bool) (m : α ⟹ β) : α ⟹ β :=
  sorry

​
Map.domain

The domain of a finite map — the set of all keys. Guaranteed duplicate-free by the Set representation. 
def domain {α : Type} [DecidableEq α] [DecidableEq β] (m : α ⟹ β) : Set α :=
  sorry

​
Map.range

The range (image) of a finite map — the set of all values. 
def range [DecidableEq α] [DecidableEq β] (m : α ⟹ β) : Set β :=
  sorry

​
Option Utilities

Two convenience notations are provided in the Std namespace to reduce verbosity when handling Option values in specifications.

​
▹ … ‖ … — full match notation

Captures the common pattern of branching on none vs some: 
notation t "▹" n "‖" s => match t with | none => n | some x => s x
t ▹ n ‖ s returns n when t is none, and applies s to the unwrapped value when t is some x.

​
▹ … — optional predicate notation

A special case that defaults to True when the option is empty: 
notation t "▹" p => match t with | none => True | some x => p x
t ▹ p holds if t is none (no constraint imposed) or if p x holds for the wrapped value x. This notation is widely used in the tutorial to express optional constraints: “if the field is present, it must satisfy P.”

Build docs developers (and LLMs) love

Get started for freeTalk to us