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.

  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 'nightly'
    info: latest update on nightly, lean version nightly-2021-12-05
    info: downloading component 'lean'
    
  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

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 & stable releases via elan (see above)

  • 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 & stable 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 (M1) macOS

Setting Up Lean

There are currently two ways to set up a Lean 4 development environment:

  • basic setup (Linux/macOS/Windows): uses elan + your preinstalled editor
  • Nix setup (Linux/macOS/WSL): uses the Nix package manager for installing all dependencies localized to your project

See also the quickstart instructions for using the basic setup with VS Code as the editor.

Basic Setup

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 release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable
# alternatively, use the latest nightly build (https://github.com/leanprover/lean4-nightly/releases)
$ elan default leanprover/lean4:nightly
# alternatively, activate Lean 4 in current directory only
$ elan override set 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).

Nix Setup

The alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension. However, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling Nix Flakes. The setup has been tested on NixOS, other Linux distributions, and macOS.

After installing (any version of) Nix (https://nixos.org/download.html), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):

$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix

While this shell is sufficient for executing the steps below, it is recommended to also set the following options in /etc/nix/nix.conf (nix.extraOptions in NixOS):

max-jobs = auto  # Allow building multiple derivations in parallel
keep-outputs = true  # Do not garbage-collect build time-only dependencies (e.g. clang)
# Allow fetching build results from the Lean Cachix cache
trusted-substituters = https://lean4.cachix.org/
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=

On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:

sudo pkill nix-daemon

The Cachix integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above. It can be set up analogously as a cache for your own project.

Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.

Basic Commands

From a Lean shell, run

$ nix flake new mypkg -t github:leanprover/lean4

to create a new Lean package in directory mypkg using the latest commit of Lean 4. Such packages follow the same directory layout as described in the basic setup above, except for a lakefile.lean replaced by a flake.nix file set up so you can run Nix commands on it, for example:

$ nix build  # build package and all dependencies
$ nix build .#executable  # compile `main` definition into executable (after you've added one)
$ nix run .#emacs-dev  # open a pinned version of Emacs with lean4-mode fully set up
$ nix run .#emacs-dev MyPackage.lean  # arguments can be passed as well, e.g. the file to open
$ nix run .#vscode-dev MyPackage.lean  # ditto, using VS Code

Note that if you rename MyPackage.lean, you also have to adjust the name attribute in flake.nix accordingly. Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.

As in the basic setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.

If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the lean wrapper script the commands above use internally:

$ nix build .#lean-dev -o result-lean-dev

The resulting ./result-lean-dev/bin/lean script essentially runs nix run .#lean in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed. This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are working on Lean itself.

Package dependencies can be added as further input flakes and passed to the deps list of buildLeanPackage. Example: https://github.com/Kha/testpkg2/blob/master/flake.nix#L5

For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:

$ nix build --override-input somedep path/to/somedep

On a build error, Nix will show the last 10 lines of the output by default. You can pass -L to nix build to show all lines, or pass the shown *.drv path to nix log to show the full log after the fact.

Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when /nix/store/ has grown too large:

nix-collect-garbage

This will remove everything not reachable from "GC roots" such as the ./result symlink created by nix build.

Note that the package information in flake.nix is currently completely independent from lakefile.lean used in the basic setup. Unifying the two formats is TBD.

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.

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.18
[]
|
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.580
as
) :
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.580
as
.
reverse: {α : Type u_1} → List α → List α
reverse
:=
α✝: Type u_1
as: List α
h: Palindrome as

Palindrome (List.reverse as)
α✝: 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.942
as
) :
as: List ?m.942
as
.
reverse: {α : Type u_1} → List α → List α
reverse
=
as: List ?m.942
as
:=
α✝: Type u_1
as: List α
h: Palindrome as

List.reverse as = as
α✝: 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]

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.1230
as
) :
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.1230
as
.
reverse: {α : Type u_1} → List α → List α
reverse
:=
α✝: Type ?u.1226
as: List α
h: Palindrome as

