chore: update Alectryon
This commit is contained in:
Sebastian Ullrich
parent
885deec745
commit
388ed62858
7 changed files with 83 additions and 83 deletions
|
|
@ -1,4 +1,4 @@
|
|||
/-|
|
||||
/-!
|
||||
# Binary Search Trees
|
||||
|
||||
If the type of keys can be totally ordered -- that is, it supports a well-behaved `≤` comparison --
|
||||
|
|
@ -9,7 +9,7 @@ This example is based on a similar example found in the ["Sofware Foundations"](
|
|||
book (volume 3).
|
||||
-/
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We use `Nat` as the key type in our implementation of BSTs,
|
||||
since it has a convenient total order with lots of theorems and automation available.
|
||||
We leave as an exercise to the reader the generalization to arbitrary types.
|
||||
|
|
@ -20,7 +20,7 @@ inductive Tree (β : Type v) where
|
|||
| node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
|
||||
deriving Repr
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The function `contains` returns `true` iff the given tree contains the key `k`.
|
||||
-/
|
||||
def Tree.contains (t : Tree β) (k : Nat) : Bool :=
|
||||
|
|
@ -34,7 +34,7 @@ def Tree.contains (t : Tree β) (k : Nat) : Bool :=
|
|||
else
|
||||
true
|
||||
|
||||
/-|
|
||||
/-!
|
||||
`t.find? k` returns `some v` if `v` is the value bound to key `k` in the tree `t`. It returns `none` otherwise.
|
||||
-/
|
||||
def Tree.find? (t : Tree β) (k : Nat) : Option β :=
|
||||
|
|
@ -48,7 +48,7 @@ def Tree.find? (t : Tree β) (k : Nat) : Option β :=
|
|||
else
|
||||
some 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 (t : Tree β) (k : Nat) (v : β) : Tree β :=
|
||||
|
|
@ -61,7 +61,7 @@ def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
|
|||
node left key value (right.insert k v)
|
||||
else
|
||||
node left k v 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.
|
||||
|
|
@ -80,7 +80,7 @@ def Tree.toList (t : Tree β) : List (Nat × β) :=
|
|||
|>.insert 1 "one"
|
||||
|>.toList
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The implemention of `Tree.toList` is inefficient because of how it uses the `++` operator.
|
||||
On a balanced tree its running time is linearithmic, because it does a linear number of
|
||||
concatentations at each level of the tree. On an unbalanced tree it's quadratic time.
|
||||
|
|
@ -94,7 +94,7 @@ where
|
|||
| leaf => acc
|
||||
| node l k v r => l.go ((k, v) :: r.go 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.
|
||||
|
|
@ -128,7 +128,7 @@ where
|
|||
induction t generalizing acc <;>
|
||||
simp [toListTR.go, toList, *, List.append_assoc]
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The `[csimp]` annotation instructs the Lean code generator to replace
|
||||
any `Tree.toList` with `Tree.toListTR` when generating code.
|
||||
-/
|
||||
|
|
@ -137,7 +137,7 @@ any `Tree.toList` with `Tree.toListTR` when generating code.
|
|||
funext β t
|
||||
apply toList_eq_toListTR
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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.
|
||||
|
|
@ -153,7 +153,7 @@ inductive ForallTree (p : Nat → β → Prop) : Tree β → Prop
|
|||
ForallTree p right →
|
||||
ForallTree p (.node left key value 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.
|
||||
|
|
@ -166,7 +166,7 @@ inductive BST : Tree β → Prop
|
|||
BST left → BST right →
|
||||
BST (.node left key value right)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We can use the `macro` command to create helper tactics for organizing our proofs.
|
||||
The macro `have_eq x y` tries to prove `x = y` using linear arithmetic, and then
|
||||
immediately uses the new equality to substitute `x` with `y` everywhere in the goal.
|
||||
|
|
@ -181,7 +181,7 @@ local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
|
|||
by simp_arith at *; apply Nat.le_antisymm <;> assumption
|
||||
try subst $lhs:term))
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The `by_cases' e` is just the regular `by_cases` followed by `simp` using all
|
||||
hypotheses in the current goal as rewriting rules.
|
||||
Recall that the `by_cases` tactic creates two goals. One where we have `h : e` and
|
||||
|
|
@ -194,13 +194,13 @@ local macro "by_cases' " e:term : tactic =>
|
|||
`(by_cases $e:term <;> simp [*])
|
||||
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We can use the attribute `[simp]` to instruct the simplifier to reduce given definitions or
|
||||
apply rewrite theorems. The `local` modifier limits the scope of this modification to this file.
|
||||
-/
|
||||
attribute [local simp] Tree.insert
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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.
|
||||
|
|
@ -237,7 +237,7 @@ theorem Tree.bst_insert_of_bst
|
|||
. have_eq key k
|
||||
exact .node h₁ h₂ b₁ b₂
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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) := { t : Tree β // BST t }
|
||||
|
|
@ -254,7 +254,7 @@ def BinTree.find? (b : BinTree β) (k : Nat) : Option β :=
|
|||
def BinTree.insert (b : BinTree β) (k : Nat) (v : β) : BinTree β :=
|
||||
⟨b.val.insert k v, b.val.bst_insert_of_bst b.property k v⟩
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Finally, we prove that `BinTree.find?` and `BinTree.insert` satisfy the map properties.
|
||||
-/
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
/-|
|
||||
/-!
|
||||
# Dependent de Bruijn Indices
|
||||
|
||||
In this example, we represent program syntax terms in a type family parameterized by a list of types,
|
||||
|
|
@ -9,7 +9,7 @@ their types are.
|
|||
Remark: this example is based on an example in the book [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) 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
|
||||
|
|
@ -24,16 +24,16 @@ inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
|
|||
| nil : HList β []
|
||||
| cons : β i → HList β is → HList β (i::is)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We overload the `List.cons` notation `::` so we can also use it to create
|
||||
heterogeneous lists.
|
||||
-/
|
||||
infix:67 " :: " => HList.cons
|
||||
|
||||
/-| We similarly overload the `List` notation `[]` for the empty heterogeneous list. -/
|
||||
/-! We similarly overload the `List` notation `[]` for the empty heterogeneous list. -/
|
||||
notation "[" "]" => HList.nil
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Variables are represented in a way isomorphic to the natural numbers, where
|
||||
number 0 represents the first element in the context, number 1 the second element, and so
|
||||
on. Actually, instead of numbers, we use the `Member` inductive family.
|
||||
|
|
@ -47,7 +47,7 @@ inductive Member : α → List α → Type
|
|||
| head : Member a (a::as)
|
||||
| tail : Member a bs → Member a (b::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.
|
||||
|
|
@ -57,7 +57,7 @@ def HList.get : HList β is → Member i is → β i
|
|||
| a::as, .head => a
|
||||
| a::as, .tail h => as.get h
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Here is the definition of the simple type system for our programming language, a simply typed
|
||||
lambda calculus with natural numbers as the base type.
|
||||
-/
|
||||
|
|
@ -65,7 +65,7 @@ inductive Ty where
|
|||
| nat
|
||||
| fn : Ty → Ty → 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
|
||||
|
|
@ -81,7 +81,7 @@ We call it the "dot notation".
|
|||
| nat => Nat
|
||||
| fn a b => a.denote → b.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»`.
|
||||
|
|
@ -96,7 +96,7 @@ inductive Term : List Ty → Ty → Type
|
|||
| lam : Term (dom :: ctx) ran → Term ctx (.fn dom ran)
|
||||
| «let» : Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx 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.
|
||||
|
||||
|
|
@ -110,7 +110,7 @@ def add : Term [] (fn nat (fn nat nat)) :=
|
|||
def three_the_hard_way : Term [] nat :=
|
||||
app (app add (const 1)) (const 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.
|
||||
|
||||
|
|
@ -125,13 +125,13 @@ the `simp` tactic. We also say this is a hint for the Lean term simplifier.
|
|||
| lam b, env => fun x => b.denote (x :: env)
|
||||
| «let» a b, env => b.denote (a.denote env :: env)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
You can show that the denotation of `three_the_hard_way` is indeed `3` using reflexivity.
|
||||
-/
|
||||
example : three_the_hard_way.denote [] = 3 :=
|
||||
rfl
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We now define the constant folding optimization that traverses a term if replaces subterms such as
|
||||
`plus (const m) (const n)` with `const (n+m)`.
|
||||
-/
|
||||
|
|
@ -146,7 +146,7 @@ We now define the constant folding optimization that traverses a term if replace
|
|||
| const n, const m => const (n+m)
|
||||
| a', b' => plus a' b'
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The correctness of the `Term.constFold` is proved using induction, case-analysis, and the term simplifier.
|
||||
We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
|
||||
use hypotheses such as `a = b` as rewriting/simplications rules.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
/-|
|
||||
/-!
|
||||
# The Well-Typed Interpreter
|
||||
|
||||
In this example, we build an interpreter for a simple functional programming language,
|
||||
|
|
@ -8,7 +8,7 @@ We will use the dependent type system to ensure that any programs which can be r
|
|||
Remark: this example is based on an example found in the Idris manual.
|
||||
-/
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Vectors
|
||||
--------
|
||||
|
||||
|
|
@ -19,12 +19,12 @@ inductive Vector (α : Type u) : Nat → Type u
|
|||
| nil : Vector α 0
|
||||
| cons : α → Vector α n → Vector α (n+1)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We can overload the `List.cons` notation `::` and use it to create `Vector`s.
|
||||
-/
|
||||
infix:67 " :: " => Vector.cons
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Now, we define the types of our simple functional language.
|
||||
We have integers, booleans, and functions, represented by `Ty`.
|
||||
-/
|
||||
|
|
@ -33,7 +33,7 @@ inductive Ty where
|
|||
| bool
|
||||
| fn (a r : 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
|
||||
|
|
@ -47,7 +47,7 @@ the builtin instance for `Add Int` as the solution.
|
|||
| bool => Bool
|
||||
| fn a r => a.interp → r.interp
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Expressions are indexed by the types of the local variables, and the type of the expression itself.
|
||||
-/
|
||||
inductive HasType : Fin n → Vector Ty n → Ty → Type where
|
||||
|
|
@ -63,12 +63,12 @@ inductive Expr : Vector Ty n → Ty → Type where
|
|||
| ife : Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
|
||||
| delay : (Unit → Expr ctx a) → Expr ctx a
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We use the command `open` to create the aliases `stop` and `pop` for `HasType.stop` and `HasType.pop` respectively.
|
||||
-/
|
||||
open HasType (stop pop)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Since expressions are indexed by their type, we can read the typing rules of the language from the definitions of the constructors.
|
||||
Let us look at each constructor in turn.
|
||||
|
||||
|
|
@ -96,7 +96,7 @@ 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.
|
||||
|
|
@ -112,7 +112,7 @@ def Env.lookup : HasType i ctx ty → Env ctx → ty.interp
|
|||
| stop, x :: xs => x
|
||||
| pop k, x :: xs => lookup k 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 (env : Env ctx) : Expr ctx ty → ty.interp
|
||||
|
|
@ -126,7 +126,7 @@ def Expr.interp (env : Env ctx) : Expr ctx ty → ty.interp
|
|||
|
||||
open Expr
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We can make some simple test functions. Firstly, adding two inputs `fun x y => y + x` is written as follows.
|
||||
-/
|
||||
|
||||
|
|
@ -135,7 +135,7 @@ def add : Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int)) :=
|
|||
|
||||
#eval add.interp Env.nil 10 20
|
||||
|
||||
/-|
|
||||
/-!
|
||||
More interestingly, a factorial function fact (e.g. `fun x => if (x == 0) then 1 else (fact (x-1) * x)`), can be written as.
|
||||
Note that this is a recursive (non-terminating) definition. For every input value, the interpreter terminates, but the
|
||||
definition itself is non-terminating. We use two tricks to make sure Lean accepts it. First, we use the auxiliary constructor
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
/-|
|
||||
/-!
|
||||
# Palindromes
|
||||
|
||||
Palindromes are lists that read the same from left to right and from right to left.
|
||||
|
|
@ -16,13 +16,13 @@ inductive Palindrome : List α → Prop where
|
|||
| single : (a : α) → Palindrome [a]
|
||||
| sandwich : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The definition distinguishes three cases: (1) `[]` is a palindrome; (2) for any element
|
||||
`a`, the singleton list `[a]` is a palindrome; (3) for any element `a` and any palindrome
|
||||
`[b₁, . . ., bₙ]`, the list `[a, b₁, . . ., bₙ, a]` is a palindrome.
|
||||
-/
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate `h : Palindrome as`.
|
||||
-/
|
||||
theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by
|
||||
|
|
@ -31,18 +31,18 @@ theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by
|
|||
| single a => exact Palindrome.single a
|
||||
| sandwich a h ih => simp; exact Palindrome.sandwich _ ih
|
||||
|
||||
/-| If a list `as` is a palindrome, then the reverse of `as` is equal to itself. -/
|
||||
/-! If a list `as` is a palindrome, then the reverse of `as` is equal to itself. -/
|
||||
theorem reverse_eq_of_palindrome (h : Palindrome as) : as.reverse = as := by
|
||||
induction h with
|
||||
| nil => rfl
|
||||
| single a => rfl
|
||||
| sandwich a h ih => simp [ih]
|
||||
|
||||
/-| Note that you can also easily prove `palindrome_reverse` using `reverse_eq_of_palindrome`. -/
|
||||
/-! Note that you can also easily prove `palindrome_reverse` using `reverse_eq_of_palindrome`. -/
|
||||
example (h : Palindrome as) : Palindrome as.reverse := by
|
||||
simp [reverse_eq_of_palindrome h, h]
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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.
|
||||
-/
|
||||
|
|
@ -50,7 +50,7 @@ def List.last : (as : List α) → as ≠ [] → α
|
|||
| [a], _ => a
|
||||
| a₁::a₂:: as, _ => (a₂::as).last (by simp)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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.
|
||||
|
|
@ -63,7 +63,7 @@ We use the attribute `@[simp]` to instruct the `simp` tactic to use this theorem
|
|||
simp [last, dropLast]
|
||||
exact dropLast_append_last (as := a₂ :: as) (by simp)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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`.
|
||||
|
|
@ -84,7 +84,7 @@ theorem List.palindrome_ind (motive : List α → Prop)
|
|||
this ▸ h₃ _ _ _ ih
|
||||
termination_by _ as => as.length
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.
|
||||
Note that we use the `using` modifier to instruct the `induction` tactic to use this induction principle
|
||||
instead of the default one for lists.
|
||||
|
|
@ -99,7 +99,7 @@ theorem List.palindrome_of_eq_reverse (h : as.reverse = as) : Palindrome as := b
|
|||
have : as.reverse = as := by simp_all
|
||||
exact Palindrome.sandwich a (ih this)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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.
|
||||
|
|
@ -107,7 +107,7 @@ because we need to compare the list elements.
|
|||
def List.isPalindrome [DecidableEq α] (as : List α) : Bool :=
|
||||
as.reverse = as
|
||||
|
||||
/-|
|
||||
/-!
|
||||
It is straightforward to prove that `isPalindrome` is correct using the previously proved theorems.
|
||||
-/
|
||||
theorem List.isPalindrome_correct [DecidableEq α] (as : List α) : as.isPalindrome ↔ Palindrome as := by
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
/-|
|
||||
/-!
|
||||
# Parametric Higher-Order Abstract Syntax
|
||||
|
||||
In contrast to first-order encodings, higher-order encodings avoid explicit modeling of variable identity.
|
||||
|
|
@ -10,7 +10,7 @@ and we can start by attempting to apply it directly in Lean.
|
|||
Remark: this example is based on an example in the book [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) by Adam Chlipala.
|
||||
-/
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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.
|
||||
-/
|
||||
|
|
@ -18,7 +18,7 @@ inductive Ty where
|
|||
| nat
|
||||
| fn : Ty → Ty → 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
|
||||
|
|
@ -34,7 +34,7 @@ We call it the "dot notation".
|
|||
| nat => Nat
|
||||
| fn a b => a.denote → b.denote
|
||||
|
||||
/-|
|
||||
/-!
|
||||
With HOAS, each object language binding construct is represented with a function of
|
||||
the meta language. Here is what we get if we apply that idea within an inductive definition
|
||||
of term syntax. However a naive encondig in Lean fails to meet the strict positivity restrictions
|
||||
|
|
@ -50,7 +50,7 @@ inductive Term' (rep : Ty → Type) : Ty → Type
|
|||
| app : Term' rep (.fn dom ran) → Term' rep dom → Term' rep ran
|
||||
| «let» : Term' rep ty₁ → (rep ty₁ → Term' rep ty₂) → Term' rep ty₂
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Lean accepts this definition because our embedded functions now merely take variables as
|
||||
arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole
|
||||
to exploit here, instantiating the parameter `rep` as term itself. However, to do that, we
|
||||
|
|
@ -68,7 +68,7 @@ namespace FirstTry
|
|||
|
||||
def Term (ty : Ty) := (rep : Ty → Type) → Term' rep ty
|
||||
|
||||
/-|
|
||||
/-!
|
||||
In the next two example, note how each is written as a function over a `rep` choice,
|
||||
such that the specific choice has no impact on the structure of the term.
|
||||
-/
|
||||
|
|
@ -80,7 +80,7 @@ def three_the_hard_way : Term nat := fun rep =>
|
|||
|
||||
end FirstTry
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The argument `rep` does not even appear in the function body for `add`. How can that be?
|
||||
By giving our terms expressive types, we allow Lean to infer many arguments for us. In fact,
|
||||
we do not even need to name the `rep` argument! By using Lean implicit arguments and lambdas,
|
||||
|
|
@ -95,7 +95,7 @@ def add : Term (fn nat (fn nat nat)) :=
|
|||
def three_the_hard_way : Term nat :=
|
||||
app (app add (const 1)) (const 2)
|
||||
|
||||
/-|
|
||||
/-!
|
||||
It may not be at all obvious that the PHOAS representation admits the crucial computable
|
||||
operations. The key to effective deconstruction of PHOAS terms is one principle: treat
|
||||
the `rep` parameter as an unconstrained choice of which data should be annotated on each
|
||||
|
|
@ -114,12 +114,12 @@ def countVars : Term' (fun _ => Unit) ty → Nat
|
|||
| lam b => countVars (b ())
|
||||
| «let» a b => countVars a + countVars (b ())
|
||||
|
||||
/-| We can now easily prove that `add` has two variables by using reflexivity -/
|
||||
/-! We can now easily prove that `add` has two variables by using reflexivity -/
|
||||
|
||||
example : countVars add = 2 :=
|
||||
rfl
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Here is another example, translating PHOAS terms into strings giving a first-order rendering.
|
||||
To implement this translation, the key insight is to tag variables with strings, giving their names.
|
||||
The function takes as an additional input `i` which is used to create variable names for binders.
|
||||
|
|
@ -141,7 +141,7 @@ def pretty (e : Term' (fun _ => String) ty) (i : Nat := 1) : String :=
|
|||
|
||||
#eval pretty three_the_hard_way
|
||||
|
||||
/-|
|
||||
/-!
|
||||
It is not necessary to convert to a different representation to support many common
|
||||
operations on terms. For instance, we can implement substitution of terms for variables.
|
||||
The key insight here is to tag variables with terms, so that, on encountering a variable, we
|
||||
|
|
@ -158,13 +158,13 @@ def squash : Term' (Term' rep) ty → Term' rep ty
|
|||
| app f a => app (squash f) (squash a)
|
||||
| «let» a b => «let» (squash a) fun x => squash (b (.var x))
|
||||
|
||||
/-|
|
||||
/-!
|
||||
To define the final substitution function over terms with single free variables, we define
|
||||
`Term1`, an analogue to Term that we defined before for closed terms.
|
||||
-/
|
||||
def Term1 (ty1 ty2 : Ty) := {rep : Ty → Type} → rep ty1 → Term' rep ty2
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Substitution is defined by (1) instantiating a `Term1` to tag variables with terms and (2)
|
||||
applying the result to a specific term to be substituted. Note how the parameter `rep` of
|
||||
`squash` is instantiated: the body of `subst` is itself a polymorphic quantification over `rep`,
|
||||
|
|
@ -175,7 +175,7 @@ tag choice for the input term.
|
|||
def subst (e : Term1 ty1 ty2) (e' : Term ty1) : Term ty2 :=
|
||||
squash (e e')
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We can view `Term1` as a term with hole. In the following example,
|
||||
`(fun x => plus (var x) (const 5))` can be viewed as the term `plus _ (const 5)` where
|
||||
the hole `_` is instantiated by `subst` with `three_the_hard_way`
|
||||
|
|
@ -183,7 +183,7 @@ the hole `_` is instantiated by `subst` with `three_the_hard_way`
|
|||
|
||||
#eval pretty <| subst (fun x => plus (var x) (const 5)) three_the_hard_way
|
||||
|
||||
/-|
|
||||
/-!
|
||||
One further development, which may seem surprising at first,
|
||||
is that we can also implement a usual term denotation function,
|
||||
when we tag variables with their denotations.
|
||||
|
|
@ -202,13 +202,13 @@ the `simp` tactic. We also say this is a hint for the Lean term simplifier.
|
|||
example : denote three_the_hard_way = 3 :=
|
||||
rfl
|
||||
|
||||
/-|
|
||||
/-!
|
||||
To summarize, the PHOAS representation has all the expressive power of more
|
||||
standard encodings (e.g., using de Bruijn indices), and a variety of translations are actually much more pleasant to
|
||||
implement than usual, thanks to the novel ability to tag variables with data.
|
||||
-/
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We now define the constant folding optimization that traverses a term if replaces subterms such as
|
||||
`plus (const m) (const n)` with `const (n+m)`.
|
||||
-/
|
||||
|
|
@ -223,7 +223,7 @@ We now define the constant folding optimization that traverses a term if replace
|
|||
| const n, const m => const (n+m)
|
||||
| a', b' => plus a' b'
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The correctness of the `constFold` is proved using induction, case-analysis, and the term simplifier.
|
||||
We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
|
||||
use hypotheses such as `a = b` as rewriting/simplications rules.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
/-|
|
||||
/-!
|
||||
# A Certified Type Checker
|
||||
|
||||
In this example, we build a certified type checker for a simple expression
|
||||
|
|
@ -12,7 +12,7 @@ inductive Expr where
|
|||
| bool : Bool → Expr
|
||||
| and : Expr → Expr → Expr
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We define a simple language of types using the inductive datatype `Ty`, and
|
||||
its typing rules using the inductive predicate `HasType`.
|
||||
-/
|
||||
|
|
@ -27,7 +27,7 @@ inductive HasType : Expr → Ty → Prop
|
|||
| bool : HasType (.bool v) .bool
|
||||
| and : HasType a .bool → HasType b .bool → HasType (.and a b) .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
|
||||
|
|
@ -37,7 +37,7 @@ goals using reflexivity.
|
|||
theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
|
||||
cases h₁ <;> cases h₂ <;> rfl
|
||||
|
||||
/-|
|
||||
/-!
|
||||
The inductive type `Maybe p` has two contructors: `found a h` and `unknown`.
|
||||
The former contains an element `a : α` and a proof that `a` satisfies the predicate `p`.
|
||||
The constructor `unknown` is used to encode "failure".
|
||||
|
|
@ -47,12 +47,12 @@ inductive Maybe (p : α → Prop) where
|
|||
| found : (a : α) → p a → Maybe p
|
||||
| unknown
|
||||
|
||||
/-|
|
||||
/-!
|
||||
We define a notation for `Maybe` that is similar to the builtin notation for the Lean builtin type `Subtype`.
|
||||
-/
|
||||
notation "{{ " x " | " p " }}" => Maybe (fun x => 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`.
|
||||
|
|
@ -79,7 +79,7 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un
|
|||
| found ty' h' => intro; have := HasType.det h₁ h'; subst this; rfl
|
||||
| unknown => intros; contradiction
|
||||
|
||||
/-|
|
||||
/-!
|
||||
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.
|
||||
|
|
@ -106,7 +106,7 @@ theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasTy
|
|||
cases ht with
|
||||
| and h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))
|
||||
|
||||
/-|
|
||||
/-!
|
||||
Finally, we show that type checking for `e` can be decided using `Expr.typeCheck`.
|
||||
-/
|
||||
instance (e : Expr) (t : Ty) : Decidable (HasType e t) :=
|
||||
|
|
|
|||
6
doc/flake.lock
generated
6
doc/flake.lock
generated
|
|
@ -3,11 +3,11 @@
|
|||
"alectryon-src": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1654264305,
|
||||
"narHash": "sha256-g3XyrKj1y2WMZjVjGxBsMZRcO5DMRfYZjzaoC03itWE=",
|
||||
"lastModified": 1654613606,
|
||||
"narHash": "sha256-IGCn1PzTyw8rrwmyWUiw3Jo/dyZVGkMslnHYW7YB8yk=",
|
||||
"owner": "Kha",
|
||||
"repo": "alectryon",
|
||||
"rev": "fbd16c38cbf261875f1db80d4c43cf0715ec56ea",
|
||||
"rev": "c3b16f650665745e1da4ddfcc048d3bd639f71d5",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue