1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45

import Std.Tactic.Do

variable [LT α] [DecidableLT α]

def Sorted (A : Array α) := Id.run do
  for hi : i in [:A.size - 1] do
    have := Membership.get_elem_helper hi rfl
    if A[i] > A[i + 1] then
      return false
  return true

def fact
  | 0 | 1 => 1
  | n + 1 => (n + 1) * fact n

def Array.sort (A : Array α) : Except String (Array α) := do
  let mut A := A
  let mut gen := mkStdGen 0
  for i in [:fact A.size ^ 69] do
    let i := randNat gen 0 <| A.size - 1
    gen := i.2
    let j := randNat gen 0 <| A.size - 1
    gen := j.2
    if h : i.1 < A.size ∧ j.1 < A.size then
      A := A.swap i.1 j.1
    if Sorted A then
      return A
  throw "This array sucks"

open Std.Do

theorem sortCorrect (A : Array α) : ⦃⌜True⌝⦄ A.sort ⦃post⟨
    fun A' => ⌜A'.Perm A ∧ Sorted A'⌝,
    fun msg => ⌜msg = "This array sucks"⌝⟩⦄ := by
  mvcgen [Array.sort] <;> expose_names
  case inv1 => exact ⇓⟨xs, A', A'', _⟩ => ⌜A''.Perm A ∧
    match A' with
    | some A' => Sorted A' ∧ A'.Perm A
    | none => True⌝
  all_goals simp_all
  case vc1.step.isTrue.isTrue | vc2.step.isTrue.isFalse =>
    have : b.2.1 = A_1 := by grind
    exact Array.Perm.trans (by apply Array.swap_perm) (this ▸ h_2).1
  case vc3.step.isFalse.isTrue => grind
  case vc4.step.isFalse.isFalse => grind