Palindrome (List.reverse as)

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₁
::
a₂: α
a₂
::
as: List α
as
, _ => (
a₂: α
a₂
::
as: List α
as
).
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last
(
α: Type ?u.1276
a₁, a₂: α
as: List α

a₂ :: as []

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.1764
as
[]: List ?m.1764
[]
) :
as: List ?m.1764
as
.
dropLast: {α : Type u_1} → List α → List α
dropLast
++ [
as: List ?m.1764
as
.
last: {α : Type u_1} → (as : List α) → as ≠ [] → α
last
h: as ≠ []
h
] =
as: List ?m.1764
as
:=
α✝: Type u_1
as: List α
h: as []

dropLast as ++ [last as h] = as
α✝: 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
α✝: Type u_1
as✝: List α
a₁, a₂: α
as: List α
h: a₁ :: a₂ :: as []

a₂ :: as []

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
(
α: Type u_1
motive: List α Prop
h₁: motive []
h₂: (a : α), motive [a]
h₃: (a b : α) (as : List α), motive as motive ([a] ++ as ++ [b])
as: List α
a₁, a₂: α
as': List α
ih: motive (dropLast (a₂ :: as'))

a₂ :: as' []

Goals accomplished! 🐙
)] =
a₁: α
a₁
::
a₂: α
a₂
::
as': List α
as'
:=
α: Type u_1
motive: List α Prop
h₁: motive []
h₂: (a : α), motive [a]
h₃: (a b : α) (as : List α), motive as motive ([a] ++ as ++ [b])
as: List α
a₁, a₂: α
as': List α
ih: motive (dropLast (a₂ :: as'))

[a₁] ++ dropLast (a₂ :: as') ++ [last (a₂ :: as') (_ : ¬a₂ :: as' = [])] = a₁ :: a₂ :: as'

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.8775
as
.
reverse: {α : Type u_1} → List α → List α
reverse
=
as: List ?m.8775
as
) :
Palindrome: {α : Type u_1} → List α → Prop
Palindrome
as: List ?m.8775
as
:=
α✝: Type u_1
as: List α
h: reverse as = as

Palindrome as
α✝: Type u_1
h: reverse [] = []

h₁
Palindrome []
α✝: Type u_1
a✝: α
h: reverse [a] = [a]
Palindrome [a]
α✝: Type u_1
a✝¹, b✝: α
as✝: List α
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 α
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 α
h: reverse ([a✝¹] ++ as ++ [b]) = [a✝¹] ++ as ++ [b]
Palindrome ([a✝¹] ++ as ++ [b])

Goals accomplished! 🐙
α✝: Type u_1
a✝¹, b✝: α
as✝: List α
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])
α✝: Type u_1
a, b: α
as: List α
ih: reverse as = as Palindrome as
h: reverse ([a] ++ as ++ [b]) = [a] ++ as ++ [b]

a = b

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])
α✝: Type u_1
a: α
as: List α
ih: reverse as = as Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]

reverse as = as

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
:=
α: Type u_1
inst✝: DecidableEq α
as: List α

