Vector.scan etc.

Stream: batteries

[cmlsharp]

I've been thinking a bit about what it would take to add scan combinators to Vector to bring it to parity with List (and Arrays+Iterators should those PRs be merged). Ideally you'd re-use the Array implementation, however this does present a problem which is that there is no theorem at present about the length of 'scanlM` (because its monadic).

It seems like there are two-ish options:
(1) prove a SatisfiesM length theorem for List/Array, and then use MonadSatisfying.satisfying to write the Vector implementation. The upside of this is that its the easiest. The downside here is this means that Vector.scanlM would carry a MonadSatisfying bound.
(2) Don't re-use Array, and just reimplement scanlM/scanrM for vector. The downside here is obviously the code duplication (though I guess you could then make the 'Array' implementation be in terms of the 'Vector' one).
(3) something else? I don't really understand mvcgen, does it do anything magical here?

[Kim Morrison]

2.

[Wrenna Robson]

@Kim Morrison ooi why is the preference to re-implement stuff for Vector?

[Wrenna Robson]

To maintain the API barrier, as it were?

[cmlsharp]

fwiw i did option 2 here:

https://github.com/leanprover-community/batteries/pull/1643

[Eric Wieser]

@Wrenna Robson, to avoid the MonadSatisfying argument I think?

[Wrenna Robson]

Ah, I am not familiar with that one.

[Kim Morrison]

Yeah, MonadSatisfying is a dead end, which we should be deleting rather than using.

[Kim Morrison]

Beyond that, I think we should consider deprecating SatisfiesM itself / moving it elsewhere, and just direct people to using mvcgen.

As far as I am aware there are no downstream projects that use SatisfiesM, except for https://github.com/FormalSAT/trestle which only uses it in a file called Trash.lean!

Within Batteries, there are many theorems with SatisfiesM in their conclusion (so, I think, deprecatable along with the framework), and then three that feel somewhat more useful (but, per above, have never been used):

theorem mapM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
    (a : Array α) (h : a.size = n) (f : α → m β) :
    (Vector.mk a h).mapM f =
      (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying (Array.size_mapM f a) := by
  rw [← _root_.map_inj_right Vector.toArray_inj.mp]
  simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapM]

theorem mapIdxM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
    (a : Array α) (h : a.size = n) (f : Nat → α → m β) :
    (Vector.mk a h).mapIdxM f =
      (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying (Array.size_mapIdxM a f) := by
  rw [← _root_.map_inj_right Vector.toArray_inj.mp]
  simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapIdxM]

theorem mapFinIdxM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
    (a : Array α) (h : a.size = n) (f : (i : Nat) → α → (h : i < n) → m β) :
    (Vector.mk a h).mapFinIdxM f =
      (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying
        (Array.size_mapFinIdxM a (fun i a h' => f i a (h ▸ h'))) := by
  rw [← _root_.map_inj_right Vector.toArray_inj.mp]
  simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapFinIdxM]

[Eric Wieser]

Kim Morrison said:

we should consider deprecating SatisfiesM itself / moving it elsewhere, and just direct people to using mvcgen.

As a starting point can we modify the docstring of SatisfiesM to note what the mvcgen analog is?

[Kim Morrison]

There's no analog, it's a completely different approach to dealing with verification of monadic code.

[Eric Wieser]

Isnt' the answer that P x -> SatisfiesM Q (f x) is instead spelt Triple P Q f or similar?

[Eric Wieser]

I'm not really asking about verification (proving), I'm asking about how to even state properties!

[cmlsharp]

How difficult would it be to port these theorems to mvcgen? (If such a thing is in fact possible) Even if they aren’t widely used, I think it might be beneficial to just have more (including simple) examples of how to use mvcgen

[cmlsharp]

(I’m speaking somewhat selfishly here)

[Kim Morrison]

@Sebastian Graf what do you think of this? I agree it worked be great to have some examples in Batteries.

[Kim Morrison]

@Sebastian Graf (apologies, I think you weren't previously subscribed here, so probably didn't see this until now), could you assist with this sorry:

import Std.Do.Triple
import Batteries.Classes.SatisfiesM

open Std.Do

