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 […]

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 […]