Skip to main content

Crate oxilean_std

Crate oxilean_std 

Source
Expand description

§OxiLean Standard Library — Core Data Types & Theorems

The standard library provides essential types, type classes, and theorems for OxiLean programs. It is written in OxiLean itself and loaded into the kernel environment at startup.

§Quick Start

§Using Standard Types

ⓘ
theorem two_plus_three : 2 + 3 = 5 := by
  norm_num

def my_list : List Nat := [1, 2, 3]

instance : Eq Nat := { ... }

§Architecture Overview

The standard library is organized into logical categories:

Standard Library Organization
├─ Primitive Types
│  ├─ nat, bool, char, int
│  ├─ string, list, array
│  ├─ option, result, sum
│  └─ prod, sigma
│
├─ Type Classes & Traits
│  ├─ Eq, Ord, Show, Repr
│  ├─ Functor, Monad, Applicative
│  ├─ Monoid, Semigroup
│  └─ Decidable
│
├─ Core Theorems & Lemmas
│  ├─ Equality (eq.rs)
│  ├─ Logic (logic.rs, prop.rs)
│  ├─ Arithmetic (nat.rs, int.rs)
│  └─ Order (ord.rs, order.rs)
│
└─ Utilities & Automation
   ├─ Tactic lemmas
   ├─ Decision procedures
   └─ Parsing combinators

§Key Concepts & Terminology

§Inductive Types

Core types are defined inductively:

Nat : Type 0
  | zero : Nat
  | succ : Nat → Nat

Bool : Prop
  | true : Bool
  | false : Bool

List α : Type 0
  | nil : List α
  | cons : α → List α → List α

Each inductive type comes with:

  • Constructors: Ways to create values
  • Recursor: Principle for inductive recursion
  • Induction principle: Structural induction proof technique

§Type Classes

Type classes enable ad-hoc polymorphism:

class Eq (α : Type u) : Prop where
  eq : α → α → Prop
  refl : ∀ x, eq x x
  symm : ∀ x y, eq x y → eq y x
  trans : ∀ x y z, eq x y → eq y z → eq x z

Instances provide implementations for specific types:

instance Eq Nat : Eq Nat where
  eq := Nat.eq
  refl := Nat.eq_refl
  ...

§Recursion Schemes

Each inductive type gets a recursor for primitive recursion:

Nat.rec :
  {motive : Nat → Sort u}
→ motive 0
→ (∀ n, motive n → motive (n + 1))
→ ∀ n, motive n

Higher-order recursion patterns (fold, map, etc.) are defined in terms of recs.

§Decidability

For computable propositions, we can decide them algorithmically:

class Decidable (p : Prop) : Type 0 where
  decide : Bool
  correct : decide = true ↔ p

Examples: 2 + 3 = 5 is decidable (computable), but ∀ n, P n usually isn’t.

§Module Organization

§Primitive Types & Constructors

ModuleTypesPurpose
natNatNatural numbers (zero, successor)
boolBoolBooleans (true, false)
intIntSigned integers
charCharUnicode characters
stringStringText strings

§Collection Types

ModuleTypesPurpose
listList αLinked lists
arrayArray αFixed-size arrays
vecVec αDynamic vectors (like Lean 4)
setSet αMathematical sets
finFin nFinite sets (0..n-1)

§Option & Alternative Types

ModuleTypesPurpose
optionOption αNullable value
resultResult α εValue or error
sumα ⊕ βTagged union
eitherEither α βAlternative representation
prodα × βPairs/products
sigmaΣ x, P xDependent pairs

§Type Classes

ModuleClassesPurpose
eqEqEquality relation
ordOrdTotal ordering
showShowString representation
reprReprDebug representation
decidableDecidableComputable propositions

§Higher-Order Abstractions

ModuleClassesPurpose
functorFunctorMap over container
applicativeApplicativeApply pure functions
monadMonadSequencing computations
algebraMonoid, SemigroupAlgebraic structures

§Logic & Propositions

