Skip to main content

Crate oxilean_meta

Crate oxilean_meta 

Source
Expand description

§OxiLean Meta Layer — Metavar-Aware Operations & Tactics

The meta layer extends the kernel with metavariable support, providing all the infrastructure for elaboration, unification, and interactive tactic proving. It mirrors LEAN 4’s Lean.Meta namespace and sits logically between the elaborator and the trusted kernel.

§Quick Start

§Creating a Meta Context

ⓘ
use oxilean_meta::{MetaContext, MetaConfig};
use oxilean_kernel::Environment;

let env = Environment::new();
let config = MetaConfig::default();
let mut meta_ctx = MetaContext::new(&env, config);

§Creating and Solving Metavariables

ⓘ
use oxilean_meta::MVarId;

let m1 = meta_ctx.mk_metavar(ty)?;
// ... unification happens ...
let solution = meta_ctx.get_assignment(m1)?;

§Running a Tactic

ⓘ
use oxilean_meta::TacticState;

let mut state = TacticState::new(&meta_ctx, goal)?;
// ... execute tactics ...
let proof = state.close()?;

§Architecture Overview

The meta layer is organized into three functional areas:

┌──────────────────────────────────────────────────────┐
│              Meta Layer (oxilean-meta)               │
├────────────────────────────────────────────────────────┤
│                                                         │
│  ┌─────────────────┐  ┌──────────────────┐             │
│  │  Core Meta Ops  │  │  Advanced Features│             │
│  ├─────────────────┤  ├──────────────────┤             │
│  │- MetaContext    │  │- Instance Synth  │             │
│  │- MetaWhnf       │  │- Discrimination  │             │
│  │- MetaDefEq      │  │  Trees           │             │
│  │- MetaInferType  │  │- App Builder     │             │
│  │- Level DefEq    │  │- Congr Theorems  │             │
│  └─────────────────┘  └──────────────────┘             │
│                                                         │
│  ┌──────────────────────────────────────┐              │
│  │     Tactic System                    │              │
│  ├──────────────────────────────────────┤              │
│  │- intro, apply, exact, rw, simp, ... │              │
│  │- Goal & TacticState management      │              │
│  │- Calc proofs, Omega solver, etc.    │              │
│  └──────────────────────────────────────┘              │
│                                                         │
└──────────────────────────────────────────────────────────┘
                         │
                         │ uses (doesn't modify)
                         ▼
┌──────────────────────────────────────────────────────┐
│              OxiLean Kernel (TCB)                    │
│         (Expression, Type Checking, WHNF, ...)      │
└──────────────────────────────────────────────────────┘

§Key Concepts & Terminology

§MetaContext vs MetaState

  • MetaContext: Global state during a proof session

    • All metavariables and their assignments
    • Configuration (recursion depth, timeouts, etc.)
    • Doesn’t change during individual tactics

  • MetaState: Local goal-solving state

    • Current goal and subgoals
    • Local context (variables and hypotheses)
    • Changes as tactics are applied

§Goal

A proof goal represented as:

x : Nat
h : P x
⊢ Q x

Components:

  • Local context: Variables x : Nat, hypotheses h : P x
  • Type (target): What to prove Q x

Goals are solved when type is inhabited (proof term provided).

§Tactic

A tactic transforms goals:

Tactic: Goal → (Proof ∪ NewGoals ∪ Error)

Examples:

  • intro: Transform ⊢ P → Q to p : P ⊢ Q
  • exact t: If t : P, close goal ⊢ P
  • rw [eq]: Transform using equality

§Metavariable Assignment

Unification solves ?m =?= expr by assigning:

?m := expr

Subsequent references to ?m automatically get the value.

§Discrimination Tree

Fast indexing structure for term-based lookup (e.g., for simp lemmas):

  • Index by discriminator: First argument, head function, etc.
  • Retrieve candidates in O(log n) instead of O(n)

§Instance Synthesis

Automated search for typeclass instances:

  • Given [C x], find value of type C x
  • Uses tabled resolution (memoization)
  • Prevents infinite loops

§Module Organization

§Batch 4.1: Core Meta Infrastructure

ModulePurpose
basicMetaContext, MetaState, MVarId, metavariable creation
whnfWeak head normal form with metavar support
def_eqDefinitional equality and unification
infer_typeType synthesis and checking (metavar-aware)
level_def_eqUniverse level unification
discr_treeDiscrimination tree indexing for fast lookup

§Batch 4.2: Advanced Features

ModulePurpose
app_builderHelpers for building common proof terms (eq, symm, etc.)
congr_theoremsAutomatic congruence lemma generation
match_basicBasic pattern matching representation
match_dectreeDecision tree compilation for patterns
match_exhaustExhaustiveness checking
synth_instanceTypeclass instance synthesis

§Batch 4.3: Core Tactics

ModulePurpose
tacticTactic engine and state management
tactic::introintro (introduce binders)
tactic::applyapply (apply theorems)
tactic::rewriterw (rewrite by equality)
tactic::simpsimp (simplification with lemmas)
tactic::omegaomega (linear arithmetic)
tactic::calccalc (calculational proofs)

§Batch 4.4: Utilities

ModulePurpose
utilUtilities: collect_mvars, collect_fvars, FunInfo
proof_replayProof term caching and memoization
simp_engineSimplification engine and simp lemma management

§Meta Operations Pipeline

§Type Inference (Meta Version)

MetaInferType::infer_synth(expr)
  │
  ├─ Recursively infer subexpressions
  ├─ Create metavars for unknown types
  ├─ Collect unification constraints
  └─ Return: (expr_with_metavars, type)

§Unification Pipeline

MetaDefEq::unify(goal_expr, expr)
  │
  ├─ Reduce both to WHNF (with metavar support)
  ├─ Check if structurally equal
  ├─ If not, try:
  │  ├─ Variable unification: ?m := expr
  │  ├─ Application: f a =? g b
  │  │  └─ Unify: f =? g, a =? b
  │  ├─ Lambda: λ x. t =? λ y. u
  │  │  └─ Unify: t[x/?a] =? u[y/?a] (fresh ?a)
  │  └─ Higher-order cases
  ├─ Occurs check: Prevent ?m := f ?m
  └─ Return: Success or failure

§Tactic Execution

TacticState::execute(tactic)
  │
  ├─ For each goal:
  │  ├─ Apply tactic to goal
  │  ├─ If success: Add new subgoals to queue
  │  ├─ If exact: Mark goal closed
  │  └─ If failure: Backtrack or error
  │
  ├─ Recursively solve subgoals
  │
  └─ When all goals closed: Construct proof term

§Usage Examples

§Example 1: Type Inference with Metavars

ⓘ
use oxilean_meta::MetaInferType;

let mut infer = MetaInferType::new(&meta_ctx);
let (expr_with_metas, ty) = infer.infer_synth(surface_expr)?;
// expr_with_metas may contain unsolved metavars

§Example 2: Unification

ⓘ
use oxilean_meta::MetaDefEq;

let mut def_eq = MetaDefEq::new(&meta_ctx);
def_eq.unify(goal, candidate)?;
// If successful, metavars are assigned

§Example 3: Tactic Execution

ⓘ
use oxilean_meta::TacticState;

let mut state = TacticState::new(&meta_ctx, initial_goal)?;
state.intro()?;  // Run intro tactic
state.apply(theorem)?;  // Run apply tactic
let proof = state.close()?;  // Get proof term

§Example 4: Instance Synthesis

ⓘ
use oxilean_meta::InstanceSynthesizer;

let synth = InstanceSynthesizer::new(&meta_ctx);
let instance = synth.synth_instance(class_type)?;
// Returns proof that satisfies typeclass constraint

§Tactic Language

Common tactics:

  • Proof construction: intro, apply, exact, refine
  • Rewriting: rw [h], simp, simp only
  • Analysis: cases x, induction x on y, split
  • Automation: omega (linear arith), decide (decidable)
  • Control: ; (then), <|> (or), repeat, try

§Integration with Other Crates

§With oxilean-kernel

  • Uses kernel Expr, Level, Environment
  • Reads kernel operations: WHNF, type checking
  • Does not modify kernel (immutable reference)
  • Proof terms eventually passed to kernel for validation

§With oxilean-elab

  • Elaborator uses MetaContext for managing elaboration state
  • MetaDefEq/MetaWhnf for type checking during elaboration
  • Instance synthesis for implicit arguments
  • Tactic execution during proof elaboration

§Performance Optimizations

  • Memoization: Cache WHNF results for repeated reductions
  • Discrimination trees: O(log n) lookup for simp lemmas
  • Proof replay: Avoid re-executing identical tactics
  • Lazy normalization: Only normalize when needed
  • Constraint postponement: Defer hard constraints

§Further Reading

  • ARCHITECTURE.md — System architecture
  • Module documentation for specific subcomponents

Re-exports§

pub use basic::MVarId;
pub use basic::MetaConfig;
pub use basic::MetaContext;
pub use basic::MetaState;
pub use basic::MetavarDecl;
pub use basic::MetavarKind;
pub use basic::PostponedConstraint;
pub use def_eq::MetaDefEq;
pub use def_eq::UnificationResult;
pub use discr_tree::DiscrTree;
pub use discr_tree::DiscrTreeKey;
pub use infer_type::MetaInferType;
pub use level_def_eq::LevelDefEq;
pub use whnf::MetaWhnf;
pub use app_builder::mk_eq;
pub use app_builder::mk_eq_refl;
pub use app_builder::mk_eq_symm;
pub use app_builder::mk_eq_trans;
pub use congr_theorems::CongrArgKind;
pub use congr_theorems::MetaCongrTheorem;
pub use match_basic::MetaMatchArm;
pub use match_basic::MetaMatchExpr;
pub use match_basic::MetaPattern;
pub use match_dectree::DecisionBranch;
pub use match_dectree::DecisionTree;
pub use match_dectree::MatchEquation;
pub use match_exhaust::ConstructorSpec;
pub use match_exhaust::ExhaustivenessResult;
pub use synth_instance::InstanceEntry;
pub use synth_instance::InstanceSynthesizer;
pub use synth_instance::SynthResult;
pub use tactic::rewrite::RewriteDirection;
pub use tactic::GoalView;
pub use tactic::TacticError;
pub use tactic::TacticResult;
pub use tactic::TacticState;
pub use tactic::calc::CalcProof;
pub use tactic::calc::CalcStep;
pub use tactic::calc::ConvSide;
pub use tactic::omega::LinearConstraint;
pub use tactic::omega::LinearExpr;
pub use tactic::omega::OmegaResult;
pub use tactic::simp::discharge::DischargeStrategy;
pub use tactic::simp::types::default_simp_lemmas;
pub use tactic::simp::types::SimpConfig;
pub use tactic::simp::types::SimpLemma;
pub use tactic::simp::types::SimpResult;
pub use tactic::simp::types::SimpTheorems;
pub use util::collect_fvars;
pub use util::collect_mvars;
pub use util::FunInfo;

Modules§

app_builder
Auto-generated module structure
ast_cache
Auto-generated module structure
basic
Auto-generated module structure
congr_theorems
Auto-generated module structure
convenience
Auto-generated module structure
def_eq
Auto-generated module structure
discr_tree
Auto-generated module structure
infer_type
Auto-generated module structure
level_def_eq
Auto-generated module structure
match_basic
Auto-generated module structure
match_dectree
Auto-generated module structure
match_exhaust
Auto-generated module structure
meta_debug
Auto-generated module structure
proof_replay
Auto-generated module structure
prop_test
Auto-generated module structure
simp_engine
Auto-generated module structure
synth_instance
Auto-generated module structure
tactic
Tactic framework for interactive proof construction.
util
Auto-generated module structure
whnf
Auto-generated module structure

Structs§

LibAnalysisPass
An analysis pass for Lib.
LibConfig
A configuration store for Lib.
LibDiagnostics
A diagnostic reporter for Lib.
LibDiff
A diff for Lib analysis results.
LibExtConfig1300
LibExtDiag1300
LibExtDiff1300
LibExtPass1300
LibExtPipeline1300
LibPipeline
A pipeline of Lib analysis passes.
MetaCache
A simple cache for memoizing meta computations.
MetaFeatures
Feature flags for the meta layer.
MetaLibBuilder
A builder pattern for MetaLib.
MetaLibCounterMap
A counter map for MetaLib frequency analysis.
MetaLibExtMap
An extended map for MetaLib keys to values.
MetaLibExtUtil
An extended utility type for MetaLib.
MetaLibStateMachine
A state machine controller for MetaLib.
MetaLibWindow
A sliding window accumulator for MetaLib.
MetaLibWorkQueue
A work queue for MetaLib items.
MetaStats
Summary statistics about a MetaContext.
PerfStats
Simple accumulator for meta-layer performance statistics.
ProofStateReport
Report of proof state completeness.
ScoredCandidate
A scored candidate.
TacticGroup
A named group of related tactics.
TacticRegistry
A named tactic registry.

Enums§

LibConfigValue
A typed slot for Lib configuration.
LibExtConfigVal1300
LibExtResult1300
LibResult
A result type for Lib analysis.
MetaLibState
A state machine for MetaLib.

Constants§

META_VERSION
Version of the meta layer.

Functions§

collect_meta_stats
Collect statistics from a MetaContext.
default_tactic_registry
Build a default tactic registry.
is_automation_tactic
Check if a tactic is an automation tactic.
is_core_tactic
Check if a tactic name is a core tactic.
meta_version_str
Return the meta layer version string.
mk_test_ctx
Helper to create a minimal MetaContext for testing.
sort_candidates
Sort candidates by descending score.
standard_tactic_groups
Return the standard tactic groups.
tactic_description
Describe a tactic’s purpose.
tactic_group_for
Find the group that a tactic belongs to.