isPalindrome as = true Palindrome as
α: 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 "Sofware 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.1270} → Tree β
leaf
=>
false: Bool
false
|
node: {β : Type ?u.1279} → 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
.
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.1603} → Tree β
leaf
=>
none: {α : Type u_1} → Option α
none
|
node: {β : Type ?u.1615} → 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.1944} → 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.1959} → 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.2304} → Tree β
leaf
=>
[]: List (Nat × β)
[]
|
node: {β : Type ?u.2316} → 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 implemention 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 concatentations 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.2796} → Tree β
leaf
=>
acc: List (Nat × β)
acc
|
node: {β : Type ?u.2806} → Tree β → Nat → β → Tree β → Tree β
node
l: Tree β
l
k: Nat
k
v: β
v
r: Tree β
r
=>
l: Tree β
l
.
go: Tree β → List (Nat × β) → List (Nat × β)
go
((
k: Nat
k
,
v: β
v
) ::
r: Tree β
r
.
go: Tree β → List (Nat × β) → List (Nat × β)
go
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 * intructs 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 intructs 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
:=
β: Type u_1
t: Tree β

toList t = toListTR t

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
:=
β: Type u_1
t✝, t: Tree β
acc: List (Nat × β)

toListTR.go t acc = toList t ++ 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 β
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 β
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
:=

@toList = @toListTR
β: 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
v: ?m.4798
v
=>
k: Nat
k
<
key: Nat
key
)
left: Tree ?m.4798
left
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
(fun
k: Nat
k
v: ?m.4798
v
=>
key: Nat
key
<
k: Nat
k
)
right: Tree ?m.4798
right
BST: {β : Type u_1} → Tree β → Prop
BST
left: Tree ?m.4798
left
BST: {β : Type u_1} → Tree β → Prop
BST
right: Tree ?m.4798
right
BST: {β : Type u_1} → Tree β → Prop
BST
(
.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
.node
left: Tree ?m.4798
left
key: Nat
key
value: ?m.4798
value
right: Tree ?m.4798
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.Syntax
lhs
:term:max
rhs: Lean.Syntax
rhs
:term:max : tactic => `((have h : $
lhs: Lean.Syntax
lhs
:term = $
rhs: Lean.Syntax
rhs
:term := -- TODO: replace with linarith by simp_arith at *; apply Nat.le_antisymm <;> assumption try subst $
lhs: Lean.Syntax
lhs
:term))

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 simplier 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.Syntax
e
:term : tactic => `(by_cases $
e: Lean.Syntax
e
:term <;> 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.6717 → Prop
p
t: Tree ?m.6717
t
) (
h₂: p key value
h₂
:
p: Nat → ?m.6717 → Prop
p
key: Nat
key
value: ?m.6717
value
) :
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
p: Nat → ?m.6717 → Prop
p
(
t: Tree ?m.6717
t
.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert
key: Nat
key
value: ?m.6717
value
) :=
β✝: 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₁: 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)

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)
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)

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)

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)

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)
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)

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)

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)

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
) :=
β: Type u_1
t: Tree β
h: BST t
key: Nat
value: β

BST (insert t key value)
β: 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)

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)
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)

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)

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)

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)
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)

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)

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)

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
β
) :=
β: Type u_1
k: Nat

find? mk k = none

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
:=
β: Type u_1
b: BinTree β
k: Nat
v: β

find? (insert b k v) k = some v
β: 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

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)

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.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)
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)

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

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

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)

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)

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

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

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.13246 → Type ?u.13246
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'
:=
β: Type u_1
k, k': Nat
b: BinTree β
h: k k'
v: β

find? (insert b k v) k' = find? b k'
β: Type u_1
k, k': Nat
b: BinTree β
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 β
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 β
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 β
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 β
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 β
v: β
h: BST Tree.leaf

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

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

leaf.inr
(if k < k' then none else some v) = none

Goals accomplished! 🐙
β: Type u_1
k, k': Nat
b: BinTree β
v: β
h: BST Tree.leaf

leaf.inr.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
v: β
h: BST Tree.leaf
False
β: Type u_1
k, k': Nat
b: BinTree β
v: β
h: BST Tree.leaf

leaf.inr.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
v: β
h: BST Tree.leaf
False
β: Type u_1
k, k': Nat
b: BinTree β
v: β
h: BST Tree.leaf

leaf.inr.inr
False
β: Type u_1
k': Nat
b: BinTree β
v: β
h: k' k'

leaf.inr.inr
False

Goals accomplished! 🐙
β: Type u_1
k, k': Nat
b: BinTree β
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 β
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 β
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 β
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 β
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.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 β
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.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 β
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

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 β
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

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 β
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

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
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

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₂
:=
e: Expr
t₁, t₂: Ty
h₁: HasType e t₁
h₂: HasType e t₂

t₁ = t₂
t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v) t₂

nat
Ty.nat = t₂
t₂: Ty
a✝², b✝: Expr
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
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
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
h₂: HasType (Expr.and a✝² b) t₂
Ty.bool = t₂
v✝: Nat

nat.nat
Ty.nat = Ty.nat
a✝⁴, b✝: Expr

plus.plus
Ty.nat = Ty.nat

Goals accomplished! 🐙

