RFC: Binders for `Std.Do.Assertion` clauses (compatible with `mvcgen`)

Proposal

In the example below, we prove the correctness of a function setZero which iteratively sets all of the elements of a state Array Nat to zero:

import Std.Tactic.Do

open Std.Do

set_option mvcgen.warning false

abbrev SM := StateM (Array Nat)

abbrev gns : SVal ((Array Nat)::[]) (Array Nat) := fun s => SVal.pure s

noncomputable def setZero : StateM (Array Nat) Unit := do
  let mut i := 0
  let len := (← get).size
  for _ in [0:len] do
    let ns ← get
    if h : i < ns.size then
      modify fun _ => ns.set i 0 h
    i := i + 1

-- see #9363
macro "mvcgen_aux" : tactic => do
  `(tactic|
    (repeat mintro ∀_
     try mframe
     mpure_intro
     simp only [SPred.and_cons, SVal.curry_cons, SVal.curry_nil, SVal.uncurry_cons, SVal.uncurry_nil, SPred.and_nil] at *))

theorem setZero_spec :
   ⦃⌜#gns = ns⌝⦄
   setZero
   ⦃⇓ _ => ⌜(#gns).size = ns.size⌝ ∧ ⌜∀ i, (h : i < (#gns).size) → (#gns)[i]'h = 0⌝⦄ := by
  unfold setZero
  mvcgen

  case inv =>
    exact ⇓ (i, sp) =>
      -- FIXME it would be very convenient to be able to name each of these
      -- components, and have mvcgen automatically call `rcases h with ...` to
      -- destruct it into separate hypotheses (using these names) in every
      -- subsequent goal. Then we wouldn't have to do it ourselves.
      ⌜(#gns).size = ns.size⌝ ∧
      ⌜ i = sp.rpref.length ⌝ ∧
      ⌜∀ j, (j < i) → (h : j < (#gns).size) → (#gns)[j]'h = 0⌝

  -- step.isTrue
  . mvcgen_aux
    rcases h with ⟨hs, hi, hz⟩ -- FIXME

    simp only [← hs]
    simp only [Array.size_set]
    and_intros
    . trivial
    . simp
      exact hi
    intros j hj hjs
    if j < b then
      rw [Array.getElem_set_ne]
      apply hz
      assumption
      omega
      omega
    else
      have : j = b := by omega
      subst this
      apply Array.getElem_set_self

  -- step.isFalse
  . mvcgen_aux
    rcases h with ⟨hs, hi, hz⟩ -- FIXME

    next hns _ _ =>
    have hns := hns.symm
    subst hns
    clear hns

    have hrng_dec_sz : (rpref.reverse ++ x :: suff).length = len := by
      rw [← h]
      simp only [List.length_range', Nat.sub_zero, Nat.add_one_sub_one, Nat.div_one]
    rw [List.length_append, List.length_reverse, List.length_cons] at hrng_dec_sz

    subst hi
    have : rpref.length < ns.size := by omega
    rw [hs] at *
    contradiction

  -- pre1
  . mvcgen_aux

    subst h
    and_intros
    rfl
    rfl
    omega

  -- post.success
  . mvcgen_aux
    rcases h with ⟨hs, hi, hz⟩ -- FIXME

    simp only [List.length_reverse, List.length_range'] at hi
    simp only [Nat.add_one_sub_one, Nat.div_one] at hi

    have hns := h.symm
    subst hns

    simp only [Nat.sub_zero] at hi
    subst hi
    rw [← hs]
    and_intros
    rfl
    intros i hi'
    apply hz
    omega
    omega

In nearly every subgoal produced by the loop, we have to destruct the components of the hypothesis h via rcases h with ⟨hs, hi, hz⟩ to get access to its components (without having to futz around with projections). It would be really quite convenient if mvcgen was somehow able to do this for us. This would probably require some specialized syntax for the assertion clauses, perhaps something like:

  case inv =>
    exact ⇓ (i, sp) =>
      -- FIXME it would be very convenient to be able to name each of these
      -- components, and have mvcgen automatically call `rcases h with ...` to
      -- destruct it into separate hypotheses (using these names) in every
      -- subsequent goal. Then we wouldn't have to do it ourselves.
      ⌜hs : (#gns).size = ns.size⌝ ∧
      ⌜hi : i = sp.rpref.length⌝ ∧
      ⌜hz : ∀ j, (j < i) → (h : j < (#gns).size) → (#gns)[j]'h = 0⌝

(Lean 4.23.0, commit a4f38cc78250f4c7f813c8d20700d97a53f0d3d6)

Community Feedback

Mentioned to Sebastian Graf in DMs.

Start with the issue's Std.Do.Assertion example and the repeated mvcgen subgoals, especially the case inv clause and the rcases h workarounds. Read the existing mvcgen assertion-clause handling and determine how named components should be represented and introduced; done means the example no longer needs those repeated destructuring steps.