Program Specification in Lean

Stream: lean4

[Paul Chisholm]

My initial motivation for looking at Lean was I wanted to use a dependently typed language for the specification of programs, having previously had a fair amount of experience with more traditional approaches: non-dependent types, functions over those types, and predicate logic to specify properties of the data and functions.

Having built up a number of examples I thought it might be useful to put them together as a kind of tutorial for using Lean as a specification language. For anyone interested, the result is here.

[Mario Carneiro]

This looks really nice. In https://github.com/paulch42/lean-spec/blob/main/md/Sort.md , you talk about how the first version of the sorting specification is unimplementable, but the second version is also unimplementable because there is nothing that says that the comparison function is lawful. If it says that nothing is LE to itself then you still have the same issue.

[Paul Chisholm]

I have always found this rather confusing. What exactly is meant by 'lawful', and what has to change to make the definition dependent on LE being lawful.

[Kevin Buzzard]

I think "lawful" means "satisfies some axioms" -- it's the difference between docs#functor and docs#category_theory.functor for example -- the latter has map_id and map_comp, the former has nothing.

[Kevin Buzzard]

In the case in question, there is LT (no axioms) and PartialOrder (LT and some axioms)

[Kevin Buzzard]

So, for example, your claim that 2 is not less than 2 cannot be proved in general for just a type with LT.

[Paul Chisholm]

Ah, to be instances of the type classes LT and LE you just need to assign a couple of binary functions. There is no guarantee they are actually the functions we normally think of as 'less than' and 'less than or equal'.

Is PartialOrder in mathlib?

[Kevin Buzzard]

Yes and yes (import Mathlib.Init.Algebra.Order). Of course for Nat and Int if there are instances then they're going to be the sensible ones, but you were using alpha.

[Paul Chisholm]

Thanks. I didn't want to include mathlib since I am interested in general purpose programming that mathlib mostly has no relevance to.

[Paul Chisholm]

Perhaps something like this belongs on std4.

[Kevin Buzzard]

def foo := Nat

instance (n : Nat) : OfNat foo n := ⟨(n : Nat)⟩

instance : LT foo := ⟨fun _ _ => True⟩

example : (2 : foo) < 2 := True.intro

[Kevin Buzzard]

You could just reword so instead of talking about LT you talk only about LT on nat or some other type with an LT that satisfies some sensible axioms. In the above code I create a type synonym for nat which type class inference can't see through, enabling me to redefine < on it.

[Patrick Massot]

Paul, the example:

def permutation₁ (as bs : List α) :=
  ∀ a : α, a ∈ as ↔ a ∈ bs

is really weird. I know that at this stage you have in mind lists with distincts elements. But nothing warns your readers, you simply wrote above that snippet "Two lists are permutations of each other if they contain the same items, irrespective of order:", which is simply not what permutation means.

[Kevin Buzzard]

permutation₁ [1,2,2] [1,1,2] :-/

[Kevin Buzzard]

But this is fixed later on with permutation₂

[Paul Chisholm]

@Kevin Buzzard Thanks for that. Yes, I will think about some suitable revision. I think there might be a couple of other places that need a similar change.

@Patrick Massot Yes, I was trying to approach it as something someone might come up with initially and get it wrong, then correct it. But I see your point.

[Patrick Massot]

I understand it is fixed later, but I think a warning is in order, something like: "let's first try a naive definition".