The inductive type Maybe p has two contructors: 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.Syntax
x
" | "
p: Lean.Syntax
p
" }}" => Maybe (fun
x: Lean.Syntax
x
=>
p: Lean.Syntax
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) → Maybe fun 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) → Maybe fun ty => HasType e ty
typeCheck
,
b: Expr
b
.
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
with |
.found .nat h₁: Maybe fun ty => HasType a ty
.found
.nat: Ty
.nat
.found .nat h₁: Maybe fun ty => HasType a ty
h₁: HasType a Ty.nat
h₁
,
.found .nat h₂: Maybe fun ty => HasType b ty
.found
.nat: Ty
.nat
.found .nat h₂: Maybe fun ty => HasType b ty
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) → Maybe fun ty => HasType e ty
typeCheck
,
b: Expr
b
.
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
with |
.found .bool h₁: Maybe fun ty => HasType a ty
.found
.bool: Ty
.bool
.found .bool h₁: Maybe fun ty => HasType a ty
h₁: HasType a Ty.bool
h₁
,
.found .bool h₂: Maybe fun ty => HasType b ty
.found
.bool: Ty
.bool
.found .bool h₂: Maybe fun ty => HasType b ty
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) → Maybe fun ty => HasType e ty
typeCheck
.unknown: {α : Sort ?u.4858} → {p : α → Prop} → Maybe p
.unknown
) :
e: Expr
e
.
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
=
.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found
ty: Ty
ty
h: HasType e ty
h
:=
e: Expr
ty: Ty
h, h₁: HasType e ty
h₂: typeCheck e Maybe.unknown

typeCheck e = Maybe.found ty h
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✝: Maybe fun 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'

found
Maybe.found ty' h' = Maybe.found ty h
;
e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
this: ty = ty'

found
Maybe.found ty' h' = Maybe.found ty h
;
e: Expr
ty: Ty
h, h₁, h': HasType e ty

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

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) → Maybe fun ty => HasType e ty
typeCheck
=
.unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown
¬
HasType: Expr → Ty → Prop
HasType
e: Expr
e
ty: Ty
ty
:=
ty: Ty
e: Expr

typeCheck e = Maybe.unknown ¬HasType e ty
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✝¹: Maybe fun ty => HasType a ty
x✝: Maybe fun ty => HasType b ty
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat

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✝²: Maybe fun ty => HasType a ty
x✝¹: Maybe fun ty => HasType b ty
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✝¹: Maybe fun ty => HasType a ty
x✝: Maybe fun ty => HasType b ty
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat

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✝²: Maybe fun ty => HasType a ty
x✝¹: Maybe fun ty => HasType b ty
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✝¹: Maybe fun ty => HasType a ty
x✝: Maybe fun ty => HasType b ty

¬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✝²: Maybe fun ty => HasType a ty
x✝¹: Maybe fun ty => HasType b ty

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: Maybe fun ty => HasType a ty
rb: Maybe fun 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: Maybe fun ty => HasType a ty
rb: Maybe fun 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: Maybe fun ty => HasType a ty
rb: Maybe fun 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✝¹: Maybe fun ty => HasType a ty
x✝: Maybe fun ty => HasType b ty
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool

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✝²: Maybe fun ty => HasType a ty
x✝¹: Maybe fun ty => HasType b ty
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✝¹: Maybe fun ty => HasType a ty
x✝: Maybe fun ty => HasType b ty
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool

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✝²: Maybe fun ty => HasType a ty
x✝¹: Maybe fun ty => HasType b ty
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✝¹: Maybe fun ty => HasType a ty
x✝: Maybe fun ty => HasType b ty