ModulePurpose
logicClassical logic (excluded middle, etc.)
propPropositional theorems
eqEquality and substitution

§Arithmetic & Order

ModulePurpose
natNatural number theorems
intInteger theorems
orderPartial orders
orderingCompare result type
rangeInteger ranges

§Advanced Structures

ModulePurpose
rbtreeRed-black trees (sorted maps)
hashmapHash maps
hashsetHash sets
streamLazy sequences
thunkDelayed computation
lazyLazy values

§Utilities

ModulePurpose
wellfoundedWell-founded relations
quotient_typesQuotient type operations
tactic_lemmasLemmas useful for automation
parsecParsing combinators
ioI/O operations

§Type Hierarchy

The standard library respects the universe hierarchy:

Data types (Nat, Bool, List) : Type 0
Type classes (Eq, Show) : Type 0 → Prop or Type 1
Propositions (Nat.add_comm) : Prop
Proofs (rfl, trans) : Prop

§Usage Examples

§Example 1: Working with Natural Numbers

ⓘ
theorem add_comm : ∀ n m : Nat, n + m = m + n := by
  intro n m
  induction n with
  | zero => simp
  | succ n ih => simp [ih]

§Example 2: List Operations

ⓘ
def append {α : Type u} : List α → List α → List α
  | [], ys => ys
  | x :: xs, ys => x :: append xs ys

theorem append_nil : ∀ xs : List α, append xs [] = xs := by
  intro xs
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [ih]

§Example 3: Type Class Instance

ⓘ
instance : Eq (List Nat) where
  eq xs ys := (append xs [] = append ys [])
  refl xs := rfl
  ...

§Example 4: Pattern Matching

ⓘ
def is_zero : Nat → Bool
  | 0 => true
  | _ + 1 => false

def head {α : Type u} : List α → Option α
  | [] => none
  | x :: _ => some x

§Environment Building

The standard library is built in phases:

  1. Phase 1: Primitives — Nat, Bool, basic operations
  2. Phase 2: Collections — List, Array, Set
  3. Phase 3: Type Classes — Eq, Show, etc.
  4. Phase 4: Theorems — Induction principles, lemmas
  5. Phase 5: Automation — Tactic lemmas, decision procedures

Loading happens in oxilean-std via build_*_env functions:

ⓘ
let env = Environment::new();
let env = build_nat_env(env)?;
let env = build_list_env(env)?;
let env = build_eq_env(env)?;
// etc...

§Integration with Elaborator & Tactics

§Decidability

The norm_num and decide tactics use decidable instances:

  • 2 + 3 = 5 via Decidable instance on Nat equality
  • decide extracts this decision to reduce proofs automatically

§Simplification

The simp tactic uses lemmas from the standard library:

  • Reflexivity: x = x
  • Commutativity: x + y = y + x
  • Associativity: (x + y) + z = x + (y + z)

§Induction

The induction tactic uses recursors and induction principles:

  • For Nat: Decompose into zero/successor cases
  • For List: Decompose into nil/cons cases

§Performance & Memory

  • Lazy evaluation: Some computations deferred via Thunk
  • Persistent data structures: Lists/sets use structural sharing
  • Universe polymorphism: Generic types work across universe levels

§Further Reading

Re-exports§

