Workshop announcement On 24 July 2024, the University of Exeter is hosting a hybrid one-day workshop on interactive theorem proving in education and research. A one-day workshop focused on how interactive theorem provers, like Lean and Isabelle, can be used in mathematics and computer science. This event is ideal for educators and researchers who use […]
Author: Gihan Marasingha
Lean 3 & the new elan on ARM Mac
Of course, Lean 3 is now deprecated. But you may still want to access old Lean 3 projects. The latest version of elan (3.1.1) can’t automatically install Lean 3 toolchains (at least not on a Mac with an ARM CPU). For example, if you have cloned a Lean 3 repo and try to run leanpkg […]
Injectivity of succ
In the last post, I showed how to prove, using only elementary tools, that zero is not the successor of any natural number, that O = succ(m) leads to a contradiction. In this post, we’ll see that the successor function is injective. Writing S in place of succ, we’ll show that if S(m) = S(n), […]
One of these things is not like the other
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. […]
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 […]