¬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✝²: Maybe fun ty => HasType a ty
x✝¹: Maybe fun ty => HasType b ty

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: Maybe fun ty => HasType a ty
rb: Maybe fun 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: Maybe fun ty => HasType a ty
rb: Maybe fun 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: Maybe fun ty => HasType a ty
rb: Maybe fun 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.found t' ht'
h'
:
e: Expr
e
.
typeCheck: (e : Expr) → Maybe fun ty => HasType e ty
typeCheck
with |
.found t' ht': Maybe fun ty => HasType e ty
.found
t': Ty
t'
.found t' ht': Maybe fun ty => HasType e ty
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: Maybe fun ty => HasType e ty
.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

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.inttoInt, 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.2009 + 1)
0
(
ty: Ty
ty
::
ctx: Vector Ty ?m.2009
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.2129
k
ctx: Vector Ty ?m.2129
ctx
ty: Ty
ty
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType
k: Fin ?m.2129
k
.
succ: {n : Nat} → Fin n → Fin (Nat.succ n)
succ
(
u: Ty
u
::
ctx: Vector Ty ?m.2129
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} → {ctx : Vector Ty n} → {ty : Ty} → {i : Fin n} → HasType i ctx ty → Expr ctx ty
var
:
HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType
i: Fin ?m.2969
i
ctx: Vector Ty ?m.2969
ctx
ty: Ty
ty
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.2969
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.2990
ctx
Ty.int: Ty
Ty.int
|
lam: {n : Nat} → {ctx : Vector Ty n} → {a 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.3087
ctx
)
ty: Ty
ty
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3087
ctx
(
Ty.fn: Ty → Ty → Ty
Ty.fn
a: Ty
a
ty: Ty
ty
) |
app: {n : Nat} → {ctx : Vector Ty n} → {ty a : 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.3176
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.3176
ctx
a: Ty
a
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3176
ctx
ty: Ty
ty
|
op: {n : Nat} → {ctx : Vector Ty n} → {c a b : 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.3266
ctx
a: Ty
a
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3266
ctx
b: Ty
b
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3266
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.3387
ctx
Ty.bool: Ty
Ty.bool
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3387
ctx
a: Ty
a
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3387
ctx
a: Ty
a
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3387
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.3430
ctx
a: Ty
a
)
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.3430
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 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 ot 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.7936
ctx
Env: {n : Nat} → Vector Ty n → Type
Env
(
a: Ty
a
::
ctx: Vector Ty ?m.7936
ctx
) infix:67 " :: " => 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.9714
i
ctx: Vector Ty ?m.9714
ctx
ty: Ty
ty
Env: {n : Nat} → Vector Ty n → Type
Env
ctx: Vector Ty ?m.9714
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.12552
ctx
) :
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.12552
ctx
ty: Ty
ty
ty: Ty
ty
.
interp: Ty → Type
interp
|
var: {n : Nat} → {ctx : Vector Ty n} → {ty : Ty} → {i : Fin n} → 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} → {ctx : Vector Ty n} → {a 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} → {ty a : 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} → {c a b : 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.16788
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} → {ctx : Vector Ty n} → {a ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam
(
lam: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam
(
op: {n : Nat} → {ctx : Vector Ty n} → {c a b : 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} → {ctx : Vector Ty n} → {ty : Ty} → {i : Fin n} → 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} → {ctx : Vector Ty n} → {ty : Ty} → {i : Fin n} → 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 viwed as "trust me, this recursive definition makes sense". Recall that sorry is an unsound axiom in Lean.

def 
fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)
fact
:
Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr
ctx: Vector Ty ?m.17174
ctx
(
Ty.fn: Ty → Ty → Ty
Ty.fn
Ty.int: Ty
Ty.int
Ty.int: Ty
Ty.int
) :=
lam: {n : Nat} → {ctx : Vector Ty n} → {a 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} → {c a b : 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} → {ctx : Vector Ty n} → {ty : Ty} → {i : Fin n} → 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} → {c a b : 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
_: Type
_
=>
app: {n : Nat} → {ctx : Vector Ty n} → {ty a : 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} → {c a b : 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} → {ctx : Vector Ty n} → {ty : Ty} → {i : Fin n} → 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} → {ctx : Vector Ty n} → {ty : Ty} → {i : Fin n} → 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
Warning: declaration uses 'sorry'

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

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

notation "[" "]" => 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.2220
a
(
a: ?m.2220
a
::
as: List ?m.2220
as
) |
tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail
:
Member: {α : Type} → α → List α → Type
Member
a: ?m.2360
a
bs: List ?m.2360
bs
Member: {α : Type} → α → List α → Type
Member
a: ?m.2360
a
(
b: ?m.2360
b
::
bs: List ?m.2360
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.2929 → Type u_1
β
is: List ?m.2929
is
Member: {α : Type} → α → List α → Type
Member
i: ?m.2929
i
is: List ?m.2929
is
β: ?m.2929 → Type u_1
β
i: ?m.2929
i
|
a: β i
a
::
as: HList β is✝
as
,
.head: Member i (i :: is✝)
.head
=>
a: β i
a
|
a: β i✝
a
::
as: HList β is✝
as
,
.tail h: Member i (i✝ :: is✝)
.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: {ctx : List Ty} → {ty : 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} → {ran dom : 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: {ctx : List Ty} → {dom 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: {ctx : List Ty} → {dom ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
(
lam: {ctx : List Ty} → {dom 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: {ctx : List Ty} → {ty : 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: {ctx : List Ty} → {ty : 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} → {ran dom : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app
(
app: {ctx : List Ty} → {ran dom : 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: {ctx : List Ty} → {ty : 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} → {ran dom : 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: {ctx : List Ty} → {dom 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
env
::
env: HList Ty.denote ctx
env
)

You can show that the denotation of three_the_hard_way is indeed 3 using reflexivity.

example: Term.denote three_the_hard_way [] = 3
example
:
three_the_hard_way: Term [] nat
three_the_hard_way
.
denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote
[] =
3: Ty.denote nat
3
:=
rfl: ∀ {α : Type} {a : α}, a = a
rfl

We now define the constant folding optimization that traverses a term if replaces subterms such as plus (const m) (const n) with const (n+m).

@[simp] def 
Term.constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
Term.constFold
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
|
const: {ctx : List Ty} → Nat → Term ctx nat
const
n: Nat
n
=>
const: {ctx : List Ty} → Nat → Term ctx nat
const
n: Nat
n
|
var: {ctx : List Ty} → {ty : Ty} → Member ty ctx → Term ctx ty
var
h: Member ty ctx
h
=>
var: {ctx : List Ty} → {ty : Ty} → Member ty ctx → Term ctx ty
var
h: Member ty ctx
h
|
app: {ctx : List Ty} → {ran dom : 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
=>
app: {ctx : List Ty} → {ran dom : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app
f: Term ctx (fn dom✝ ty)
f
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
a: Term ctx dom✝
a
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
|
lam: {ctx : List Ty} → {dom ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
b: Term (dom✝ :: ctx) ran✝
b
=>
lam: {ctx : List Ty} → {dom ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam
b: Term (dom✝ :: ctx) ran✝
b
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
|
«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
=>
«let»: {ctx : List Ty} → {ty₂ ty₁ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let»
a: Term ctx ty₁✝
a
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
b: Term (ty₁✝ :: ctx) ty
b
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
|
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus
a: Term ctx nat
a
b: Term ctx nat
b
=> match
a: Term ctx nat
a
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
,
b: Term ctx nat
b
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
with |
const: {ctx : List Ty} → Nat → Term ctx nat
const
n: Nat
n
,
const: {ctx : List Ty} → Nat → Term ctx nat
const
m: Nat
m
=>
const: {ctx : List Ty} → Nat → Term ctx nat
const
(
n: Nat
n
+
m: Nat
m
) |
a': Term ctx nat
a'
,
b': Term ctx nat
b'
=>
plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus
a': Term ctx nat
a'
b': Term ctx nat
b'

The correctness of the Term.constFold is proved using induction, case-analysis, and the term simplifier. We prove all cases but the one for plus using simp [*]. This tactic instructs the term simplifier to use hypotheses such as a = b as rewriting/simplications rules. We use the split to break the nested match expression in the plus case into two cases. The local variables iha and ihb are the induction hypotheses for a and b. The modifier in a term simplifier argument instructs the term simplier to use the equation as a rewriting rule in the "reverse direction. That is, given h : a = b, ← h instructs the term simplifier to rewrite b subterms to a.

theorem 
Term.constFold_sound: ∀ {ctx : List Ty} {ty : Ty} {env : HList Ty.denote ctx} (e : Term ctx ty), denote (constFold e) env = denote e env
Term.constFold_sound
(
e: Term ctx ty
e
:
Term: List Ty → Ty → Type
Term
ctx: List Ty
ctx
ty: Ty
ty
) :
e: Term ctx ty
e
.
constFold: {ctx : List Ty} → {ty : Ty} → Term ctx ty → Term ctx ty
constFold
.