proofs about values in `do` notation

Stream: lean4

[Siddharth Bhat]

Consider the following MWE:

structure DepProof where
   val: Nat
   H: val = 0

def MonadicDepProof [Mon: Monad M]: M DepProof := do
   let v ← pure 0
   return {
      val := v
      H := by {
         /-
         M: Type → Type ?u.380
         Mon: Monad M
         v: ℕ
         ⊢ v = 0
         -/
         sorry
      }
   }

How to see in the proof mode that v originated from pure 0, to create a M DepProof?

[Leonardo de Moura]

Recall that let v <- ..; return ... is the bind application bind (pure 0) (fun v : Nat => ...). You can use a let v := ... or use subtypes to communicate the fact that v is zero.

def MonadicDepProof [Mon: Monad M]: M DepProof := do
   let v : { x : Nat // x = 0 } ← pure ⟨0, rfl⟩
   return {
      val := v
      H := by rw [v.property]
   }

def MonadicDepProof' [Mon: Monad M]: M DepProof := do
   let v := 0
   return {
      val := v
      H := rfl
   }

[Siddharth Bhat]

Thanks, the former example helps. The latter doesn't work for me; I was using pure to demonstrate an example monadic value that in the larger example I have no control over.

[Sébastien Michelland]

The idea that pure 0 could be something opaque instead reminds me that the layered monadic interpretation paper from ICFP'22 generalizes the notion of image from ITrees to arbitrary monads. This characterizes what the return values of a monadic action can be. This seems to be what you're manipulating there...

[Mario Carneiro]

this seems to be overanalyzing the situation. When you call a function foo(x) you have some parameter x that is passed in, and even if it happens to be called on the value 2 you don't have access to that fact inside the body of the function. That's all that is happening here. It's the exact same thing that is the difference between have and let binders in lean: have x := e; e2 is just syntax for (fun x => e2) e, so inside the body of the lambda you cannot make use of any facts about x other than its type because it is a parameter. In a do block, it is just syntax for bind applications, in this case bind (pure 0) (fun v => ...) so inside that lambda you have no information about v other than its type.

[Sébastien Michelland]

Right. But isn't the whole point of that proof to show that the bind reduces to (fun v => ...) 0, and thus you can beta-reduce and expose the 0? And if instead of pure 0 you have some arbitrary code, then you don't know whether it's 0, but you might know there are some properties on the value. That's how I understand it at least...

[Mario Carneiro]

You can of course prove after the fact that the function is only called on 0, but you can't make use of this inside the body of the function itself. Dependent types and monads don't play well together

[Mario Carneiro]

the nearest thing you can do is what Leo showed: if the function is modified to return a subtype then you can pattern match on it and get a fact about the return value of the previous operation

[Mario Carneiro]

it isn't very compositional though, I have had many issues doing that sort of thing in practice when you have to call monadic functions and preserve invariants on the side

[Mario Carneiro]

For example, if you have a f : m A, and (separately) a proof that f always returns values x : A satisfying p x, there is no way to combine these pieces of data together into an element of m {x : A // p x}, or (equivalently) to monadic bind f with a partial function (x : A) -> p x -> m B.

[Sébastien Michelland]

I see, this makes a lot of sense. It happens that the framework Siddharth and I have been working with has this kind of tool with properties about the image of monadic actions, and the paper I referenced generalized it to a number of monads; that's why it came to mind. But that's definitely a construction on top of the language.

[Mario Carneiro]

It seems somewhat similar to the SatisfiesM predicate I developed for proving properties of monadic functions in std?

[Sébastien Michelland]

Yes that's pretty much it!

[Mario Carneiro]

I was thinking that one way to improve that to make it useful for dependently typed programs would be to have a function doing what I just said is impossible above: given f : m A and SatisfiesM p f, construct a m {x : A // p x}. In the logic we can do this using the axiom of choice since SatisfiesM p f basically asserts the existence of such an object, and in the compiler we can just unsafeCast f to the desired type

[Sébastien Michelland]

Right. In the framework I mentioned above, most of the monads are play are not black boxes and so you get the bind-with-postcondition construction. The ICFP'22 paper approach is to provide a typeclass for that postcondition predicate and then you provide an implementation for each monad that you want to support, at which point you have the ability to look into the monadic code and bind-with-postcondition recursively.