# Zulip Chat Archive

## Stream: new members

### Topic: Checking that a Monad instance is a Monad

#### Lars Ericson (Sep 10 2023 at 20:57):

@David Thrane Christiansen, in this exercise in Functional Programming in Lean, you give an example

```
instance : Monad Option where
pure x := some x
bind opt next := none
```

Lean accepts this as a Monad instance, but this one violates the Monad contract, which is that

```
(bind (pure v) = f v ) ∧
(bind v pure = v ) ∧
(bind (bind v f) g = bind v (fun x => bind (f x) g))
```

Lean being Lean, shouldn't these 3 properties be checked or require proof be supplied in order to instantiate a Monad? I don't see these three properties directly stated in the code for Monad:

```
class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) where
map f x := bind x (Function.comp pure f)
seq f x := bind f fun y => Functor.map y (x ())
seqLeft x y := bind x fun a => bind (y ()) (fun _ => pure a)
seqRight x y := bind x fun _ => y ()
```

Should the Monad contract be in there so that incorrect instances can't be derived? Is the Monad contract somewhere else in the code? What should I know about separating understanding of Lean as a programming language and Lean as a theorem prover? Is there a crossover between programming and theorem proving that I'm expecting (the idea of programs which are derived in accordance with specifications) which is not actually part of the paradigm?

#### Kyle Miller (Sep 10 2023 at 21:06):

There's docs#LawfulMonad for recording that a monad is *really* a monad

#### Kyle Miller (Sep 10 2023 at 21:09):

I think the split between `Monad`

and `LawfulMonad`

is for the functional programming side of things. Another split for example is docs#BEq and docs#LawfulBEq for whether this equality operation actually captures substitution-invariance.

#### David Thrane Christiansen (Sep 11 2023 at 06:27):

What Kyle said is totally right - the Lean library provides a version of `Monad`

that requires you to show that you follow the rules, and one that doesn't. I figured I'd supplement with why this exercise is the way it is.

The goal of this book is to be usable as a first introduction to functional programming. My guess is that it doesn't entirely succeed at this, but I really tried not to overwhelm and intimidate readers who haven't done these things before. The reason I chose to spend a fair bit of space on informally reasoning about monad laws, and the reason for this exercise, is to start getting people to start thinking in a way that is conducive to proving things, but that "feels" more like debugging a program.

In particular, I think it's important to learn informal reasoning about code before learning formal reasoning, because it helps reduce the risk of making a bit of progress by just hammering away with `induction`

and `simp`

, and then getting stuck as soon as something more is needed. I was once angrily told "Think before you hack!" in an oral exam by a famous computer scientist - I try to *gently* pass this important lesson onward.

#### Lars Ericson (Sep 16 2023 at 15:25):

Thanks I didn't know about `LawfulMonad`

. I see there is also `CategoryTheory.Monad`

.

If you were to make a follow-on version of the `Monad`

chapter which added in the use of `LawfulMonad`

, for the same set of examples, how much longer would it be? Twice as long? Book length? Intractable?

There are 3 things to think about:

- Pure functional programming
- Proving theorems in blackboard math in Lean
- Providing functional programs with an accompanying proof of correctness, typically by deriving them via stepwise refinement in correctness-preserving ways from specifications. This is shown to some extent in the chapter with a section on the use of
`_`

to fill out programs, except that the use in the chapter doesn't keep a proof that the result is as desired, just that the result is in the right type. The instance in the book of an unlawful`Monad`

shows the difference between being in the right type and being as desired.

Lean is programmed in Lean. 785 lines of code in Lean refer to `Monad`

. There are 112 references to `CategoryTheory.Monad`

and 101 references to `LawfulMonad`

. How much of Lean in Lean in general is functional programming without proof of correctness? The whole interpreter? How hard would it be to convert it all to a "lawful" style, that is, where every functional programming construct uses a `Lawful`

variant?

#### Eric Wieser (Sep 16 2023 at 15:27):

What are you counting as a reference? When you write `def foo [Monad m] : m Nat`

, that doesn't mean `foo`

is unlawful; it just means you're still allowed to use it even if `m`

isn't lawful.

#### Eric Wieser (Sep 16 2023 at 15:28):

It's only `instance : Monad m`

that you should worry about, and even then only when there isn't a `instance : LawfulMonad m`

that appears later

#### Ioannis Konstantoulas (Sep 16 2023 at 15:34):

I have a question regarding this: do we have theorems that say monad transformers transform lawful monads to lawful monads? And if so, for which transformers do we have such theorems?

#### Ioannis Konstantoulas (Sep 16 2023 at 15:34):

(same question for functors and applicatives)

#### Henrik Böving (Sep 16 2023 at 15:39):

Ioannis Konstantoulas said:

I have a question regarding this: do we have theorems that say monad transformers transform lawful monads to lawful monads? And if so, for which transformers do we have such theorems?

Those wouldn't be theorems they would be LawfulMonad instnaces and if you check the docs you will see we have a bunch of those: https://leanprover-community.github.io/mathlib4_docs/Init/Control/Lawful.html#LawfulMonad including for transformers, e.g. ExceptT: https://leanprover-community.github.io/mathlib4_docs/Init/Control/Lawful.html#ExceptT.instLawfulMonadExceptTInstMonadExceptT

#### Lars Ericson (Sep 17 2023 at 19:14):

Suppose I want to take this snippet:

