golf with `grind`

Stream: general

[Asei Inoue]

import Std.Tactic.Do
import Batteries

open Std

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

@[grind =]
def ICan'tBelieveItCanSort (arr : Array α) := Id.run do
  let N := arr.size
  let mut vec := arr.toVector
  for hi : i in [:N] do
    for hj : j in [: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]

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

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

@[grind! =>]
theorem 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 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 grind

  case vc1 =>
    simp [Array.pairwise_iff_getElem] at *
    grind

  case vc4 =>
    simp [Array.pairwise_iff_getElem] at *
    grind

Could we make the proof finish directly at the with grind part by adding the right grind lemmas?

[Asei Inoue]

（this code is based on one given by Anthony Wang, thanks ）

[Asei Inoue]

Background

I’m interested in verifying algorithms with mvcgen. After trying various examples, it seems that proofs involving index accesses become difficult for grind to handle. I’m curious whether adding appropriate grind lemmas could eliminate that difficulty.

[Asei Inoue]

succeed!

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

open Std

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

@[grind =]
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 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.pairwise_take_swap {α : Type} [LE α] [IsPartialOrder α] {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 *
  grind

grind_pattern Array.pairwise_take_swap => Array.Pairwise (· ≤ ·) ((arr.swap s t).take s)

theorem Array.pairwise_take_succ {α : Type} [LE α] [IsPartialOrder α] {arr : Array α}
  (k : Nat) (hk : k < arr.size)
  (h : Array.Pairwise (· ≤ ·) (arr.take k))
  (le : ∀ (i : Nat) (_ : i < arr.size), arr[i] ≤ arr[k])
    : Array.Pairwise (· ≤ ·) (arr.take (k + 1)) := by
  simp [Array.pairwise_iff_getElem] at *
  grind

grind_pattern Array.pairwise_take_succ => Array.Pairwise (· ≤ ·) (arr.take (k + 1))

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)