How to desugar a `do` block

Stream: new members

[Philogy]

Hi, I was wondering what tactic you use do desugar / simplify an assumption which is a call of a function which contains a large do block?

It has a bunch of left arrow statements, such as:

    let x ← Except.ok [x, x]

I'm wondering how I turn the do into the underlying bind and even better untop of that simplify things like Except.ok y >>= (fun x => x ... ) to (y ...) directly, thanks!

[Kyle Miller]

If you set set_option pp.notation false, you can see the bind operations. It's just pretty printed with do.

[Kyle Miller]

To simplify things like Except.ok y >>= f, it's best to write the missing simplification lemmas

[Philogy]

Kyle Miller said:

If you set set_option pp.notation false, you can see the bind operations. It's just pretty printed with do.

That makes sense, could you help me out getting the fully universe polymorphic variant of the lemma to work? I could only get the typechecker to be ok with it if α and β were from the same universe:

universe u_1 u_2 u_3

theorem ok_bind_simp
  {α : Type u_1}
  {β : Type u_2}
  {ε : Type u_3}
  (z : α) (z' : Except ε β) (f : α → Except ε β):
  (z' = Except.ok z >>= f) → (z' = f z) := by {

  }

(let alone making this generic over monads)

[Philogy]

Also definining:

theorem ok_bind_simp
  (z : α) (z' : Except ε β) (f : α → Except ε β):
  (z' = bind (Except.ok z) f) → (z' = f z) := by {
    intro h
    subst h
    rfl
  }

Also now that I've written this theorem how do I apply it? simp and simp_all don't seem to find a way to apply it?

[Philogy]

Looks like I didn't need the lemma simp_all [bind, Except.bind, Builtin.call] (Builtin.call) is a thing related to me worked.

Is there a tactic that simplifies, computes and expands all open function definitions?

[Kyle Miller]

Here's a formulation that's useful for simp, and I think I got the universes as general as possible.

universe u v

@[simp] theorem Except.ok_bind {α β : Type u} {ε : Type v}
    (f : α → Except ε β) (z : α) : Except.ok z >>= f = f z := rfl

[Kyle Miller]

This would also be useful:

@[simp] theorem Except.error_bind {α β : Sort u} {ε : Sort v}
    (f : α → Except ε β) (e : ε) : Except.error e >>= f = Except.error e := rfl

[Kyle Miller]

Rule of thumb: for simp lemmas you don't want equality hypotheses between a variable and a term — just substitute the variable in.

[Kyle Miller]

(I checked universe generality by replacing Type u and Type v with Type _ and hovering over Except.ok_bind to see the type of the resulting declaration.)

[Philogy]

Kyle Miller said:

of the resulting declaration.)

Do alpha and beta need to inhabit the same type universe for the definition to work?

[Kyle Miller]

Yeah, I found that out by using Type _

[Philogy]

I see, in regards to simplification, is there any tactic that just expands and simplifies any available definitions in your scope? My proof ended up looking like this:

theorem ast_square_eq_op_square (x : Nat):
  equiv_no_err square_plus_one sq_ops x = true := by
  simp [
    pure, bind,
    List.foldlM, List.find?, List.enum,
    Except.bind, Except.pure,
    ListMap.set_by_key, ListMap.get_by_key?, index_of?,
    Symbols.apply_assign, Symbols.eval_expr,
    Ast.run,
    ok_with_err,
    equiv_no_err, sq_ops, compile, compile_assign,
    as_ops, square_plus_one,
    Builtin.call, square_plus_one,
    eval_ops, step,
    Builtin.call,
    Stack.dup, Stack.pop
  ]

[Kyle Miller]

Using universe level variables is a way to ensure you have the amount of universe polymorphism you're expecting, but if you use _ then Lean will give you the most-general version automatically.

[Kyle Miller]

You shouldn't need to unfold pure and bind. Needing to unfold lots of definitions is usually indicating missing simp lemmas. People around here call this "missing API"

[Kyle Miller]

But, yes, there are some simp config options for unfolding definitions. A shorthand to get one of them is simp!

[Kyle Miller]

There's also simp (config := { ground := true }), but that doesn't seem to apply here. That's meant for "ground terms", i.e. terms with no metavariables or free variables. The purpose of this is to use simp to reduce terms more efficiently than whnf could (and, importantly, beyond what whnf could), I believe.

[Philogy]

Kyle Miller said:

You shouldn't need to unfold pure and bind. Needing to unfold lots of definitions is usually indicating missing simp lemmas. People around here call this "missing API"

Hmm, I'd assume so, do I create my own library of lemmas to simplify common functions? Or is there some tactic library I can use? I have Aesop and Mathlib imported at the top level along with a specific import or two from the lib.

Your help is very appreciated btw :big_smile: :pray:

[Kyle Miller]

Even though there's lots of material in the libraries, there are lots of gaps in the libraries, and believe it or not, given how basic bind lemmas for Except should be, it seems like you're doing something that no one's done before (or at least, no one whose been here in your situation has contributed the lemmas back!)

The way development works is that you collect lots of these simplification lemmas and (hopefully, if you're kind enough to slog through the nontrivial effort of contributing) eventually create PRs to help the next person.

But, yes, you should make a library of these simple lemmas, at least for your own project.

[Kyle Miller]

If you do end up with a library of Except lemmas (etc), feel free to ping me and I can try to see where in Lean, Batteries, or Mathlib they could go.

[Kyle Miller]

It's possible that there is automation that can do this automatically, but I'm not aware of it at the moment. Hopefully, if there is, someone will chime in.

[Philogy]

Do you think there could be a simpler way to register new simp lemmas? In the current way it seems like you'd have to manually unwrap the definition for every function you'd want to define a lemma for.

[Kyle Miller]

Sometimes you can add @[simp] to a definition (or, in your own files, write attribute [simp] theDefinition), and other times @[simps] is useful for generating a number of lemmas.

[Mario Carneiro]

this theorem already exists as pure_bind I think, you just have to apply the fact that Except.ok is pure

[Kyle Miller]

Ah, so if you write a simp lemma that Except.ok z = pure z then this will automatically apply

[Philogy]

Kyle Miller said:

Sometimes you can add @[simp] to a definition (or, in your own files, write attribute [simp] theDefinition), and other times @[simps] is useful for generating a number of lemmas.

Awesome, yeah adding @[simp] to my own definitions and the following defs:

@[simp] theorem Except.ok_bind {α β : Type u} {ε : Type v}
    (f : α → Except ε β) (z : α) : Except.ok z >>= f = f z := rfl

attribute [simp] List.foldlM
attribute [simp] List.find?
attribute [simp] List.enum

Let me reduce my proof from the above abomination to just:

theorem ast_square_eq_op_square (x : Nat):
  equiv_no_err square_plus_one sq_ops x = true := by
  simp [ equiv_no_err, square_plus_one, sq_ops ]

[Philogy]

In terms of contributing back the lemmas the Except.ok_bind would just go into prelude and adding the simp tags to all the list definitions should do the trick, right?

[Kyle Miller]

You do have to be careful with attribute [simp] for definitions, since they're not always the right lemmas, and also if they just eliminate the definition (like List.enum.eq_1 does) then you have to think about what you want as the simp normal form.

There's also the consideration for how the lemma should be phrased. For example, with List.find?, the equation lemma that is added to simp is

theorem List.find?.eq_2.{u} : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α),
  List.find? p (a :: as) =
    match p a with
    | true => some a
    | false => List.find? p as

There are actually already some simp lemmas in the prelude for this, via docs#List.find?_cons_of_pos and docs#List.find?_cons_of_neg, which are conditional simp lemmas that only apply if p a can be decided.