```
def Reader (ρ : Type) (α : Type) : Type := ρ → α
def read : Reader ρ ρ := fun env => env
def Reader.pure (x : α) : Reader ρ α := fun _ => x
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => next (result env) env
instance : Monad (Reader ρ) where
pure x := fun _ => x
bind x f := fun env => f (x env) env
```

and make it lawful by replacing `Monad`

with `LawfulMonad`

. If I do that then I get this message:

```
hw_monad9.lean:12:11
failed to synthesize instance
Monad (Reader ρ)
```

on

```
instance : LawfulMonad (Reader ρ) where
```

So it seems to want me to say that `Reader`

is a `Monad`

before I can say that it is a `LawfulMonad`

. So I try that:

```
def Reader (ρ : Type) (α : Type) : Type := ρ → α
def read : Reader ρ ρ := fun env => env
def Reader.pure (x : α) : Reader ρ α := fun _ => x
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => next (result env) env
instance : Monad (Reader ρ) where
pure x := fun _ => x
bind x f := fun env => f (x env) env
instance : LawfulMonad (Reader ρ) where
pure x := fun _ => x
bind x f := fun env => f (x env) env
```

Then I get an error on ` pure x := fun _ => x`

saying that

```
'pure' is not a field of structure 'LawfulMonad'
```

My next tactic would be "programming by example". So I look at the declaration of `LawfulMonad List`

in file Data/List/Basic.lean around line 516. It has this:

```
instance : LawfulMonad List := LawfulMonad.mk'
(id_map := map_id)
(pure_bind := fun _ _ => List.append_nil _)
(bind_assoc := List.bind_assoc)
(bind_pure_comp := fun _ _ => (map_eq_bind _ _).symm)
```

If I try running that on it's own, I get:

```
unknown constant 'LawfulMonad.mk''
```

So unless I am missing an import, even though `LawfulMonad.mk'`

is available in the context of `Basic.lean`

and `LawfulMonad`

is available without import in the context of my example, `LawfulMonad.mk'`

is not. I also can't find it explicitly declared in any file. I only see uses of it:

```
~/mathlib4/Mathlib$ grep -r LawfulMonad --include \*.lean | grep mk
Data/List/Basic.lean:instance : LawfulMonad List := LawfulMonad.mk'
Data/PFun.lean:instance lawfulMonad : LawfulMonad (PFun α) := LawfulMonad.mk'
Data/LazyList/Basic.lean:instance : LawfulMonad LazyList := LawfulMonad.mk'
Data/Seq/Computation.lean:instance : LawfulMonad Computation := LawfulMonad.mk'
Data/Seq/Seq.lean:instance lawfulMonad : LawfulMonad Seq1 := LawfulMonad.mk'
Data/Semiquot.lean:instance : LawfulMonad Semiquot := LawfulMonad.mk'
Data/Set/Functor.lean:instance : LawfulMonad Set := LawfulMonad.mk'
Data/Multiset/Functor.lean:instance : LawfulMonad Multiset := LawfulMonad.mk'
GroupTheory/FreeGroup.lean:instance : LawfulMonad FreeGroup.{u} := LawfulMonad.mk'
GroupTheory/FreeAbelianGroup.lean:instance : LawfulMonad FreeAbelianGroup.{u} := LawfulMonad.mk'
Algebra/Free.lean:instance : LawfulMonad FreeMagma.{u} := LawfulMonad.mk'
Algebra/Free.lean:instance : LawfulMonad FreeSemigroup.{u} := LawfulMonad.mk'
Probability/ProbabilityMassFunction/Constructions.lean:instance : LawfulMonad Pmf := LawfulMonad.mk'
```

This is why a worked example of converting a `Monad`

to a `LawfulMonad`

would be helpful in the Functional Programming text. In general my sense is that, wherever possible, unless it slows things down considerably, even (and maybe especially) the lowest levels of the implementation of Lean in Lean should employ `Lawful`

variants wherever feasible. Teaching this to Lean developers (likely readers of Functional Programming in Lean) from the get-go would promote this as a best practice.

#### Eric Wieser (Sep 17 2023 at 19:15):

I recommend you write

```
instance : LawfulMonad (Reader ρ) := _
```

and use the code action for filling in the fields

#### Eric Wieser (Sep 17 2023 at 19:16):

`grep`

is not a reasonable way to find definitions in Lean. The sensible way is to use something that actually understands the lean code, such as VSCode's goto definition, or the docs search (docs#LawfulMonad.mk'). Note that immediately tells you that you were looking in the wrong directory, `mk'`

is defined in `Std`

!

#### Lars Ericson (Sep 24 2023 at 17:36):

@Eric Wieser I don't know how to "use the code action" in VS Code. With just the underscore, it says that it wants something of type `⊢ LawfulMonad (Reader ρ)`

, but it doesn't know how to synthesize placeholder context. This just restates the goal on the left-hand-side of the `:=`

.

Screenshot-from-2023-09-24-13-32-28.png

#### Kyle Miller (Sep 24 2023 at 18:39):

If you put your cursor before the `_`

