What is Lean

Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.

Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.

-- Defines a function that takes a name and produces a greeting.
def getGreeting (name : String) := s!"Hello, {name}! Isn't Lean great?"

-- The `main` function is the entry point of your program.
-- Its type is `IO Unit` because it can perform `IO` operations (side effects).
def main : IO Unit :=
  -- Define a list of names
  let names := ["Sebastian", "Leo", "Daniel"]

  -- Map each name to a greeting
  let greetings := names.map getGreeting

  -- Print the list of greetings
  for greeting in greetings do
    IO.println greeting

Lean has numerous features, including:

Tour of Lean

The best way to learn about Lean is to read and write Lean code. This article will act as a tour through some of the key features of the Lean language and give you some code snippets that you can execute on your machine. To learn about setting up a development environment, check out Setting Up Lean.

There are two primary concepts in Lean: functions and types. This tour will emphasize features of the language which fall into these two concepts.

Functions and Namespaces

The most fundamental pieces of any Lean program are functions organized into namespaces. Functions perform work on inputs to produce outputs, and they are organized under namespaces, which are the primary way you group things in Lean. They are defined using the def command, which give the function a name and define its arguments.

namespace BasicFunctions

-- The `#eval` command evaluates an expression on the fly and prints the result.
#eval 2+2

-- You use 'def' to define a function. This one accepts a natural number
-- and returns a natural number.
-- Parentheses are optional for function arguments, except for when
-- you use an explicit type annotation.
-- Lean can often infer the type of the function's arguments.
def sampleFunction1 x := x*x + 3

-- Apply the function, naming the function return result using 'def'.
-- The variable type is inferred from the function return type.
def result1 := sampleFunction1 4573

-- This line uses an interpolated string to print the result. Expressions inside
-- braces `{}` are converted into strings using the polymorphic method `toString`
#eval println! "The result of squaring the integer 4573 and adding 3 is {result1}"

-- When needed, annotate the type of a parameter name using '(argument : type)'.
def sampleFunction2 (x : Nat) := 2*x*x - x + 3

def result2 := sampleFunction2 (7 + 4)

#eval println! "The result of applying the 2nd sample function to (7 + 4) is {result2}"

-- Conditionals use if/then/else
def sampleFunction3 (x : Int) :=
  if x > 100 then
    2*x*x - x + 3
  else
    2*x*x + x - 37

#eval println! "The result of applying sampleFunction3 to 2 is {sampleFunction3 2}"

end BasicFunctions

-- Lean has first-class functions.
-- `twice` takes two arguments `f` and `a` where
-- `f` is a function from natural numbers to natural numbers, and
-- `a` is a natural number.
def twice (f : Nat → Nat) (a : Nat) :=
  f (f a)

-- `fun` is used to declare anonymous functions
#eval twice (fun x => x + 2) 10

-- You can prove theorems about your functions.
-- The following theorem states that for any natural number `a`,
-- adding 2 twice produces a value equal to `a + 4`.
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
  -- The proof is by reflexivity. Lean "symbolically" reduces both sides of the equality
  -- until they are identical.
  rfl

-- `(· + 2)` is syntax sugar for `(fun x => x + 2)`. The parentheses + `·` notation
-- is useful for defining simple anonymous functions.
#eval twice (· + 2) 10

-- Enumerated types are a special case of inductive types in Lean,
-- which we will learn about later.
-- The following command creates a new type `Weekday`.
inductive Weekday where
  | sunday    : Weekday
  | monday    : Weekday
  | tuesday   : Weekday
  | wednesday : Weekday
  | thursday  : Weekday
  | friday    : Weekday
  | saturday  : Weekday

-- `Weekday` has 7 constructors/elements.
-- The constructors live in the `Weekday` namespace.
-- Think of `sunday`, `monday`, …, `saturday` as being distinct elements of `Weekday`,
-- with no other distinguishing properties.
-- The command `#check` prints the type of a term in Lean.
#check Weekday.sunday
#check Weekday.monday

-- The `open` command opens a namespace, making all declarations in it accessible without
-- qualification.
open Weekday
#check sunday
#check tuesday

-- You can define functions by pattern matching.
-- The following function converts a `Weekday` into a natural number.
def natOfWeekday (d : Weekday) : Nat :=
  match d with
  | sunday    => 1
  | monday    => 2
  | tuesday   => 3
  | wednesday => 4
  | thursday  => 5
  | friday    => 6
  | saturday  => 7

#eval natOfWeekday tuesday

def isMonday : Weekday → Bool :=
  -- `fun` + `match`  is a common idiom.
  -- The following expression is syntax sugar for
  -- `fun d => match d with | monday => true | _ => false`.
  fun
    | monday => true
    | _      => false

#eval isMonday monday
#eval isMonday sunday

-- Lean has support for type classes and polymorphic methods.
-- The `toString` method converts a value into a `String`.
#eval toString 10
#eval toString (10, 20)

-- The method `toString` converts values of any type that implements
-- the class `ToString`.
-- You can implement instances of `ToString` for your own types.
instance : ToString Weekday where
  toString (d : Weekday) : String :=
    match d with
    | sunday    => "Sunday"
    | monday    => "Monday"
    | tuesday   => "Tuesday"
    | wednesday => "Wednesday"
    | thursday  => "Thursday"
    | friday    => "Friday"
    | saturday  => "Saturday"

#eval toString (sunday, 10)

def Weekday.next (d : Weekday) : Weekday :=
  match d with
  | sunday    => monday
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday

#eval Weekday.next Weekday.wednesday
-- Since the `Weekday` namespace has already been opened, you can also write
#eval next wednesday

-- Matching on a parameter like in the previous definition
-- is so common that Lean provides syntax sugar for it. The following
-- function uses it.
def Weekday.previous : Weekday -> Weekday
  | sunday    => saturday
  | monday    => sunday
  | tuesday   => monday
  | wednesday => tuesday
  | thursday  => wednesday
  | friday    => thursday
  | saturday  => friday

#eval next (previous wednesday)

-- We can prove that for any `Weekday` `d`, `next (previous d) = d`
theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d :=
  match d with
  | sunday    => rfl
  | monday    => rfl
  | tuesday   => rfl
  | wednesday => rfl
  | thursday  => rfl
  | friday    => rfl
  | saturday  => rfl

-- You can automate definitions such as `Weekday.nextOfPrevious`
-- using metaprogramming (or "tactics").
theorem Weekday.nextOfPrevious' (d : Weekday) : next (previous d) = d := by
  cases d       -- A proof by case distinction
  all_goals rfl  -- Each case is solved using `rfl`

Quickstart

These instructions will walk you through setting up Lean using the "basic" setup and VS Code as the editor. See Setup for other ways, supported platforms, and more details on setting up Lean.

See quick walkthrough demo video.

  1. Install VS Code.

  2. Launch VS Code and install the lean4 extension.

    installing the vscode-lean4 extension

  3. Create a new file using "File > New Text File" (Ctrl+N). Click the Select a language prompt, type in lean4, and hit ENTER. You should see the following popup: elan

    Click the "Install Lean using Elan" button. You should see some progress output like this:

    info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.0.0
info: downloading component 'lean'

    If there is no popup, you probably have Elan installed already. You may want to make sure that your default toolchain is Lean 4 in this case by running elan default leanprover/lean4:stable and reopen the file, as the next step will fail otherwise.

  4. While it is installing, you can paste the following Lean program into the new file:

    #eval Lean.versionString

    When the installation has finished, the Lean Language Server should start automatically and you should get syntax-highlighting and a "Lean Infoview" popping up on the right. You will see the output of the #eval statement when you place your cursor at the end of the statement.

    successful setup

You are set up!

Create a Lean Project

If your goal is to contribute to mathlib4 or use it as a dependency, please see its readme for specific instructions on how to do that.

You can now create a Lean project in a new folder. Run lake init foo from "View > Terminal" to create a package, followed by lake build to get an executable version of your Lean program. On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.

Note: Packages have to be opened using "File > Open Folder..." for imports to work. Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (Ctrl+Shift+X).

Troubleshooting

The InfoView says "Waiting for Lean server to start..." forever.

Check that the VS Code Terminal is not showing some installation errors from elan. If that doesn't work, try also running the VS Code command Developer: Reload Window.

Supported Platforms

Tier 1

Platforms built & tested by our CI, available as nightly releases via elan (see below)

  • x86-64 Linux with glibc 2.27+
  • x86-64 macOS 10.15+
  • x86-64 Windows 10+

Tier 2

Platforms cross-compiled but not tested by our CI, available as nightly releases

Releases may be silently broken due to the lack of automated testing. Issue reports and fixes are welcome.

  • aarch64 Linux with glibc 2.27+
  • aarch64 (Apple Silicon) macOS
  • x86 (32-bit) Linux
  • Emscripten Web Assembly

Setting Up Lean

See also the quickstart instructions for a standard setup with VS Code as the editor.

Release builds for all supported platforms are available at https://github.com/leanprover/lean4/releases. Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager elan instead:

$ elan self update  # in case you haven't updated elan in a while
# download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable

lake

Lean 4 comes with a package manager named lake. Use lake init foo to initialize a Lean package foo in the current directory, and lake build to typecheck and build it as well as all its dependencies. Use lake help to learn about further commands. The general directory structure of a package foo is

lakefile.lean  # package configuration
lean-toolchain # specifies the lean version to use
Foo.lean       # main file, import via `import Foo`
Foo/
  A.lean       # further files, import via e.g. `import Foo.A`
  A/...        # further nesting
build/         # `lake` build output directory

After running lake build you will see a binary named ./build/bin/foo and when you run it you should see the output:

Hello, world!

Editing

Lean implements the Language Server Protocol that can be used for interactive development in Emacs, VS Code, and possibly other editors.

Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).

Theorem Proving in Lean

We strongly encourage you to read the book Theorem Proving in Lean. Many Lean users consider it to be the Lean Bible.

Functional Programming in Lean

The goal of this book is to be an accessible introduction to using Lean 4 as a programming language. It should be useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming. It does not assume any background with functional programming, though it's probably not a good first book on programming in general. New content will be added once per month until it's done.

Examples

Palindromes

Palindromes are lists that read the same from left to right and from right to left. For example, [a, b, b, a] and [a, h, a] are palindromes.

We use an inductive predicate to specify whether a list is a palindrome or not. Recall that inductive predicates, or inductively defined propositions, are a convenient way to specify functions of type ... → Prop.

This example is a based on an example from the book "The Hitchhiker's Guide to Logical Verification".

inductive 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α → 
Prop: Type
Prop where
  | 
nil: ∀ {α : Type u_1}, Palindrome []
nil      : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
[]: List ?m.17
[]
  | 
single: ∀ {α : Type u_1} (a : α), Palindrome [a]
single   : (
a: α
a : 
α: Type u_1
α) → 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome [
a: α
a]
  | 
sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
sandwich : (
a: α
a : 
α: Type u_1
α) → 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List α
as → 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome ([
a: α
a] ++ 
as: List α
as ++ [
a: α
a])

The definition distinguishes three cases: (1) [] is a palindrome; (2) for any element a, the singleton list [a] is a palindrome; (3) for any element a and any palindrome [b₁, . . ., bₙ], the list [a, b₁, . . ., bₙ, a] is a palindrome.

We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate h : Palindrome as.

theorem 
palindrome_reverse: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)
palindrome_reverse (
h: Palindrome as
h : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.394
as) : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.394
as.
reverse: {α : Type u_1} → List α → List α
reverse := 
Goals accomplished! 🐙

  
α✝: Type u_1
as: List α✝
h: Palindrome as
Palindrome (List.reverse as)

  
α✝: Type u_1
as: List α✝
nil
Palindrome (List.reverse [])
 
Goals accomplished! 🐙

  
α✝: Type u_1
as: List α✝
a: α✝
single
Palindrome (List.reverse [a])
 
Goals accomplished! 🐙

  
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome (List.reverse as✝)
sandwich
Palindrome (List.reverse ([a] ++ as✝ ++ [a]))
 
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome (List.reverse as✝)
sandwich
Palindrome (a :: (List.reverse as✝ ++ [a]))
; 
Goals accomplished! 🐙

If a list as is a palindrome, then the reverse of as is equal to itself.

theorem 
reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → List.reverse as = as
reverse_eq_of_palindrome (
h: Palindrome as
h : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.696
as) : 
as: List ?m.696
as.
reverse: {α : Type u_1} → List α → List α
reverse = 
as: List ?m.696
as := 
Goals accomplished! 🐙

  
α✝: Type u_1
as: List α✝
h: Palindrome as
List.reverse as = as

  
α✝: Type u_1
as: List α✝
nil
List.reverse [] = []
 
Goals accomplished! 🐙

  
α✝: Type u_1
as: List α✝
a: α✝
single
List.reverse [a] = [a]
 
Goals accomplished! 🐙

  
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: List.reverse as✝ = as✝
sandwich
List.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]
 
Warning: unused variable `h` [linter.unusedVariables]
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: List.reverse as✝ = as✝
sandwich
List.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]
 
ih: List.reverse as✝ = as✝
α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: List.reverse as✝ = as✝
sandwich
List.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]
 
Goals accomplished! 🐙

Note that you can also easily prove palindrome_reverse using reverse_eq_of_palindrome.

example: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)
example (
h: Palindrome as
h : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.946
as) : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.946
as.
reverse: {α : Type u_1} → List α → List α
reverse := 
Goals accomplished! 🐙

  
Goals accomplished! 🐙

Given a nonempty list, the function List.last returns its element. Note that we use (by simp) to prove that a₂ :: as ≠ [] in the recursive application.

def 
List.last: {α : Type u_1} → (as : List α) → as ≠ [] → α
List.last : (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) → 
as: List α
as ≠ 
[]: List α
[] → 
α: Type u_1
α
  | [
a: α
a],         _ => 
a: α
a
  | _::
a₂: α
a₂:: 
as: List α
as, _ => (
a₂: α
a₂::
as: List α
as).
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last (
Goals accomplished! 🐙
 
Goals accomplished! 🐙
)

We use the function List.last to prove the following theorem that says that if a list as is not empty, then removing the last element from as and appending it back is equal to as. We use the attribute @[simp] to instruct the simp tactic to use this theorem as a simplification rule.

@[simp] theorem 
List.dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), dropLast as ++ [last as h] = as
List.dropLast_append_last (
h: as ≠ []
h : 
as: List ?m.1696
as ≠ 
[]: List ?m.1696
[]) : 
as: List ?m.1696
as.
dropLast: {α : Type u_1} → List α → List α
dropLast ++ [
as: List ?m.1696
as.
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last 
h: as ≠ []
h] = 
as: List ?m.1696
as := 
Goals accomplished! 🐙

  
α✝: Type u_1
as: List α✝
h: as ≠ []
dropLast as ++ [last as h] = as

  
α✝: Type u_1
as: List α✝
h: [] ≠ []
dropLast [] ++ [last [] h] = []
 
Goals accomplished! 🐙

  
α✝: Type u_1
as: List α✝
a: α✝
h: [a] ≠ []
dropLast [a] ++ [last [a] h] = [a]
 
Goals accomplished! 🐙

  
α✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []
dropLast (a₁ :: a₂ :: as) ++ [last (a₁ :: a₂ :: as) h] = a₁ :: a₂ :: as

    
α✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []
dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: as

    
α✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []
dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: as
Goals accomplished! 🐙
 
Goals accomplished! 🐙
Goals accomplished! 🐙

We now define the following auxiliary induction principle for lists using well-founded recursion on as.length. We can read it as follows, to prove motive as, it suffices to show that: (1) motive []; (2) motive [a] for any a; (3) if motive as holds, then motive ([a] ++ as ++ [b]) also holds for any a, b, and as. Note that the structure of this induction principle is very similar to the Palindrome inductive predicate.

theorem 
List.palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
  motive [] →
    (∀ (a : α), motive [a]) →
      (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive as
List.palindrome_ind (
motive: List α → Prop
motive : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α → 
Prop: Type
Prop)
    (
h₁: motive []
h₁ : 
motive: List α → Prop
motive 
[]: List α
[])
    (
h₂: ∀ (a : α), motive [a]
h₂ : (
a: α
a : 
α: Type u_1
α) → 
motive: List α → Prop
motive [
a: α
a])
    (
h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])
h₃ : (
a: α
a 
b: α
b : 
α: Type u_1
α) → (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) → 
motive: List α → Prop
motive 
as: List α
as → 
motive: List α → Prop
motive ([
a: α
a] ++ 
as: List α
as ++ [
b: α
b]))
    (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α)
    : 
motive: List α → Prop
motive 
as: List α
as :=
  match 
as: List α
as with
  | []  => 
h₁: motive []
h₁
  | [
a: α
a] => 
h₂: ∀ (a : α), motive [a]
h₂ 
a: α
a
  | 
a₁: α
a₁::
a₂: α
a₂::
as': List α
as' =>
    have 
ih: motive (dropLast (a₂ :: as'))
ih := 
palindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop),
  motive [] →
    (∀ (a : α), motive [a]) →
      (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive as
palindrome_ind 
motive: List α → Prop
motive 
h₁: motive []
h₁ 
h₂: ∀ (a : α), motive [a]
h₂ 
h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])
h₃ (
a₂: α
a₂::
as': List α
as').
dropLast: {α : Type u_1} → List α → List α
dropLast
    have : [
a₁: α
a₁] ++ (
a₂: α
a₂::
as': List α
as').
dropLast: {α : Type u_1} → List α → List α
dropLast ++ [(
a₂: α
a₂::
as': List α
as').
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last (
Goals accomplished! 🐙
 
Goals accomplished! 🐙
)] = 
a₁: α
a₁::
a₂: α
a₂::
as': List α
as' := 
Goals accomplished! 🐙
 
Goals accomplished! 🐙

    
this: [a₁] ++ dropLast (a₂ :: as') ++ [last (a₂ :: as') (_ : ¬a₂ :: as' = [])] = a₁ :: a₂ :: as'
this ▸ 
h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])
h₃ 
_: α
_ 
_: α
_ 
_: List α
_ 
ih: motive (dropLast (a₂ :: as'))
ih
termination_by _ as => 
as: List α
as.
length: {α : Type u_1} → List α → Nat
length

We use our new induction principle to prove that if as.reverse = as, then Palindrome as holds. Note that we use the using modifier to instruct the induction tactic to use this induction principle instead of the default one for lists.

theorem 
List.palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, reverse as = as → Palindrome as
List.palindrome_of_eq_reverse (
h: reverse as = as
h : 
as: List ?m.10517
as.
reverse: {α : Type u_1} → List α → List α
reverse = 
as: List ?m.10517
as) : 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List ?m.10517
as := 
Goals accomplished! 🐙

  
α✝: Type u_1
h: reverse [] = []
h₁
Palindrome []
α✝: Type u_1
a✝: α✝
h: reverse [a✝] = [a✝]
Palindrome [a✝]
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]
Palindrome ([a✝¹] ++ as✝ ++ [b✝])

  
α✝: Type u_1
h: reverse [] = []
h₁
Palindrome []
α✝: Type u_1
a✝: α✝
h: reverse [a✝] = [a✝]
Palindrome [a✝]
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]
Palindrome ([a✝¹] ++ as✝ ++ [b✝])
 
Goals accomplished! 🐙

  
α✝: Type u_1
a✝: α✝
h: reverse [a✝] = [a✝]
h₂
Palindrome [a✝]
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]
Palindrome ([a✝¹] ++ as✝ ++ [b✝])
 
Goals accomplished! 🐙

  
α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]
h₃
Palindrome ([a✝¹] ++ as✝ ++ [b✝])

    
α✝: Type u_1
a, b: α✝
as: List α✝
ih: reverse as = as → Palindrome as
h: reverse ([a] ++ as ++ [b]) = [a] ++ as ++ [b]
Palindrome ([a] ++ as ++ [b])
 
Goals accomplished! 🐙
 
Goals accomplished! 🐙

    
α✝: Type u_1
a: α✝
as: List α✝
ih: reverse as = as → Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]
Palindrome ([a] ++ as ++ [a])

    
α✝: Type u_1
a: α✝
as: List α✝
ih: reverse as = as → Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]
Palindrome ([a] ++ as ++ [a])
 
Goals accomplished! 🐙
 
Goals accomplished! 🐙

    
Goals accomplished! 🐙

We now define a function that returns true iff as is a palindrome. The function assumes that the type α has decidable equality. We need this assumption because we need to compare the list elements.

def 
List.isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → Bool
List.isPalindrome [
DecidableEq: Type u_1 → Type u_1
DecidableEq 
α: Type u_1
α] (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) : 
Bool: Type
Bool :=
    
as: List α
as.
reverse: {α : Type u_1} → List α → List α
reverse = 
as: List α
as

It is straightforward to prove that isPalindrome is correct using the previously proved theorems.

theorem 
List.isPalindrome_correct: ∀ {α : Type u_1} [inst : DecidableEq α] (as : List α), isPalindrome as = true ↔ Palindrome as
List.isPalindrome_correct [
DecidableEq: Type u_1 → Type u_1
DecidableEq 
α: Type u_1
α] (
as: List α
as : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) : 
as: List α
as.
isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → Bool
isPalindrome ↔ 
Palindrome: {α : Type u_1} → List α → Prop
Palindrome 
as: List α
as := 
Goals accomplished! 🐙

  
α: Type u_1
inst✝: DecidableEq α
as: List α
reverse as = as ↔ Palindrome as

  
Goals accomplished! 🐙



true

 [
1: Nat
1, 
2: Nat
2, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome

false

 [
1: Nat
1, 
2: Nat
2, 
3: Nat
3, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome


example: List.isPalindrome [1, 2, 1] = true
example : [
1: Nat
1, 
2: Nat
2, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome := 
rfl: ∀ {α : Type} {a : α}, a = a
rfl

example: List.isPalindrome [1, 2, 2, 1] = true
example : [
1: Nat
1, 
2: Nat
2, 
2: Nat
2, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome := 
rfl: ∀ {α : Type} {a : α}, a = a
rfl

example: (!List.isPalindrome [1, 2, 3, 1]) = true
example : ![
1: Nat
1, 
2: Nat
2, 
3: Nat
3, 
1: Nat
1].
isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool
isPalindrome := 
rfl: ∀ {α : Type} {a : α}, a = a
rfl

Binary Search Trees

If the type of keys can be totally ordered -- that is, it supports a well-behaved ≤ comparison -- then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.

This example is based on a similar example found in the "Software Foundations" book (volume 3).

We use Nat as the key type in our implementation of BSTs, since it has a convenient total order with lots of theorems and automation available. We leave as an exercise to the reader the generalization to arbitrary types.

inductive 
Tree: Type v → Type v
Tree (
β: Type v
β : 
Type v: Type (v + 1)
Type v) where
  | 
leaf: {β : Type v} → Tree β
leaf
  | 
node: {β : Type v} → Tree β → Nat → β → Tree β → Tree β
node (
left: Tree β
left : 
Tree: Type v → Type v
Tree 
β: Type v
β) (
key: Nat
key : 
Nat: Type
Nat) (
value: β
value : 
β: Type v
β) (
right: Tree β
right : 
Tree: Type v → Type v
Tree 
β: Type v
β)
  deriving 
Repr: Type u → Type u
Repr

The function contains returns true iff the given tree contains the key k.

def 
Tree.contains: {β : Type u_1} → Tree β → Nat → Bool
Tree.contains (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) : 
Bool: Type
Bool :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.1676} → Tree β
leaf => 
false: Bool
false
  | 
node: {β : Type ?u.1685} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
Warning: unused variable `value` [linter.unusedVariables]
 
right: Tree β
right =>
    if 
k: Nat
k < 
key: Nat
key then
      
left: Tree β
left.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains 
k: Nat
k
    else if 
key: Nat
key < 
k: Nat
k then
      
right: Tree β
right.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains 
k: Nat
k
    else
      
true: Bool
true

t.find? k returns some v if v is the value bound to key k in the tree t. It returns none otherwise.

def 
Tree.find?: {β : Type u_1} → Tree β → Nat → Option β
Tree.find? (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) : 
Option: Type u_1 → Type u_1
Option 
β: Type u_1
β :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.2139} → Tree β
leaf => 
none: {α : Type u_1} → Option α
none
  | 
node: {β : Type ?u.2151} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
value: β
value 
right: Tree β
right =>
    if 
k: Nat
k < 
key: Nat
key then
      
left: Tree β
left.
find?: {β : Type u_1} → Tree β → Nat → Option β
find? 
k: Nat
k
    else if 
key: Nat
key < 
k: Nat
k then
      
right: Tree β
right.
find?: {β : Type u_1} → Tree β → Nat → Option β
find? 
k: Nat
k
    else
      
some: {α : Type u_1} → α → Option α
some 
value: β
value

t.insert k v is the map containing all the bindings of t along with a binding of k to v.

def 
Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) (
v: β
v : 
β: Type u_1
β) : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.2611} → Tree β
leaf => 
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node 
leaf: {β : Type u_1} → Tree β
leaf 
k: Nat
k 
v: β
v 
leaf: {β : Type u_1} → Tree β
leaf
  | 
node: {β : Type ?u.2626} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
value: β
value 
right: Tree β
right =>
    if 
k: Nat
k < 
key: Nat
key then
      
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node (
left: Tree β
left.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert 
k: Nat
k 
v: β
v) 
key: Nat
key 
value: β
value 
right: Tree β
right
    else if 
key: Nat
key < 
k: Nat
k then
      
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
key: Nat
key 
value: β
value (
right: Tree β
right.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert 
k: Nat
k 
v: β
v)
    else
      
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node 
left: Tree β
left 
k: Nat
k 
v: β
v 
right: Tree β
right

Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs. If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list. Here's a function that does so with an in-order traversal of the tree.

def 
Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toList (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β) :=
  match 
t: Tree β
t with
  | 
leaf: {β : Type ?u.3120} → Tree β
leaf => 
[]: List (Nat × β)
[]
  | 
node: {β : Type ?u.3132} → Tree β → Nat → β → Tree β → Tree β
node 
l: Tree β
l 
k: Nat
k 
v: β
v 
r: Tree β
r => 
l: Tree β
l.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList ++ [(
k: Nat
k, 
v: β
v)] ++ 
r: Tree β
r.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList


Tree.node (Tree.node (Tree.leaf) 1 "one" (Tree.leaf)) 2 "two" (Tree.node (Tree.leaf) 3 "three" (Tree.leaf))

 
Tree.leaf: {β : Type} → Tree β
Tree.leaf.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
2: Nat
2 
"two": String
"two"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
3: Nat
3 
"three": String
"three"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
1: Nat
1 
"one": String
"one"


[(1, "one"), (2, "two"), (3, "three")]

 
Tree.leaf: {β : Type} → Tree β
Tree.leaf.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
2: Nat
2 
"two": String
"two"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
3: Nat
3 
"three": String
"three"
      |>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert 
1: Nat
1 
"one": String
"one"
      |>.
toList: {β : Type} → Tree β → List (Nat × β)
toList

The implementation of Tree.toList is inefficient because of how it uses the ++ operator. On a balanced tree its running time is linearithmic, because it does a linear number of concatenations at each level of the tree. On an unbalanced tree it's quadratic time. Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:

def 
Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toListTR (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β) :=
  
go: Tree β → List (Nat × β) → List (Nat × β)
go 
t: Tree β
t 
[]: List (Nat × β)
[]
where
  
go: Tree β → List (Nat × β) → List (Nat × β)
go (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
acc: List (Nat × β)
acc : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β)) : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β) :=
    match 
t: Tree β
t with
    | 
leaf: {β : Type ?u.9422} → Tree β
leaf => 
acc: List (Nat × β)
acc
    | 
node: {β : Type ?u.9432} → Tree β → Nat → β → Tree β → Tree β
node 
l: Tree β
l 
k: Nat
k 
v: β
v 
r: Tree β
r => 
go: Tree β → List (Nat × β) → List (Nat × β)
go 
l: Tree β
l ((
k: Nat
k, 
v: β
v) :: 
go: Tree β → List (Nat × β) → List (Nat × β)
go 
r: Tree β
r 
acc: List (Nat × β)
acc)

We now prove that t.toList and t.toListTR return the same list. The proof is on induction, and as we used the auxiliary function go to define Tree.toListTR, we use the auxiliary theorem go to prove the theorem.

The proof of the auxiliary theorem is by induction on t. The generalizing acc modifier instructs Lean to revert acc, apply the induction theorem for Trees, and then reintroduce acc in each case. By using generalizing, we obtain the more general induction hypotheses

  • left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc

  • right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc

Recall that the combinator tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'. In this theorem, we use it to apply simp and close each subgoal produced by the induction tactic.

The simp parameters toListTR.go and toList instruct the simplifier to try to reduce and/or apply auto generated equation theorems for these two functions. The parameter * instructs the simplifier to use any equation in a goal as rewriting rules. In this particular case, simp uses the induction hypotheses as rewriting rules. Finally, the parameter List.append_assoc instructs the simplifier to use the List.append_assoc theorem as a rewriting rule.

theorem 
Tree.toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), toList t = toListTR t
Tree.toList_eq_toListTR (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β)
        : 
t: Tree β
t.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList = 
t: Tree β
t.
toListTR: {β : Type u_1} → Tree β → List (Nat × β)
toListTR := 
Goals accomplished! 🐙

  
Goals accomplished! 🐙

where
  
go: ∀ (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = toList t ++ acc
go (
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β) (
acc: List (Nat × β)
acc : 
List: Type u_1 → Type u_1
List (
Nat: Type
Nat × 
β: Type u_1
β))
     : 
toListTR.go: {β : Type u_1} → Tree β → List (Nat × β) → List (Nat × β)
toListTR.go 
t: Tree β
t 
acc: List (Nat × β)
acc = 
t: Tree β
t.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList ++ 
acc: List (Nat × β)
acc := 
Goals accomplished! 🐙

    
β: Type u_1
t: Tree β
acc: List (Nat × β)
leaf
toListTR.go leaf acc = toList leaf ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = toList left✝ ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = toList right✝ ++ acc
acc: List (Nat × β)
toListTR.go (node left✝ key✝ value✝ right✝) acc = toList (node left✝ key✝ value✝ right✝) ++ acc
 
β: Type u_1
t: Tree β
acc: List (Nat × β)
leaf
toListTR.go leaf acc = toList leaf ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = toList left✝ ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = toList right✝ ++ acc
acc: List (Nat × β)
toListTR.go (node left✝ key✝ value✝ right✝) acc = toList (node left✝ key✝ value✝ right✝) ++ acc

      
Goals accomplished! 🐙

The [csimp] annotation instructs the Lean code generator to replace any Tree.toList with Tree.toListTR when generating code.

@[csimp] theorem 
Tree.toList_eq_toListTR_csimp: @toList = @toListTR
Tree.toList_eq_toListTR_csimp
                 : @
Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toList = @
Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toListTR := 
Goals accomplished! 🐙

  
β: Type u_1
t: Tree β
h.h
toList t = toListTR t

  
Goals accomplished! 🐙

The implementations of Tree.find? and Tree.insert assume that values of type tree obey the BST invariant: for any non-empty node with key k, all the values of the left subtree are less than k and all the values of the right subtree are greater than k. But that invariant is not part of the definition of tree.

So, let's formalize the BST invariant. Here's one way to do so. First, we define a helper ForallTree to express that idea that a predicate holds at every node of a tree:

inductive 
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree (
p: Nat → β → Prop
p : 
Nat: Type
Nat → 
β: Type u_1
β → 
Prop: Type
Prop) : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β → 
Prop: Type
Prop
  | 
leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p Tree.leaf
leaf : 
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree 
p: Nat → β → Prop
p 
.leaf: {β : Type u_1} → Tree β
.leaf
  | 
node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
  ForallTree p left → p key value → ForallTree p right → ForallTree p (Tree.node left key value right)
node :
     
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree 
p: Nat → β → Prop
p 
left: Tree β
left →
     
p: Nat → β → Prop
p 
key: Nat
key 
value: β
value →
     
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree 
p: Nat → β → Prop
p 
right: Tree β
right →
     
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree 
p: Nat → β → Prop
p (
.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
.node 
left: Tree β
left 
key: Nat
key 
value: β
value 
right: Tree β
right)

Second, we define the BST invariant: An empty tree is a BST. A non-empty tree is a BST if all its left nodes have a lesser key, its right nodes have a greater key, and the left and right subtrees are themselves BSTs.

inductive 
BST: {β : Type u_1} → Tree β → Prop
BST : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β → 
Prop: Type
Prop
  | 
leaf: ∀ {β : Type u_1}, BST Tree.leaf
leaf : 
BST: {β : Type u_1} → Tree β → Prop
BST 
.leaf: {β : Type u_1} → Tree β
.leaf
  | 
node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
  ForallTree (fun k v => k < key) left →
    ForallTree (fun k v => key < k) right → BST left → BST right → BST (Tree.node left key value right)
node :
     
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree (fun 
k: Nat
k 
Warning: unused variable `v` [linter.unusedVariables]
 => 
k: Nat
k < 
key: Nat
key) 
left: Tree ?m.11579
left →
     
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree (fun 
k: Nat
k 
Warning: unused variable `v` [linter.unusedVariables]
 => 
key: Nat
key < 
k: Nat
k) 
right: Tree ?m.11579
right →
     
BST: {β : Type u_1} → Tree β → Prop
BST 
left: Tree ?m.11579
left → 
BST: {β : Type u_1} → Tree β → Prop
BST 
right: Tree ?m.11579
right →
     
BST: {β : Type u_1} → Tree β → Prop
BST (
.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
.node 
left: Tree ?m.11579
left 
key: Nat
key 
value: ?m.11579
value 
right: Tree ?m.11579
right)

We can use the macro command to create helper tactics for organizing our proofs. The macro have_eq x y tries to prove x = y using linear arithmetic, and then immediately uses the new equality to substitute x with y everywhere in the goal.

The modifier local specifies the scope of the macro.

/-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
    and then replaces `lhs` with `rhs`. -/
local macro "have_eq " 
lhs: Lean.TSyntax `term
lhs:
term: Lean.Parser.Category
term:max 
rhs: Lean.TSyntax `term
rhs:
term: Lean.Parser.Category
term:max : 
tactic: Lean.Parser.Category
tactic =>
  `(tactic|
    (have h : $
lhs: Lean.TSyntax `term
lhs = $
rhs: Lean.TSyntax `term
rhs :=
       -- TODO: replace with linarith
       by simp_arith at *; apply Nat.le_antisymm <;> assumption
     try subst $
lhs: Lean.TSyntax `term
lhs))