pub use algebra::build_algebra_env;
pub use array::build_array_env;
pub use bitvec::build_bitvec_env;
pub use bool::build_bool_env;
pub use category_theory::build_category_theory_env;
pub use char::build_char_env;
pub use decidable::build_decidable_env;
pub use either::build_either_env;
pub use eq::build_eq_env;
pub use fin::build_fin_env;
pub use functor::build_functor_env;
pub use group_theory::build_group_theory_env;
pub use hashmap::build_hashmap_env;
pub use hashset::build_hashset_env;
pub use int::build_int_env;
pub use io::build_io_env;
pub use lazy::build_lazy_env;
pub use list::build_list_env;
pub use logic::build_logic_env;
pub use monad::build_monad_env;
pub use nat::build_nat_env;
pub use option::build_option_env;
pub use ord::build_ord_env;
pub use order::build_order_env;
pub use ordering::build_ordering_env;
pub use parsec::build_parsec_env;
pub use prod::build_prod_env;
pub use prop::build_prop_env;
pub use quotient_types::build_quotient_types_env;
pub use range::build_range_env;
pub use rbtree::build_rbtree_env;
pub use real::build_real_env;
pub use repr::build_repr_env;
pub use result::build_result_env;
pub use set::build_set_env;
pub use show::build_show_env;
pub use sigma::build_sigma_env;
pub use stream::build_stream_env;
pub use string::build_string_env;
pub use sum::build_sum_env;
pub use tactic_lemmas::build_tactic_lemmas_env;
pub use thunk::build_thunk_env;
pub use topology::build_topology_env;
pub use vec::build_vec_env;
pub use wellfounded::build_wellfounded_env;

Modules§