, there should be a blue lightbulb that appears at the beginning of the line. (There might be some command to get a list of available code actions, but I don't know about this yet.)

#### Lars Ericson (Sep 24 2023 at 18:45):

@Kyle Miller , placing the cursor to the right of the `_`

reiterates what is shown in the InfoView, namely that it doesn't know how to synthesize the placeholder context, which I'm guessing means that it doesn't have a code suggestion:

Screenshot-from-2023-09-24-14-43-28.png

#### Kyle Miller (Sep 24 2023 at 18:48):

This is the blue lightbulb that I see:

Maybe you're not importing any of Std or Mathlib?

#### Kyle Miller (Sep 24 2023 at 18:49):

I actually have no idea what this symbol is supposed to be, but it's blue

#### Eric Wieser (Sep 24 2023 at 18:52):

This almost certainly needs `import Std`

#### Lars Ericson (Sep 24 2023 at 18:53):

I have a problem with `import Std`

, maybe I need to reinstall Lean, my copy is too old? I'm not sure how to update other than reinstall. I am on Ubuntu:

Screenshot-from-2023-09-24-14-53-24.png

#### Yaël Dillies (Sep 24 2023 at 18:54):

What's the end of the error message? The start is (usually) a bunch of junk.

#### Lars Ericson (Sep 24 2023 at 18:54):

It is

```
error: stdout:
./lake-packages/std/././Std/Linter/UnnecessarySeqFocus.lean:64:6: error: unknown constant 'Parser.Tactic.Conv.«convNext__=>_»'
error: external command `/home/catskills/.elan/toolchains/leanprover--lean4---nightly-2023-05-16/bin/lean` exited with code 1
```

#### Kyle Miller (Sep 24 2023 at 18:55):

Even with the part of the error that's visible, it looks like your Lean version isn't the one that your Std is expecting, but that's just a guess.

#### Kyle Miller (Sep 24 2023 at 18:57):

One thing you need to be sure of is that your `lean-toolchain`

file is referring to a compatible version of Lean. You could take a look at the one at `lake-packages/std/lean-toolchain`

#### Kyle Miller (Sep 24 2023 at 18:58):

If you're using mathlib, there's also the one at `lake-packages/mathlib/lean-toolchain`

#### Lars Ericson (Sep 24 2023 at 18:59):

The instructions for Ubuntu install are

- Launch VS Code.
- Click on the extension icon (image of icon) (or (image of icon) in older versions) in the side bar on the left edge of the screen (or press ShiftCtrlX) and search for leanprover.
- Select the lean4 extension (unique name leanprover.lean4).

That gives me an "Uninstall" option so I will try that and then reinstall.

#### Kyle Miller (Sep 24 2023 at 18:59):

You might be able to just copy the contents from the `lake-packages/std/lean-toolchain`

and replace `lean-toolchain`

. Then when you restart Lean from vs code, it will download the compatible version.

#### Kyle Miller (Sep 24 2023 at 19:03):

(I don't think uninstalling and reinstalling the Lean 4 extension will change anything for you.)

#### Lars Ericson (Sep 24 2023 at 19:05):

The uninstall didn't help, I'm still in a stuck state. What are the shell `lake`

or `elan`

commands to reinstall the latest Lean 4 standard and `MathLib`

files?

Uploading Screenshot from 2023-09-24 15-03-35.png…

#### Lars Ericson (Sep 24 2023 at 19:05):

Screenshot-from-2023-09-24-15-03-35.png

#### Lars Ericson (Sep 24 2023 at 19:06):

Is it this:

```
wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile
```

#### Kyle Miller (Sep 24 2023 at 19:13):

Kyle Miller said:

You might be able to just copy the contents from the

`lake-packages/std/lean-toolchain`

and replace`lean-toolchain`

. Then when you restart Lean from vs code, it will download the compatible version.

Did you try this?

#### Kyle Miller (Sep 24 2023 at 19:15):

Lars Ericson said:

Is it this:

`wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile`

No, no need to run that again. That command is just to (1) install elan and (2) make sure you have VS Code installed.

#### Lars Ericson (Sep 24 2023 at 19:30):

I took a brute force approach. I removed .elan and .mathlib and uninstalled `elan`

and restarted `code`

. That forced a reinstall of .elan. That got me an infoview but it still didn't know `Std`

package. Then I did this:

```
lake +leanprover/lean4:nightly-2023-02-04 new lean_homework math
```

This got me here, I will try the suggested `lake update`

next:

Screenshot-from-2023-09-24-15-29-46.png

#### Yaël Dillies (Sep 24 2023 at 19:32):

Do **not** run `lake update`

#### Yaël Dillies (Sep 24 2023 at 19:32):

The safe(r) version of that is `lake update YourProjectName`

#### Yaël Dillies (Sep 24 2023 at 19:34):

But the error clearly tells you the problem: your project is missing a `lake-manifest.json`

. Here's the one from my LeanCamCombi project, which you could copy in and hope that works.

#### Lars Ericson (Sep 24 2023 at 19:40):

So now I get the blue lightbulb. Thanks!

Screenshot-from-2023-09-24-15-40-44.png

#### Kyle Miller (Sep 24 2023 at 19:46):

This could have probably been resolved in one step, by making sure your `lean-toolchain`

file had the correct Lean version, but glad you found a way to get `import Std`

to work in the end!

#### Yaël Dillies (Sep 24 2023 at 19:48):

What exactly does "making sure" mean here? I've heard the phrase a lot, but I still don't know what it means concretely.

#### Lars Ericson (Sep 24 2023 at 19:49):

I don't have much state to carry over, and I don't know lake/elan at all or the underlying structure of Lean projects and Std and Mathlib libraries, and Lean 4 is frequently updated. The simplest solution is to delete everything and do an install from scratch, which doesn't take that long.

#### Kyle Miller (Sep 24 2023 at 19:51):

Yaël Dillies said:

What exactly does "making sure" mean here? I've heard the phrase a lot, but I still don't know what it means concretely.

It means making sure that `lean-toolchain`

is `lake-packages/mathlib/lean-toolchain`

for example. At least that's what I do. This isn't something that `lake`

manages, as far as I'm aware.

#### Lars Ericson (Sep 24 2023 at 19:52):

Note that following the example of the instances in the docs is not the right direction, i.e. this doesn't get me a blue lightbulb (I get a yellow one):

```
instance : LawfulMonad (Reader ρ) := LawfulMonad.mk' _
```

failing with

```
type mismatch
fun id_map pure_bind bind_assoc => LawfulMonad.mk' ?m.1464 id_map pure_bind bind_assoc
has type
(∀ {α : Type ?u.1463} (x : ?m.1464 α), id <$> x = x) →
(∀ {α β : Type ?u.1463} (x : α) (f : α → ?m.1464 β), pure x >>= f = f x) →
(∀ {α β γ : Type ?u.1463} (x : ?m.1464 α) (f : α → ?m.1464 β) (g : β → ?m.1464 γ),
x >>= f >>= g = x >>= fun x => f x >>= g) →
LawfulMonad ?m.1464 : Prop
but is expected to have type
LawfulMonad (Reader ρ) : Prop
```

Staring with `instance : LawfulMonad (Reader ρ) := _`

, Ihe blue lightbulb suggests filling out the instance of a `LawfulMonad`

instead:

```
instance : LawfulMonad (Reader ρ) where
map_const := _
id_map := _
comp_map := _
seqLeft_eq := _
seqRight_eq := _
pure_seq := _
map_pure := _
seq_pure := _
seq_assoc := _
bind_pure_comp := _
bind_map := _
pure_bind := _
bind_assoc := _
```

I should be able to use`Reader.pure`

and `Reader.bind`

to make a`pure_bind`

, then I just need to fill out 12 more functions.

#### Eric Wieser (Sep 24 2023 at 20:12):

The error message is telling you that `mk'`

expects more arguments, which you can provide with `_`

s

#### Lars Ericson (Sep 25 2023 at 01:28):

@Eric Wieser , adding underscores until it is full, it is telling me that the first thing it wants is a proof for the `id_map`

proposition asserting `⊢ ∀ {α : Type} (x : Reader ρ α), id <$> x = x`

. I define this verbatim with `sorry`

:

```
theorem idMap: ∀ {α : Type} (x : Reader ρ α), id <$> x = x := sorry
```

This has type

```
idMap (ρ : Type) {α : Type} (x : Reader ρ α) : id <$> x = x
```

which is not exactly what I'm proving, or maybe it is. However, it doesn't fit in

```
instance : LawfulMonad (Reader ρ) :=
@LawfulMonad.mk' idMap _ _ _ _ _ _ _ _ _
```

The error message is

```
application type mismatch
@LawfulMonad.mk' idMap
argument
idMap
has type
∀ (ρ : Type) {α : Type} (x : Reader ρ α), id <$> x = x : Prop
but is expected to have type
Type ?u.1615 → Type ?u.1614 : Type (max (?u.1614 + 1) (?u.1615 + 1))
```

To fill out the `LawfulMonad`

, I want to define propositions proved with `sorry`

to match the requested slots, which are `id_map`

, `pure_bind`

, `bind_assoc`

, `map_const`

, `seqLeft_eq`

, `seqRight_eq`

and `bind_map`

. However, based on my first attempt, I'm not sure how to go about this. Here is the full example:

Screenshot-from-2023-09-24-21-27-02.png

#### Eric Wieser (Sep 25 2023 at 07:48):

Why did you add the `@`

?

#### Lars Ericson (Sep 30 2023 at 14:29):

@Eric Wieser I added the @ to try to nail down the arguments one by one. Without it, Lean fills in implicit arguments and may shift argument positions that I find makes it harder to figure out what is going on. In this case I was unable to create a matching type even though I used the exact type that it requested.

#### Eric Wieser (Sep 30 2023 at 14:31):

The best strategy to count arguments in my opinion is:

- don't use
`@`

. You'll get an error on the function name. - keep writing
`_`

s until lean draws a red squiggle on the underscores instead of the name; now you're done!

#### Lars Ericson (Sep 30 2023 at 15:17):

If I remove the `@`

and use underscores, the name starts with red squiggles. If I add up to 3 `_`

s, it is still red squiggles:

Screenshot-from-2023-09-30-11-05-50.png

If I add one more `_`

, the first `_`

and the name lose their red squiggles, but I am left with 3 underscores with red squiggles:

Screenshot-from-2023-09-30-11-07-08.png

It seems like it needs the arguments that it is red-squiggling because it gives each one a name, as we can see in the InfoView, it gives me names and expectations for 9 `_`

s:

Screenshot-from-2023-09-30-11-14-24.png

It is giving me expectations for the red squiggle items, each of which is named, starting with `id_map`

. The first, undecorated `_`

has no expectation, it just has a type of `Type \to Type`

:

```
All Messages (8)
hw_monad9.lean:18:20
don't know how to synthesize placeholder for argument 'id_map'
context:
ρ: Type
⊢ ∀ {α : Type} (x : Reader ρ α), id <$> x = x
hw_monad9.lean:18:22
don't know how to synthesize placeholder for argument 'pure_bind'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : α) (f : α → Reader ρ β), pure x >>= f = f x
hw_monad9.lean:18:24
don't know how to synthesize placeholder for argument 'bind_assoc'
context:
ρ: Type
⊢ ∀ {α β γ : Type} (x : Reader ρ α) (f : α → Reader ρ β) (g : β → Reader ρ γ), x >>= f >>= g = x >>= fun x => f x >>= g
hw_monad9.lean:18:26
don't know how to synthesize placeholder for argument 'map_const'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : α) (y : Reader ρ β), Functor.mapConst x y = Function.const β x <$> y
hw_monad9.lean:18:28
don't know how to synthesize placeholder for argument 'seqLeft_eq'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : Reader ρ α) (y : Reader ρ β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a
hw_monad9.lean:18:30
don't know how to synthesize placeholder for argument 'seqRight_eq'
context:
ρ: Type
⊢ ∀ {α β : Type} (x : Reader ρ α) (y : Reader ρ β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y
hw_monad9.lean:18:32
don't know how to synthesize placeholder for argument 'bind_pure_comp'
context:
ρ: Type
⊢ ∀ {α β : Type} (f : α → β) (x : Reader ρ α),
(do
let y ← x
pure (f y)) =
f <$> x
hw_monad9.lean:18:34
don't know how to synthesize placeholder for argument 'bind_map'
context:
ρ: Type
⊢ ∀ {α β : Type} (f : Reader ρ (α → β)) (x : Reader ρ α),
(do
let x_1 ← f
x_1 <$> x) =
Seq.seq f fun x_1 => x
```

#### Lars Ericson (Sep 30 2023 at 15:18):

I have no idea how to proceed. I will look at code examples for `LawfulMonad.mk'`

in the `MathLib`

source. There are more instances there than I see in the doc#LawfulMonad.

#### Sky Wilshaw (Sep 30 2023 at 15:20):

The last five parameters are `autoParam`

s. This means that you're allowed to omit them, and Lean will work them out for you.

#### Sky Wilshaw (Sep 30 2023 at 15:21):

So you only need to provide proofs for `id_map`

, `pure_bind`

, and `bind_assoc`

.

#### Sky Wilshaw (Sep 30 2023 at 15:22):

One way to do this would be

```
instance : LawfulMonad (Reader \rho) := by
refine LawfulMonad.mk _ ?id_map ?pure_bind ?bind_assoc
case id_map =>
sorry
case pure_bind =>
sorry
case bind_assoc =>
sorry
```

#### Sky Wilshaw (Sep 30 2023 at 15:23):

Note that the first `_`

is just the type of the monad, i.e. `Reader \rho`

. Lean can figure this out so you don't need to fill the hole yourself.

#### Eric Wieser (Sep 30 2023 at 15:28):

This is all a lot easier in tactic mode (though not idiomatic); you could have just used `apply LawfulMonad.mk'`

and it would have played the underscore game for you

#### Lars Ericson (Sep 30 2023 at 15:35):

Thank you @Sky Wilshaw . That doesn't quite get me to a happy proof-by-`sorry`

state, i.e. one in which there are no messages except "proof by sorry". Here is what I see:

Screenshot-from-2023-09-30-11-33-38.png

Looking for other examples, the following files have `LawfulMonad`

instances:

```
$ grep -r LawfulMonad --include \*.lean | grep "instance :"
lake-packages/mathlib/Mathlib/Data/Part.lean:instance : LawfulMonad
lake-packages/mathlib/Mathlib/Data/Quot.lean:instance : LawfulMonad Trunc where
lake-packages/mathlib/Mathlib/Data/Seq/Computation.lean:instance : LawfulMonad Computation := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Semiquot.lean:instance : LawfulMonad Semiquot := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Set/Functor.lean:instance : LawfulMonad Set := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Multiset/Functor.lean:instance : LawfulMonad Multiset := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Data/Finset/Functor.lean:instance : LawfulMonad Finset :=
lake-packages/mathlib/Mathlib/GroupTheory/FreeGroup.lean:instance : LawfulMonad FreeGroup.{u} := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/GroupTheory/FreeAbelianGroup.lean:instance : LawfulMonad FreeAbelianGroup.{u} := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean:instance : LawfulMonad Pmf := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Control/Monad/Cont.lean:instance : LawfulMonad (ContT r m) := LawfulMonad.mk'
lake-packages/mathlib/Mathlib/Control/Monad/Cont.lean:instance : LawfulMonadCont (ContT r m) where
lake-packages/mathlib/Mathlib/Control/Basic.lean:instance : LawfulMonad (Sum.{v, u} e) where
lake-packages/mathlib/Mathlib/Control/ULift.lean:instance : LawfulMonad PLift where
lake-packages/mathlib/Mathlib/Control/ULift.lean:instance : LawfulMonad ULift where
lake-packages/std/Std/Classes/LawfulMonad.lean:instance : LawfulMonad (Except ε) := LawfulMonad.mk'
lake-packages/std/Std/Classes/LawfulMonad.lean:instance : LawfulMonad Option := LawfulMonad.mk'
```

For example, here is `LazyList`

:

```
instance : LawfulMonad LazyList := LawfulMonad.mk'
(bind_pure_comp := by
intro _ _ f xs
simp only [bind, Functor.map, pure, singleton]
induction' xs using LazyList.rec with _ _ _ _ ih
· rfl
· simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]; congr
· ext; apply ih)
(pure_bind := by
intros
simp only [bind, pure, singleton, LazyList.bind]
apply append_nil)
(bind_assoc := by
intro _ _ _ xs _ _
induction' xs using LazyList.rec with _ _ _ _ ih
· rfl
· simp only [bind, LazyList.bind, append_bind]; congr
· congr; funext; apply ih)
(id_map := by
intro _ xs
induction' xs using LazyList.rec with _ _ _ _ ih
· rfl
· simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]
· ext; apply ih)
```

From this the pattern would be:

```
instance : LawfulMonad (Reader ρ) := LawfulMonad.mk'
(bind_pure_comp := by sorry)
(pure_bind := by sorry)
(bind_assoc := by sorry)
(id_map := by sorry)
```

That works:

Screenshot-from-2023-09-30-11-34-53.png

#### Sky Wilshaw (Sep 30 2023 at 15:40):

Ah, sorry, missed a prime on `mk'`

.

#### Sky Wilshaw (Sep 30 2023 at 15:41):

Both ways should work, and the one you found seems more commonly used.

#### Lars Ericson (Sep 30 2023 at 15:41):

@Eric Wieser , using `apply`

gives me 8 goals rather than 4 for the version above, but at least the red squiggle problem mostly goes away (it is squiggling the `by`

to tell me that I have more work to do):

Screenshot-from-2023-09-30-11-40-55.png

#### Sky Wilshaw (Sep 30 2023 at 15:45):

Sky Wilshaw said:

Ah, sorry, missed a prime on

`mk'`

.

Incidentally, it's easier to help if you copy+paste a working #mwe rather than a screenshot, because then we can test your code.

#### Sky Wilshaw (Sep 30 2023 at 15:46):

(and test our suggestions)

#### Lars Ericson (Sep 30 2023 at 23:37):

Thank you @Sky Wilshaw this is the #mwe:

```
import Std
def Reader (ρ : Type) (α : Type) : Type := ρ → α
def read : Reader ρ ρ := fun env => env
def Reader.pure (x : α) : Reader ρ α := fun _ => x
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => next (result env) env
instance : Monad (Reader ρ) where
pure x := fun _ => x
bind x f := fun env => f (x env) env
instance : LawfulMonad (Reader ρ) := LawfulMonad.mk'
(bind_pure_comp := sorry)
(pure_bind := fun a f => rfl)
(bind_assoc := fun x f g => sorry)
(id_map := fun x => sorry)
```

Also this is a nice way to present examples, except it requires a tiny url due to presence of parentheses.

#### Alex J. Best (Oct 01 2023 at 00:05):

Anyone can click on the button in the top right of your code block to "view in lean 4 playground" and it will open the required lean 4 online interface for them

#### Lars Ericson (Oct 01 2023 at 14:51):

Going back to the motivating problem, in the text, a lawful monad is described as one which satisfies the "monad contract":

**LI**:`pure`

should be a left identity of`bind`

:`bind (pure v) = f v`

**RI**:`pure`

should be a right identity of`bind`

:`bind v pure = v`

**Assoc**:`bind`

should be associative:`bind (bind v f) g = bind v (fun x => bind (f x) g)`

In MathLib, the `LawfulMonad.mk'`

contract is a little different. One instance shows four conditions are required:

```
instance : LawfulMonad Option := LawfulMonad.mk'
(id_map := fun x => by cases x <;> rfl)
(pure_bind := fun x f => rfl)
(bind_assoc := fun x f g => by cases x <;> rfl)
(bind_pure_comp := fun f x => by cases x <;> rfl)
```

Another instance only requires three:

```
instance : LawfulMonad (Except ε) := LawfulMonad.mk'
(id_map := fun x => by cases x <;> rfl)
(pure_bind := fun a f => rfl)
(bind_assoc := fun a f g => by cases a <;> rfl)
```

This instance requires `bind_map`

as well:

```
instance : LawfulMonad Set := LawfulMonad.mk'
(id_map := image_id)
(pure_bind := biUnion_singleton)
(bind_assoc := fun _ _ _ => by simp only [bind_def, biUnion_iUnion])
(bind_pure_comp := fun _ _ => (image_eq_iUnion _ _).symm)
(bind_map := fun _ _ => seq_def.symm)
```

So `bind_pure_comp`

and `bind_map`

come with proofs which doesn't always work (more of a tactic?), and when they don't, it suffices to substitute a working proof (something I didn't know). There are additional properties to the `LawfulMonad.mk'`

supplied with proofs that might not work, namely `seqLeft_eq`

, `seqRight_eq`

, in which case we would need to supply them.

So, the five essential elements of the `LawfulMonad.mk'`

contract are:

**id_map**:`∀ {α} (x : m α), id <$> x = x`

**pure_bind**:`∀ {α β} (x : α) (f : α → m β), ((pure x) >>= f)= (f x))`

**bind_assoc**:`∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ), ((x >>= f) >>= g) = (x >>= (fun x => (f x >>= g)))`

**bind_pure_comp**:`∀ {α β} (f : α → β) (x : m α), (x >>= (fun y => pure (f y))) = (f <$> x)`

**bind_map**:`∀ {α β} (f : m (α → β)) (x : m α), f >>= (. <$> x) = f <*> x`

Pairing these up with the book's monad contract:

**bind_assoc**:`∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ), ((x >>= f) >>= g) = (x >>= (fun x => (f x >>= g)))`

**Assoc**:`bind`

should be associative:`bind (bind v f) g = bind v (fun x => bind (f x) g)`

and

**RI**:`pure`

should be a right identity of`bind`

:`bind v pure = v`

**id_map**:`∀ {α} (x : m α), id <$> x = x`

and

**LI**:`pure`

should be a left identity of`bind`

:`bind (pure v) = f v`

**pure_bind**:`∀ {α β} (x : α) (f : α → m β), ((pure x) >>= f)= (f x))`

and these are extra:

**bind_pure_comp**:`∀ {α β} (f : α → β) (x : m α), (x >>= (fun y => pure (f y))) = (f <$> x)`

**bind_map**:`∀ {α β} (f : m (α → β)) (x : m α), f >>= (. <$> x) = f <*> x`

I don't really have a clue how to prove these properties from scratch. In desperation, I look at all examples in Mathlib of proofs these properties:

```
(pure_bind := by intros; simp [Bind.bind, Pure.pure, WriterT.mk])
(pure_bind := fun x f => funext fun a => Part.bind_some _ (f x))
(pure_bind := by intros; simp only [bind, pure, singleton, LazyList.bind]; apply append_nil)
(pure_bind := @ret_bind)
(pure_bind := fun {α β} x f => ext.2 <| by simp)
(pure_bind := fun _ _ ↦ by simp only [pure_def, bind_def, singleton_bind])
(pure_bind := fun x f => pure_bind f x)
(pure_bind := fun x f ↦ pure_bind f x)
(pure_bind := fun f x ↦ rfl)
(pure_bind := pure_bind)
(pure_bind := fun _ _ => List.append_nil _)
(pure_bind := by intros; apply OptionT.ext; simp)
(pure_bind := by intros; ext; rfl)
(pure_bind := by intros; simp [Bind.bind, Pure.pure, WriterT.mk])
(id_map := by intros; simp [Functor.map, WriterT.mk])
(id_map := fun f => by funext a; dsimp [Functor.map, PFun.map]; cases f a; rfl)
(id_map := by intro _ xs; induction' xs using LazyList.rec with _ _ _ _ ih; · rfl; · simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]; · ext; apply ih)
(id_map := @map_id)
(id_map := fun {α} q => ext.2 <| by simp)
(id_map := fun _ ↦ by simp only [fmap_def, id_eq, map_id'])
(id_map := fun x => FreeGroup.induction_on x (map_one id) (fun x => map_pure id x) (fun x ih => by rw [map_inv, ih]); fun x y ihx ihy => by rw [map_mul, ihx, ihy])
(id_map := fun x ↦ FreeAbelianGroup.induction_on' x (FreeAbelianGroup.map_zero id) (map_pure id); (fun x ih ↦ by rw [FreeAbelianGroup.map_neg, ih]); fun x y ihx ihy ↦ by rw [FreeAbelianGroup.map_add, ihx, ihy])
(id_map := fun x ↦ FreeMagma.recOnPure x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by rw [map_mul', ih1, ih2]);(id_map := id_map);(id_map := map_id);(id_map := by;intros;apply OptionT.ext;simp only [OptionT.run_map];rw [map_congr, id_map];intro a;cases a <;> rfl)
(id_map := by intros; rfl)
(id_map := by intros; simp [Functor.map, WriterT.mk])
(bind_assoc := by intros; simp [Bind.bind, mul_assoc, WriterT.mk, ← bind_pure_comp])
(bind_assoc := fun f g k => funext fun a => (f a).bind_assoc (fun b => g b a) fun b => k b a)
(bind_assoc := by intro _ _ _ xs _ _; induction' xs using LazyList.rec with _ _ _ _ ih; · rfl; · simp only [bind, LazyList.bind, append_bind]; congr; · congr; funext; apply ih)
(bind_assoc := @bind_assoc)
(bind_assoc := fun {α β} γ s f g => ext.2 <| by simp only [bind_def, mem_bind]; exact fun c => ⟨fun ⟨b, ⟨a, as, bf⟩, cg⟩ => ⟨a, as, b, bf, cg⟩,; fun ⟨a, as, b, bf, cg⟩ => ⟨b, ⟨a, as, bf⟩, cg⟩⟩)
(bind_assoc := @bind_assoc)
(bind_assoc := fun x => FreeGroup.induction_on x(by intros; iterate 3 rw [one_bind])(fun x => by intros; iterate 2 rw [pure_bind])(fun x ih => by intros;(iterate 3 rw [inv_bind]); rw [ih])(fun x y ihx ihy => by intros;(iterate 3 rw [mul_bind]); rw [ihx, ihy]))
(bind_assoc := fun x f g ↦ FreeAbelianGroup.induction_on' x (by iterate 3 rw [zero_bind]) (fun x ↦ by iterate 2 rw [pure_bind]) (fun x ih ↦ by iterate 3 rw [neg_bind] <;> try rw [ih]) fun x y ihx ihy ↦ by iterate 3 rw [add_bind] <;> try rw [ihx, ihy])
(bind_assoc := fun x f g ↦ FreeMagma.recOnPure x (fun x ↦ rfl) fun x y ih1 ih2 ↦ by rw [mul_bind, mul_bind, mul_bind, ih1, ih2])
(bind_assoc := bind_bind)
(bind_assoc := List.bind_assoc)
(bind_assoc := by intros; apply OptionT.ext; simp only [OptionT.run_bind, bind_assoc] rw [bind_congr] intro a; cases a <;> simp)
(bind_assoc := by intros; ext; rfl)
(bind_assoc := by intros; simp [Bind.bind, mul_assoc, WriterT.mk, ← bind_pure_comp])
(bind_pure_comp := by intros; simp [Bind.bind, Functor.map, Pure.pure, WriterT.mk, bind_pure_comp])
(bind_pure_comp := fun f x => funext fun a => Part.bind_some_eq_map _ _)
(bind_pure_comp := by intro _ _ f xs; simp only [bind, Functor.map, pure, singleton]; induction' xs using LazyList.rec with _ _ _ _ ih; · rfl; · simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]; congr; · ext; apply ih)
(bind_pure_comp := @bind_pure)
(bind_pure_comp := fun {α β} f s => ext.2 <| by simp [eq_comm])
(bind_pure_comp := fun _ _ ↦ by simp only [pure_def, bind_def, bind_singleton, fmap_def])
(bind_pure_comp := fun f x => FreeGroup.induction_on x (by rw [one_bind, map_one]) (fun x => by rw [pure_bind, map_pure]); (fun x ih => by rw [inv_bind, map_inv, ih]) fun x y ihx ihy => by; rw [mul_bind, map_mul, ihx, ihy])
(bind_pure_comp := fun f x => rfl)
(bind_pure_comp := fun _ _ => (map_eq_bind _ _).symm)
(bind_pure_comp := by intros; simp [Bind.bind, Functor.map, Pure.pure, WriterT.mk, bind_pure_comp])
```

I use the simplest method for the first 3, and I guess I don't need a proof of `bind_pure_comp`

. It just works:

```
import Std
def Reader (ρ : Type) (α : Type) : Type := ρ → α
def read : Reader ρ ρ := fun env => env
def Reader.pure (x : α) : Reader ρ α := fun _ => x
def Reader.bind {ρ : Type} {α : Type} {β : Type}
(result : ρ → α) (next : α → ρ → β) : ρ → β :=
fun env => next (result env) env
instance : Monad (Reader ρ) where
pure x := fun _ => x
bind x f := fun env => f (x env) env
instance : LawfulMonad (Reader ρ) := LawfulMonad.mk'
(pure_bind := fun a f => rfl)
(id_map := by intros; rfl)
(bind_assoc := by intros; rfl)
```

I have no idea what these 3 proofs do. They just work.

I have no idea when the default proofs of the other properties such as `bind_pure_comp`

and `bind_map`

might be insufficient, and why.

My editorial takeaway is that, while it doesn't add a substantial amount of additional code in this example, it does seem like developers implementing the more operational aspects of Lean in Lean, or developers tempted to use Lean as a programming language for some other application, would have a very hard time making all of their implementation code "lawful", in the sense of proving that every piece of implementation code satisfied some initial pre-coding-phase functional specification.

#### Lars Ericson (Oct 01 2023 at 16:20):

So anyway, I would mark this Resolved, but I can't:

Screenshot-from-2023-10-01-12-19-45.png

#### Henrik Böving (Oct 01 2023 at 16:23):

Dont worry about it we generally don't use the resolve feature much here

#### Mario Carneiro (Oct 01 2023 at 16:52):

(in fact you should not use it, it breaks links)

#### Mario Carneiro (Oct 01 2023 at 17:02):

The reason there are additional fields is because Lean's `Monad`

typeclass allows you to customize the `map`

function, rather than assuming it is defined in terms of `bind`

and `pure`

. If you do such customization, you have to prove this as an equality instead, that's the `bind_pure_comp`

theorem. If you don't do any customization, those three axioms you mention are sufficient:

```
import Std
def M (α : Type) : Type := sorry
def M.pure {α} (x : α) : M α := sorry
def M.bind {α : Type} {β : Type} (result : M α) (next : α → M β) : M β := sorry
instance : Monad M where
pure := M.pure
bind := M.bind
instance : LawfulMonad M := LawfulMonad.mk'
(pure_bind := fun a f => show M.bind (M.pure a) f = f a from sorry)
(bind_assoc := fun v f g => show bind (bind v f) g = bind v (fun x => bind (f x) g) from sorry)
(id_map := fun x => show M.bind x M.pure = x from sorry)
```

#### Lars Ericson (Oct 08 2023 at 04:02):

@Mario Carneiro the fact that the supplied proof of a field in a structure after the `:=`

is a default that can be overriden is something I learned only in this exercise. It's an interesting feature, good to know. I'm not sure where it should go in a full Lean curriculum. My self-training curriculum for now is in this order:

- Functional Programming in Lean
- Theorem Proving in Lean 4
- The mechanics of proof
- Mathematics in Lean
- LTCM 2020 Exercises

#### Eric Wieser (Oct 08 2023 at 06:36):

That last step makes no sense, the code you link to is lean 3!

#### Lars Ericson (Oct 08 2023 at 16:29):

Is there a Lean 4 version of the LTCM exercises? That would be an exercise in itself.

#### Eric Wieser (Oct 08 2023 at 20:17):

Well, there's LFTCM2023

#### Jireh Loreaux (Oct 09 2023 at 01:58):

@Lars Ericson default definitions are covered in #fpil, namely https://lean-lang.org/functional_programming_in_lean/functor-applicative-monad/inheritance.html?highlight=default#default-declarations

#### Jireh Loreaux (Oct 09 2023 at 02:09):

Lars Ericson said:

I have no idea what these 3 proofs do. They just work.

Just hover on the tactics and it will explain what they do.

My editorial takeaway is that, while it doesn't add a substantial amount of additional code in this example, it does seem like developers implementing the more operational aspects of Lean in Lean, or developers tempted to use Lean as a programming language for some other application, would have a very hard time making all of their implementation code "lawful", in the sense of proving that every piece of implementation code satisfied some initial pre-coding-phase functional specification.

I'm sure part of the reason docs#Monad doesn't include the lawful properties is so that developers aren't forced to provide the proofs when they don't want to. Making *all* their implementation code lawful could indeed be a burden, but I think it's not fair to say the proofs in the above example are hard (it's just that they're true by definition after all).

Last updated: Dec 20 2023 at 11:08 UTC