mvcgen doesn't produce any invariant goals

Stream: new members

[Anthony Wang]

Inspired by #new members > Easy program verification advice @ 💬, I'm trying to verify the bubble sort implementation in that post using mvcgen in Lean v4.24.0-rc1. This is my code so far:

import Std.Tactic.Do
import Mathlib

def BubbleSort {α} [LT α] [DecidableLT α] (a: Array α) : Array α := Id.run do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hj
      if a[j] > a[j + 1] then
        a := a.swap j (j+1)
  return a.toArray

open Std.Do

theorem BubbleSortSameElements [LT α] [DecidableLT α] (A : Array α) : Multiset.ofList A.toList = Multiset.ofList (BubbleSort A).toList := by
  generalize h : BubbleSort A = x
  apply Id.of_wp_run_eq h
  mvcgen

However, mvcgen doesn't produce any invariants goals for me to assign loop invariants to, and instead changes the goal to this:

(wp⟦forIn (List.range (n✝ - 1)) a✝ fun i r => do
        let r ←
          forIn' (List.range (n✝ - i - 1)) r fun a m b =>
              if b[a] > b[a + 1] then do
                pure PUnit.unit
                pure (ForInStep.yield (b.swap a (a + 1) ⋯ ⋯))
              else do
                pure PUnit.unit
                pure (ForInStep.yield b)
        pure PUnit.unit
        pure (ForInStep.yield r)⟧
    (fun a => wp⟦pure a.toArray⟧ (PostCond.noThrow fun a => { down := ↑A.toList = ↑a.toList }), ExceptConds.false)).down

Is this because of some limitation in mvcgen or am I using it incorrectly?

[Asei Inoue]

@Sebastian Graf may be right person to ask..?

[Sebastian Graf]

Thanks for pinging me. I just had a look and it seems like you found a bug. Will look for a fix tomorrow!

[Sebastian Graf]

Sigh. It's a universe polymorphism issue (it almost always is)! BubbleSort has a universe parameter for the type of α, and the specification for forIn requires this parameter to always be the same as that of the list element type Nat : Type, which is 0. I'll see if I can generalize the specification lemma. Meanwhile, you can keep exploring mvcgen by instantiating BubbleSort.{0} in the theorem statemtnt:

import Std.Tactic.Do
import Mathlib

def BubbleSort {α} [LT α] [DecidableLT α] (a: Array α) : Array α := Id.run do
  let n := a.size
  let mut a : Vector α n := a.toVector
  for i in List.range (n - 1) do
    for hj : j in List.range (n - i - 1) do
      have := List.mem_range.mp hj
      if a[j] > a[j + 1] then
        a := a.swap j (j+1)
  return a.toArray

open Std.Do

theorem BubbleSortSameElements [LT α] [DecidableLT α] (A : Array α) : Multiset.ofList A.toList = Multiset.ofList (BubbleSort.{0} A).toList := by
  generalize h : BubbleSort A = x
  apply Id.of_wp_run_eq h
  mvcgen

[Sebastian Graf]

Fixed in https://github.com/leanprover/lean4/pull/10865.

[Anthony Wang]

Thanks @Sebastian Graf! mvcgen still wasn't producing the right invariant goals with your .{0} trick and Lean v4.24.0, but updating to v4.25.0-rc1 fixed the problem. I finally completed my proof of correctness for a sorting algorithm (not bubble sort but a very closely related algorithm)!

[Asei Inoue]

I want to see your sorting algorithm verification

[Anthony Wang]

Here's the code: https://git.unnamed.website/miscelleaneous/plain/Sort.lean

[Anthony Wang]

(deleted)

[Sebastian Graf]

Yes, in v4.25.0 I fixed a problem where the invariant of the inner loop got instantiated with the invariant of the outer loop. Good call trying v4.25.0 and congrats on finishing your proof :)

[Asei Inoue]

@Anthony Wang

Thank you for providing nice code example!

I removed Mathlib dependency from your example (Std has IsLinearOrder type class! :) )

import Std.Tactic.Do
import Batteries

open Std

variable {α : Type} (A : Array α)
variable [LT α] [DecidableLT α]

def ICan'tBelieveItCanSort := Id.run do
  let N := A.size
  let mut A := A.toVector
  for hi : i in [:N] do
    for hj : j in [:N] do
      if A[i] < A[j] then
        A := A.swap i j
  return A.toArray

open Std.Do

set_option mvcgen.warning false

theorem ICan'tBelieveItCanSort_perm (arr : Array α) : Array.Perm (ICan'tBelieveItCanSort arr) arr := by
  generalize h : ICan'tBelieveItCanSort arr = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · ⇓⟨_cursor, vec⟩ => ⌜Array.Perm arr vec.toArray⌝
  · ⇓⟨_cursor, vec⟩ => ⌜Array.Perm arr vec.toArray⌝
  with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm]