abstract_algebra_adv
Auto-generated module structure
abstract_algebra_advanced
Auto-generated module structure
abstract_interpretation
Auto-generated module structure
algebra
Auto-generated module structure
algebraic_combinatorics
Auto-generated module structure
algebraic_effects
Auto-generated module structure
algebraic_geometry
Auto-generated module structure
algebraic_number_theory
Auto-generated module structure
algebraic_topology
Auto-generated module structure
analytic_number_theory
Auto-generated module structure
approximation_algorithms
Auto-generated module structure
arithmetic_geometry
Auto-generated module structure
array
Auto-generated module structure
automata_theory
Auto-generated module structure
bayesian_networks
Auto-generated module structure
bioinformatics
Auto-generated module structure
birational_geometry
Auto-generated module structure
bitvec
Auto-generated module structure
bool
Auto-generated module structure
categorical_logic
Auto-generated module structure
category_theory
Auto-generated module structure
category_theory_ext
Auto-generated module structure
certified_algorithms
Auto-generated module structure
chaos_theory
Auto-generated module structure
char
Auto-generated module structure
chromatic_homotopy
Auto-generated module structure
coalgebra_theory
Auto-generated module structure
coding_theory
Auto-generated module structure
combinatorial_game_theory
Auto-generated module structure
combinatorial_optimization
Auto-generated module structure
combinatorics
Auto-generated module structure
compiler_theory
Auto-generated module structure
complex
Auto-generated module structure
complexity
Auto-generated module structure
computational_geometry
Auto-generated module structure
concurrency_theory
Auto-generated module structure
constructive_mathematics
Auto-generated module structure
control_theory
Auto-generated module structure
convex_analysis
Auto-generated module structure
convex_geometry
Auto-generated module structure
convex_optimization
Auto-generated module structure
cryptographic_protocols
Auto-generated module structure
cryptography
Auto-generated module structure
cubical_type_theory
Auto-generated module structure
data_structures
Auto-generated module structure
decidable
Auto-generated module structure
denotational_semantics
Auto-generated module structure
derived_algebraic_geometry
Auto-generated module structure
descriptive_set_theory
Auto-generated module structure
differential_equations
Auto-generated module structure
differential_geometry
Auto-generated module structure
differential_privacy
Auto-generated module structure
diophantine_geometry
Auto-generated module structure
distributed_systems_theory
Auto-generated module structure
domain_theory
Auto-generated module structure
either
Auto-generated module structure
elliptic_curves
Auto-generated module structure
env_builder
Auto-generated module structure
eq
Auto-generated module structure
ergodic_theory
Auto-generated module structure
fin
Auto-generated module structure
finite_element_method
Auto-generated module structure
forcing_theory
Auto-generated module structure
formal_languages
Auto-generated module structure
formal_verification
Auto-generated module structure
functional_analysis
Auto-generated module structure
functional_calculus
Auto-generated module structure
functional_programming
Auto-generated module structure
functor
Auto-generated module structure
fuzzy_logic
Auto-generated module structure
game_theory
Auto-generated module structure
game_theory_ext
Auto-generated module structure
geometric_group_theory
Auto-generated module structure
geometric_measure_theory
Auto-generated module structure
graph
Auto-generated module structure
groebner_bases
Auto-generated module structure
group_theory
Auto-generated module structure
harmonic_analysis
Auto-generated module structure
hashmap
Auto-generated module structure
hashset
Auto-generated module structure
higher_category_theory
Auto-generated module structure
homological_algebra
Auto-generated module structure
homological_computations
Auto-generated module structure
homotopy_theory
Auto-generated module structure
homotopy_type_theory
Auto-generated module structure
information_geometry
Auto-generated module structure
information_theoretic_security
Auto-generated module structure
information_theory
Auto-generated module structure
information_theory_ext
Auto-generated module structure
int
Auto-generated module structure
intersection_theory
Auto-generated module structure
io
Auto-generated module structure
iwasawa_theory
Auto-generated module structure
k_theory
Auto-generated module structure
knot_theory
Auto-generated module structure
lambda_calculus
Auto-generated module structure
lattice_theory
Auto-generated module structure
lazy
Auto-generated module structure
lie_theory
Auto-generated module structure
linear_algebra
Auto-generated module structure
linear_logic
Auto-generated module structure
linear_programming
Auto-generated module structure
list
Auto-generated module structure
logic
Auto-generated module structure
low_dimensional_topology
Auto-generated module structure
machine_learning
Auto-generated module structure
mathematical_ecology
Auto-generated module structure
mathematical_physics
Auto-generated module structure
measure_theory
Auto-generated module structure
mechanism_design
Auto-generated module structure
modal_logic
Auto-generated module structure
model_checking
Auto-generated module structure
model_theory
Auto-generated module structure
modular_forms
Auto-generated module structure
monad
Auto-generated module structure
motivic_cohomology
Auto-generated module structure
nat
Auto-generated module structure
network_theory
Auto-generated module structure
noncommutative_geometry
Auto-generated module structure
nonstandard_analysis
Auto-generated module structure
number_theory
Auto-generated module structure
numerical_analysis
Auto-generated module structure
numerical_linear_algebra
Auto-generated module structure
observational_type_theory
Auto-generated module structure
operations_research
Auto-generated module structure
operator_algebras
Auto-generated module structure
optimization_theory
Auto-generated module structure
option
Auto-generated module structure
ord
Auto-generated module structure
order
Auto-generated module structure
order_topology
Auto-generated module structure
ordering
Auto-generated module structure
padic_analysis
Auto-generated module structure
padic_hodge_theory
Auto-generated module structure
parameterized_complexity
Auto-generated module structure
parametricity
Auto-generated module structure
parsec
Auto-generated module structure
pde_theory
Auto-generated module structure
point_free_topology
Auto-generated module structure
point_set_topology
Auto-generated module structure
post_quantum_crypto
Auto-generated module structure
probabilistic_programming
Auto-generated module structure
probability
Auto-generated module structure
prod
Auto-generated module structure
program_logics
Auto-generated module structure
program_synthesis
Auto-generated module structure
proof_mining
Auto-generated module structure
proof_theory
Auto-generated module structure
prop
Auto-generated module structure
quantum_computing
Auto-generated module structure
quantum_error_correction
Auto-generated module structure
quantum_field_theory
Auto-generated module structure
quantum_information
Auto-generated module structure
quotient_types
Auto-generated module structure
random_matrix_theory
Auto-generated module structure
range
Auto-generated module structure
rbtree
Auto-generated module structure
real
Auto-generated module structure
repr
Auto-generated module structure
representation_theory
Auto-generated module structure
result
Auto-generated module structure
reverse_mathematics
Auto-generated module structure
rough_set_theory
Auto-generated module structure
session_types
Auto-generated module structure
set
Auto-generated module structure
set_theory_zfc
Auto-generated module structure
sheaf_theory
Auto-generated module structure
show
Auto-generated module structure
sigma
Auto-generated module structure
social_choice_theory
Auto-generated module structure
spectral_methods
Auto-generated module structure
spectral_theory
Auto-generated module structure
static_analysis
Auto-generated module structure
statistical_learning
Auto-generated module structure
statistical_mechanics
Auto-generated module structure
stochastic_control
Auto-generated module structure
stochastic_processes
Auto-generated module structure
stream
Auto-generated module structure
string
Auto-generated module structure
string_theory_basics
Auto-generated module structure
sum
Auto-generated module structure
surreal_numbers
Auto-generated module structure
symplectic_geometry
Auto-generated module structure
systems_biology
Auto-generated module structure
tactic_lemmas
Auto-generated module structure
tauberian_theory
Auto-generated module structure
temporal_logic
Auto-generated module structure
term_rewriting
Auto-generated module structure
thunk
Auto-generated module structure
topological_data_analysis
Auto-generated module structure
topological_quantum_computation
Auto-generated module structure
topology
Auto-generated module structure
topology_ext
Auto-generated module structure
topos_theory
Auto-generated module structure
tropical_geometry
Auto-generated module structure
type_inference_algorithms
Auto-generated module structure
type_theory
Auto-generated module structure
type_theory_advanced
Auto-generated module structure
universal_algebra
Auto-generated module structure
variational_analysis
Auto-generated module structure
variational_calculus
Auto-generated module structure
vec
Auto-generated module structure
wellfounded
Auto-generated module structure

