Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanToTypeTheory  |
|
| | ||||
|
| | ||||
| | |||||
▪
TypeTheory is a Calculus of Inductive Constructions kernel written in the Wolfram Language. gives the result of checking the import with it, independently of Lean's kernel: a , or a naming the Lean constant TypeTheory rejects.
▪
The constants are taken in dependency order. An inductive type comes with its constructors; its recursor is generated by TypeTheory as , and then compared with Lean's: a recursor whose type differs gives a .
X.rec
InductiveRecursor["X"]
"RecursorMismatch"
▪
Lean names stay strings, so the imported theorem is the constant of the TypeTheory environment, and Lean's becomes its natural numbers, so literals mean the same.
"Nat.zero_add"
"Nat.zero_add"
Nat
▪
Every term is imported as a core term of TypeTheory, with every argument and every universe level given, so nothing is filled in again on the TypeTheory side. A subterm that occurs many times, as in a proof that a tactic such as writes, is imported once and shared, as Lean shares it.
omega
▪
The option gives a to import into; constants it already declares are not imported again.
"Environment"
▪
A block of mutually inductive types is imported as one declaration of all its types, and a type nested in a container, as Lean's syntax trees are in , as itself: TypeTheory checks the nesting as Lean's kernel does. Every recursor of the block, on a container included as , is compared with Lean's.
Array
X.rec_k
InductiveRecursor["X",k]
▪
A string literal is written as Lean's kernel reads it: applied to the list of its characters, each of its code point.
String.ofList
Char.ofNat
▪
The operations Lean's kernel computes on literals with GMP, , , , , and the others, are registered with TypeTheory as they are imported, so it computes them on literals with integers too, and a proof about numbers near 2^64 checks at once.
Nat.add
Nat.mul
Nat.pow
Nat.div
Nat.ble
▪
Lean's quotient types, , , and , are TypeTheory's own: the import declares them at once with , and TypeTheory's kernel computes a lift on a class as Lean's does. Under rules without quotients, given with the option , and with a TypeTheory before 0.13, they are axioms, and the import adds their computation as the rewrite rules and where the rules allow rewrite rules.
Quot
Quot.mk
Quot.lift
Quot.ind
TypeTheoryQuotients["Eq",{"Quot","Quot.mk","Quot.lift","Quot.ind"}]
"Environment"
"Quot.lift computes"
"Quot.ind computes"
▪
The first call loads the paclet , which must be installed.
WolframInstitute/TypeTheory
Examples
(6)
Basic Examples
(1)
A Lean theorem, compiled from source:
In[1]:=
lean=
["theorem probe (n : Nat) : 0 + n = n := Nat.zero_add n"]
 | LeanImportString |
Out[1]=
LeanEnvironment
 |
|
Import with what it depends on:
Eq.symm
In[2]:=
env=
[lean,"Eq.symm"]
| LeanToTypeTheory |
Out[2]=
TypeTheoryEnvironment
|
|
The constants TypeTheory checked:
In[3]:=
Keys[env]
Out[3]=
{Eq,Eq.refl,InductiveRecursor[Eq],rfl,Eq.symm}
The imported theorem, read back in TypeTheory:
In[4]:=
env["Eq.symm"]
Out[4]=
theorem | Eq.symm | : | ∀ {α:Sortu} ∀ {a:α} ∀ {b:α} |
Scope
(5)
 |
|
 |
|
 |
|
""