Abstract
Features
Art & Science
Chistine combines the simplicity of Frank and the power of Tactical Equational Reasoning. It constitutes the core of the type checker and tactic language of the Coq (Rocq) theorem proover.
Correct and Canonical
Unlike Hindley-Milner and other strongly typed non-consistent languages Christine remains Sound, Complete, Canonical, Total, Consistent, Decidable, and Conservative.
Runtime Extraction
Ready for production code extraction for Erlang/OTP and AtomVM (GRiSP).
Intro
Syntax
type term =
| Var of name
| Universe of level
| Pi of name * term * term
| Lam of name * term * term
| App of term * term
| Inductive of inductive
| Constr of int * inductive * term list
| Elim of inductive * term * term list * term
| Fixpoint of term * term * term * term (* Fixpoint n d b a *)
type inductive = {
name : string;
params : (name * term) list;
level : level;
constrs : (int * term) list
}
type goal = {
ctx : context; (* Current context *)
target : term; (* Type to prove *)
id : int; (* Goal identifier *)
}
type proof_state = {
goals : goal list; (* List of open goals *)
solved : (int * term) list; (* Solved goals with their terms *)
}
let initial_state target = {
goals = [{ ctx = empty_ctx; target; id = 1 }];
solved = [];
}
type tactic =
| Intro of name (* Introduce a variable *)
| Elim of term (* Case analysis *)
| Apply of term (* Apply a term or hypothesis *)
| Assumption (* Use a hypothesis from context *)
| Auto (* Simple automation *)
| Exact of term (* Provide an exact term *)
Semantics
Syntactic Equality
The function equal implements judgmental equality with substitution to handle bound variables, avoiding explicit α-conversion by assuming fresh names (a simplification over full de Bruijn indices [3]). The recursive descent ensures congruence, but lacks normalization, making it weaker than CIC’s definitional equality, which includes β-reduction.
Terminal Cases: Variables `Var x` are equal if names match; universes `Universe i` if levels are identical. Resursive Cases: `App (f, arg)` requires equality of function and argument. `Pi (x, a, b)` compares domains and codomains, adjusting for variable renaming via substitution. `Inductive d` checks name, level, and parameters. `Constr` and `Elim` compare indices, definitions, and arguments/cases. Default: Returns false for mismatched constructors.
Theorem 1. Equality is reflexive, symmetric, and transitive modulo α-equivalence (cf. [1], Section 2). For `Pi (x, a, b)` and `Pi (y, a', b')`, equality holds if `a = a'` and `b[x := Var x] = b'[y := Var x]`, ensuring capture-avoiding substitution preserves meaning. ∎
Context Variables Lookup
The function lookup_var retrieves a variable’s type from the context. Context are the objects in the Substitutions categories. Searches `ctx` for `(x, ty)` using `List.assoc`. Returns `Some ty` if found, `None` otherwise.
Theorem 2: Context lookup is well-defined under uniqueness of names (cf. [1], Section 3). If `ctx = Γ, x : A, Δ`, then `lookup_var ctx x = Some A`. ∎
Substitution Calculus
The function subst substitute term `s` for variable `x` in term `t`. Substitutions are morphisms in Substitution categorties.
The capture-avoiding check `if x = y` prevents variable capture but assumes distinct bound names, a simplification over full renaming or de Bruijn indices. For Elim, substituting in the motive and cases ensures recursive definitions remain sound, aligning with CIC’s eliminator semantics. Var: Replaces `x` with `s`, leaves others unchanged. Pi/Lam: Skips substitution if bound variable shadows `x`, else recurses on domain and body. App/Constr/Elim: Recurses on subterms. Inductive: No substitution (assumes no free variables).
Theorem 3. Substitution preserves typing (cf. [13], Lemma 2.1). If `Γ ⊢ t : T` and `Γ ⊢ s : A`, then `Γ ⊢ t[x := s] : T[x := s]` under suitable conditions on x. ∎
Inductive Instantiation
The function apply_inductive instantiates an inductive type’s constructors with parameters, used only in infer_Ind.
This function ensures type-level parametricity, critical for polymorphic inductives like List A. The fold-based substitution avoids explicit recursion, leveraging OCaml’s functional style, but assumes args are well-typed, deferring validation to infer. 1) Validates argument count against d.params. 2) Substitutes each parameter into constructor types using subst_param.
Theorem 4. Parameter application preserves inductiveness (cf. [4], Section 4). If D is an inductive type with parameters P, then D[P] is well-formed with substituted constructors. ∎
Context Variables Lookup
The function infer_ctor validates constructor arguments against its type.
This function implements the dependent application rule for constructors, ensuring each argument satisfies the constructor’s domain type in sequence. The recursive descent mirrors the structure of Pi types, where ty is peeled layer by the layer, and subst x arg b updates the type for the next argument. 1) Recursively matches ty (a Pi chain) with args, checking each argument and substituting. 2) Returns the final type when all arguments are consumed.
Theorem 5. Constructor typing is preserved (cf. [1], Section 4, Application Rule; [1], Section 4.3). If ctx ⊢ c : Π (x:A), B and ctx ⊢ a : A, then ctx ⊢ c a : B[x := a]. ∎
Infer General Induction
The function infer_Ind type-checks an dependent elimination (induction principle) over inductive type d.
This function implements the dependent elimination rule of CIC, generalizing both computation (e.g., plus : Nat → Nat → Nat) and proof (e.g., nat_elim : Πx:Nat.Type0). The check equal env ctx t_ty a ensures the motive’s domain aligns with the target, while compute_case_type constructs the induction principle by injecting App (p, var) as the hypothesis type for recursive occurrences, mirroring the fixpoint-style eliminators of CIC [1]. The flexibility in result_ty avoids hardcoding it to D, supporting higher-type motives (e.g., Type0).
Theorem 6. Elimination preserves typing (cf. [1], Section 4.5; Elimination Rule for Inductive Types). For an inductive type D with constructors c_j, if ctx ⊢ t : D and ctx ⊢ P : D → Type_i, and each case case_j has type Πx:A_j.P(c_j x) where A_j are the argument types of c_j (including recursive hypotheses), then ctx ⊢ Ind(D, P, cases, t) : P t. ∎
Infer Equality Induction
The function infer_J ensures `J (ty, a, b, c, d, p)` has type `c a b p by` validating the motive, base case, and path against CIC’s equality elimination rule.
The `infer_J` function implements the dependent elimination rule for identity types in the Calculus of Inductive Constructions (CIC), enabling proofs and computations over equality (e.g., `symmetry : Π a b : ty, Π p : Id (ty, a, b), Id(ty, b, a)`). It type-checks the term `J (ty, a, b, c, d, p)` by ensuring `ty : Universe 0` is the underlying type, `a : ty` and `b : ty` are endpoints, `c : Π (x:ty), Π (y:ty), Π (p: Id(ty, x, y)), Type0` is a motive over all paths, `d : Π (x:ty), c x x (Refl x)` handles the reflexive case, and `p : Id(ty, a, b)` is the path being eliminated. The function constructs fresh variables to define the motive and base case types, checks each component, and returns `c a b p` (normalized), reflecting the result of applying the motive to the specific path.
Theorem 7. For an environment `env` and context `ctx`, given a type `A : Type_i`, terms `a : A`, `b : A`, a motive `C : Π (x:A), Π (y:A), Π(p:Id(A, x, y)),Type_j`, a base case `d : Π(x:A), C x x (Refl x)`, and a path `p : Id(A, a, b)`, the term `J (A, a, b, C, d, p)` is well-typed with type `C a b p`. (Reference: CIC [1], Section 4.5; Identity Type Elimination Rule). ∎
Type Inference
The function infer infers the type of term t in context ctx and environment env.
For Pi and Lam, universe levels ensure consistency (e.g., Type i : Type (i + 1)), while Elim handles induction, critical for dependent elimination. Note that lambda agrument should be typed for easier type synthesis [13].
Theorem 8. Type inferense is sound. For any environment env, context ctx, and well-formed term t, if the function infer env ctx t returns Some T, then ctx ⊢ t : T holds in the present type theory. Moreover, if infer env ctx t = None, then there is no type T such that ctx ⊢ t : T is derivable (modulo the limitations coming from the syntactic equality algorithm and the absence of full η-reduction, η-expansion or judgmental η-equality. ∎
Check Universes
The function check_universe ensures t is a universe, returning its level. Infers type of t, expects Universe i.
This auxiliary enforces universe hierarchy, preventing paradoxes (e.g., Type : Type). It relies on infer, assuming its correctness, and throws errors for non-universe types, aligning with ITT’s stratification.
Theorem 9: Universe checking is decidable (cf. [13]). If ctx ⊢ t : Universe i, then check_universe env ctx t = i. ∎
Check
The function check checks that t has type ty: 1) Lam: Ensures the domain is a type, extends the context, and checks the body against the codomain. 2) Constr: Infers the constructor’s type and matches it to the expected inductive type. 3) Elim: Computes the elimination type via check_elim and verifies it equals ty. 4) Default: Infers t’s type, normalizes ty, and checks equality.
The function leverages bidirectional typing: specific cases (e.g., Lam) check directly, while the default case synthesizes via infer and compares with a normalized ty, ensuring definitional equality (β-reduction). Completeness hinges on normalize terminating (ITT’s strong normalization) and equal capturing judgmental equality.
Theorem 10. Type checking is complete (cf. [1], Normalization). If ctx ⊢ t : T in the type theory, then check env ctx t T succeeds, assuming normalization and sound inference. ∎
Branch Evaluation
The function apply_case applies a case branch to constructor arguments, used only in reduce.
This function realizes CIC’s ι-reduction for inductive eliminators [1], where a case branch is applied to constructor arguments, including recursive hypotheses. For Nat’s succ in plus, ty = Πn:Nat.Nat, case = λk.λih.succ ih, and args = [n]. The recursive check a = Inductive d triggers for n : Nat, computing ih = Elim(Nat, Π_:Nat.Nat, [m; λk.λih.succ ih], n), ensuring succ ih : Nat. The nested apply_term handles multi-argument lambdas (e.g., k and ih), avoiding explicit uncurrying, while substitution preserves typing per CIC’s rules.
Theorem 11. Case application is sound (cf. [1] Elimination Typing). If case : Πx:A.P(c x) and args match A, then apply_case env ctx d p cases case ty args yields a term of type P(c args). ∎
One-step β-reductor
The function reduce performs one-step β-reduction or inductive elimination.
The function implements a one-step reduction strategy combining ITT’s β-reduction with CIC’s ι-reduction for inductives. The App (Lam, arg) case directly applies substitution, while Elim (Constr) uses apply_case to handle induction, ensuring recursive calls preserve typing via the motive p. The Pi case, though unconventional, supports type-level computation, consistent with CIC’s flexibility: 1) App (Lam, arg): Substitutes arg into the lambda body (β-reduction). 2) App (Pi, arg): Substitutes arg into the codomain (type-level β-reduction). 3) App (f, arg): Reduces f, then arg if f is unchanged. 4) Elim (d, p, cases, Constr): Applies the appropriate case to constructor arguments, computing recursive calls (ι-reduction). 5) Elim (d, p, cases, t'): Reduces the target t'. 6) Constr: Reduces arguments. 7) Default: Returns unchanged.
Theorem 12. Reduction preserves typing (cf. [8], Normalization Lemma, Subject Reduction). If ctx ⊢ t : T and t → t' via β-reduction or inductive elimination, then ctx ⊢ t' : T. ∎
Normalization
The function normalize reduces a term t to its normal form by iteratively applying one-step reductions via reduce until no further changes occur, ensuring termination for well-typed terms.
This function implements strong normalization, a cornerstone of MLTT [9] and CIC [1], where all reduction sequences terminate. The fixpoint iteration relies on reduce’s one-step reductions (β for lambdas, ι for inductives), with equal acting as the termination oracle. For plus 2 2, it steps to succ succ succ succ zero, terminating at a constructor form.
Theorem 13. Normalization terminates (cf. [1]. Strong Normalization via CIC). Every well-typed term in the system has a ormal form under β- and ι-reductions. ∎