Structs§

BitSet64
A fixed-size bit set backed by a single u64. Supports positions 0..63.
Counter
A monotonically increasing counter, useful for generating fresh variable IDs.
Diagnostic
A single compiler diagnostic.
DiagnosticBag
Accumulator for multiple diagnostics.
DirectedGraph
A directed graph with n nodes, represented as an adjacency list.
FreshNameGen
Generates fresh name strings of the form prefix_N.
Located
A value annotated with a Span.
MinHeap
A min-heap priority queue.
ModuleDep
A dependency pair: (dependent, dependency).
MultiMap
A simple multi-map: each key may map to multiple values.
NameTable
A simple string-interning table backed by a Vec.
ScopeTable
A scoped symbol table supporting nested scopes.
Span
Utility type for carrying source-location metadata.
StdEntry
A record of a single OxiLean standard library theorem or definition that the elaborator knows about.
StdFeatures
Feature flags for optional standard library components.
StdLibStats
Standard library module statistics.
StdModuleEntry
A registry entry describing one standard library module.
StdVersion
Version information for the OxiLean standard library.
StringSet
A set of String values backed by a sorted Vec for deterministic output.
Trie
A simple trie mapping byte strings to values.

Enums§

BuildPhase
Represents a phase in the standard library build process.
DiagnosticLevel
Severity levels for compiler diagnostics.
StdCategory
A category tag for standard library modules.

Constants§

STD_KNOWN_ENTRIES
A representative sample of well-known standard library entries.
STD_VERSION
OxiLean standard library version string.

Statics§

CORE_DEPS
Minimal dependency graph for core standard library modules.
STD_MODULE_REGISTRY
Inventory of all standard library modules.

Functions§

all_modules
Get all modules.
all_theorems
Return all theorems (non-definitions) in the standard library sample.
count_default_modules
Count how many modules are loaded by default.
count_total_modules
Count total number of registered standard library modules.
default_modules
Get all default-loaded modules.
dependents_of
Get all modules that depend on the given module.
direct_deps
Get all dependencies of a named module (direct only).
entries_in_module
Return all entries from a given module.
find_module
Look up a module entry by its qualified name.
lookup_std_entry
Look up a standard library entry by its qualified name.
module_category
Map a module name to its StdCategory.
modules_for_phase
Get all module entries for a specific build phase.
topological_sort_modules
Compute a topological ordering of modules based on CORE_DEPS.