theorem Triple.of_satisfiesM [Monad m] [LawfulMonad m] [MonadSatisfying m] [WPMonad m .pure]
    {p : α → Prop} {x : m α}
    (h : SatisfiesM p x) :
    Triple x ⌜True⌝ (⇓ a => ⌜p a⌝) := by
  -- Get the witness from SatisfiesM
  obtain ⟨x', hx'⟩ := h
  -- Rewrite x as Subtype.val <$> x'
  rw [← hx']
  -- Unfold Triple to get the entailment goal
  simp only [Triple, WPMonad.wp_map, PredTrans.map_apply]
  -- The postcondition (fun a => ⌜p a.val⌝) is equivalent to (fun _ => ⌜True⌝)
  -- because for a : {a // p a}, we have a.property : p a.val
  have heq : (fun (a : {a // p a}) => ⌜p a.val⌝) = (fun _ => (⌜True⌝ : Assertion .pure)) := by
    funext ⟨a, ha⟩
    show SPred.pure (p a) = SPred.pure True
    simp only [SPred.pure_nil]
    exact congrArg ULift.up (propext ⟨fun _ => trivial, fun _ => ha⟩)
  rw [heq]
  simp only [SPred.entails_nil, SPred.pure_nil, forall_const]
  -- ⊢ (wp⟦x'⟧ (fun x => { down := True }, ExceptConds.false)).down
  sorry

[cmlsharp]

Kim Morrison said:

Sebastian Graf what do you think of this? I agree it worked be great to have some examples in Batteries.

I played around with mvcgen a bit this weekend, and I was able to port some of the SatisfiesM theorems over (specs for mapM, anyM, mapFinIdx, and a few lemmas about them). Would a PR to batteries aiming to port these and the rest of the satisfiesM theorems to mvcgen be of interest?

[Kim Morrison]

I think so, yes.

[Kim Morrison]

Note that a lot is already in the lean4 repo, although sometimes still in more general form than I know what to do with.

As an example, the

theorem satisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (h₀ : motive b)
    (h₁ : ∀ (b) (_ : motive b) (a : α) (_ : a ∈ l), SatisfiesM motive (f b a)) :
    SatisfiesM motive (List.foldlM f b l) := by
  induction l generalizing b with
  | nil => exact SatisfiesM.pure h₀
  | cons hd tl ih =>
    simp only [foldlM_cons]
    apply SatisfiesM.bind_pre
    let ⟨q, qh⟩ := h₁ b h₀ hd mem_cons_self
    exact ⟨(fun ⟨b, bh⟩ => ⟨b, ih bh (fun b bh a am => h₁ b bh a (mem_cons_of_mem hd am))⟩) <$> q,
      by simpa using qh⟩

in Batteries would be replaced by
docs#Std.Do.Spec.foldlM_list_const_inv, although the Batteries version we have today is really the two step specialization given by:

/-- Triple version of foldlM specification.
If each step preserves the motive and doesn't throw, the whole fold preserves the motive
and doesn't throw. -/
theorem foldlM_triple {α : Type u} {β : Type u} {m : Type u → Type v}
    [Monad m] [WPMonad m ps] {f : β → α → m β} {motive : β → Prop}
    {init : β} {l : List α}
    (h₁ : ∀ a b, Triple (f b a) ⌜motive b⌝ (⇓ b' => ⌜motive b'⌝)) :
    Triple (List.foldlM f init l) ⌜motive init⌝ (⇓ b' => ⌜motive b'⌝) :=
  Spec.foldlM_list_const_inv (inv := ⟨fun x => ⌜motive x⌝, ExceptConds.false⟩) h₁

/-- Triple version of foldlM specification with `motive init` as a hypothesis.
This gives a trivial `True` precondition in the conclusion. -/
theorem foldlM_triple' {α : Type u} {β : Type u} {m : Type u → Type v}
    [Monad m] [WPMonad m ps] {f : β → α → m β} {motive : β → Prop}
    {init : β} {l : List α}
    (h₀ : motive init)
    (h₁ : ∀ a b, Triple (f b a) ⌜motive b⌝ (⇓ b' => ⌜motive b'⌝)) :
    Triple (List.foldlM f init l) ⌜True⌝ (⇓ b' => ⌜motive b'⌝) :=
  (SPred.pure_intro h₀).trans (foldlM_triple h₁)

[Sebastian Graf]

The analogue for SatisfiesM m is Std.Do.WP m .pure, which is used in the definition of Std.Do.Triple. I played around with SatisfiesM last year and IIRC concluded that it is weaker (even too weak) compared to Std.Do.WP. Therefore, I don't think you can prove Triple.of_satisfiesM.

Furthermore, Std.Do.WP lacks a generic notion of adequacy lemma (i.e., the field of a hypothetical LawfulWP), so there are instance-specific ones for Id, StateM, Except, etc. For example docs#Std.Do.Id.of_wp_run_eq. That's a TODO I keep around for some time now... I'll resolve it once I know how it interacts with MonadAttach and LawfulMonadAttach which is yet another way of expressing a variant of SatisfiesM.

For foldlM specifically, there is the spec docs#Std.Do.Spec.foldlM_list_const_inv, although docs#Std.Do.Spec.foldlM_list is the one that is picked up by mvcgen (which requires the user to state an invariant). It would be great to have similar specs for other functions in batteries. I understand that the spec lemmas involving loop invariants are challenging to understand, though.

Completely unrelated: I'm still unhappy with the naming convention I picked. Since you are experienced library maintainers, I would love input here: Where would you put the spec docs#Std.Do.Spec.foldlM_list for foldlM? Perhaps List.foldlM.spec is better? Any other ideas? Fortunately it's unlikely that users will refer to these by name very often...

[cmlsharp]

(I don’t qualify as an advanced library maintainer, but my personal experience is I usually don’t have to go manually hunting for theorems because things in the standard library usually have the names you expect, and my editor’s autocomplete is usually sufficient. The specs for foldlM etc were an exception because they weren’t somewhere in the List (resp. Array) namespace)

But on the other hand, I was not searching for these to use them by name (as you say, mvcgen itself picked them up for me), however I had to know what specs existed so I knew e.g. to write a mapM spec I should rewrite it in terms of foldlM

[cmlsharp]

Kim Morrison said:

I think so, yes.

draft PR with my current progress batteries#1649