More style tweaks (last time I swear)

Changes

1 changed files (+28/-30)

• Velvet.lean
  • @@ -1,42 +1,40 @@
    - -- This needs Lean v4.24.0 and Loom added as a dependency in the lakefile.toml - - import CaseStudies.Velvet.Std + -- This needs Lean v4.24.0 and https://github.com/verse-lab/velvet/ added as a dependency in the lakefile.toml + -- https://github.com/verse-lab/velvet/blob/master/Velvet/Examples/Examples.lean + import Velvet.Std set_option loom.semantics.termination "total" set_option loom.semantics.choice "demonic" attribute [grind] Array.multiset_swap - method insertionSort_total (mut arr : Array ℤ) return (u : Unit) - require 1 ≤ arr.size - ensures ∀ i j, 0 ≤ i ∧ i ≤ j ∧ j < arr.size → arr[i]! ≤ arr[j]! - ensures arrOld.toMultiset = arr.toMultiset + method insertionSort_total (mut A : Array ℤ) return (u : Unit) + require 1 ≤ A.size + ensures ∀ i j, 0 ≤ i ∧ i ≤ j ∧ j < A.size → A[i]! ≤ A[j]! + ensures AOld.toMultiset = A.toMultiset do - let arr₀ := arr - let arr_size := arr.size - let mut n := 1 - while n ≠ arr.size - invariant arr.size = arr_size - invariant 1 ≤ n ∧ n ≤ arr.size - invariant ∀ i j, 0 ≤ i ∧ i < j ∧ j ≤ n - 1 → arr[i]! ≤ arr[j]! - invariant arr.toMultiset = arr₀.toMultiset - -- Explicit decreasing measure for loop termination is required in TotalCorrectness - decreasing arr.size - n + let A' := A + let N := A.size + let mut i := 1 + while i ≠ A.size + invariant A.size = N + invariant 1 ≤ i ∧ i ≤ A.size + invariant ∀ i' j', 0 ≤ i' ∧ i' < j' ∧ j' ≤ i - 1 → A[i']! ≤ A[j']! + invariant A.toMultiset = A'.toMultiset + decreasing A.size - i do - let mut mind := n - while mind ≠ 0 - invariant arr.size = arr_size - invariant mind ≤ n - invariant ∀ i j, 0 ≤ i ∧ i < j ∧ j ≤ n ∧ j ≠ mind → arr[i]! ≤ arr[j]! - invariant arr.toMultiset = arr₀.toMultiset - decreasing mind + let mut j := i + while j ≠ 0 + invariant A.size = N + invariant j ≤ i + invariant ∀ i' j', 0 ≤ i' ∧ i' < j' ∧ j' ≤ i ∧ j' ≠ j → A[i']! ≤ A[j']! + invariant A.toMultiset = A'.toMultiset + decreasing j do - if arr[mind]! < arr[mind - 1]! then - swap! arr[mind - 1]! arr[mind]! - mind := mind - 1 - -- Comment out line below to check produced goals - n := n + 1 + if A[j]! < A[j - 1]! then + swap! A[j - 1]! A[j]! + j := j - 1 + i := i + 1 return set_option maxHeartbeats 1000000 in prove_correct insertionSort_total by - loom_solve! + loom_solve