Wolfram Cloud Resource Object

Paclet Resource

WolframInstitute/TypeTheory

A proof engine for the Calculus of Inductive Constructions, written in the Wolfram Language

Contributed By: Nik Murzin

TypeTheoryTerm writes terms; TypeOf, TypeTheoryCheck, WeakHeadNormalForm and DefinitionallyEqualQ check and compute them. TypeTheoryEnvironment builds environments from the declarations TypeTheoryAxiom, TypeTheoryDefinition, TypeTheoryTheorem, TypeTheoryInductiveType and TypeTheoryNaturalNumbers. TypeTheoryProof and TypeTheoryTactic prove theorems interactively. TypeUniverse, ImpredicativeMaximum and InductiveRecursor are part of the term language, and TrueIntroduction, AndIntroduction, EqualityReflexivity, EqualityCongruence and the other constants of the prelude are proofs to build on.

Installation Instructions

To install this paclet in your Wolfram Language environment, evaluate this code:
PacletInstall[ResourceObject["https://wolfr.am/1I8wGKYz5"]]


To load the code after installation, evaluate this code:
Needs["WolframInstitute`TypeTheory`"]

Details

TypeTheory is a proof engine for the Calculus of Inductive Constructions, the dependent type theory of Lean and Rocq, written entirely in the Wolfram Language, with no native library and no dependency on Lean.
Terms are ordinary expressions built from built-in symbols - Function, Typed, ForAll, Implies, Equal, Plus - held in a TypeTheoryTerm, which displays them in mathematical notation.
Declarations are inert constructors - TypeTheoryAxiom, TypeTheoryDefinition, TypeTheoryTheorem, TypeTheoryInductiveType and TypeTheoryNaturalNumbers - that a small kernel checks when they are added to a TypeTheoryEnvironment. There is no global state: an environment is a value, a handle to a store of definitions, and every term and proof carries the environment it lives in, the prelude unless it names another.
The kernel infers types, reduces terms, decides definitional equality (with eta for functions and structures, and proof irrelevance), checks inductive families for strict positivity and universe constraints, and generates their recursors.
TypeTheoryProof and TypeTheoryTactic build proofs step by step. Nothing a tactic does is trusted: the kernel checks the finished proof term.
The prelude has logic (True, False, Not, And, Or, Exists), equality (Equal) and the natural numbers (NonNegativeIntegers, with Plus), so that literals are natural numbers. It is the environment of every term, proof and list of declarations that names none.
Terms display as mathematics: ∀, ∃, ↦, ⇒, ∧, ∨, ¬, universes as Prop, Type and Sort, and the natural numbers as 0 and n + 1, as Lean shows them.

Paclet Guide

Examples

Disclosures

  • Wolfram Language built-in symbols

Paclet Source

Source Metadata

  • Citation: Thierry Coquand, Gérard Huet, *The Calculus of Constructions*, Information and Computation 76, 1988, Christine Paulin-Mohring, *Inductive Definitions in the System Coq: Rules and Properties*, TLCA 1993, Mario Carneiro, *The Type Theory of Lean*, Master's thesis, Carnegie Mellon University, 2019