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;
pub use functions::collect_meta_stats;
pub use functions::default_tactic_registry;
pub use functions::is_automation_tactic;
pub use functions::is_core_tactic;
pub use functions::meta_version_str;
pub use functions::mk_test_ctx;
pub use functions::sort_candidates;
pub use functions::standard_tactic_groups;
pub use functions::tactic_description;
pub use functions::tactic_group_for;
pub use functions::META_VERSION;
pub use types::LibAnalysisPass;
pub use types::LibConfig;
pub use types::LibConfigValue;
pub use types::LibDiagnostics;
pub use types::LibDiff;
pub use types::LibExtConfig1300;
pub use types::LibExtConfigVal1300;
pub use types::LibExtDiag1300;
pub use types::LibExtDiff1300;
pub use types::LibExtPass1300;
pub use types::LibExtPipeline1300;
pub use types::LibExtResult1300;
pub use types::LibPipeline;
pub use types::LibResult;
pub use types::MetaCache;
pub use types::MetaFeatures;
pub use types::MetaLibBuilder;
pub use types::MetaLibCounterMap;
pub use types::MetaLibExtMap;
pub use types::MetaLibExtUtil;
pub use types::MetaLibState;
pub use types::MetaLibStateMachine;
pub use types::MetaLibWindow;
pub use types::MetaLibWorkQueue;
pub use types::MetaStats;
pub use types::PerfStats;
pub use types::ProofStateReport;
pub use types::ScoredCandidate;
pub use types::TacticGroup;
pub use types::TacticRegistry;

Modules§

app_builder
Auto-generated module structure
ast_cache
Auto-generated module structure
basic
Auto-generated module structure
coercion_system
Coercion system — automatic type coercion (casting) infrastructure.
congr_theorems
Auto-generated module structure
convenience
Auto-generated module structure
def_eq
Auto-generated module structure
discr_tree
Auto-generated module structure
elaboration_hooks
Elaboration hooks — callbacks that run at key points during elaboration.
functions
Auto-generated module
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.
tactic_reflection
Tactic reflection — inspect and construct tactic expressions at meta-level.
tc_synthesis
Type class instance synthesis module.
types
Auto-generated module
util
Auto-generated module structure
whnf
Auto-generated module structure