The simplest type type with a recursive constructor is the type of natural numbers. Here’s our own implementation. Note O is the capital letter O, not the numeral 0. The most transparent parts of this definition are the constructors. We know O : mynat and we know succ n : mynat, given n : mynat. […]
Category: Fundamental concepts
Well-founded recursion
Abstract Well-founded recursion generalises both strong induction and recursion. In this post we’ll: Discuss the (informal) notion of a well-founded relation. Show how to use well-founded relations (initially just with the < relation on ℕ) to define recursive functions and prove theorems using the equation compiler and by writing proof terms. Explain why rfl proofs […]
What the rec? Types dependent on terms, Lean eliminators, and threshold concepts
Abstract Lean eliminators combine the notions of recursion and induction. Put another way, eliminators are used to define functions on an inductive type (such as \(\mathbb N\)). The motive describes what kind of function is being defined. To understand motives, one needs to know about types-dependent-on-terms, a threshold concept (in the language of education) that […]
Vectors and dependent function types
Ordinary mathematical functions have a domain and a codomain. In Lean, we write f : α → β to denote that f is a function with domain α and codomain β. More briefly, that f is a function from α to β. The following is a simple example of a function from ℕ to ℤ that we’ve called double. […]
Decidable propositions III
We’ve seen the basics of decidable in Decidable propositions I and if-then-else constructions in Decidable propostions II. Now, we’ll see how to prove results through type class inference. If you’ve been following along and recreating decidable in your own hidden namespace, it’s now time to declare an important, albeit trivial, instance. That is, it is […]
Decidable propositions II
Recall from our previous post the definition of decidable. We’ll later discuss how this class works in conjunction with type class inference to automate proofs of decidable propositions. In this post, we show how conditionals are implemented in Lean using the decidable recursor. If-then-else The ite function is one of two Lean implementations of an […]
Decidable propositions I
In our last post, we looked at relations and briefly showed how Lean can sometimes prove a relation is decidable. Here, we take a closer look at decidability, a concept that rests on three pillars: An inductive type class through which propositions can be marked as decidable. A type class inference system for automatically proving […]
Relations in Lean
What is a relation? In a typical undergraduate mathematics course, a relation on a set is defined to be a subset of , the cartesian product of with itself. In the Lean approach, a relation on a type α is a function of type α → α → Prop. That is, a function that takes two terms x and […]