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:
- Type inference
- First-class functions
- Powerful data types
- Pattern matching
- Type classes
- Monads
- Extensible syntax
- Hygienic macros
- Dependent types
- Metaprogramming
- Multithreading
- Verification: you can prove properties of your functions using Lean itself
Tour of Lean
The best way to learn about Lean is to read and write Lean code. This article will act as a tour through some of the key features of the Lean language and give you some code snippets that you can execute on your machine. To learn about setting up a development environment, check out Setting Up Lean.
There are two primary concepts in Lean: functions and types. This tour will emphasize features of the language which fall into these two concepts.
Functions and Namespaces
The most fundamental pieces of any Lean program are functions organized into namespaces.
Functions perform work on inputs to produce outputs,
and they are organized under namespaces,
which are the primary way you group things in Lean.
They are defined using the def
command,
which give the function a name and define its arguments.
namespace BasicFunctions
-- The `#eval` command evaluates an expression on the fly and prints the result.
#eval 2+2
-- You use 'def' to define a function. This one accepts a natural number
-- and returns a natural number.
-- Parentheses are optional for function arguments, except for when
-- you use an explicit type annotation.
-- Lean can often infer the type of the function's arguments.
def sampleFunction1 x := x*x + 3
-- Apply the function, naming the function return result using 'def'.
-- The variable type is inferred from the function return type.
def result1 := sampleFunction1 4573
-- This line uses an interpolated string to print the result. Expressions inside
-- braces `{}` are converted into strings using the polymorphic method `toString`
#eval println! "The result of squaring the integer 4573 and adding 3 is {result1}"
-- When needed, annotate the type of a parameter name using '(argument : type)'.
def sampleFunction2 (x : Nat) := 2*x*x - x + 3
def result2 := sampleFunction2 (7 + 4)
#eval println! "The result of applying the 2nd sample function to (7 + 4) is {result2}"
-- Conditionals use if/then/else
def sampleFunction3 (x : Int) :=
if x > 100 then
2*x*x - x + 3
else
2*x*x + x - 37
#eval println! "The result of applying sampleFunction3 to 2 is {sampleFunction3 2}"
end BasicFunctions
-- Lean has first-class functions.
-- `twice` takes two arguments `f` and `a` where
-- `f` is a function from natural numbers to natural numbers, and
-- `a` is a natural number.
def twice (f : Nat → Nat) (a : Nat) :=
f (f a)
-- `fun` is used to declare anonymous functions
#eval twice (fun x => x + 2) 10
-- You can prove theorems about your functions.
-- The following theorem states that for any natural number `a`,
-- adding 2 twice produces a value equal to `a + 4`.
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
-- The proof is by reflexivity. Lean "symbolically" reduces both sides of the equality
-- until they are identical.
rfl
-- `(· + 2)` is syntax sugar for `(fun x => x + 2)`. The parentheses + `·` notation
-- is useful for defining simple anonymous functions.
#eval twice (· + 2) 10
-- Enumerated types are a special case of inductive types in Lean,
-- which we will learn about later.
-- The following command creates a new type `Weekday`.
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
-- `Weekday` has 7 constructors/elements.
-- The constructors live in the `Weekday` namespace.
-- Think of `sunday`, `monday`, …, `saturday` as being distinct elements of `Weekday`,
-- with no other distinguishing properties.
-- The command `#check` prints the type of a term in Lean.
#check Weekday.sunday
#check Weekday.monday
-- The `open` command opens a namespace, making all declarations in it accessible without
-- qualification.
open Weekday
#check sunday
#check tuesday
-- You can define functions by pattern matching.
-- The following function converts a `Weekday` into a natural number.
def natOfWeekday (d : Weekday) : Nat :=
match d with
| sunday => 1
| monday => 2
| tuesday => 3
| wednesday => 4
| thursday => 5
| friday => 6
| saturday => 7
#eval natOfWeekday tuesday
def isMonday : Weekday → Bool :=
-- `fun` + `match` is a common idiom.
-- The following expression is syntax sugar for
-- `fun d => match d with | monday => true | _ => false`.
fun
| monday => true
| _ => false
#eval isMonday monday
#eval isMonday sunday
-- Lean has support for type classes and polymorphic methods.
-- The `toString` method converts a value into a `String`.
#eval toString 10
#eval toString (10, 20)
-- The method `toString` converts values of any type that implements
-- the class `ToString`.
-- You can implement instances of `ToString` for your own types.
instance : ToString Weekday where
toString (d : Weekday) : String :=
match d with
| sunday => "Sunday"
| monday => "Monday"
| tuesday => "Tuesday"
| wednesday => "Wednesday"
| thursday => "Thursday"
| friday => "Friday"
| saturday => "Saturday"
#eval toString (sunday, 10)
def Weekday.next (d : Weekday) : Weekday :=
match d with
| sunday => monday
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => saturday
| saturday => sunday
#eval Weekday.next Weekday.wednesday
-- Since the `Weekday` namespace has already been opened, you can also write
#eval next wednesday
-- Matching on a parameter like in the previous definition
-- is so common that Lean provides syntax sugar for it. The following
-- function uses it.
def Weekday.previous : Weekday -> Weekday
| sunday => saturday
| monday => sunday
| tuesday => monday
| wednesday => tuesday
| thursday => wednesday
| friday => thursday
| saturday => friday
#eval next (previous wednesday)
-- We can prove that for any `Weekday` `d`, `next (previous d) = d`
theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d :=
match d with
| sunday => rfl
| monday => rfl
| tuesday => rfl
| wednesday => rfl
| thursday => rfl
| friday => rfl
| saturday => rfl
-- You can automate definitions such as `Weekday.nextOfPrevious`
-- using metaprogramming (or "tactics").
theorem Weekday.nextOfPrevious' (d : Weekday) : next (previous d) = d := by
cases d -- A proof by case distinction
all_goals rfl -- Each case is solved using `rfl`
Quickstart
These instructions will walk you through setting up Lean using the "basic" setup and VS Code as the editor. See Setup for other ways, supported platforms, and more details on setting up Lean.
See quick walkthrough demo video.
-
Install VS Code.
-
Launch VS Code and install the
lean4
extension. -
Create a new file using "File > New Text File" (
Ctrl+N
). Click theSelect a language
prompt, type inlean4
, and hit ENTER. You should see the following popup:Click the "Install Lean using Elan" button. You should see some progress output like this:
info: syncing channel updates for 'stable' info: latest update on stable, lean version v4.0.0 info: downloading component 'lean'
If there is no popup, you probably have Elan installed already. You may want to make sure that your default toolchain is Lean 4 in this case by running
elan default leanprover/lean4:stable
and reopen the file, as the next step will fail otherwise. -
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.
You are set up!
Create a Lean Project
If your goal is to contribute to mathlib4 or use it as a dependency, please see its readme for specific instructions on how to do that.
You can now create a Lean project in a new folder. Run lake init foo
from "View > Terminal" to create a package, followed by lake build
to get an executable version of your Lean program.
On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.
Note: Packages have to be opened using "File > Open Folder..." for imports to work.
Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (Ctrl+Shift+X
).
Troubleshooting
The InfoView says "Waiting for Lean server to start..." forever.
Check that the VS Code Terminal is not showing some installation errors from elan
.
If that doesn't work, try also running the VS Code command Developer: Reload Window
.
Supported Platforms
Tier 1
Platforms built & tested by our CI, available as nightly releases via elan (see below)
- x86-64 Linux with glibc 2.27+
- x86-64 macOS 10.15+
- x86-64 Windows 10+
Tier 2
Platforms cross-compiled but not tested by our CI, available as nightly releases
Releases may be silently broken due to the lack of automated testing. Issue reports and fixes are welcome.
- aarch64 Linux with glibc 2.27+
- aarch64 (Apple Silicon) macOS
- x86 (32-bit) Linux
- Emscripten Web Assembly
Setting Up Lean
See also the quickstart instructions for a standard setup with VS Code as the editor.
Release builds for all supported platforms are available at https://github.com/leanprover/lean4/releases.
Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager elan
instead:
$ elan self update # in case you haven't updated elan in a while
# download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable
lake
Lean 4 comes with a package manager named lake
.
Use lake init foo
to initialize a Lean package foo
in the current directory, and lake build
to typecheck and build it as well as all its dependencies. Use lake help
to learn about further commands.
The general directory structure of a package foo
is
lakefile.lean # package configuration
lean-toolchain # specifies the lean version to use
Foo.lean # main file, import via `import Foo`
Foo/
A.lean # further files, import via e.g. `import Foo.A`
A/... # further nesting
build/ # `lake` build output directory
After running lake build
you will see a binary named ./build/bin/foo
and when you run it you should see the output:
Hello, world!
Editing
Lean implements the Language Server Protocol that can be used for interactive development in Emacs, VS Code, and possibly other editors.
Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).
Theorem Proving in Lean
We strongly encourage you to read the book Theorem Proving in Lean. Many Lean users consider it to be the Lean Bible.
Functional Programming in Lean
The goal of this book is to be an accessible introduction to using Lean 4 as a programming language. It should be useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming. It does not assume any background with functional programming, though it's probably not a good first book on programming in general. New content will be added once per month until it's done.
Examples
- Palindromes
- Binary Search Trees
- A Certified Type Checker
- The Well-Typed Interpreter
- Dependent de Bruijn Indices
- Parametric Higher-Order Abstract Syntax
Palindromes
Palindromes are lists that read the same from left to right and from right to left.
For example, [a, b, b, a]
and [a, h, a]
are palindromes.
We use an inductive predicate to specify whether a list is a palindrome or not.
Recall that inductive predicates, or inductively defined propositions, are a convenient
way to specify functions of type ... → Prop
.
This example is a based on an example from the book "The Hitchhiker's Guide to Logical Verification".
inductive Palindrome: {α : Type u_1} → List α → Prop
Palindrome : List: Type u_1 → Type u_1
List α: Type u_1
α → Prop: Type
Prop where
| nil: ∀ {α : Type u_1}, Palindrome []
nil : Palindrome: {α : Type u_1} → List α → Prop
Palindrome []: List ?m.17
[]
| single: ∀ {α : Type u_1} (a : α), Palindrome [a]
single : (a: α
a : α: Type u_1
α) → Palindrome: {α : Type u_1} → List α → Prop
Palindrome [a: α
a]
| sandwich: ∀ {α : Type u_1} {as : List α} (a : α), Palindrome as → Palindrome ([a] ++ as ++ [a])
sandwich : (a: α
a : α: Type u_1
α) → Palindrome: {α : Type u_1} → List α → Prop
Palindrome as: List α
as → Palindrome: {α : Type u_1} → List α → Prop
Palindrome ([a: α
a] ++ as: List α
as ++ [a: α
a])
The definition distinguishes three cases: (1) []
is a palindrome; (2) for any element
a
, the singleton list [a]
is a palindrome; (3) for any element a
and any palindrome
[b₁, . . ., bₙ]
, the list [a, b₁, . . ., bₙ, a]
is a palindrome.
We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate h : Palindrome as
.
theorempalindrome_reverse (palindrome_reverse: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)h :h: Palindrome asPalindromePalindrome: {α : Type u_1} → List α → Propas) :as: List ?m.394PalindromePalindrome: {α : Type u_1} → List α → Propas.as: List ?m.394reverse :=reverse: {α : Type u_1} → List α → List αGoals accomplished! 🐙α✝: Type u_1
as: List α✝
h: Palindrome asPalindrome (List.reverse as)α✝: Type u_1
as: List α✝
nilPalindrome (List.reverse [])Goals accomplished! 🐙α✝: Type u_1
as: List α✝
a: α✝
singlePalindrome (List.reverse [a])Goals accomplished! 🐙α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome (List.reverse as✝)
sandwichPalindrome (List.reverse ([a] ++ as✝ ++ [a]));α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: Palindrome (List.reverse as✝)
sandwichPalindrome (a :: (List.reverse as✝ ++ [a]))Goals accomplished! 🐙
If a list as
is a palindrome, then the reverse of as
is equal to itself.
theoremreverse_eq_of_palindrome (reverse_eq_of_palindrome: ∀ {α : Type u_1} {as : List α}, Palindrome as → List.reverse as = ash :h: Palindrome asPalindromePalindrome: {α : Type u_1} → List α → Propas) :as: List ?m.696as.as: List ?m.696reverse =reverse: {α : Type u_1} → List α → List αas :=as: List ?m.696Goals accomplished! 🐙α✝: Type u_1
as: List α✝
h: Palindrome asList.reverse as = asα✝: Type u_1
as: List α✝
nilList.reverse [] = []Goals accomplished! 🐙α✝: Type u_1
as: List α✝
a: α✝
singleList.reverse [a] = [a]Goals accomplished! 🐙α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: List.reverse as✝ = as✝
sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: List.reverse as✝ = as✝
sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]ih: List.reverse as✝ = as✝α✝: Type u_1
as, as✝: List α✝
a: α✝
h: Palindrome as✝
ih: List.reverse as✝ = as✝
sandwichList.reverse ([a] ++ as✝ ++ [a]) = [a] ++ as✝ ++ [a]Goals accomplished! 🐙
Note that you can also easily prove palindrome_reverse
using reverse_eq_of_palindrome
.
example (example: ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)h :h: Palindrome asPalindromePalindrome: {α : Type u_1} → List α → Propas) :as: List ?m.946PalindromePalindrome: {α : Type u_1} → List α → Propas.as: List ?m.946reverse :=reverse: {α : Type u_1} → List α → List αGoals accomplished! 🐙Goals accomplished! 🐙
Given a nonempty list, the function List.last
returns its element.
Note that we use (by simp)
to prove that a₂ :: as ≠ []
in the recursive application.
defList.last : (List.last: {α : Type u_1} → (as : List α) → as ≠ [] → αas :as: List αListList: Type u_1 → Type u_1α) →α: Type u_1as ≠as: List α[] →[]: List αα | [α: Type u_1a], _ =>a: αa | _::a: αa₂::a₂: αas, _ => (as: List αa₂::a₂: αas).as: List αlast (last: {α : Type u_1} → (as : List α) → as ≠ [] → αGoals accomplished! 🐙)Goals accomplished! 🐙
We use the function List.last
to prove the following theorem that says that if a list as
is not empty,
then removing the last element from as
and appending it back is equal to as
.
We use the attribute @[simp]
to instruct the simp
tactic to use this theorem as a simplification rule.
@[simp] theoremList.dropLast_append_last (List.dropLast_append_last: ∀ {α : Type u_1} {as : List α} (h : as ≠ []), dropLast as ++ [last as h] = ash :h: as ≠ []as ≠as: List ?m.1696[]) :[]: List ?m.1696as.as: List ?m.1696dropLast ++ [dropLast: {α : Type u_1} → List α → List αas.as: List ?m.1696lastlast: {α : Type u_1} → (as : List α) → as ≠ [] → αh] =h: as ≠ []as :=as: List ?m.1696Goals accomplished! 🐙α✝: Type u_1
as: List α✝
h: as ≠ []dropLast as ++ [last as h] = asα✝: Type u_1
as: List α✝
h: [] ≠ []dropLast [] ++ [last [] h] = []Goals accomplished! 🐙α✝: Type u_1
as: List α✝
a: α✝
h: [a] ≠ []dropLast [a] ++ [last [a] h] = [a]Goals accomplished! 🐙α✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []dropLast (a₁ :: a₂ :: as) ++ [last (a₁ :: a₂ :: as) h] = a₁ :: a₂ :: asα✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: asα✝: Type u_1
as✝: List α✝
a₁, a₂: α✝
as: List α✝
h: a₁ :: a₂ :: as ≠ []dropLast (a₂ :: as) ++ [last (a₂ :: as) (_ : ¬a₂ :: as = [])] = a₂ :: asGoals accomplished! 🐙Goals accomplished! 🐙Goals accomplished! 🐙
We now define the following auxiliary induction principle for lists using well-founded recursion on as.length
.
We can read it as follows, to prove motive as
, it suffices to show that: (1) motive []
; (2) motive [a]
for any a
;
(3) if motive as
holds, then motive ([a] ++ as ++ [b])
also holds for any a
, b
, and as
.
Note that the structure of this induction principle is very similar to the Palindrome
inductive predicate.
theoremList.palindrome_ind (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 asmotive :motive: List α → PropListList: Type u_1 → Type u_1α →α: Type u_1Prop) (Prop: Typeh₁ :h₁: motive []motivemotive: List α → Prop[]) ([]: List αh₂ : (h₂: ∀ (a : α), motive [a]a :a: αα) →α: Type u_1motive [motive: List α → Propa]) (a: αh₃ : (h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])aa: αb :b: αα) → (α: Type u_1as :as: List αListList: Type u_1 → Type u_1α) →α: Type u_1motivemotive: List α → Propas →as: List αmotive ([motive: List α → Propa] ++a: αas ++ [as: List αb])) (b: αas :as: List αListList: Type u_1 → Type u_1α) :α: Type u_1motivemotive: List α → Propas := matchas: List αas with | [] =>as: List αh₁ | [h₁: motive []a] =>a: αh₂h₂: ∀ (a : α), motive [a]a |a: αa₁::a₁: αa₂::a₂: αas' => haveas': List αih :=ih: motive (dropLast (a₂ :: as'))palindrome_indpalindrome_ind: ∀ {α : Type u_1} (motive : List α → Prop), motive [] → (∀ (a : α), motive [a]) → (∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])) → ∀ (as : List α), motive asmotivemotive: List α → Proph₁h₁: motive []h₂h₂: ∀ (a : α), motive [a]h₃ (h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])a₂::a₂: αas').as': List αdropLast have : [dropLast: {α : Type u_1} → List α → List αa₁] ++ (a₁: αa₂::a₂: αas').as': List αdropLast ++ [(dropLast: {α : Type u_1} → List α → List αa₂::a₂: αas').as': List αlast (last: {α : Type u_1} → (as : List α) → as ≠ [] → αGoals accomplished! 🐙)] =Goals accomplished! 🐙a₁::a₁: αa₂::a₂: αas' :=as': List αGoals accomplished! 🐙Goals accomplished! 🐙this ▸this: [a₁] ++ dropLast (a₂ :: as') ++ [last (a₂ :: as') (_ : ¬a₂ :: as' = [])] = a₁ :: a₂ :: as'h₃h₃: ∀ (a b : α) (as : List α), motive as → motive ([a] ++ as ++ [b])__: α__: α__: List αih termination_by _ as =>ih: motive (dropLast (a₂ :: as'))as.as: List αlengthlength: {α : Type u_1} → List α → Nat
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.
theoremList.palindrome_of_eq_reverse (List.palindrome_of_eq_reverse: ∀ {α : Type u_1} {as : List α}, reverse as = as → Palindrome ash :h: reverse as = asas.as: List ?m.10517reverse =reverse: {α : Type u_1} → List α → List αas) :as: List ?m.10517PalindromePalindrome: {α : Type u_1} → List α → Propas :=as: List ?m.10517Goals accomplished! 🐙α✝: Type u_1
h: reverse [] = []
h₁Palindrome []α✝: Type u_1
a✝: α✝
h: reverse [a✝] = [a✝]Palindrome [a✝]α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]Palindrome ([a✝¹] ++ as✝ ++ [b✝])α✝: Type u_1
h: reverse [] = []
h₁Palindrome []α✝: Type u_1
a✝: α✝
h: reverse [a✝] = [a✝]Palindrome [a✝]α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]Palindrome ([a✝¹] ++ as✝ ++ [b✝])Goals accomplished! 🐙α✝: Type u_1
a✝: α✝
h: reverse [a✝] = [a✝]
h₂Palindrome [a✝]α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]Palindrome ([a✝¹] ++ as✝ ++ [b✝])Goals accomplished! 🐙α✝: Type u_1
a✝¹, b✝: α✝
as✝: List α✝
a✝: reverse as✝ = as✝ → Palindrome as✝
h: reverse ([a✝¹] ++ as✝ ++ [b✝]) = [a✝¹] ++ as✝ ++ [b✝]
h₃Palindrome ([a✝¹] ++ as✝ ++ [b✝])α✝: Type u_1
a, b: α✝
as: List α✝
ih: reverse as = as → Palindrome as
h: reverse ([a] ++ as ++ [b]) = [a] ++ as ++ [b]Palindrome ([a] ++ as ++ [b])Goals accomplished! 🐙Goals accomplished! 🐙α✝: Type u_1
a: α✝
as: List α✝
ih: reverse as = as → Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]Palindrome ([a] ++ as ++ [a])α✝: Type u_1
a: α✝
as: List α✝
ih: reverse as = as → Palindrome as
h: reverse ([a] ++ as ++ [a]) = [a] ++ as ++ [a]Palindrome ([a] ++ as ++ [a])Goals accomplished! 🐙Goals accomplished! 🐙Goals accomplished! 🐙
We now define a function that returns true
iff as
is a palindrome.
The function assumes that the type α
has decidable equality. We need this assumption
because we need to compare the list elements.
def List.isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → Bool
List.isPalindrome [DecidableEq: Type u_1 → Type u_1
DecidableEq α: Type u_1
α] (as: List α
as : List: Type u_1 → Type u_1
List α: Type u_1
α) : Bool: Type
Bool :=
as: List α
as.reverse: {α : Type u_1} → List α → List α
reverse = as: List α
as
It is straightforward to prove that isPalindrome
is correct using the previously proved theorems.
theoremList.isPalindrome_correct [List.isPalindrome_correct: ∀ {α : Type u_1} [inst : DecidableEq α] (as : List α), isPalindrome as = true ↔ Palindrome asDecidableEqDecidableEq: Type u_1 → Type u_1α] (α: Type u_1as :as: List αListList: Type u_1 → Type u_1α) :α: Type u_1as.as: List αisPalindrome ↔isPalindrome: {α : Type u_1} → [inst : DecidableEq α] → List α → BoolPalindromePalindrome: {α : Type u_1} → List α → Propas :=as: List αGoals accomplished! 🐙α: Type u_1
inst✝: DecidableEq α
as: List αreverse as = as ↔ Palindrome asGoals accomplished! 🐙[1,1: Nat2,2: Nat1].1: NatisPalindromeisPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Bool[1,1: Nat2,2: Nat3,3: Nat1].1: NatisPalindromeisPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolexample : [example: List.isPalindrome [1, 2, 1] = true1,1: Nat2,2: Nat1].1: NatisPalindrome :=isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl: ∀ {α : Type} {a : α}, a = aexample : [example: List.isPalindrome [1, 2, 2, 1] = true1,1: Nat2,2: Nat2,2: Nat1].1: NatisPalindrome :=isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl: ∀ {α : Type} {a : α}, a = aexample : ![example: (!List.isPalindrome [1, 2, 3, 1]) = true1,1: Nat2,2: Nat3,3: Nat1].1: NatisPalindrome :=isPalindrome: {α : Type} → [inst : DecidableEq α] → List α → Boolrflrfl: ∀ {α : Type} {a : α}, a = a
Binary Search Trees
If the type of keys can be totally ordered -- that is, it supports a well-behaved ≤
comparison --
then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time
proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.
This example is based on a similar example found in the "Software Foundations" book (volume 3).
We use Nat
as the key type in our implementation of BSTs,
since it has a convenient total order with lots of theorems and automation available.
We leave as an exercise to the reader the generalization to arbitrary types.
inductive Tree: Type v → Type v
Tree (β: Type v
β : Type v: Type (v + 1)
Type v) where
| leaf: {β : Type v} → Tree β
leaf
| node: {β : Type v} → Tree β → Nat → β → Tree β → Tree β
node (left: Tree β
left : Tree: Type v → Type v
Tree β: Type v
β) (key: Nat
key : Nat: Type
Nat) (value: β
value : β: Type v
β) (right: Tree β
right : Tree: Type v → Type v
Tree β: Type v
β)
deriving Repr: Type u → Type u
Repr
The function contains
returns true
iff the given tree contains the key k
.
defTree.contains (Tree.contains: {β : Type u_1} → Tree β → Nat → Boolt :t: Tree βTreeTree: Type u_1 → Type u_1β) (β: Type u_1k :k: NatNat) :Nat: TypeBool := matchBool: Typet with |t: Tree βleaf =>leaf: {β : Type ?u.1676} → Tree βfalse |false: Boolnodenode: {β : Type ?u.1685} → Tree β → Nat → β → Tree β → Tree βleftleft: Tree βkeykey: Natright => ifright: Tree βk <k: Natkey thenkey: Natleft.left: Tree βcontainscontains: {β : Type u_1} → Tree β → Nat → Boolk else ifk: Natkey <key: Natk thenk: Natright.right: Tree βcontainscontains: {β : Type u_1} → Tree β → Nat → Boolk elsek: Nattruetrue: Bool
t.find? k
returns some v
if v
is the value bound to key k
in the tree t
. It returns none
otherwise.
def Tree.find?: {β : Type u_1} → Tree β → Nat → Option β
Tree.find? (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) (k: Nat
k : Nat: Type
Nat) : Option: Type u_1 → Type u_1
Option β: Type u_1
β :=
match t: Tree β
t with
| leaf: {β : Type ?u.2139} → Tree β
leaf => none: {α : Type u_1} → Option α
none
| node: {β : Type ?u.2151} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value right: Tree β
right =>
if k: Nat
k < key: Nat
key then
left: Tree β
left.find?: {β : Type u_1} → Tree β → Nat → Option β
find? k: Nat
k
else if key: Nat
key < k: Nat
k then
right: Tree β
right.find?: {β : Type u_1} → Tree β → Nat → Option β
find? k: Nat
k
else
some: {α : Type u_1} → α → Option α
some value: β
value
t.insert k v
is the map containing all the bindings of t
along with a binding of k
to v
.
def Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) (k: Nat
k : Nat: Type
Nat) (v: β
v : β: Type u_1
β) : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β :=
match t: Tree β
t with
| leaf: {β : Type ?u.2611} → Tree β
leaf => node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node leaf: {β : Type u_1} → Tree β
leaf k: Nat
k v: β
v leaf: {β : Type u_1} → Tree β
leaf
| node: {β : Type ?u.2626} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value right: Tree β
right =>
if k: Nat
k < key: Nat
key then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node (left: Tree β
left.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert k: Nat
k v: β
v) key: Nat
key value: β
value right: Tree β
right
else if key: Nat
key < k: Nat
k then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value (right: Tree β
right.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert k: Nat
k v: β
v)
else
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left k: Nat
k v: β
v right: Tree β
right
Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs. If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list. Here's a function that does so with an in-order traversal of the tree.
defTree.toList (Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)t :t: Tree βTreeTree: Type u_1 → Type u_1β) :β: Type u_1List (List: Type u_1 → Type u_1Nat ×Nat: Typeβ) := matchβ: Type u_1t with |t: Tree βleaf =>leaf: {β : Type ?u.3120} → Tree β[] |[]: List (Nat × β)nodenode: {β : Type ?u.3132} → Tree β → Nat → β → Tree β → Tree βll: Tree βkk: Natvv: βr =>r: Tree βl.l: Tree βtoList ++ [(toList: {β : Type u_1} → Tree β → List (Nat × β)k,k: Natv)] ++v: βr.r: Tree βtoListtoList: {β : Type u_1} → Tree β → List (Nat × β)Tree.leaf.Tree.leaf: {β : Type} → Tree βinsertinsert: {β : Type} → Tree β → Nat → β → Tree β22: Nat"two" |>."two": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β33: Nat"three" |>."three": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β11: Nat"one""one": StringTree.leaf.Tree.leaf: {β : Type} → Tree βinsertinsert: {β : Type} → Tree β → Nat → β → Tree β22: Nat"two" |>."two": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β33: Nat"three" |>."three": Stringinsertinsert: {β : Type} → Tree β → Nat → β → Tree β11: Nat"one" |>."one": StringtoListtoList: {β : Type} → Tree β → List (Nat × β)
The implementation of Tree.toList
is inefficient because of how it uses the ++
operator.
On a balanced tree its running time is linearithmic, because it does a linear number of
concatenations at each level of the tree. On an unbalanced tree it's quadratic time.
Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:
def Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toListTR (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) : List: Type u_1 → Type u_1
List (Nat: Type
Nat × β: Type u_1
β) :=
go: Tree β → List (Nat × β) → List (Nat × β)
go t: Tree β
t []: List (Nat × β)
[]
where
go: Tree β → List (Nat × β) → List (Nat × β)
go (t: Tree β
t : Tree: Type u_1 → Type u_1
Tree β: Type u_1
β) (acc: List (Nat × β)
acc : List: Type u_1 → Type u_1
List (Nat: Type
Nat × β: Type u_1
β)) : List: Type u_1 → Type u_1
List (Nat: Type
Nat × β: Type u_1
β) :=
match t: Tree β
t with
| leaf: {β : Type ?u.9422} → Tree β
leaf => acc: List (Nat × β)
acc
| node: {β : Type ?u.9432} → Tree β → Nat → β → Tree β → Tree β
node l: Tree β
l k: Nat
k v: β
v r: Tree β
r => go: Tree β → List (Nat × β) → List (Nat × β)
go l: Tree β
l ((k: Nat
k, v: β
v) :: go: Tree β → List (Nat × β) → List (Nat × β)
go r: Tree β
r acc: List (Nat × β)
acc)
We now prove that t.toList
and t.toListTR
return the same list.
The proof is on induction, and as we used the auxiliary function go
to define Tree.toListTR
, we use the auxiliary theorem go
to prove the theorem.
The proof of the auxiliary theorem is by induction on t
.
The generalizing acc
modifier instructs Lean to revert acc
, apply the
induction theorem for Tree
s, and then reintroduce acc
in each case.
By using generalizing
, we obtain the more general induction hypotheses
-
left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc
-
right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc
Recall that the combinator tac <;> tac'
runs tac
on the main goal and tac'
on each produced goal,
concatenating all goals produced by tac'
. In this theorem, we use it to apply
simp
and close each subgoal produced by the induction
tactic.
The simp
parameters toListTR.go
and toList
instruct the simplifier to try to reduce
and/or apply auto generated equation theorems for these two functions.
The parameter *
instructs the simplifier to use any equation in a goal as rewriting rules.
In this particular case, simp
uses the induction hypotheses as rewriting rules.
Finally, the parameter List.append_assoc
instructs the simplifier to use the
List.append_assoc
theorem as a rewriting rule.
theoremTree.toList_eq_toListTR (Tree.toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), toList t = toListTR tt :t: Tree βTreeTree: Type u_1 → Type u_1β) :β: Type u_1t.t: Tree βtoList =toList: {β : Type u_1} → Tree β → List (Nat × β)t.t: Tree βtoListTR :=toListTR: {β : Type u_1} → Tree β → List (Nat × β)Goals accomplished! 🐙whereGoals accomplished! 🐙go (go: ∀ (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = toList t ++ acct :t: Tree βTreeTree: Type u_1 → Type u_1β) (β: Type u_1acc :acc: List (Nat × β)List (List: Type u_1 → Type u_1Nat ×Nat: Typeβ)) :β: Type u_1toListTR.gotoListTR.go: {β : Type u_1} → Tree β → List (Nat × β) → List (Nat × β)tt: Tree βacc =acc: List (Nat × β)t.t: Tree βtoList ++toList: {β : Type u_1} → Tree β → List (Nat × β)acc :=acc: List (Nat × β)Goals accomplished! 🐙β: Type u_1
t: Tree β
acc: List (Nat × β)
leaftoListTR.go leaf acc = toList leaf ++ accβ: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = toList left✝ ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = toList right✝ ++ acc
acc: List (Nat × β)toListTR.go (node left✝ key✝ value✝ right✝) acc = toList (node left✝ key✝ value✝ right✝) ++ accβ: Type u_1
t: Tree β
acc: List (Nat × β)
leaftoListTR.go leaf acc = toList leaf ++ accβ: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = toList left✝ ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = toList right✝ ++ acc
acc: List (Nat × β)toListTR.go (node left✝ key✝ value✝ right✝) acc = toList (node left✝ key✝ value✝ right✝) ++ accGoals accomplished! 🐙
The [csimp]
annotation instructs the Lean code generator to replace
any Tree.toList
with Tree.toListTR
when generating code.
@[csimp] theoremTree.toList_eq_toListTR_csimp : @Tree.toList_eq_toListTR_csimp: @toList = @toListTRTree.toList = @Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)Tree.toListTR :=Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)Goals accomplished! 🐙β: Type u_1
t: Tree β
h.htoList t = toListTR tGoals 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.
inductiveBST :BST: {β : Type u_1} → Tree β → PropTreeTree: Type u_1 → Type u_1β →β: Type u_1Prop |Prop: Typeleaf :leaf: ∀ {β : Type u_1}, BST Tree.leafBSTBST: {β : Type u_1} → Tree β → Prop.leaf |.leaf: {β : Type u_1} → Tree βnode :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)ForallTree (funForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Propkk: Nat=>k <k: Natkey)key: Natleft →left: Tree ?m.11579ForallTree (funForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Propkk: Nat=>key <key: Natk)k: Natright →right: Tree ?m.11579BSTBST: {β : Type u_1} → Tree β → Propleft →left: Tree ?m.11579BSTBST: {β : Type u_1} → Tree β → Propright →right: Tree ?m.11579BST (BST: {β : Type u_1} → Tree β → Prop.node.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree βleftleft: Tree ?m.11579keykey: Natvaluevalue: ?m.11579right)right: Tree ?m.11579
We can use the macro
command to create helper tactics for organizing our proofs.
The macro have_eq x y
tries to prove x = y
using linear arithmetic, and then
immediately uses the new equality to substitute x
with y
everywhere in the goal.
The modifier local
specifies the scope of the macro.
/-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
and then replaces `lhs` with `rhs`. -/
local macro "have_eq " lhs: Lean.TSyntax `term
lhs:term: Lean.Parser.Category
term:max rhs: Lean.TSyntax `term
rhs:term: Lean.Parser.Category
term:max : tactic: Lean.Parser.Category
tactic =>
`(tactic|
(have h : $lhs: Lean.TSyntax `term
lhs = $rhs: Lean.TSyntax `term
rhs :=
-- TODO: replace with linarith
by simp_arith at *; apply Nat.le_antisymm <;> assumption
try subst $lhs: Lean.TSyntax `term
lhs))
The by_cases' e
is just the regular by_cases
followed by simp
using all
hypotheses in the current goal as rewriting rules.
Recall that the by_cases
tactic creates two goals. One where we have h : e
and
another one containing h : ¬ e
. The simplifier uses the h
to rewrite e
to True
in the first subgoal, and e
to False
in the second. This is particularly
useful if e
is the condition of an if
-statement.
/-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
local macro "by_cases' " e: Lean.TSyntax `term
e:term: Lean.Parser.Category
term : tactic: Lean.Parser.Category
tactic =>
`(tactic| by_cases $e: Lean.TSyntax `term
e <;> simp [*])
We can use the attribute [simp]
to instruct the simplifier to reduce given definitions or
apply rewrite theorems. The local
modifier limits the scope of this modification to this file.
attribute [local simp] Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert
We now prove that Tree.insert
preserves the BST invariant using induction and case analysis.
Recall that the tactic . tac
focuses on the main goal and tries to solve it using tac
, or else fails.
It is used to structure proofs in Lean.
The notation ‹e›
is just syntax sugar for (by assumption : e)
. That is, it tries to find a hypothesis h : e
.
It is useful to access hypothesis that have auto generated names (aka "inaccessible") names.
theoremTree.forall_insert_of_forall (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)h₁ :h₁: ForallTree p tForallTreeForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Proppp: Nat → ?m.18569 → Propt) (t: Tree ?m.18569h₂ :h₂: p key valuepp: Nat → ?m.18569 → Propkeykey: Natvalue) :value: ?m.18569ForallTreeForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Propp (p: Nat → ?m.18569 → Propt.t: Tree ?m.18569insertinsert: {β : Type u_1} → Tree β → Nat → β → Tree βkeykey: Natvalue) :=value: ?m.18569Goals accomplished! 🐙β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₁: ForallTree p t
h₂: p key valueForallTree p (insert t key value)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
leafForallTree 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)
nodeForallTree 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)
nodeForallTree p (insert (node left✝ k value✝ right✝) key value)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: key < k
node.inlForallTree p (node (insert left✝ key value) k value✝ right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: ¬key < kForallTree p (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: key < k
node.inlForallTree p (node (insert left✝ key value) k value✝ right✝)Goals accomplished! 🐙β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝: ¬key < k
node.inrForallTree p (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inlForallTree p (node left✝ k value✝ (insert right✝ key value))β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < keyForallTree p (node left✝ key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inlForallTree p (node left✝ k value✝ (insert right✝ key value))Goals accomplished! 🐙β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₂: p key value
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
ihl: ForallTree p (insert left✝ key value)
ihr: ForallTree p (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < key
node.inr.inrForallTree p (node left✝ key value right✝)β✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
value: β✝
left✝: Tree β✝
k: Nat
value✝: β✝
right✝: Tree β✝
hl: ForallTree p left✝
hp: p k value✝
hr: ForallTree p right✝
h₂: p k value
ihl: ForallTree p (insert left✝ k value)
ihr: ForallTree p (insert right✝ k value)
h✝¹, h✝: ¬k < k
node.inr.inrForallTree p (node left✝ k value right✝)theoremGoals accomplished! 🐙Tree.bst_insert_of_bst {Tree.bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (insert t key value)t :t: Tree βTreeTree: Type u_1 → Type u_1β} (β: Type u_1h :h: BST tBSTBST: {β : Type u_1} → Tree β → Propt) (t: Tree βkey :key: NatNat) (Nat: Typevalue :value: ββ) :β: Type u_1BST (BST: {β : Type u_1} → Tree β → Propt.t: Tree βinsertinsert: {β : Type u_1} → Tree β → Nat → β → Tree βkeykey: Natvalue) :=value: βGoals accomplished! 🐙β: Type u_1
t: Tree β
h: BST t
key: Nat
value: βBST (insert t key value)β: Type u_1
t: Tree β
key: Nat
value: β
leafBST (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)
nodeBST (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)
nodeBST (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)
nodeBST (if key < k then node (insert left✝ key value) k value✝ right✝ else if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: key < k
node.inlBST (node (insert left✝ key value) k value✝ right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: ¬key < kBST (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: key < k
node.inlBST (node (insert left✝ key value) k value✝ right✝)Goals accomplished! 🐙β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝: ¬key < k
node.inrBST (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inlBST (node left✝ k value✝ (insert right✝ key value))β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < keyBST (node left✝ key value right✝)β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: k < key
node.inr.inlBST (node left✝ k value✝ (insert right✝ key value))Goals accomplished! 🐙β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ key value)
ih₂: BST (insert right✝ key value)
h✝¹: ¬key < k
h✝: ¬k < key
node.inr.inrBST (node left✝ key value right✝)β: Type u_1
t: Tree β
value: β
k: Nat
left✝, right✝: Tree β
value✝: β
h₁: ForallTree (fun k_1 v => k_1 < k) left✝
h₂: ForallTree (fun k_1 v => k < k_1) right✝
b₁: BST left✝
b₂: BST right✝
ih₁: BST (insert left✝ k value)
ih₂: BST (insert right✝ k value)
h✝¹, h✝: ¬k < k
node.inr.inrBST (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 BinTree
s.
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.mkBinTree.mk: {β : Type u_1} → BinTree βBinTree.containsBinTree.contains: {β : Type u_1} → BinTree β → Nat → BoolBinTree.find?BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option βBinTree.insertBinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree βTree.find?Tree.find?: {β : Type u_1} → Tree β → Nat → Option βTree.containsTree.contains: {β : Type u_1} → Tree β → Nat → BoolTree.insert theoremTree.insert: {β : Type u_1} → Tree β → Nat → β → Tree βBinTree.find_mk (BinTree.find_mk: ∀ {β : Type u_1} (k : Nat), find? mk k = nonek :k: NatNat) :Nat: TypeBinTree.mk.BinTree.mk: {β : Type u_1} → BinTree βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk = (k: Natnone :none: {α : Type u_1} → Option αOptionOption: Type u_1 → Type u_1β) :=β: Type u_1Goals accomplished! 🐙theoremGoals accomplished! 🐙BinTree.find_insert (BinTree.find_insert: ∀ {β : Type u_1} (b : BinTree β) (k : Nat) (v : β), find? (insert b k v) k = some vb :b: BinTree βBinTreeBinTree: Type u_1 → Type u_1β) (β: Type u_1k :k: NatNat) (Nat: Typev :v: ββ) : (β: Type u_1b.b: BinTree βinsertinsert: {β : Type u_1} → BinTree β → Nat → β → BinTree βkk: Natv).v: βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk =k: Natsomesome: {α : Type u_1} → α → Option αv :=v: βGoals accomplished! 🐙;β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST tfind? (insert { val := t, property := h } k v) k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST tTree.find? (Tree.insert t k v) k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST tTree.find? (Tree.insert t k v) k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
nodeTree.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)
nodeTree.find? (if k < key then Tree.node (Tree.insert left k v) key value right else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: k < key
node.inlTree.find? (Tree.insert left k v) k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: ¬k < keyTree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: k < key
node.inlTree.find? (Tree.insert left k v) k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inl.nodeTree.find? (Tree.insert left k v) k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inl.nodeBST leftGoals accomplished! 🐙β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: ¬k < key
node.inrTree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k = some vβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝¹: ¬k < key
h✝: key < k
node.inr.inlTree.find? (Tree.insert right k v) k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inr.inl.nodeTree.find? (Tree.insert right k v) k = some v;β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k = some v
ihr: BST right → Tree.find? (Tree.insert right k v) k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right
node.inr.inl.nodeBST righttheoremGoals accomplished! 🐙BinTree.find_insert_of_ne (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'b :b: BinTree βBinTreeBinTree: Type u_1 → Type u_1β) (β: Type u_1h :h: k ≠ k'k ≠k: Natk') (k': Natv :v: ββ) : (β: Type u_1b.b: BinTree βinsertinsert: {β : Type u_1} → BinTree β → Nat → β → BinTree βkk: Natv).v: βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk' =k': Natb.b: BinTree βfind?find?: {β : Type u_1} → BinTree β → Nat → Option βk' :=k': NatGoals accomplished! 🐙;β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
t: Tree β
h: BST tfind? (insert { val := t, property := h } k v) k' = find? { val := t, property := h } k'β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
t: Tree β
h: BST tTree.find? (Tree.insert t k v) k' = Tree.find? t k'β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
t: Tree β
h: BST tTree.find? (Tree.insert t k v) k' = Tree.find? t k'β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
nodeTree.find? (if k < key then Tree.node (Tree.insert left k v) key value right else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' = if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
h: BST Tree.leaf
leaf(if k' < k then none else if k < k' then none else some v) = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inlnone = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k(if k < k' then none else some v) = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inlnone = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k(if k < k' then none else some v) = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inlnone = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: k' < k
leaf.inlnone = noneGoals accomplished! 🐙Goals accomplished! 🐙β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k
leaf.inr(if k < k' then none else some v) = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: k < k'
leaf.inr.inlnone = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'Falseβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: k < k'
leaf.inr.inlnone = noneβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'Falseβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inrFalseβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inrFalseβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inrFalseβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
leaf.inr.inrFalseβ: Type u_1
k': Nat
b: BinTree β
v: β
h✝²: BST Tree.leaf
h: k' ≠ k'
h✝¹, h✝: ¬k' < k'
leaf.inr.inrFalseGoals accomplished! 🐙β: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
nodeTree.find? (if k < key then Tree.node (Tree.insert left k v) key value right else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' = if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
nodeTree.find? (if k < key then Tree.node (Tree.insert left k v) key value right else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' = if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
nodeTree.find? (if k < key then Tree.node (Tree.insert left k v) key value right else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' = if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
h✝: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
nodeTree.find? (if k < key then Tree.node (Tree.insert left k v) key value right else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' = if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value;β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h✝: ¬k < key
node.inrTree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' = if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h✝¹: ¬k < key
h✝: ¬key < k
node.inr.inr(if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some v) = if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
h✝²: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝¹, h✝: ¬k < k
node.inr.inr(if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some v) = if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some value;β: Type u_1
k, k': Nat
b: BinTree β
h✝³: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝², h✝¹: ¬k < k
h✝: ¬k' < k
node.inr.inr.inr(if k < k' then Tree.find? right k' else some v) = if k < k' then Tree.find? right k' else some valueβ: Type u_1
k, k': Nat
b: BinTree β
h✝⁴: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'
h: BST (Tree.node left k value right)
hl: ForallTree (fun k_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝³, h✝²: ¬k < k
h✝¹: ¬k' < k
h✝: ¬k < k'
node.inr.inr.inr.inrv = valueβ: Type u_1
k': Nat
b: BinTree β
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
h✝⁴: k' ≠ k'
ihl: Tree.find? (Tree.insert left k' v) k' = Tree.find? left k'
ihr: Tree.find? (Tree.insert right k' v) k' = Tree.find? right k'
h: BST (Tree.node left k' value right)
hl: ForallTree (fun k v => k < k') left
hr: ForallTree (fun k v => k' < k) right
h✝³, h✝², h✝¹, h✝: ¬k' < k'
node.inr.inr.inr.inrv = valueGoals 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.
theoremHasType.det (HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂h₁ :h₁: HasType e t₁HasTypeHasType: Expr → Ty → Propee: Exprt₁) (t₁: Tyh₂ :h₂: HasType e t₂HasTypeHasType: Expr → Ty → Propee: Exprt₂) :t₂: Tyt₁ =t₁: Tyt₂ :=t₂: TyGoals accomplished! 🐙t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
natTy.nat = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (Expr.plus a✝² b✝) t₂Ty.nat = t₂t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂Ty.bool = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (Expr.and a✝² b✝) t₂Ty.bool = t₂t₂: Ty
v✝: Nat
h₂: HasType (Expr.nat v✝) t₂
natTy.nat = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.nat
a✝: HasType b✝ Ty.nat
h₂: HasType (Expr.plus a✝² b✝) t₂Ty.nat = t₂t₂: Ty
v✝: Bool
h₂: HasType (Expr.bool v✝) t₂Ty.bool = t₂t₂: Ty
a✝², b✝: Expr
a✝¹: HasType a✝² Ty.bool
a✝: HasType b✝ Ty.bool
h₂: HasType (Expr.and a✝² b✝) t₂Ty.bool = t₂a✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.bool
a✝²: HasType b✝ Ty.bool
a✝¹: HasType a✝⁴ Ty.bool
a✝: HasType b✝ Ty.bool
and.andTy.bool = Ty.boolv✝: Nat
nat.natTy.nat = Ty.nata✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.nat
a✝²: HasType b✝ Ty.nat
a✝¹: HasType a✝⁴ Ty.nat
a✝: HasType b✝ Ty.natTy.nat = Ty.natv✝: BoolTy.bool = Ty.boola✝⁴, b✝: Expr
a✝³: HasType a✝⁴ Ty.bool
a✝²: HasType b✝ Ty.bool
a✝¹: HasType a✝⁴ Ty.bool
a✝: HasType b✝ Ty.boolTy.bool = Ty.boolGoals accomplished! 🐙
The inductive type Maybe p
has two constructors: found a h
and unknown
.
The former contains an element a : α
and a proof that a
satisfies the predicate p
.
The constructor unknown
is used to encode "failure".
inductive Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe (p: α → Prop
p : α: Sort u_1
α → Prop: Type
Prop) where
| found: {α : Sort u_1} → {p : α → Prop} → (a : α) → p a → Maybe p
found : (a: α
a : α: Sort u_1
α) → p: α → Prop
p a: α
a → Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe p: α → Prop
p
| unknown: {α : Sort u_1} → {p : α → Prop} → Maybe p
unknown
We define a notation for Maybe
that is similar to the builtin notation for the Lean builtin type Subtype
.
notation "{{ " x: Lean.TSyntax `term
x " | " p: Lean.TSyntax `term
p " }}" => Maybe: {α : Sort u_1} → (α → Prop) → Sort (max 1 u_1)
Maybe (fun x: Lean.TSyntax `term
x => p: Lean.TSyntax `term
p)
The function Expr.typeCheck e
returns a type ty
and a proof that e
has type ty
,
or unknown
.
Recall that, def Expr.typeCheck ...
in Lean is notation for namespace Expr def typeCheck ... end Expr
.
The term .found .nat .nat
is sugar for Maybe.found Ty.nat HasType.nat
. Lean can infer the namespaces using
the expected types.
defExpr.typeCheck (Expr.typeCheck: (e : Expr) → {{ ty | HasType e ty }}e :e: ExprExpr) : {{Expr: Typety |ty: TyHasTypeHasType: Expr → Ty → Propee: Exprty }} := matchty: Tye with |e: Exprnat .. =>nat: Nat → Expr.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat.nat: Ty.nat |.nat: ∀ {v : Nat}, HasType (nat v) Ty.natbool .. =>bool: Bool → Expr.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool.bool: Ty.bool |.bool: ∀ {v : Bool}, HasType (bool v) Ty.boolplusplus: Expr → Expr → Expraa: Exprb => matchb: Expra.a: ExprtypeCheck,typeCheck: (e : Expr) → {{ ty | HasType e ty }}b.b: ExprtypeCheck with |typeCheck: (e : Expr) → {{ ty | HasType e ty }}.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat.nat: Tyh₁,h₁: HasType a Ty.nat.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat.nat: Tyh₂ =>h₂: HasType b Ty.nat.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.nat (.nat: Ty.plus.plus: ∀ {a b : Expr}, HasType a Ty.nat → HasType b Ty.nat → HasType (plus a b) Ty.nath₁h₁: HasType a Ty.nath₂) | _, _ =>h₂: HasType b Ty.nat.unknown |.unknown: {α : Type} → {p : α → Prop} → Maybe pandand: Expr → Expr → Expraa: Exprb => matchb: Expra.a: ExprtypeCheck,typeCheck: (e : Expr) → {{ ty | HasType e ty }}b.b: ExprtypeCheck with |typeCheck: (e : Expr) → {{ ty | HasType e ty }}.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool.bool: Tyh₁,h₁: HasType a Ty.bool.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool.bool: Tyh₂ =>h₂: HasType b Ty.bool.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p.bool (.bool: Ty.and.and: ∀ {a b : Expr}, HasType a Ty.bool → HasType b Ty.bool → HasType (and a b) Ty.boolh₁h₁: HasType a Ty.boolh₂) | _, _ =>h₂: HasType b Ty.bool.unknown theorem.unknown: {α : Type} → {p : α → Prop} → Maybe pExpr.typeCheck_correct (Expr.typeCheck_correct: ∀ {e : Expr} {ty : Ty} {h : HasType e ty}, HasType e ty → typeCheck e ≠ Maybe.unknown → typeCheck e = Maybe.found ty hh₁ :h₁: HasType e tyHasTypeHasType: Expr → Ty → Propee: Exprty) (ty: Tyh₂ :h₂: typeCheck e ≠ Maybe.unknowne.e: ExprtypeCheck ≠typeCheck: (e : Expr) → {{ ty | HasType e ty }}.unknown) :.unknown: {α : Sort ?u.23455} → {p : α → Prop} → Maybe pe.e: ExprtypeCheck =typeCheck: (e : Expr) → {{ ty | HasType e ty }}.found.found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe ptyty: Tyh :=h: HasType e tyGoals accomplished! 🐙e: Expr
ty: Ty
h, h₁: HasType e tytypeCheck e ≠ Maybe.unknown → typeCheck e = Maybe.found ty he: Expr
ty: Ty
h, h₁: HasType e ty
x✝: {{ ty | HasType e ty }}x✝ ≠ Maybe.unknown → x✝ = Maybe.found ty he: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
foundMaybe.found ty' h' ≠ Maybe.unknown → Maybe.found ty' h' = Maybe.found ty h;e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
h₂✝: Maybe.found ty' h' ≠ Maybe.unknown
foundMaybe.found ty' h' = Maybe.found ty h;e: Expr
ty: Ty
h, h₁: HasType e ty
ty': Ty
h': HasType e ty'
h₂✝: Maybe.found ty' h' ≠ Maybe.unknown
this: ty = ty'
foundMaybe.found ty' h' = Maybe.found ty h;e: Expr
ty: Ty
h, h₁, h': HasType e ty
h₂✝: Maybe.found ty h' ≠ Maybe.unknown
foundMaybe.found ty h' = Maybe.found ty hGoals accomplished! 🐙e: Expr
ty: Ty
h, h₁: HasType e ty
unknownMaybe.unknown ≠ Maybe.unknown → Maybe.unknown = Maybe.found ty h;e: Expr
ty: Ty
h, h₁: HasType e ty
h₂✝: Maybe.unknown ≠ Maybe.unknown
unknownMaybe.unknown = Maybe.found ty hGoals 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
.
theoremExpr.typeCheck_complete {Expr.typeCheck_complete: ∀ {ty : Ty} {e : Expr}, typeCheck e = Maybe.unknown → ¬HasType e tye :e: ExprExpr} :Expr: Typee.e: ExprtypeCheck =typeCheck: (e : Expr) → {{ ty | HasType e ty }}.unknown → ¬.unknown: {α : Type} → {p : α → Prop} → Maybe pHasTypeHasType: Expr → Ty → Propee: Exprty :=ty: TyGoals accomplished! 🐙ty: Ty
e: ExprtypeCheck e = Maybe.unknown → ¬HasType e tyGoals 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) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: typeCheck a = Maybe.found Ty.nat h₁✝
heq✝: typeCheck b = Maybe.found Ty.nat h₂✝
plus.h_1Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown → ¬HasType (plus a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (plus a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: typeCheck a = Maybe.found Ty.nat h₁✝
heq✝: typeCheck b = Maybe.found Ty.nat h₂✝
plus.h_1Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown → ¬HasType (plus a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (plus a b) ty;ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.nat
h₂✝: HasType b Ty.nat
heq✝¹: typeCheck a = Maybe.found Ty.nat h₁✝
heq✝: typeCheck b = Maybe.found Ty.nat h₂✝
a✝: Maybe.found Ty.nat (_ : HasType (plus a b) Ty.nat) = Maybe.unknown¬HasType (plus a b) tyGoals accomplished! 🐙ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
plus.h_2Maybe.unknown = Maybe.unknown → ¬HasType (plus a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (plus a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (plus a b) tyht: HasType (plus a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (plus a b) tyFalsety: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (plus a b) tyFalsea, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), typeCheck a = Maybe.found Ty.nat h₁ → typeCheck b = Maybe.found Ty.nat h₂ → False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.nat
h₂: HasType b Ty.nat
iha: typeCheck a = Maybe.unknown → ¬HasType a Ty.nat
ihb: typeCheck b = Maybe.unknown → ¬HasType b Ty.nat
plusFalseGoals 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) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: typeCheck a = Maybe.found Ty.bool h₁✝
heq✝: typeCheck b = Maybe.found Ty.bool h₂✝
and.h_1Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown → ¬HasType (and a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (and a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: typeCheck a = Maybe.found Ty.bool h₁✝
heq✝: typeCheck b = Maybe.found Ty.bool h₂✝
and.h_1Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown → ¬HasType (and a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (and a b) ty;ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝¹: {{ ty | HasType a ty }}
x✝: {{ ty | HasType b ty }}
h₁✝: HasType a Ty.bool
h₂✝: HasType b Ty.bool
heq✝¹: typeCheck a = Maybe.found Ty.bool h₁✝
heq✝: typeCheck b = Maybe.found Ty.bool h₂✝
a✝: Maybe.found Ty.bool (_ : HasType (and a b) Ty.bool) = Maybe.unknown¬HasType (and a b) tyGoals accomplished! 🐙ty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
x✝²: {{ ty | HasType a ty }}
x✝¹: {{ ty | HasType b ty }}
x✝: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
and.h_2Maybe.unknown = Maybe.unknown → ¬HasType (and a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (and a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → FalseMaybe.unknown = Maybe.unknown → ¬HasType (and a b) tyht: HasType (and a b) tyty: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (and a b) tyFalsety: Ty
a, b: Expr
iha: typeCheck a = Maybe.unknown → ¬HasType a ty
ihb: typeCheck b = Maybe.unknown → ¬HasType b ty
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
ht: HasType (and a b) tyFalsea, b: Expr
ra: {{ ty | HasType a ty }}
rb: {{ ty | HasType b ty }}
hnp: ∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), typeCheck a = Maybe.found Ty.bool h₁ → typeCheck b = Maybe.found Ty.bool h₂ → False
h: Maybe.unknown = Maybe.unknown
h₁: HasType a Ty.bool
h₂: HasType b Ty.bool
iha: typeCheck a = Maybe.unknown → ¬HasType a Ty.bool
ihb: typeCheck b = Maybe.unknown → ¬HasType b Ty.bool
andFalseGoals accomplished! 🐙
Finally, we show that type checking for e
can be decided using Expr.typeCheck
.
instance: (e : Expr) → (t : Ty) → Decidable (HasType e t)
instance (e: Expr
e : Expr: Type
Expr) (t: Ty
t : Ty: Type
Ty) : Decidable: Prop → Type
Decidable (HasType: Expr → Ty → Prop
HasType e: Expr
e t: Ty
t) :=
match h': Expr.typeCheck e = Maybe.unknown
h' : e: Expr
e.typeCheck: (e : Expr) → {{ ty | HasType e ty }}
typeCheck with
| .found: {α : Type} → {p : α → Prop} → (a : α) → p a → Maybe p
.found t': Ty
t' ht': HasType e t'
ht' =>
if heq: t = t'
heq : t: Ty
t = t': Ty
t' then
isTrue: {p : Prop} → p → Decidable p
isTrue (heq: t = t'
heq ▸ ht': HasType e t'
ht')
else
isFalse: {p : Prop} → ¬p → Decidable p
isFalse fun ht: HasType e t
ht => heq: ¬t = t'
heq (HasType.det: ∀ {e : Expr} {t₁ t₂ : Ty}, HasType e t₁ → HasType e t₂ → t₁ = t₂
HasType.det ht: HasType e t
ht ht': HasType e t'
ht')
| .unknown: {α : Type} → {p : α → Prop} → Maybe p
.unknown => isFalse: {p : Prop} → ¬p → Decidable p
isFalse (Expr.typeCheck_complete: ∀ {ty : Ty} {e : Expr}, Expr.typeCheck e = Maybe.unknown → ¬HasType e ty
Expr.typeCheck_complete h': Expr.typeCheck e = Maybe.unknown
h')
The Well-Typed Interpreter
In this example, we build an interpreter for a simple functional programming language,
with variables, function application, binary operators and an if...then...else
construct.
We will use the dependent type system to ensure that any programs which can be represented are well-typed.
Remark: this example is based on an example found in the Idris manual.
Vectors
A Vector
is a list of size n
whose elements belong to a type α
.
inductive Vector: Type u → Nat → Type u
Vector (α: Type u
α : Type u: Type (u + 1)
Type u) : Nat: Type
Nat → Type u: Type (u + 1)
Type u
| nil: {α : Type u} → Vector α 0
nil : Vector: Type u → Nat → Type u
Vector α: Type u
α 0: Nat
0
| cons: {α : Type u} → {n : Nat} → α → Vector α n → Vector α (n + 1)
cons : α: Type u
α → Vector: Type u → Nat → Type u
Vector α: Type u
α n: Nat
n → Vector: Type u → Nat → Type u
Vector α: Type u
α (n: Nat
n+1: Nat
1)
We can overload the List.cons
notation ::
and use it to create Vector
s.
infix:67 " :: " => Vector.cons: {α : Type u} → {n : Nat} → α → Vector α n → Vector α (n + 1)
Vector.cons
Now, we define the types of our simple functional language.
We have integers, booleans, and functions, represented by Ty
.
inductive Ty: Type
Ty where
| int: Ty
int
| bool: Ty
bool
| fn: Ty → Ty → Ty
fn (a: Ty
a r: Ty
r : Ty: Type
Ty)
We can write a function to translate Ty
values to a Lean type
— remember that types are first class, so can be calculated just like any other value.
We mark Ty.interp
as [reducible]
to make sure the typeclass resolution procedure can
unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
Add (Ty.interp Ty.int)
. Since Ty.interp
is marked as [reducible]
,
the typeclass resolution procedure can reduce Ty.interp Ty.int
to Int
, and use
the builtin instance for Add Int
as the solution.
@[reducible] def Ty.interp: Ty → Type
Ty.interp : Ty: Type
Ty → Type: Type 1
Type
| int: Ty
int => Int: Type
Int
| bool: Ty
bool => Bool: Type
Bool
| fn: Ty → Ty → Ty
fn a: Ty
a r: Ty
r => a: Ty
a.interp: Ty → Type
interp → r: Ty
r.interp: Ty → Type
interp
Expressions are indexed by the types of the local variables, and the type of the expression itself.
inductive HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType : Fin: Nat → Type
Fin n: Nat
n → Vector: Type → Nat → Type
Vector Ty: Type
Ty n: Nat
n → Ty: Type
Ty → Type: Type 1
Type where
| stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType 0: Fin (?m.8928 + 1)
0 (ty: Ty
ty :: ctx: Vector Ty ?m.8928
ctx) ty: Ty
ty
| pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) ty
pop : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType k: Fin ?m.9102
k ctx: Vector Ty ?m.9102
ctx ty: Ty
ty → HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType k: Fin ?m.9102
k.succ: {n : Nat} → Fin n → Fin (Nat.succ n)
succ (u: Ty
u :: ctx: Vector Ty ?m.9102
ctx) ty: Ty
ty
inductive Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr : Vector: Type → Nat → Type
Vector Ty: Type
Ty n: Nat
n → Ty: Type
Ty → Type: Type 1
Type where
| var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType i: Fin ?m.9859
i ctx: Vector Ty ?m.9859
ctx ty: Ty
ty → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.9859
ctx ty: Ty
ty
| val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val : Int: Type
Int → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.9880
ctx Ty.int: Ty
Ty.int
| lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr (a: Ty
a :: ctx: Vector Ty ?m.10034
ctx) ty: Ty
ty → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10034
ctx (Ty.fn: Ty → Ty → Ty
Ty.fn a: Ty
a ty: Ty
ty)
| app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
app : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10181
ctx (Ty.fn: Ty → Ty → Ty
Ty.fn a: Ty
a ty: Ty
ty) → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10181
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10181
ctx ty: Ty
ty
| op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op : (a: Ty
a.interp: Ty → Type
interp → b: Ty
b.interp: Ty → Type
interp → c: Ty
c.interp: Ty → Type
interp) → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10271
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10271
ctx b: Ty
b → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10271
ctx c: Ty
c
| ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10392
ctx Ty.bool: Ty
Ty.bool → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10392
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10392
ctx a: Ty
a → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10392
ctx a: Ty
a
| delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay : (Unit: Type
Unit → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10435
ctx a: Ty
a) → Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.10435
ctx a: Ty
a
We use the command open
to create the aliases stop
and pop
for HasType.stop
and HasType.pop
respectively.
open HasType (stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) ty
pop)
Since expressions are indexed by their type, we can read the typing rules of the language from the definitions of the constructors. Let us look at each constructor in turn.
We use a nameless representation for variables — they are de Bruijn indexed.
Variables are represented by a proof of their membership in the context, HasType i ctx ty
,
which is a proof that variable i
in context ctx
has type ty
.
We can treat stop
as a proof that the most recently defined variable is well-typed,
and pop n
as a proof that, if the n
th most recently defined variable is well-typed, so is the n+1
th.
In practice, this means we use stop
to refer to the most recently defined variable,
pop stop
to refer to the next, and so on, via the Expr.var
constructor.
A value Expr.val
carries a concrete representation of an integer.
A lambda Expr.lam
creates a function. In the scope of a function of type Ty.fn a ty
, there is a
new local variable of type a
.
A function application Expr.app
produces a value of type ty
given a function from a
to ty
and a value of type a
.
The constructor Expr.op
allows us to use arbitrary binary operators, where the type of the operator informs what the types of the arguments must be.
Finally, the constructor Exp.ife
represents a if-then-else
expression. The condition is a Boolean, and each branch must have the same type.
The auxiliary constructor Expr.delay
is used to delay evaluation.
When we evaluate an Expr
, we’ll need to know the values in scope, as well as their types. Env
is an environment,
indexed over the types in scope. Since an environment is just another form of list, albeit with a strongly specified connection
to the vector of local variable types, we overload again the notation ::
so that we can use the usual list syntax.
Given a proof that a variable is defined in the context, we can then produce a value from the environment.
inductive Env: {n : Nat} → Vector Ty n → Type
Env : Vector: Type → Nat → Type
Vector Ty: Type
Ty n: Nat
n → Type: Type 1
Type where
| nil: Env Vector.nil
nil : Env: {n : Nat} → Vector Ty n → Type
Env Vector.nil: {α : Type} → Vector α 0
Vector.nil
| cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)
cons : Ty.interp: Ty → Type
Ty.interp a: Ty
a → Env: {n : Nat} → Vector Ty n → Type
Env ctx: Vector Ty ?m.14745
ctx → Env: {n : Nat} → Vector Ty n → Type
Env (a: Ty
a :: ctx: Vector Ty ?m.14745
ctx)
infix:67 " :: " => Env.cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)
Env.cons
def Env.lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp ty
Env.lookup : HasType: {n : Nat} → Fin n → Vector Ty n → Ty → Type
HasType i: Fin ?m.23254
i ctx: Vector Ty ?m.23254
ctx ty: Ty
ty → Env: {n : Nat} → Vector Ty n → Type
Env ctx: Vector Ty ?m.23254
ctx → ty: Ty
ty.interp: Ty → Type
interp
| stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) ty
stop, x: Ty.interp ty
x :: xs: Env ctx✝
xs => x: Ty.interp ty
x
| pop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) ty
pop k: HasType k✝ ctx✝ ty
k, x: Ty.interp u✝
x :: xs: Env ctx✝
xs => lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp ty
lookup k: HasType k✝ ctx✝ ty
k xs: Env ctx✝
xs
Given this, an interpreter is a function which translates an Expr
into a Lean value with respect to a specific environment.
def Expr.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
Expr.interp (env: Env ctx
env : Env: {n : Nat} → Vector Ty n → Type
Env ctx: Vector Ty ?m.28662
ctx) : Expr: {n : Nat} → Vector Ty n → Ty → Type
Expr ctx: Vector Ty ?m.28662
ctx ty: Ty
ty → ty: Ty
ty.interp: Ty → Type
interp
| var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx ty
var i: HasType i✝ ctx ty
i => env: Env ctx
env.lookup: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Env ctx → Ty.interp ty
lookup i: HasType i✝ ctx ty
i
| val: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int
val x: Int
x => x: Int
x
| lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
lam b: Expr (a✝ :: ctx) ty✝
b => fun x: Ty.interp a✝
x => b: Expr (a✝ :: ctx) ty✝
b.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp (Env.cons: {a : Ty} → {x : Nat} → {ctx : Vector Ty x} → Ty.interp a → Env ctx → Env (a :: ctx)
Env.cons x: Ty.interp a✝
x env: Env ctx
env)
| app: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
app f: Expr ctx (Ty.fn a✝ ty)
f a: Expr ctx a✝
a => f: Expr ctx (Ty.fn a✝ ty)
f.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env (a: Expr ctx a✝
a.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env)
| op: {n : Nat} →
{ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c
op o: Ty.interp a✝ → Ty.interp b✝ → Ty.interp ty
o x: Expr ctx a✝
x y: Expr ctx b✝
y => o: Ty.interp a✝ → Ty.interp b✝ → Ty.interp ty
o (x: Expr ctx a✝
x.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env) (y: Expr ctx b✝
y.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env)
| ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
ife c: Expr ctx Ty.bool
c t: Expr ctx ty
t e: Expr ctx ty
e => if c: Expr ctx Ty.bool
c.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env then t: Expr ctx ty
t.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env else e: Expr ctx ty
e.interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env
| delay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a
delay a: Unit → Expr ctx ty
a => (a: Unit → Expr ctx ty
a (): Unit
()).interp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp ty
interp env: Env ctx
env
open Expr
We can make some simple test functions. Firstly, adding two inputs fun x y => y + x
is written as follows.
defadd :add: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int))ExprExpr: {n : Nat} → Vector Ty n → Ty → Typectx (ctx: Vector Ty ?m.36312Ty.fnTy.fn: Ty → Ty → TyTy.int (Ty.int: TyTy.fnTy.fn: Ty → Ty → TyTy.intTy.int: TyTy.int)) :=Ty.int: Tylam (lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)lam (lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)opop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c(·+·) ((·+·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.intvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop) (stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyvar (var: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx typoppop: {x : Nat} → {k : Fin x} → {ctx : Vector Ty x} → {ty u : Ty} → HasType k ctx ty → HasType (Fin.succ k) (u :: ctx) tystop))))stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyadd.add: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int))interpinterp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyEnv.nilEnv.nil: Env Vector.nil1010: Ty.interp Ty.int2020: Ty.interp Ty.int
More interestingly, a factorial function fact (e.g. fun x => if (x == 0) then 1 else (fact (x-1) * x)
), can be written as.
Note that this is a recursive (non-terminating) definition. For every input value, the interpreter terminates, but the
definition itself is non-terminating. We use two tricks to make sure Lean accepts it. First, we use the auxiliary constructor
Expr.delay
to delay its unfolding. Second, we add the annotation decreasing_by sorry
which can be viewed as
"trust me, this recursive definition makes sense". Recall that sorry
is an unsound axiom in Lean.
def:ExprExpr: {n : Nat} → Vector Ty n → Ty → Typectx (ctx: Vector Ty ?m.39574Ty.fnTy.fn: Ty → Ty → TyTy.intTy.int: TyTy.int) :=Ty.int: Tylam (lam: {n : Nat} → {a : Ty} → {ctx : Vector Ty n} → {ty : Ty} → Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)ife (ife: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx aopop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c(·==·) ((·==·): Ty.interp Ty.int → Ty.interp Ty.int → Boolvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop) (stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyvalval: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int0)) (0: Intvalval: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int1) (1: Intopop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c(·*·) ((·*·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.intdelay fundelay: {n : Nat} → {ctx : Vector Ty n} → {a : Ty} → (Unit → Expr ctx a) → Expr ctx a_ =>_: Unitappapp: {n : Nat} → {ctx : Vector Ty n} → {a ty : Ty} → Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx tyfact (fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)opop: {n : Nat} → {ctx : Vector Ty n} → {a b c : Ty} → (Ty.interp a → Ty.interp b → Ty.interp c) → Expr ctx a → Expr ctx b → Expr ctx c(·-·) ((·-·): Ty.interp Ty.int → Ty.interp Ty.int → Ty.interp Ty.intvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop) (stop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyvalval: {n : Nat} → {ctx : Vector Ty n} → Int → Expr ctx Ty.int1))) (1: Intvarvar: {n : Nat} → {i : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType i ctx ty → Expr ctx tystop))) decreasing_bystop: {ty : Ty} → {x : Nat} → {ctx : Vector Ty x} → HasType 0 (ty :: ctx) tyGoals accomplished! 🐙fact.fact: {a : Nat} → {ctx : Vector Ty a} → Expr ctx (Ty.fn Ty.int Ty.int)interpinterp: {a : Nat} → {ctx : Vector Ty a} → {ty : Ty} → Env ctx → Expr ctx ty → Ty.interp tyEnv.nilEnv.nil: Env Vector.nil1010: Ty.interp Ty.int
Dependent de Bruijn Indices
In this example, we represent program syntax terms in a type family parameterized by a list of types, representing the typing context, or information on which free variables are in scope and what their types are.
Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.
Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a “type-level” list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Lean.
We parameterize our heterogeneous lists by at type α
and an α
-indexed type β
.
inductive HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList {α: Type v
α : Type v: Type (v + 1)
Type v} (β: α → Type u
β : α: Type v
α → Type u: Type (u + 1)
Type u) : List: Type v → Type v
List α: Type v
α → Type (max u v): Type ((max u v) + 1)
Type (max u v)
| nil: {α : Type v} → {β : α → Type u} → HList β []
nil : HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList β: α → Type u
β []: List α
[]
| cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
cons : β: α → Type u
β i: α
i → HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList β: α → Type u
β is: List α
is → HList: {α : Type v} → (α → Type u) → List α → Type (max u v)
HList β: α → Type u
β (i: α
i::is: List α
is)
We overload the List.cons
notation ::
so we can also use it to create
heterogeneous lists.
infix:67 " :: " => HList.cons: {α : Type v} → {β : α → Type u} → {i : α} → {is : List α} → β i → HList β is → HList β (i :: is)
HList.cons
We similarly overload the List
notation []
for the empty heterogeneous list.
notation "[" "]" => HList.nil: {α : Type v} → {β : α → Type u} → HList β []
HList.nil
Variables are represented in a way isomorphic to the natural numbers, where
number 0 represents the first element in the context, number 1 the second element, and so
on. Actually, instead of numbers, we use the Member
inductive family.
The value of type Member a as
can be viewed as a certificate that a
is
an element of the list as
. The constructor Member.head
says that a
is in the list if the list begins with it. The constructor Member.tail
says that if a
is in the list bs
, it is also in the list b::bs
.
inductive Member: {α : Type} → α → List α → Type
Member : α: Type
α → List: Type → Type
List α: Type
α → Type: Type 1
Type
| head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head : Member: {α : Type} → α → List α → Type
Member a: ?m.14887
a (a: ?m.14887
a::as: List ?m.14887
as)
| tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail : Member: {α : Type} → α → List α → Type
Member a: ?m.15049
a bs: List ?m.15049
bs → Member: {α : Type} → α → List α → Type
Member a: ?m.15049
a (b: ?m.15049
b::bs: List ?m.15049
bs)
Given a heterogeneous list HList β is
and value of type Member i is
, HList.get
retrieves an element of type β i
from the list.
The pattern .head
and .tail h
are sugar for Member.head
and Member.tail h
respectively.
Lean can infer the namespace using the expected type.
defHList.get :HList.get: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β iHListHList: {α : Type} → (α → Type u_1) → List α → Type u_1ββ: ?m.15578 → Type u_1is →is: List ?m.15578MemberMember: {α : Type} → α → List α → Typeii: ?m.15578is →is: List ?m.15578ββ: ?m.15578 → Type u_1i |i: ?m.15578a::a: β ias,as: HList β is✝.head =>.head: Member i (i :: is✝)a |a: β i::as,as: HList β is✝.tail.tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)h =>h: Member i is✝as.as: HList β is✝getget: {α : Type} → {β : α → Type u_1} → {is : List α} → {i : α} → HList β is → Member i is → β ihh: Member i is✝
Here is the definition of the simple type system for our programming language, a simply typed lambda calculus with natural numbers as the base type.
inductive Ty: Type
Ty where
| nat: Ty
nat
| fn: Ty → Ty → Ty
fn : Ty: Type
Ty → Ty: Type
Ty → Ty: Type
Ty
We can write a function to translate Ty
values to a Lean type
— remember that types are first class, so can be calculated just like any other value.
We mark Ty.denote
as [reducible]
to make sure the typeclass resolution procedure can
unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
Add (Ty.denote Ty.nat)
. Since Ty.denote
is marked as [reducible]
,
the typeclass resolution procedure can reduce Ty.denote Ty.nat
to Nat
, and use
the builtin instance for Add Nat
as the solution.
Recall that the term a.denote
is sugar for denote a
where denote
is the function being defined.
We call it the "dot notation".
@[reducible] def Ty.denote: Ty → Type
Ty.denote : Ty: Type
Ty → Type: Type 1
Type
| nat: Ty
nat => Nat: Type
Nat
| fn: Ty → Ty → Ty
fn a: Ty
a b: Ty
b => a: Ty
a.denote: Ty → Type
denote → b: Ty
b.denote: Ty → Type
denote
Here is the definition of the Term
type, including variables, constants, addition,
function application and abstraction, and let binding of local variables.
Since let
is a keyword in Lean, we use the "escaped identifier" «let»
.
You can input the unicode (French double quotes) using \f<<
(for «
) and \f>>
(for »
).
The term Term ctx .nat
is sugar for Term ctx Ty.nat
, Lean infers the namespace using the expected type.
inductive Term: List Ty → Ty → Type
Term : List: Type → Type
List Ty: Type
Ty → Ty: Type
Ty → Type: Type 1
Type
| var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var : Member: {α : Type} → α → List α → Type
Member ty: Ty
ty ctx: List Ty
ctx → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx ty: Ty
ty
| const: {ctx : List Ty} → Nat → Term ctx Ty.nat
const : Nat: Type
Nat → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx .nat: Ty
.nat
| plus: {ctx : List Ty} → Term ctx Ty.nat → Term ctx Ty.nat → Term ctx Ty.nat
plus : Term: List Ty → Ty → Type
Term ctx: List Ty
ctx .nat: Ty
.nat → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx .nat: Ty
.nat → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx .nat: Ty
.nat
| app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (Ty.fn dom ran) → Term ctx dom → Term ctx ran
app : Term: List Ty → Ty → Type
Term ctx: List Ty
ctx (.fn: Ty → Ty → Ty
.fn dom: Ty
dom ran: Ty
ran) → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx dom: Ty
dom → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx ran: Ty
ran
| lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (Ty.fn dom ran)
lam : Term: List Ty → Ty → Type
Term (dom: Ty
dom :: ctx: List Ty
ctx) ran: Ty
ran → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx (.fn: Ty → Ty → Ty
.fn dom: Ty
dom ran: Ty
ran)
| «let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» : Term: List Ty → Ty → Type
Term ctx: List Ty
ctx ty₁: Ty
ty₁ → Term: List Ty → Ty → Type
Term (ty₁: Ty
ty₁ :: ctx: List Ty
ctx) ty₂: Ty
ty₂ → Term: List Ty → Ty → Type
Term ctx: List Ty
ctx ty₂: Ty
ty₂
Here are two example terms encoding, the first addition packaged as a two-argument curried function, and the second of a sample application of addition to constants.
The command open Ty Term Member
opens the namespaces Ty
, Term
, and Member
. Thus,
you can write lam
instead of Term.lam
.
open Ty Term Member
def add: Term [] (fn nat (fn nat nat))
add : Term: List Ty → Ty → Type
Term []: List Ty
[] (fn: Ty → Ty → Ty
fn nat: Ty
nat (fn: Ty → Ty → Ty
fn nat: Ty
nat nat: Ty
nat)) :=
lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam (lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam (plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus (var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var (tail: {α : Type} → {a : α} → {bs : List α} → {b : α} → Member a bs → Member a (b :: bs)
tail head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head)) (var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var head: {α : Type} → {a : α} → {as : List α} → Member a (a :: as)
head)))
def three_the_hard_way: Term [] nat
three_the_hard_way : Term: List Ty → Ty → Type
Term []: List Ty
[] nat: Ty
nat :=
app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app (app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app add: Term [] (fn nat (fn nat nat))
add (const: {ctx : List Ty} → Nat → Term ctx nat
const 1: Nat
1)) (const: {ctx : List Ty} → Nat → Term ctx nat
const 2: Nat
2)
Since dependent typing ensures that any term is well-formed in its context and has a particular type, it is easy to translate syntactic terms into Lean values.
The attribute [simp]
instructs Lean to always try to unfold Term.denote
applications when one applies
the simp
tactic. We also say this is a hint for the Lean term simplifier.
@[simp] def Term.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
Term.denote : Term: List Ty → Ty → Type
Term ctx: List Ty
ctx ty: Ty
ty → HList: {α : Type} → (α → Type) → List α → Type
HList Ty.denote: Ty → Type
Ty.denote ctx: List Ty
ctx → ty: Ty
ty.denote: Ty → Type
denote
| var: {ty : Ty} → {ctx : List Ty} → Member ty ctx → Term ctx ty
var h: Member ty ctx
h, env: HList Ty.denote ctx
env => env: HList Ty.denote ctx
env.get: {α : Type} → {β : α → Type} → {is : List α} → {i : α} → HList β is → Member i is → β i
get h: Member ty ctx
h
| const: {ctx : List Ty} → Nat → Term ctx nat
const n: Nat
n, _ => n: Nat
n
| plus: {ctx : List Ty} → Term ctx nat → Term ctx nat → Term ctx nat
plus a: Term ctx nat
a b: Term ctx nat
b, env: HList Ty.denote ctx
env => a: Term ctx nat
a.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote env: HList Ty.denote ctx
env + b: Term ctx nat
b.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote env: HList Ty.denote ctx
env
| app: {ctx : List Ty} → {dom ran : Ty} → Term ctx (fn dom ran) → Term ctx dom → Term ctx ran
app f: Term ctx (fn dom✝ ty)
f a: Term ctx dom✝
a, env: HList Ty.denote ctx
env => f: Term ctx (fn dom✝ ty)
f.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote env: HList Ty.denote ctx
env (a: Term ctx dom✝
a.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote env: HList Ty.denote ctx
env)
| lam: {dom : Ty} → {ctx : List Ty} → {ran : Ty} → Term (dom :: ctx) ran → Term ctx (fn dom ran)
lam b: Term (dom✝ :: ctx) ran✝
b, env: HList Ty.denote ctx
env => fun x: Ty.denote dom✝
x => b: Term (dom✝ :: ctx) ran✝
b.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote (x: Ty.denote dom✝
x :: env: HList Ty.denote ctx
env)
| «let»: {ctx : List Ty} → {ty₁ ty₂ : Ty} → Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
«let» a: Term ctx ty₁✝
a b: Term (ty₁✝ :: ctx) ty
b, env: HList Ty.denote ctx
env => b: Term (ty₁✝ :: ctx) ty
b.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote (a: Term ctx ty₁✝
a.denote: {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Ty.denote ty
denote env: HList Ty.denote ctx