@[simp, grind =]
theorem Vector.toArray_extract_size {α : Type} {n : Nat} (v : Vector α n) :
    v.toArray.extract 0 n = v.toArray := by
  grind

@[grind! =>]
theorem lemm (n : Nat) (xs : [0:n].toList.Cursor) : xs.pos ≤ n := by
  have : xs.prefix.length + xs.suffix.length = n := by
    simp [← List.length_append, xs.property]
  grind

variable [LE α] [IsLinearOrder α] [LawfulOrderLT α]

theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by
  generalize h : ICan'tBelieveItCanSort A = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝
  · ⇓⟨xs, A'⟩ => by
    expose_names
    exact ⌜(A'.take cur |>.toArray.Pairwise (· ≤ ·)) ∧ ∀ i (_ : i < xs.pos), A'[i]'(by grind) ≤ A'[cur]'(by grind)⌝
  with grind

  case vc1.step.isTrue =>
    expose_names
    simp [Array.pairwise_iff_getElem] at *
    refine ⟨?_, by grind⟩
    grind
  case vc4.step.post.success =>
    simp_all
    grind [= Array.pairwise_iff_getElem]

[Asei Inoue]

I tried to keep the code as concise as possible and arranged things so that the proof would finish with just grind, but I couldn’t push it any further than this.

[Asei Inoue]

done!!

import Std.Tactic.Do
import Batteries.Data.Array

open Std

variable {α : Type}
variable [LT α] [DecidableLT α]

def ICan'tBelieveItCanSort (arr : Array α) := Id.run do
  let n := arr.size
  let mut vec := arr.toVector
  for hi : i in [0:n] do
    for hj : j in [0:n] do
      if vec[i] < vec[j] then
        vec := vec.swap i j
  return vec.toArray

open Std.Do

set_option mvcgen.warning false

theorem ICan'tBelieveItCanSort_perm (arr : Array α) : Array.Perm (ICan'tBelieveItCanSort arr) arr := by
  generalize h : ICan'tBelieveItCanSort arr = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · ⇓⟨_cursor, vec⟩ => ⌜Array.Perm arr vec.toArray⌝
  · ⇓⟨_cursor, vec⟩ => ⌜Array.Perm arr vec.toArray⌝
  with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm]

@[grind =]
theorem Vector.toArray_extract_size {α : Type} {n : Nat} (v : Vector α n) :
    v.toArray.extract 0 n = v.toArray := by
  grind

@[grind! =>]
theorem List.Cursor.pos_le_length (n : Nat) (xs : [0:n].toList.Cursor) : xs.pos ≤ n := by
  have : xs.prefix.length + xs.suffix.length = n := by
    simp [← List.length_append, xs.property]
  grind only

theorem Array.sorted_take_swap {α : Type} [LE α] [IsPreorder α] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise (· ≤ ·) (arr.take s))
  (le1 : arr[s] ≤ arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), arr[i] ≤ arr[s])
    : Array.Pairwise (· ≤ ·) ((arr.swap s t).take s) := by
  simp [Array.pairwise_iff_getElem] at h ⊢
  grind

@[grind <=]
theorem Array.pairwise_take_swap {α : Type} {R : α → α → Prop} [Refl R] [Trans R R R] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise R (arr.take s))
  (le1 : R arr[s] arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), R arr[i] arr[s])
    : Array.Pairwise R ((arr.swap s t).take s) := by
  let : LE α := { le := R }
  have : IsPreorder α := {
    le_refl := Refl.refl
    le_trans _ _ _ := Trans.trans
  }
  apply Array.sorted_take_swap <;> assumption

@[grind <=]
theorem Array.pairwise_take_succ {α : Type} {R : α → α → Prop} {arr : Array α}
  (k : Nat) (hk : k < arr.size)
  (h : Array.Pairwise R (arr.take k))
  (le : ∀ (i : Nat) (_ : i < arr.size), R arr[i] arr[k])
    : Array.Pairwise R (arr.take (k + 1)) := by
  simp [Array.pairwise_iff_getElem] at h ⊢
  grind

variable [LE α] [IsLinearOrder α] [LawfulOrderLT α]

theorem ICan'tBelieveItCanSort_sorted (arr : Array α) : ICan'tBelieveItCanSort arr |>.Pairwise (· ≤ ·) := by
  generalize h : ICan'tBelieveItCanSort arr = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · ⇓⟨cursor, vec⟩ => ⌜vec.take cursor.pos |>.toArray.Pairwise (· ≤ ·)⌝
  · ⇓⟨cursor, vec⟩ => by
    expose_names
    exact ⌜(vec.take cur |>.toArray.Pairwise (· ≤ ·)) ∧
      ∀ i (_ : i < cursor.pos), vec[i]'(by grind) ≤ vec[cur]'(by grind)⌝
  with (simp at *; grind)