Learning Lean 4 as a programming language 6 – Predicate and Subtypes monads
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 p_β' : β → Prop, that means I want a function with type signature: Subtype p_α → (β → Subtype p_β) → Subtype p_β‘. This looks almost like the type signature of the monadic bind. It’s not quite the same, since Subtype uses a predicate, rather than a type as an argument. But with a small tweak, it’s possible to construct a functor Subtypes which is also a lawful monad. The reason this is possible is because in Lean 4 Predicate is a lawful (covariant) functor and monad.
The Predicate monad
In the context of Lean, a predicate is a map from a type α to Prop. While there is a DecidablePred in mathlib, there doesn’t exist a Predicate type yet, so I define it myself. This also includes the imports I need and starts the Predicate namespace.
import Mathlib.Data.Set.Functor
import Mathlib.Tactic
import Enumerations.Tactic
def Predicate (α : Type u) := α → Prop
namespace PredicateThe most obvious way to create a new predicate from a given predicate and a function is simple composition.
def contramap {α β : Type u} (f : α → β) (p : β → Prop) := p ∘ fI’ve called this function contramap because it is contravariant, given a function f : α → β, I get a function contramap f : Predicate β → Predicate α, which switches α and β. This turns Predicate into a contravariant functor, a construction which is also possible in Haskell. But in Lean it is also possible to define the following covariant map function, which uses the existential quantor.
def map {α β : Type u} (f : α → β) (p : α → Prop) := fun b : β => ∃ a : α, p a ∧ b = f aThe resulting Predicate is in general undecidable, since finding the preimage of a function is in general undecidable. But this doesn’t worry me here, since I can still use it to reason about programs, even if computing such a predicate would require proving decidability.
With this I can create a Functor instance and prove it is lawful.
instance instFunctor : Functor Predicate where
map := map
def map_def {α β : Type u} (f : α → β) (p : α → Prop) := by
transform (f <$> p : Predicate β) =>
simp [Functor.map]
unfold map
instance instFunctor.instLawful : LawfulFunctor Predicate where
map_const := by
intro α β
apply Eq.refl
id_map := by
intro α a
simp only [map_def, id_eq, exists_eq_right']
comp_map := by
intros α β γ g h p
funext c
simp only [map_def, Function.comp_apply, eq_iff_iff]
constructor
· intro ⟨a, _⟩
use g a
simp_all only [and_true]
use a
simp_all only [and_self]
· intro ⟨b, ⟨a, _⟩, eq⟩
subst eq
use a
simp_all only [and_self]But Predicate is more than just a Functor, it is also a Monad.
def pure {α : Type u} (a : α) : Predicate α := fun a' => a' = a
def bind {α : Type u} {β : Type v} (p : Predicate α) (f : α → Predicate β) : Predicate β :=
fun b => ∃ a : α, p a ∧ f a b
instance instMonad : Monad Predicate where
pure := pure
bind := bindI find the definition for pure quite natural, and the definition of bind uses the same trick as map.
In the next part, I am using a custom tactic, which allows me to use tactics to write a theorem, almost like in a computer algebra system. It only works for def rather than theorem, and I don’t understand the downsides of that, but as far as I’ve seen, it works quite nicely.
def pure_def {α : Type u} (a : α) := by
transform (Pure.pure a : Predicate α) =>
simp only [Pure.pure]
unfold pure
def bind_def {α β : Type u} (f : α → Predicate β) (p : Predicate α) := by
transform p >>= f =>
simp only [Bind.bind]
unfold bind
def seq_def {α β : Type u} (f : Predicate (α → β)) (p : Predicate α) := by
transform f <*> p =>
simp only [Seq.seq, map_def]
unfold bind
simp only
@[simp]
theorem pure_apply {α : Type u} (a a' : α) : (Pure.pure a : Predicate α) a' ↔ a' = a := by rflI am still learning Lean and I have wondered why the monad laws are in a separate LawfulMonad type class and not folded into the Monad type class, but this turned out to be really useful here, since it allowed me to define the monad first and prove these properties of it, which I could then use to prove the monad laws.
instance instMonad.instLawful : LawfulMonad Predicate := by
apply LawfulMonad.mk'
· intro α a
funext a'
simp only [map_def, id_eq, exists_eq_right']
· intro α β a f
funext b
simp only [pure_def, bind_def]
apply propext; apply Iff.intro
· intro ⟨a', eq, h⟩
subst eq
exact h
· intro h
use a
· intros α β γ p f g
simp only [bind_def]
funext c
apply propext; apply Iff.intro
· intro ⟨b, ⟨a, _, _⟩, _⟩
use a
simp_all only [true_and]
use b
· intro ⟨a, _, ⟨b, _, _⟩⟩
use b
simp_all only [and_true]
use a
· intros α β f p
rfl
· intros α β p q
rfl
· intros α β p q
rfl
· intros α β f p
funext b
simp only [bind_def, map_def, pure_def]
· intros α β f p
simp only [bind_def, map_def, pure_def, seq_def]The Subtypes monad
Subtype obviously isn’t a functor, because it has the wrong type signature, but the following related type has the right signature.
import Enumerations.Predicate
structure Subtypes (α : Type u) : Type u where
predicate : (α → Prop)
val : α
property : predicate val
namespace SubtypesSince it only has α as a parameter, predicate needs to be another field in addition to val and property. I chose the plural name, because Subtypes α represents all possible Subtype-s for predicates over α.
def toSubtype {α : Type u} (s : Subtypes α) : Subtype s.predicate := ⟨s.val, s.property⟩
def fromSubtype {α : Type u} {p : α → Prop} (s : Subtype p) : Subtypes α := ⟨p, s.val, s.property⟩
instance {α : Type u} {p : α → Prop} : CoeOut (Subtype p) (Subtypes α) := ⟨fromSubtype⟩It’s straight forward to go from Subtype to Subtypes, though I don’t if it’s possible or advisable to setup a coercion from Subtypes to Subtype.
For the definition of map, I use that Predicate is a functor.
def map {α β : Type u} (f : α → β) (s : Subtypes α) :=
Subtypes.mk (f <$> s.predicate : Predicate β) (f s.val) <| by
simp only [Predicate.map_def]
use s.val
simp only [s.property, and_self]
instance instFunctor : Functor Subtypes where
map := map
def map_def {α β : Type u} (f : α → β) (s : Subtypes α) := by
transform (f <$> s) =>
simp only [Functor.map]
unfold map
@[simp]
theorem map_predicate {α β : Type u} (f : α → β) (s : Subtypes α) : (f <$> s).predicate = (f <$> s.predicate : Predicate β) := by
simp only [map_def, Set.fmap_eq_image]
@[simp]
theorem map_val {α β : Type u} (f : α → β) (s : Subtypes α) : (f <$> s).val = f s.val := by
simp only [map_def, Set.fmap_eq_image]
instance instFunctor.instLawful : LawfulFunctor Subtypes where
map_const := by
intro α β
rfl
id_map := by
intro α a
simp only [map_def, id_map, id_eq]
comp_map := by
intros α β γ g h p
simp only [map_def, comp_map, Function.comp_apply]The lawfulness of the Subtypes functor is a direct consequence of the lawfulness of the Predicate functor.
Defining the Subtypes monad and proving it’s lawfulness is analogous to what I’ve shown above.
def pure {α : Type u} (a : α) : Subtypes α := Subtypes.mk (Pure.pure a : Predicate α) a <| by
simp only [Predicate.pure_def]
def bind {α β : Type u} (s : Subtypes α) (f : α → Subtypes β) : Subtypes β :=
mk (s.predicate >>= fun a => (f a).predicate : Predicate β) (f s.val).val <| by
simp only [Predicate.bind_def]
use s.val
simp only [s.property, (f s.val).property, and_self]
instance instMonad : Monad Subtypes where
pure := pure
bind := bind
def pure_def {α : Type u} (a : α) := by
transform (Pure.pure a : Subtypes α) =>
simp only [Pure.pure]
unfold pure
def bind_def {α β : Type u} (f : α → Subtypes β) (s : Subtypes α) := by
transform s >>= f =>
simp only [Bind.bind]
unfold bind
@[simp]
theorem pure_predicate {α : Type u} (a : α) : (pure a).predicate = (Pure.pure a : Predicate α) := rfl
@[simp]
theorem bind_predicate {α β : Type u} (f : α → Subtypes β) (s : Subtypes α) :
(s >>= f).predicate = (s.predicate >>= fun x => (f x).predicate : Predicate β) := rfl
instance instMonad.instLawful : LawfulMonad Subtypes := by
apply LawfulMonad.mk'
· intro α a
simp only [map_def, id_map, id_eq]
· intro α β a f
simp only [pure_def, bind_def, pure_bind]
· intro α β γ a f g
simp only [bind_def, bind_assoc]
· intro α β f p
rfl
· intro α β f p
rfl
· intro α β f p
rfl
· intro α β f p
simp only [pure_def, bind_def, bind_pure_comp, map_def]
· intro α β f p
rfl
This Subtypes monad gets me a long way, but it isn’t the ultimate monad I want to use. The Subtypes monad allows me to express postconditions, but I also want to be able to easily state that the postcondition is the strongest possible. For this I constructed another monad, which I call Enumerations, and which I will present in a future post.