DTT and its Specific Variant for Lean
Dependent type theory (DTT) allows you to express complex mathematical assertions and reason about them in a "natural and uniform" way.
Lean is based on a version of DTT called the Calculus of Constructions, with a "countable hierarchy of non-cumulative inverses and inductive types". This sounds complex.
The following section explains this.
First, let's talk Simple Type Theory
In "type theory" every expression has a specific type. e.g. the expression x+0 may denote a natural number in a specific context. In another context, it may be a floating point number, of a particular precision.
In Lean, a natural number is an arbitrary precision unsigned integer.
Our use of the arbitrary precision (unsigned) integer, reflects the unnatural way of thinking about counting numbers from a computing perspective. In computing, we think of the object, but also the memory it occupies - so we speak of 16 bit integers, 32 bit integers and so on - a nod to the physical limitations of computers. n-bit integers where n is not predefined underlies this concept of arbitrary precision.
An arbitrary-precision integer can grow to any number of bits, limited only by available memory.
This differs from so-called fixed-width integers (8-, 32-, 64- bit).
A variable-length array of digits/bits are used so it can represent arbitrarily large integers without overflow. (Analogies include - BigInt in Java, or System.Numerics.BigInteger in C#).
Defining Contants in Lean with the def keyword
Let's define some constants in Lean.
/- Define some constants. -/
def m: Nat := 1 --m is a natural number
def n : Nat := 0
def b1: Bool := true --b1 is a Boolean
def b2: Bool := false
Now check their types using: #check m; #check n; #check n+0 etc. You can also run some "evals" in Lean: #eval 5*4; #eval m+2 etc.
The def keyword introduces new constant symbols to the working environment. The #check command asks Lean to report their types. The #eval command asks Lean to evaluate the given expression.
Composing New Types from Existing Ones
What makes simple type theory powerful is you can build new types out of others.
For example, if a and b are types, a->b denote the type of functions from a to b, a × b denotes the type of pairs consisting of an element of type a and element of type b.
Note on use of Unicode: (From the Lean Manual): "The judicious use of Unicode improves legibility, and all modern editors have great support for it. In the Lean standard library, you often see Greek letters to denote types, and the Unicode symbol → as a more compact version of ->."
