Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
TypeTheoryToLean  |
|
| | ||||
|
| | ||||
▪
The declarations are read back from the environment exactly and written with every application explicit () and every universe level given, so Lean fills in nothing.
@fab
▪
A constant that came from Lean, through , keeps its Lean name and is not declared again.
▪
TypeTheory's prelude constants that Lean has in are written as Lean's: is , is , is , is , is , and their constructors and recursors likewise; the Booleans' constants , , , and are , , , and , with the same definitions. becomes , which computes the same on constructors, so a proof that does not depend on how is defined checks in Lean too.
Init
NonNegativeIntegers
Nat
Equal
Eq
And
And
Equivalent
Iff
Booleans
Bool
"true"
"false"
"not"
"and"
"or"
Bool.true
Bool.false
Bool.not
Bool.and
Bool.or
Plus
Nat.add
Plus
▪
The prelude's axioms are Lean's: is , is and is , so a classical proof depends on Lean's own axioms and declares none.
PropositionalExtensionality
propext
FunctionExtensionality
funext
Choice
Classical.choice
▪
Every other constant is declared under the namespace , as an , a , a or an ; a block of mutually inductive types is written as Lean's block.
TypeTheory
axiom
noncomputabledef
theorem
inductive
mutual
▪
Compiling the source with has Lean's kernel check every declaration, independently of TypeTheory's.
▪
Lean's kernel follows the calculus of inductive constructions, the rules of TypeTheory's prelude. An environment whose rules have no Prop, such as TypeTheory's HoTT environment, or that has rewrite rules other than the quotient rules adds, which are Lean's own, gives .
Failure["UnsupportedRules",...]
Examples
(5)
Basic Examples
(1)
Prove by induction in TypeTheory:
0+n==n
In[1]:=
proof=TypeTheoryProof[ForAll[{Typed[n,NonNegativeIntegers]},0+nn],{TypeTheoryTactic["Introduce",n],TypeTheoryTactic["Induction",n],TypeTheoryTactic["Reflexivity"],TypeTheoryTactic["Introduce",k,ih],TypeTheoryTactic["Exact",EqualityCongruence[NaturalNumberSuccessor,ih]]}]
Out[1]=
A theorem with that proof, added to the prelude:
In[2]:=
proved=TypeTheoryEnvironment[{TypeTheoryTheorem[ZeroLeftIdentity,proof]}]
Out[2]=
TypeTheoryEnvironment
 |
|
Write the theorem as Lean source:
In[3]:=
source=
[proved,ZeroLeftIdentity]
 | TypeTheoryToLean |
Out[3]=
-- Generated by LeanLink's TypeTheoryToLean: TypeTheory declarations, for Lean's kernel to check.theorem TypeTheory.EqualityCongruence.{u, v} : ({α : Sort u} -> {β : Sort v} -> {x : α} -> {y : α} -> (f : (α -> β)) -> ((@Eq.{u} α x y) -> (@Eq.{v} β (f x) (f y)))) := (@fun {α : Sort u} {β : Sort v} {x : α} {y : α} (f : (α -> β)) (h : (@Eq.{u} α x y)) => (@Eq.rec.{0, u} α x (@fun (z : α) (e : (@Eq.{u} α x z)) => (@Eq.{v} β (f x) (f z))) (@Eq.refl.{v} β (f x)) y h))theorem TypeTheory.ZeroLeftIdentity : ((n : @Nat) -> (@Eq.{1} @Nat (@Nat.add (0 : Nat) n) n)) := (@fun (n : @Nat) => (@Nat.rec.{0} (@fun (n1 : @Nat) => (@Eq.{1} @Nat (@Nat.add (0 : Nat) n1) n1)) (@Eq.refl.{1} @Nat (@Nat.add (0 : Nat) @Nat.zero)) (@fun (k : @Nat) (ih : (@Eq.{1} @Nat (@Nat.add (0 : Nat) k) k)) => (@TypeTheory.EqualityCongruence.{1, 1} @Nat @Nat (@Nat.add (0 : Nat) k) k @Nat.succ ih)) n))
Lean compiles it, and its kernel accepts the proof:
In[4]:=
leanEnv=
[source]
| LeanImportString |
Out[4]=
LeanEnvironment
|
|
The theorem, as Lean states it:
In[5]:=
leanEnv["TypeTheory.ZeroLeftIdentity"]["TypeForm"]
Out[5]=
∀ (n : Nat), Nat.add 0 n = n
Scope
(2)
Possible Issues
(2)
 |
|
 |
|
""