The by_cases' e is just the regular by_cases followed by simp using all hypotheses in the current goal as rewriting rules. Recall that the by_cases tactic creates two goals. One where we have h : e and another one containing h : ¬ e. The simplifier uses the h to rewrite e to True in the first subgoal, and e to False in the second. This is particularly useful if e is the condition of an if-statement.

/-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
local macro "by_cases' " 
e: Lean.TSyntax `term
e:
term: Lean.Parser.Category
term :  
tactic: Lean.Parser.Category
tactic =>
  `(tactic| by_cases $
e: Lean.TSyntax `term
e <;> simp [*])

We can use the attribute [simp] to instruct the simplifier to reduce given definitions or apply rewrite theorems. The local modifier limits the scope of this modification to this file.

attribute [local simp] 
Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert

We now prove that Tree.insert preserves the BST invariant using induction and case analysis. Recall that the tactic . tac focuses on the main goal and tries to solve it using tac, or else fails. It is used to structure proofs in Lean. The notation ‹e› is just syntax sugar for (by assumption : e). That is, it tries to find a hypothesis h : e. It is useful to access hypothesis that have auto generated names (aka "inaccessible") names.

theorem 
Tree.forall_insert_of_forall: ∀ {β : Type u_1} {p : Nat → β → Prop} {t : Tree β} {key : Nat} {value : β},
  ForallTree p t → p key value → ForallTree p (insert t key value)
Tree.forall_insert_of_forall
        (
h₁: ForallTree p t
h₁ : 
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree 
p: Nat → ?m.18569 → Prop
p 
t: Tree ?m.18569
t) (
h₂: p key value
h₂ : 
p: Nat → ?m.18569 → Prop
p 
key: Nat
key 
value: ?m.18569
value)
        : 
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree 
p: Nat → ?m.18569 → Prop
p (
t: Tree ?m.18569
t.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert 
key: Nat
key 
value: ?m.18569
value) := 
Goals accomplished! 🐙

  
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₁: ForallTree p t
h₂: p key value
ForallTree p (insert t key value)

  
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
leaf
ForallTree p (insert leaf key value)
 
Goals accomplished! 🐙

  
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
key✝: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p key✝ value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
node
ForallTree p (insert (node left✝ key✝ value✝ right✝) key value)

    
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
node
ForallTree p (insert (node left✝ k value✝ right✝) key value)

    
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: key < k
node.inl
ForallTree p (node (insert left✝ key value) k value✝ right✝)
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: ¬key < k
ForallTree p (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)

    
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: key < k
node.inl
ForallTree p (node (insert left✝ key value) k value✝ right✝)
 
Goals accomplished! 🐙

    
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: ¬key < k
node.inr
ForallTree p (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)
 
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inl
ForallTree p (node left✝ k value✝ (insert right✝ key value))
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < key
ForallTree p (node left✝ key value right✝)

      
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inl
ForallTree p (node left✝ k value✝ (insert right✝ key value))
 
Goals accomplished! 🐙

      
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < key
node.inr.inr
ForallTree p (node left✝ key value right✝)
 
β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
value: β✝
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
h₂: p k value
ihl: ForallTree p (insert left✝ k value)
ihr: ForallTree p (insert right✝ k value)
h✝¹, h✝: ¬k < k
node.inr.inr
ForallTree p (node left✝ k value right✝)

        
Goals accomplished! 🐙


theorem 
Tree.bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (insert t key value)
Tree.bst_insert_of_bst
        {
t: Tree β
t : 
Tree: Type u_1 → Type u_1
Tree 
β: Type u_1
β} (
h: BST t
h : 
BST: {β : Type u_1} → Tree β → Prop
BST 
t: Tree β
t) (
key: Nat
key : 
Nat: Type
Nat) (
value: β
value : 
β: Type u_1
β)
        : 
BST: {β : Type u_1} → Tree β → Prop
BST (
t: Tree β
t.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert 
key: Nat
key 
value: β
value) := 
Goals accomplished! 🐙

  
β: Type u_1
t: Tree β
h: BST t
key: Nat
value: β
BST (insert t key value)

  
β: Type u_1
t: Tree β
key: Nat
value: β
leaf
BST (insert leaf key value)
 
Goals accomplished! 🐙

  
β: Type u_1
t: Tree β
key: Nat
value: β
key✝: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k v => k < key✝) left✝
h₂: ForallTree (fun k v => key✝ < k) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
node
BST (insert (node left✝ key✝ value✝ right✝) key value)

    
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
node
BST (insert (node left✝ k value✝ right✝) key value)

    
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
node
BST
  (if key < k then node (insert left✝ key value) k value✝ right✝
  else if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)

    
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: key < k
node.inl
BST (node (insert left✝ key value) k value✝ right✝)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: ¬key < k
BST (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)

    
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: key < k
node.inl
BST (node (insert left✝ key value) k value✝ right✝)
 
Goals accomplished! 🐙

    
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: ¬key < k
node.inr
BST (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)
 
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inl
BST (node left✝ k value✝ (insert right✝ key value))
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < key
BST (node left✝ key value right✝)

      
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inl
BST (node left✝ k value✝ (insert right✝ key value))
 
Goals accomplished! 🐙

      
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < key
node.inr.inr
BST (node left✝ key value right✝)
 
β: Type u_1
t: Tree β
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ k value)
ih₂: BST (insert right✝ k value)
h✝¹, h✝: ¬k < k
node.inr.inr
BST (node left✝ k value right✝)

        
Goals accomplished! 🐙

Now, we define the type BinTree using a Subtype that states that only trees satisfying the BST invariant are BinTrees.

def 
BinTree: Type u → Type u
BinTree (
β: Type u
β : 
Type u: Type (u + 1)
Type u) := { 
t: Tree β
t : 
Tree: Type u → Type u
Tree 
β: Type u
β // 
BST: {β : Type u} → Tree β → Prop
BST 
t: Tree β
t }

def 
BinTree.mk: {β : Type u_1} → BinTree β
BinTree.mk : 
BinTree: Type u_1 → Type u_1
BinTree 
β: Type u_1
β :=
  ⟨
.leaf: {β : Type u_1} → Tree β
.leaf, 
.leaf: ∀ {β : Type u_1}, BST Tree.leaf
.leaf⟩

def 
BinTree.contains: {β : Type u_1} → BinTree β → Nat → Bool
BinTree.contains (
b: BinTree β
b : 
BinTree: Type u_1 → Type u_1
BinTree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) : 
Bool: Type
Bool :=
  
b: BinTree β
b.
val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains 
k: Nat
k

def 
BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option β
BinTree.find? (
b: BinTree β
b : 
BinTree: Type u_1 → Type u_1
BinTree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) : 
Option: Type u_1 → Type u_1
Option 
β: Type u_1
β :=
  
b: BinTree β
b.
val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.
find?: {β : Type u_1} → Tree β → Nat → Option β
find? 
k: Nat
k

def 
BinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
BinTree.insert (
b: BinTree β
b : 
BinTree: Type u_1 → Type u_1
BinTree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) (
v: β
v : 
β: Type u_1
β) : 
BinTree: Type u_1 → Type u_1
BinTree 
β: Type u_1
β :=
  ⟨
b: BinTree β
b.
val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert 
k: Nat
k 
v: β
v, 
b: BinTree β
b.
val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val.
bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (Tree.insert t key value)
bst_insert_of_bst 
b: BinTree β
b.
property: ∀ {α : Type u_1} {p : α → Prop} (self : Subtype p), p self.val
property 
k: Nat
k 
v: β
v⟩

Finally, we prove that BinTree.find? and BinTree.insert satisfy the map properties.

attribute [local simp]
  
BinTree.mk: {β : Type u_1} → BinTree β
BinTree.mk 
BinTree.contains: {β : Type u_1} → BinTree β → Nat → Bool
BinTree.contains 
BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option β
BinTree.find?
  
BinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
BinTree.insert 
Tree.find?: {β : Type u_1} → Tree β → Nat → Option β
Tree.find? 
Tree.contains: {β : Type u_1} → Tree β → Nat → Bool
Tree.contains 
Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert

theorem 
BinTree.find_mk: ∀ {β : Type u_1} (k : Nat), find? mk k = none
BinTree.find_mk (
k: Nat
k : 
Nat: Type
Nat)
        : 
BinTree.mk: {β : Type u_1} → BinTree β
BinTree.mk.
find?: {β : Type u_1} → BinTree β → Nat → Option β
find? 
k: Nat
k = (
none: {α : Type u_1} → Option α
none : 
Option: Type u_1 → Type u_1
Option 
β: Type u_1
β) := 
Goals accomplished! 🐙

  
Goals accomplished! 🐙


theorem 
BinTree.find_insert: ∀ {β : Type u_1} (b : BinTree β) (k : Nat) (v : β), find? (insert b k v) k = some v
BinTree.find_insert (
b: BinTree β
b : 
BinTree: Type u_1 → Type u_1
BinTree 
β: Type u_1
β) (
k: Nat
k : 
Nat: Type
Nat) (
v: β
v : 
β: Type u_1
β)
        : (
b: BinTree β
b.
insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
insert 
k: Nat
k 
v: β
v).
find?: {β : Type u_1} → BinTree β → Nat → Option β
find? 
k: Nat
k = 
some: {α : Type u_1} → α → Option α
some 
v: β
v := 
Goals accomplished! 🐙

  
β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t
find? (insert { val := t, property := h } k v) k = some v
; 
β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t
Tree.find? (Tree.insert t k v) k = some v

  
β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t
Tree.find? (Tree.insert t k v) k = some v
 
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
node
Tree.find?
    (if k < key then Tree.node (Tree.insert left k v) key value right
    else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
    k =
  some v

  
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
node
Tree.find?
    (if k < key then Tree.node (Tree.insert left k v) key value right
    else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
    k =
  some v

    
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: k < key
node.inl
Tree.find? (Tree.insert left k v) k = some v
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: ¬k < key
Tree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k = some v

    
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: k < key
node.inl
Tree.find? (Tree.insert left k v) k = some v
 
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inl.node
Tree.find? (Tree.insert left k v) k = some v
; 
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inl.node
BST left
; 
Goals accomplished! 🐙

    
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: ¬k < key
node.inr
Tree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k = some v
 
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝¹: ¬k < key
h✝: key < k
node.inr.inl
Tree.find? (Tree.insert right k v) k = some v

      
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inr.inl.node
Tree.find? (Tree.insert right k v) k = some v
; 
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inr.inl.node
BST right
; 
Goals accomplished! 🐙


theorem 
BinTree.find_insert_of_ne: ∀ {β : Type u_1} {k k' : Nat} (b : BinTree β), k ≠ k' → ∀ (v : β), find? (insert b k v) k' = find? b k'
BinTree.find_insert_of_ne (
b: BinTree β
b : 
BinTree: Type u_1 → Type u_1
BinTree 
β: Type u_1
β) (
h: k ≠ k'
h : 
k: Nat
k ≠ 
k': Nat
k') (
v: β
v : 
β: Type u_1
β)
        : (
b: BinTree β
b.
insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
insert 
k: Nat
k 
v: β
v).
find?: {β : Type u_1} → BinTree β → Nat → Option β
find? 
k': Nat
k' = 
b: BinTree β
b.
find?: {β : Type u_1} → BinTree β → Nat → Option β
find? 
k': Nat
k' := 
Goals accomplished! 🐙

  
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
t: Tree β
h: BST t
find? (insert { val := t, property := h } k v) k' = find? { val := t, property := h } k'
; 
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
t: Tree β
h: BST t
Tree.find? (Tree.insert t k v) k' = Tree.find? t k'

  
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
t: Tree β
h: BST t
Tree.find? (Tree.insert t k v) k' = Tree.find? t k'
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
node
Tree.find?
    (if k < key then Tree.node (Tree.insert left k v) key value right
    else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
    k' =
  if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value

  
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
h: BST Tree.leaf
leaf
(if k' < k then none else if k < k' then none else some v) = none

    
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k
(if k < k' then none else some v) = none
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k
(if k < k' then none else some v) = none
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inl
none = none
 
Goals accomplished! 🐙
Goals accomplished! 🐙
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k
leaf.inr
(if k < k' then none else some v) = none
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: k < k'
leaf.inr.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
False
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: k < k'
leaf.inr.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
False
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inr
False
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inr
False
 
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inr
False
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inr
False

    
β: Type u_1
k': Nat
b: BinTree β
v: β
h✝²: BST Tree.leaf
h: k' ≠ k'
h✝¹, h✝: ¬k' < k'
leaf.inr.inr
False

    
Goals accomplished! 🐙

  
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
node
Tree.find?
    (if k < key then Tree.node (Tree.insert left k v) key value right
    else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
    k' =
  if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value

    
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
node
Tree.find?
    (if k < key then Tree.node (Tree.insert left k v) key value right
    else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
    k' =
  if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value

    
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
node
Tree.find?
    (if k < key then Tree.node (Tree.insert left k v) key value right
    else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
    k' =
  if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value

    
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
node
Tree.find?
    (if k < key then Tree.node (Tree.insert left k v) key value right
    else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
    k' =
  if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value

    
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h✝: ¬k < key
node.inr
Tree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' =
  if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value
; 
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h✝¹: ¬k < key
h✝: ¬key < k
node.inr.inr
(if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some v) =
  if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value

    
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝¹, h✝: ¬k < k
node.inr.inr
(if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some v) =
  if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some value

    
β: Type u_1
k, k': Nat
b: BinTree β
h✝³: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝², h✝¹: ¬k < k
h✝: ¬k' < k
node.inr.inr.inr
(if k < k' then Tree.find? right k' else some v) = if k < k' then Tree.find? right k' else some value
; 
β: Type u_1
k, k': Nat
b: BinTree β
h✝⁴: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝³, h✝²: ¬k < k
h✝¹: ¬k' < k
h✝: ¬k < k'
node.inr.inr.inr.inr
v = value

    
β: Type u_1
k': Nat
b: BinTree β
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
h✝⁴: k' ≠ k'
ihl: Tree.find? (Tree.insert left k' v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k' v) k' = Tree.find? right k'
h: BST (Tree.node left k' value right)
hl: ForallTree (fun k v => k < k') left
hr: ForallTree (fun k v => k' < k) right
h✝³, h✝², h✝¹, h✝: ¬k' < k'
node.inr.inr.inr.inr
v = value

    
Goals accomplished! 🐙

A Certified Type Checker

In this example, we build a certified type checker for a simple expression language.

Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.

inductive 
Expr: Type
Expr where
  | 
nat: Nat → Expr
nat  : 
Nat: Type
Nat → 
Expr: Type
Expr
  | 
plus: Expr → Expr → Expr
plus : 
Expr: Type
Expr → 
Expr: Type
Expr → 
Expr: Type
Expr
  | 
bool: Bool → Expr
bool : 
Bool: Type
Bool → 
Expr: Type
Expr
  | 
and: Expr → Expr → Expr
and  : 
Expr: Type
Expr → 
Expr: Type
Expr → 
Expr: Type
Expr

We define a simple language of types using the inductive datatype Ty, and its typing rules using the inductive predicate HasType.

inductive 
Ty: Type
Ty where
  | 
nat: Ty
nat
  | 
bool: Ty
bool
  deriving 
DecidableEq: Sort u → Sort (max 1 u)
DecidableEq

inductive 
HasType: Expr → Ty → Prop
HasType : 
Expr: Type
Expr → 
Ty: Type
Ty → 
Prop: Type
Prop
  | 
nat: ∀ {v : Nat}, HasType (Expr.nat v) Ty.nat
nat  : 
HasType: Expr → Ty → Prop
HasType (
.nat: Nat → Expr
.nat 
v: Nat
v) 
.nat: Ty
.nat
  | 
plus: ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (Expr.plus a b) Ty.nat
plus : 
HasType: Expr → Ty → Prop
HasType 
a: Expr
a 
.nat: Ty
.nat → 
HasType: Expr → Ty → Prop
HasType 
b: Expr
b 
.nat: Ty
.nat → 
HasType: Expr → Ty → Prop
HasType (
.plus: Expr → Expr → Expr
.plus 
a: Expr
a 
b: Expr
b) 
.nat: Ty
.nat
  | 
bool: ∀ {v : Bool}, HasType (Expr.bool v) Ty.bool
bool : 
HasType: Expr → Ty → Prop
HasType (
.bool: Bool → Expr
.bool 
v: Bool
v) 
.bool: Ty
.bool
  | 
and: ∀ {a b : Expr}, HasType a Ty.bool → HasType b Ty.bool → HasType (Expr.and a b) Ty.bool
and  : 
HasType: Expr → Ty → Prop
HasType 
a: Expr
a 
.bool: Ty
.bool → 
HasType: Expr → Ty → Prop
HasType 
b: Expr
b 
.bool: Ty
.bool → 
HasType: Expr → Ty → Prop
HasType (
.and: Expr → Expr → Expr
.and 
a: Expr
a 
b: Expr
b) 
.bool: Ty
.bool

We can easily show that if e has type t₁ and type t₂, then t₁ and t₂ must be equal by using the the cases tactic. This tactic creates a new subgoal for every constructor, and automatically discharges unreachable cases. The tactic combinator tac₁ <;> tac₂ applies tac₂ to each subgoal produced by tac₁. Then, the tactic rfl is used to close all produced goals using reflexivity.

theorem 
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det (
h₁: HasType e t₁
h₁ : 
HasType: Expr → Ty → Prop
HasType 
e: Expr
e 
t₁: Ty
t₁) (
h₂: HasType e t₂
h₂ : 
HasType: Expr → Ty → Prop
HasType 
e: Expr
e 
t₂: Ty
t₂) : 
t₁: Ty
t₁ = 
t₂: Ty
t₂ := 
Goals accomplished! 🐙

  
t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
nat
Ty.nat = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (Expr.plus a✝² b✝) t₂
Ty.nat = t₂
t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂
Ty.bool = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (Expr.and a✝² b✝) t₂
Ty.bool = t₂
 
t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
nat
Ty.nat = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (Expr.plus a✝² b✝) t₂
Ty.nat = t₂
t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂
Ty.bool = t₂
t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (Expr.and a✝² b✝) t₂
Ty.bool = t₂
 
a✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.bool
a✝²: HasType b✝ Ty.bool
a✝¹: HasType a✝⁴ Ty.bool
a✝: HasType b✝ Ty.bool
and.and
Ty.bool = Ty.bool
 
v✝: Nat
nat.nat
Ty.nat = Ty.nat
a✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.nat
a✝²: HasType b✝ Ty.nat
a✝¹: HasType a✝⁴ Ty.nat
a✝: HasType b✝ Ty.nat
Ty.nat = Ty.nat
v✝: Bool
Ty.bool = Ty.bool
a✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.bool
a✝²: HasType b✝ Ty.bool
a✝¹: HasType a✝⁴ Ty.bool
a✝: HasType b✝ Ty.bool
Ty.bool = Ty.bool
 
Goals accomplished! 🐙

The inductive type Maybe p has two constructors: found a h and unknown. The former contains an element a : α and a proof that a satisfies the predicate p. The constructor unknown is used to encode "failure".

inductive 
Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe (
p: α → Prop
p : 
α: Sort u_1
α → 
Prop: Type
Prop) where
  | 
found: {α : Sort u_1} → {p : α → Prop} → (a : α) → p a → Maybe p
found : (
a: α
a : 
α: Sort u_1
α) → 
p: α → Prop
p 
a: α
a → 
Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe 
p: α → Prop
p
  | 
unknown: {α : Sort u_1} → {p : α → Prop} → Maybe p
unknown

We define a notation for Maybe that is similar to the builtin notation for the Lean builtin type Subtype.

notation "{{ " 
x: Lean.TSyntax `term
x " | " 
p: Lean.TSyntax `term
p " }}" => 
Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe (fun 
x: Lean.TSyntax `term
x => 
p: Lean.TSyntax `term
p)

The function Expr.typeCheck e returns a type ty and a proof that e has type ty, or unknown. Recall that, def Expr.typeCheck ... in Lean is notation for namespace Expr def typeCheck ... end Expr. The term .found .nat .nat is sugar for Maybe.found Ty.nat HasType.nat. Lean can infer the namespaces using the expected types.

def 
Expr.typeCheck: (e : Expr) → {{ ty | HasType e ty }}
Expr.typeCheck (
e: Expr
e : 
Expr: Type
Expr) : {{ 
ty: Ty
ty | 
HasType: Expr → Ty → Prop
HasType 
e: Expr
e 
ty: Ty
ty }} :=
  match 
e: Expr
e with
  | 
nat: Nat → Expr
nat ..   => 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.nat: Ty
.nat 
.nat: ∀ {v : Nat}, HasType (nat v) Ty.nat
.nat
  | 
bool: Bool → Expr
bool ..  => 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.bool: Ty
.bool 
.bool: ∀ {v : Bool}, HasType (bool v) Ty.bool
.bool
  | 
plus: Expr → Expr → Expr
plus 
a: Expr
a 
b: Expr
b =>
    match 
a: Expr
a.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck, 
b: Expr
b.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck with
    | 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.nat: Ty
.nat 
h₁: HasType a Ty.nat
h₁, 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.nat: Ty
.nat 
h₂: HasType b Ty.nat
h₂ => 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.nat: Ty
.nat (
.plus: ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (plus a b) Ty.nat
.plus 
h₁: HasType a Ty.nat
h₁ 
h₂: HasType b Ty.nat
h₂)
    | _, _ => 
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown
  | 
and: Expr → Expr → Expr
and 
a: Expr
a 
b: Expr
b =>
    match 
a: Expr
a.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck, 
b: Expr
b.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck with
    | 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.bool: Ty
.bool 
h₁: HasType a Ty.bool
h₁, 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.bool: Ty
.bool 
h₂: HasType b Ty.bool
h₂ => 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
.bool: Ty
.bool (
.and: ∀ {a b : Expr}, HasType a Ty.bool → HasType b Ty.bool → HasType (and a b) Ty.bool
.and 
h₁: HasType a Ty.bool
h₁ 
h₂: HasType b Ty.bool
h₂)
    | _, _ => 
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown

theorem 
Expr.typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → typeCheck e ≠ Maybe.unknown → typeCheck e = Maybe.found ty h
Expr.typeCheck_correct (
h₁: HasType e ty
h₁ : 
HasType: Expr → Ty → Prop
HasType 
e: Expr
e 
ty: Ty
ty) (
h₂: typeCheck e ≠ Maybe.unknown
h₂ : 
e: Expr
e.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck ≠ 
.unknown: {α : Sort ?u.23455} → {p : α → Prop} → Maybe p
.unknown)
        : 
e: Expr
e.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck = 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
ty: Ty
ty 
h: HasType e ty
h := 
Goals accomplished! 🐙

  
e: Expr
ty: Ty
h, h₁: HasType e ty
typeCheck e ≠ Maybe.unknown → typeCheck e = Maybe.found ty h

  
e: Expr
ty: Ty
h, h₁: HasType e ty
x✝: {{ ty | HasType e ty }}
x✝ ≠ Maybe.unknown → x✝ = Maybe.found ty h

  
e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
found
Maybe.found ty' h' ≠ Maybe.unknown → Maybe.found ty' h' = Maybe.found ty h
 
e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
h₂✝: Maybe.found ty' h' ≠ Maybe.unknown
found
Maybe.found ty' h' = Maybe.found ty h
; 
e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
h₂✝: Maybe.found ty' h' ≠ Maybe.unknown
this: ty = ty'
found
Maybe.found ty' h' = Maybe.found ty h
; 
e: Expr
ty: Ty
h, h₁, h': HasType e ty
h₂✝: Maybe.found ty h' ≠ Maybe.unknown
found
Maybe.found ty h' = Maybe.found ty h
; 
Goals accomplished! 🐙

  
e: Expr
ty: Ty
h, h₁: HasType e ty
unknown
Maybe.unknown ≠ Maybe.unknown → Maybe.unknown = Maybe.found ty h
 
e: Expr
ty: Ty
h, h₁: HasType e ty
h₂✝: Maybe.unknown ≠ Maybe.unknown
unknown
Maybe.unknown = Maybe.found ty h
; 
Goals accomplished! 🐙

Now, we prove that if Expr.typeCheck e returns Maybe.unknown, then forall ty, HasType e ty does not hold. The notation e.typeCheck is sugar for Expr.typeCheck e. Lean can infer this because we explicitly said that e has type Expr. The proof is by induction on e and case analysis. The tactic rename_i is used to to rename "inaccessible" variables. We say a variable is inaccessible if it is introduced by a tactic (e.g., cases) or has been shadowed by another variable introduced by the user. Note that the tactic simp [typeCheck] is applied to all goal generated by the induction tactic, and closes the cases corresponding to the constructors Expr.nat and Expr.bool.

theorem 
Expr.typeCheck_complete: ∀ {ty : Ty} {e : Expr}, typeCheck e = Maybe.unknown → ¬HasType e ty
Expr.typeCheck_complete {
e: Expr
e : 
Expr: Type
Expr} : 
e: Expr
e.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck = 
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown → ¬ 
HasType: Expr → Ty → Prop
HasType 
e: Expr
e 
ty: Ty
ty := 
Goals accomplished! 🐙

  
ty: Ty
e: Expr
typeCheck e = Maybe.unknown → ¬HasType e ty
 
Goals accomplished! 🐙

  
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
plus
(match typeCheck a, typeCheck b with
    | Maybe.found Ty.nat h₁, Maybe.found Ty.nat h₂ => Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat)
    | x, x_1 => Maybe.unknown) =
    Maybe.unknown →
  ¬HasType (plus a b) ty

    
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: typeCheck a = Maybe.found Ty.nat h₁✝
heq✝: typeCheck b = Maybe.found Ty.nat h₂✝
plus.h_1
Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown → ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (plus a b) ty

    
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: typeCheck a = Maybe.found Ty.nat h₁✝
heq✝: typeCheck b = Maybe.found Ty.nat h₂✝
plus.h_1
Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown → ¬HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (plus a b) ty
 
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: typeCheck a = Maybe.found Ty.nat h₁✝
heq✝: typeCheck b = Maybe.found Ty.nat h₂✝
a✝: Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown
¬HasType (plus a b) ty
; 
Goals accomplished! 🐙

    
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
plus.h_2
Maybe.unknown = Maybe.unknown → ¬HasType (plus a b) ty

      
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (plus a b) ty
 
Warning: unused variable `h` [linter.unusedVariables]
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (plus a b) ty
 
ht: HasType (plus a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (plus a b) ty
False

      
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (plus a b) ty
False

      
a, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
  typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.nat
h₂: HasType b Ty.nat
iha: typeCheck a = Maybe.unknown → ¬HasType a Ty.nat
ihb: typeCheck b = Maybe.unknown → ¬HasType b Ty.nat
plus
False
 
Goals accomplished! 🐙

  
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
and
(match typeCheck a, typeCheck b with
    | Maybe.found Ty.bool h₁, Maybe.found Ty.bool h₂ => Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool)
    | x, x_1 => Maybe.unknown) =
    Maybe.unknown →
  ¬HasType (and a b) ty

    
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: typeCheck a = Maybe.found Ty.bool h₁✝
heq✝: typeCheck b = Maybe.found Ty.bool h₂✝
and.h_1
Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown → ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (and a b) ty

    
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: typeCheck a = Maybe.found Ty.bool h₁✝
heq✝: typeCheck b = Maybe.found Ty.bool h₂✝
and.h_1
Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown → ¬HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (and a b) ty
 
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: typeCheck a = Maybe.found Ty.bool h₁✝
heq✝: typeCheck b = Maybe.found Ty.bool h₂✝
a✝: Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown
¬HasType (and a b) ty
; 
Goals accomplished! 🐙

    
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
and.h_2
Maybe.unknown = Maybe.unknown → ¬HasType (and a b) ty

      
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (and a b) ty
 
Warning: unused variable `h` [linter.unusedVariables]
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
Maybe.unknown = Maybe.unknown → ¬HasType (and a b) ty
 
ht: HasType (and a b) ty
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (and a b) ty
False

      
ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (and a b) ty
False

      
a, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
  typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.bool
h₂: HasType b Ty.bool
iha: typeCheck a = Maybe.unknown → ¬HasType a Ty.bool
ihb: typeCheck b = Maybe.unknown → ¬HasType b Ty.bool
and
False
  
Goals accomplished! 🐙

Finally, we show that type checking for e can be decided using Expr.typeCheck.

instance: (e : Expr) → (t : Ty) → Decidable (HasType e t)
instance (
e: Expr
e : 
Expr: Type
Expr) (
t: Ty
t : 
Ty: Type
Ty) : 
Decidable: Prop → Type
Decidable (
HasType: Expr → Ty → Prop
HasType 
e: Expr
e 
t: Ty
t) :=
  match 
h': Expr.typeCheck e = Maybe.unknown
h' : 
e: Expr
e.
typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck with
  | 
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found 
t': Ty
t' 
ht': HasType e t'
ht' =>
    if 
heq: t = t'
heq : 
t: Ty
t = 
t': Ty
t' then
      
isTrue: {p : Prop} → p → Decidable p
isTrue (
heq: t = t'
heq ▸ 
ht': HasType e t'
ht')
    else
      
isFalse: {p : Prop} → ¬p → Decidable p
isFalse fun 
ht: HasType e t
ht => 
heq: ¬t = t'
heq (
HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det 
ht: HasType e t
ht 
ht': HasType e t'
ht')
  | 
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown => 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse (
Expr.typeCheck_complete: ∀ {ty : Ty} {e : Expr}, Expr.typeCheck e = Maybe.unknown → ¬HasType e ty
Expr.typeCheck_complete 
h': Expr.typeCheck e = Maybe.unknown
h')

The Well-Typed Interpreter

In this example, we build an interpreter for a simple functional programming language, with variables, function application, binary operators and an if...then...else construct. We will use the dependent type system to ensure that any programs which can be represented are well-typed.

Remark: this example is based on an example found in the Idris manual.

Vectors

A Vector is a list of size n whose elements belong to a type α.

inductive 
Vector: Type u → Nat → Type u
Vector (
α: Type u
α : 
Type u: Type (u + 1)
Type u) : 
Nat: Type
Nat → 
Type u: Type (u + 1)
Type u
  | 
nil: {α : Type u} → Vector α 0
nil : 
Vector: Type u → Nat → Type u
Vector 
α: Type u
α 
0: Nat
0
  | 
cons: {α : Type u} → {n : Nat} → α → Vector α n → Vector α (n + 1)
cons : 
α: Type u
α → 
Vector: Type u → Nat → Type u
Vector 
α: Type u
α 
n: Nat
n → 
Vector: Type u → Nat → Type u
Vector 
α: Type u
α (
n: Nat
n+
1: Nat
1)

We can overload the List.cons notation :: and use it to create Vectors.

infix:67 " :: " => 
Vector.cons: {α : Type u} → {n : Nat} → α → Vector α n → Vector α (n + 1)
Vector.cons

Now, we define the types of our simple functional language. We have integers, booleans, and functions, represented by Ty.

inductive 
Ty: Type
Ty where
  | 
int: Ty
int
  | 
bool: Ty
bool
  | 
fn: Ty → Ty → Ty
fn (
a: Ty
a 
r: Ty
r : 
Ty: Type
Ty)

We can write a function to translate Ty values to a Lean type — remember that types are first class, so can be calculated just like any other value. We mark Ty.interp as [reducible] to make sure the typeclass resolution procedure can unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance Add (Ty.interp Ty.int). Since Ty.interp is marked as [reducible], the typeclass resolution procedure can reduce Ty.interp Ty.int to Int, and use the builtin instance for Add Int as the solution.

@[reducible] def 
Ty.interp: Ty → Type
Ty.interp : 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
int: Ty
int    => 
Int: Type
Int
  | 
bool: Ty
bool   => 
Bool: Type
Bool
  | 
fn: Ty → Ty → Ty
fn 
a: Ty
a 
r: Ty
r => 
a: Ty
a.
interp: Ty → Type
interp → 
r: Ty
r.
interp: Ty → Type
interp

Expressions are indexed by the types of the local variables, and the type of the expression itself.

inductive 
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType : 
Fin: Nat → Type
Fin 
n: Nat
n → 
Vector: Type → Nat → Type
Vector 
Ty: Type
Ty 
n: Nat
n → 
Ty: Type
Ty → 
Type: Type 1
Type where
  | 
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop : 
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType 
0: Fin (?m.8928 + 1)
0 (
ty: Ty
ty :: 
ctx: Vector Ty ?m.8928
ctx) 
ty: Ty
ty
  | 
pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) ty
pop  : 
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType 
k: Fin ?m.9102
k 
ctx: Vector Ty ?m.9102
ctx 
ty: Ty
ty → 
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType 
k: Fin ?m.9102
k.
succ: {n : Nat} → Fin n → Fin (Nat.succ n)
succ (
u: Ty
u :: 
ctx: Vector Ty ?m.9102
ctx) 
ty: Ty
ty

inductive 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr : 
Vector: Type → Nat → Type
Vector 
Ty: Type
Ty 
n: Nat
n → 
Ty: Type
Ty → 
Type: Type 1
Type where
  | 
var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var   : 
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType 
i: Fin ?m.9859
i 
ctx: Vector Ty ?m.9859
ctx 
ty: Ty
ty → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.9859
ctx 
ty: Ty
ty
  | 
val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val   : 
Int: Type
Int → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.9880
ctx 
Ty.int: Ty
Ty.int
  | 
lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam   : 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr (
a: Ty
a :: 
ctx: Vector Ty ?m.10034
ctx) 
ty: Ty
ty → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10034
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
a: Ty
a 
ty: Ty
ty)
  | 
app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
app   : 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10181
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
a: Ty
a 
ty: Ty
ty) → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10181
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10181
ctx 
ty: Ty
ty
  | 
op: {n : Nat} →
  {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op    : (
a: Ty
a.
interp: Ty → Type
interp → 
b: Ty
b.
interp: Ty → Type
interp → 
c: Ty
c.
interp: Ty → Type
interp) → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10271
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10271
ctx 
b: Ty
b → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10271
ctx 
c: Ty
c
  | 
ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife   : 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10392
ctx 
Ty.bool: Ty
Ty.bool → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10392
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10392
ctx 
a: Ty
a → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10392
ctx 
a: Ty
a
  | 
delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay : (
Unit: Type
Unit → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10435
ctx 
a: Ty
a) → 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.10435
ctx 
a: Ty
a

We use the command open to create the aliases stop and pop for HasType.stop and HasType.pop respectively.

open HasType (
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop 
pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) ty
pop)

Since expressions are indexed by their type, we can read the typing rules of the language from the definitions of the constructors. Let us look at each constructor in turn.

We use a nameless representation for variables — they are de Bruijn indexed. Variables are represented by a proof of their membership in the context, HasType i ctx ty, which is a proof that variable i in context ctx has type ty.

We can treat stop as a proof that the most recently defined variable is well-typed, and pop n as a proof that, if the nth most recently defined variable is well-typed, so is the n+1th. In practice, this means we use stop to refer to the most recently defined variable, pop stop to refer to the next, and so on, via the Expr.var constructor.

A value Expr.val carries a concrete representation of an integer.

A lambda Expr.lam creates a function. In the scope of a function of type Ty.fn a ty, there is a new local variable of type a.

A function application Expr.app produces a value of type ty given a function from a to ty and a value of type a.

The constructor Expr.op allows us to use arbitrary binary operators, where the type of the operator informs what the types of the arguments must be.

Finally, the constructor Exp.ife represents a if-then-else expression. The condition is a Boolean, and each branch must have the same type.

The auxiliary constructor Expr.delay is used to delay evaluation.

When we evaluate an Expr, we’ll need to know the values in scope, as well as their types. Env is an environment, indexed over the types in scope. Since an environment is just another form of list, albeit with a strongly specified connection to the vector of local variable types, we overload again the notation :: so that we can use the usual list syntax. Given a proof that a variable is defined in the context, we can then produce a value from the environment.

inductive 
Env: {n : Nat} → Vector Ty n → Type
Env : 
Vector: Type → Nat → Type
Vector 
Ty: Type
Ty 
n: Nat
n → 
Type: Type 1
Type where
  | 
nil: Env Vector.nil
nil  : 
Env: {n : Nat} → Vector Ty n → Type
Env 
Vector.nil: {α : Type} → Vector α 0
Vector.nil
  | 
cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)
cons : 
Ty.interp: Ty → Type
Ty.interp 
a: Ty
a → 
Env: {n : Nat} → Vector Ty n → Type
Env 
ctx: Vector Ty ?m.14745
ctx → 
Env: {n : Nat} → Vector Ty n → Type
Env (
a: Ty
a :: 
ctx: Vector Ty ?m.14745
ctx)

infix:67 " :: " => 
Env.cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)
Env.cons

def 
Env.lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp ty
Env.lookup : 
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType 
i: Fin ?m.23254
i 
ctx: Vector Ty ?m.23254
ctx 
ty: Ty
ty → 
Env: {n : Nat} → Vector Ty n → Type
Env 
ctx: Vector Ty ?m.23254
ctx → 
ty: Ty
ty.
interp: Ty → Type
interp
  | 
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop,  
x: Ty.interp ty
x :: 
xs: Env ctx✝
xs => 
x: Ty.interp ty
x
  | 
pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) ty
pop 
k: HasType k✝ ctx✝ ty
k, 
x: Ty.interp u✝
x :: 
xs: Env ctx✝
xs => 
lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp ty
lookup 
k: HasType k✝ ctx✝ ty
k 
xs: Env ctx✝
xs

Given this, an interpreter is a function which translates an Expr into a Lean value with respect to a specific environment.

def 
Expr.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
Expr.interp (
env: Env ctx
env : 
Env: {n : Nat} → Vector Ty n → Type
Env 
ctx: Vector Ty ?m.28662
ctx) : 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.28662
ctx 
ty: Ty
ty → 
ty: Ty
ty.
interp: Ty → Type
interp
  | 
var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
i: HasType i✝ ctx ty
i     => 
env: Env ctx
env.
lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp ty
lookup 
i: HasType i✝ ctx ty
i
  | 
val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val 
x: Int
x     => 
x: Int
x
  | 
lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam 
b: Expr (a✝ :: ctx) ty✝
b     => fun 
x: Ty.interp a✝
x => 
b: Expr (a✝ :: ctx) ty✝
b.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp (
Env.cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)
Env.cons 
x: Ty.interp a✝
x 
env: Env ctx
env)
  | 
app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
app 
f: Expr ctx (Ty.fn a✝ ty)
f 
a: Expr ctx a✝
a   => 
f: Expr ctx (Ty.fn a✝ ty)
f.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env (
a: Expr ctx a✝
a.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env)
  | 
op: {n : Nat} →
  {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op 
o: Ty.interp a✝ → Ty.interp b✝ → Ty.interp ty
o 
x: Expr ctx a✝
x 
y: Expr ctx b✝
y  => 
o: Ty.interp a✝ → Ty.interp b✝ → Ty.interp ty
o (
x: Expr ctx a✝
x.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env) (
y: Expr ctx b✝
y.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env)
  | 
ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife 
c: Expr ctx Ty.bool
c 
t: Expr ctx ty
t 
e: Expr ctx ty
e => if 
c: Expr ctx Ty.bool
c.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env then 
t: Expr ctx ty
t.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env else 
e: Expr ctx ty
e.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env
  | 
delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay 
a: Unit → Expr ctx ty
a   => (
a: Unit → Expr ctx ty
a 
(): Unit
()).
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
env: Env ctx
env

open Expr

We can make some simple test functions. Firstly, adding two inputs fun x y => y + x is written as follows.

def 
add: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int))
add : 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.36312
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
Ty.int: Ty
Ty.int (
Ty.fn: Ty → Ty → Ty
Ty.fn 
Ty.int: Ty
Ty.int 
Ty.int: Ty
Ty.int)) :=
  
lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam (
lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam (
op: {n : Nat} →
  {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·+·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.int
(·+·) (
var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop) (
var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var (
pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) ty
pop 
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop))))


30

 
add: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int))
add.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
Env.nil: Env Vector.nil
Env.nil 
10: Ty.interp Ty.int
10 
20: Ty.interp Ty.int
20

More interestingly, a factorial function fact (e.g. fun x => if (x == 0) then 1 else (fact (x-1) * x)), can be written as. Note that this is a recursive (non-terminating) definition. For every input value, the interpreter terminates, but the definition itself is non-terminating. We use two tricks to make sure Lean accepts it. First, we use the auxiliary constructor Expr.delay to delay its unfolding. Second, we add the annotation decreasing_by sorry which can be viewed as "trust me, this recursive definition makes sense". Recall that sorry is an unsound axiom in Lean.

def 
Warning: declaration uses 'sorry'
 : 
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr 
ctx: Vector Ty ?m.39574
ctx (
Ty.fn: Ty → Ty → Ty
Ty.fn 
Ty.int: Ty
Ty.int 
Ty.int: Ty
Ty.int) :=
  
lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam (
ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife (
op: {n : Nat} →
  {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·==·): Ty.interp Ty.int → Ty.interp Ty.int → Bool
(·==·) (
var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop) (
val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val 
0: Int
0))
           (
val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val 
1: Int
1)
           (
op: {n : Nat} →
  {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·*·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.int
(·*·) (
delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay fun 
_: Unit
_ => 
app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
app 
fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)
fact (
op: {n : Nat} →
  {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op 
(·-·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.int
(·-·) (
var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop) (
val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val 
1: Int
1))) (
var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var 
stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop)))
  decreasing_by 
Goals accomplished! 🐙



3628800

 
fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)
fact.
interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp 
Env.nil: Env Vector.nil
Env.nil 
10: Ty.interp Ty.int
10

Dependent de Bruijn Indices

In this example, we represent program syntax terms in a type family parameterized by a list of types, representing the typing context, or information on which free variables are in scope and what their types are.

Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.

Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a “type-level” list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Lean.

We parameterize our heterogeneous lists by at type α and an α-indexed type β.

inductive 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList {
α: Type v
α : 
Type v: Type (v + 1)
Type v} (
β: α → Type u
β : 
α: Type v
α → 
Type u: Type (u + 1)
Type u) : 
List: Type v → Type v
List 
α: Type v
α → 
Type (max u v): Type ((max u v) + 1)
Type (max u v)
  | 
nil: {α : Type v} → {β : α → Type u} → HList β []
nil  : 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList 
β: α → Type u
β 
[]: List α
[]
  | 
cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
cons : 
β: α → Type u
β 
i: α
i → 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList 
β: α → Type u
β 
is: List α
is → 
HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList 
β: α → Type u
β (
i: α
i::
is: List α
is)

We overload the List.cons notation :: so we can also use it to create heterogeneous lists.

infix:67 " :: " => 
HList.cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
HList.cons

We similarly overload the List notation [] for the empty heterogeneous list.

notation "[" "]" => 
HList.nil: {α : Type v} → {β : α → Type u} → HList β []
HList.nil

Variables are represented in a way isomorphic to the natural numbers, where number 0 represents the first element in the context, number 1 the second element, and so on. Actually, instead of numbers, we use the Member inductive family.

The value of type Member a as can be viewed as a certificate that a is an element of the list as. The constructor Member.head says that a is in the list if the list begins with it. The constructor Member.tail says that if a is in the list bs, it is also in the list b::bs.

inductive 
Member: {α : Type} → α → List α → Type
Member : 
α: Type
α → 
List: Type → Type
List 
α: Type
α → 
Type: Type 1
Type
  | 
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head : 
Member: {α : Type} → α → List α → Type
Member 
a: ?m.14887
a (
a: ?m.14887
a::
as: List ?m.14887
as)
  | 
tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail : 
Member: {α : Type} → α → List α → Type
Member 
a: ?m.15049
a 
bs: List ?m.15049
bs → 
Member: {α : Type} → α → List α → Type
Member 
a: ?m.15049
a (
b: ?m.15049
b::
bs: List ?m.15049
bs)

Given a heterogeneous list HList β is and value of type Member i is, HList.get retrieves an element of type β i from the list. The pattern .head and .tail h are sugar for Member.head and Member.tail h respectively. Lean can infer the namespace using the expected type.

def 
HList.get: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β i
HList.get : 
HList: {α : Type} → (α → Type u_1) → List α → Type u_1
HList 
β: ?m.15578 → Type u_1
β 
is: List ?m.15578
is → 
Member: {α : Type} → α → List α → Type
Member 
i: ?m.15578
i 
is: List ?m.15578
is → 
β: ?m.15578 → Type u_1
β 
i: ?m.15578
i
  | 
a: β i
a::
as: HList β is✝
as, 
.head: Member i (i :: is✝)
.head => 
a: β i
a
  | 
Warning: unused variable `a` [linter.unusedVariables]
::
as: HList β is✝
as, 
.tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
.tail 
h: Member i is✝
h => 
as: HList β is✝
as.
get: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β i
get 
h: Member i is✝
h

Here is the definition of the simple type system for our programming language, a simply typed lambda calculus with natural numbers as the base type.

inductive 
Ty: Type
Ty where
  | 
nat: Ty
nat
  | 
fn: Ty → Ty → Ty
fn : 
Ty: Type
Ty → 
Ty: Type
Ty → 
Ty: Type
Ty

We can write a function to translate Ty values to a Lean type — remember that types are first class, so can be calculated just like any other value. We mark Ty.denote as [reducible] to make sure the typeclass resolution procedure can unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance Add (Ty.denote Ty.nat). Since Ty.denote is marked as [reducible], the typeclass resolution procedure can reduce Ty.denote Ty.nat to Nat, and use the builtin instance for Add Nat as the solution.

Recall that the term a.denote is sugar for denote a where denote is the function being defined. We call it the "dot notation".

@[reducible] def 
Ty.denote: Ty → Type
Ty.denote : 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
nat: Ty
nat    => 
Nat: Type
Nat
  | 
fn: Ty → Ty → Ty
fn 
a: Ty
a 
b: Ty
b => 
a: Ty
a.
denote: Ty → Type
denote → 
b: Ty
b.
denote: Ty → Type
denote

Here is the definition of the Term type, including variables, constants, addition, function application and abstraction, and let binding of local variables. Since let is a keyword in Lean, we use the "escaped identifier" «let». You can input the unicode (French double quotes) using \f<< (for «) and \f>> (for »). The term Term ctx .nat is sugar for Term ctx Ty.nat, Lean infers the namespace using the expected type.

inductive 
Term: List Ty → Ty → Type
Term : 
List: Type → Type
List 
Ty: Type
Ty → 
Ty: Type
Ty → 
Type: Type 1
Type
  | 
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var   : 
Member: {α : Type} → α → List α → Type
Member 
ty: Ty
ty 
ctx: List Ty
ctx → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty: Ty
ty
  | 
const: {ctx : List Ty} → Nat → Term ctx Ty.nat
const : 
Nat: Type
Nat → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat
  | 
plus: {ctx : List Ty} → Term ctx Ty.nat → Term ctx Ty.nat → Term ctx Ty.nat
plus  : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
.nat: Ty
.nat
  | 
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (Ty.fn dom ran) → Term ctx dom → Term ctx ran
app   : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx (
.fn: Ty → Ty → Ty
.fn 
dom: Ty
dom 
ran: Ty
ran) → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
dom: Ty
dom → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ran: Ty
ran
  | 
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (Ty.fn dom ran)
lam   : 
Term: List Ty → Ty → Type
Term (
dom: Ty
dom :: 
ctx: List Ty
ctx) 
ran: Ty
ran → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx (
.fn: Ty → Ty → Ty
.fn 
dom: Ty
dom 
ran: Ty
ran)
  | 
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty₁: Ty
ty₁ → 
Term: List Ty → Ty → Type
Term (
ty₁: Ty
ty₁ :: 
ctx: List Ty
ctx) 
ty₂: Ty
ty₂ → 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty₂: Ty
ty₂

Here are two example terms encoding, the first addition packaged as a two-argument curried function, and the second of a sample application of addition to constants.

The command open Ty Term Member opens the namespaces Ty, Term, and Member. Thus, you can write lam instead of Term.lam.

open Ty Term Member
def 
add: Term [] (fn nat (fn nat nat))
add : 
Term: List Ty → Ty → Type
Term 
[]: List Ty
[] (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat (
fn: Ty → Ty → Ty
fn 
nat: Ty
nat 
nat: Ty
nat)) :=
  
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam (
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam (
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus (
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var (
tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail 
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head)) (
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var 
head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head)))

def 
three_the_hard_way: Term [] nat
three_the_hard_way : 
Term: List Ty → Ty → Type
Term 
[]: List Ty
[] 
nat: Ty
nat :=
  
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app (
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app 
add: Term [] (fn nat (fn nat nat))
add (
const: {ctx : List Ty} → Nat → Term ctx nat
const 
1: Nat
1)) (
const: {ctx : List Ty} → Nat → Term ctx nat
const 
2: Nat
2)

Since dependent typing ensures that any term is well-formed in its context and has a particular type, it is easy to translate syntactic terms into Lean values.

The attribute [simp] instructs Lean to always try to unfold Term.denote applications when one applies the simp tactic. We also say this is a hint for the Lean term simplifier.

@[simp] def 
Term.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
Term.denote : 
Term: List Ty → Ty → Type
Term 
ctx: List Ty
ctx 
ty: Ty
ty → 
HList: {α : Type} → (α → Type) → List α → Type
HList 
Ty.denote: Ty → Type
Ty.denote 
ctx: List Ty
ctx → 
ty: Ty
ty.
denote: Ty → Type
denote
  | 
var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var 
h: Member ty ctx
h,     
env: HList Ty.denote ctx
env => 
env: HList Ty.denote ctx
env.
get: {α : Type} → {β : α → Type} → {is : List α} → {i : α} → HList β is → Member i is → β i
get 
h: Member ty ctx
h
  | 
const: {ctx : List Ty} → Nat → Term ctx nat
const 
n: Nat
n,   _   => 
n: Nat
n
  | 
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus 
a: Term ctx nat
a 
b: Term ctx nat
b,  
env: HList Ty.denote ctx
env => 
a: Term ctx nat
a.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote 
env: HList Ty.denote ctx
env + 
b: Term ctx nat
b.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote 
env: HList Ty.denote ctx
env
  | 
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app 
f: Term ctx (fn dom✝ ty)
f 
a: Term ctx dom✝
a,   
env: HList Ty.denote ctx
env => 
f: Term ctx (fn dom✝ ty)
f.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote 
env: HList Ty.denote ctx
env (
a: Term ctx dom✝
a.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote 
env: HList Ty.denote ctx
env)
  | 
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam 
b: Term (dom✝ :: ctx) ran✝
b,     
env: HList Ty.denote ctx
env => fun 
x: Ty.denote dom✝
x => 
b: Term (dom✝ :: ctx) ran✝
b.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote (
x: Ty.denote dom✝
x :: 
env: HList Ty.denote ctx
env)
  | 
«let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» 
a: Term ctx ty₁✝
a 
b: Term (ty₁✝ :: ctx) ty
b, 
env: HList Ty.denote ctx
env => 
b: Term (ty₁✝ :: ctx) ty
b.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote (
a: Term ctx ty₁✝
a.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote 
env: HList Ty.denote ctx