In my last post I described a style which uses Subtype as a return type in order to merge the primary theorem about a function with its type signature. If I use this style for my own code, my functions will take inputs of some arbitrary types, but always return a Subtype as a final result. And when writing new code I will want to combine such functions by applying one to the result of another. More precisely, given a value of type Subtype p_α, with p_α : α → Prop, and a function f : α → Subtype p_β , with p_β : β → Prop, I want to get a result of type Subtype p_β‘, for some suitable[…]
Tag: Proofs
I haven’t posted a new article since my previous post on Fibonacci numbers. I found the idea of proving the correctness of my function highly tantalizing, but also more cumbersome than necessary. So I started working on some code which would help me prove statements about functions. This has absorbed the entire time I spend with Lean since then and I haven’t solved any additional Euler problems yet. This post describes the starting point of my journey. The standard style which I find in Mathlib is to write functions with functional code, just like I would in Haskell, and have separate theorems about properties of these functions with proofs. This is the style which I also used for the Fibonacci[…]
I am fascinated by Lean 4, because it looks like a great programming language and on top of this it also provides the facilities for proving theorems about code written in this language. Today, in a typical software engineering project, I would define a custom structure, to represent a concept, i.e. I have a network of interdependent tasks, which need to be run under certain circumstances. Usually there are some requirements on the state of this structure, such that it makes sense based on this concept, i.e. the tasks have lists of upstream and downstream tasks and a tasks needs to be in the downstream list of each of the tasks in its upstream list. These are called “(class) invariants”[…]