ICan'tBelieveItCanSort

Changes

5 changed files (+68/-19)

• Sort.lean (new)
  • @@ -0,0 +1,49 @@
    + import CaseStudies.Velvet.Std + + set_option loom.semantics.termination "total" + set_option loom.semantics.choice "demonic" + + attribute [grind] Array.multiset_swap + + method ICan'tBelieveItCanSort (mut A : Array ℤ) return (u : Unit) + ensures ∀ i, 0 < i ∧ i < A.size → A[i - 1]! ≤ A[i]! + ensures AOld.toMultiset = A.toMultiset + do + let A' := A + let N := A.size + let mut i : ℕ := 0 + while i < A.size + invariant A.size = N + invariant ∀ j, 0 < j ∧ j < i → A[j - 1]! ≤ A[j]! + invariant A.toMultiset = A'.toMultiset + decreasing A.size - i + do + let mut j := 0 + while j < A.size + invariant A.size = N + invariant ∀ k, 0 ≤ k ∧ k < j → A[k]! ≤ A[i]! + invariant ∀ k, 0 < k ∧ k < i → A[k - 1]! ≤ A[k]! + invariant A.toMultiset = A'.toMultiset + decreasing A.size - j + do + if A[i]! < A[j]! then + swap! A[i]! A[j]! + j := j + 1 + i := i + 1 + return + set_option maxHeartbeats 1000000 in + prove_correct ICan'tBelieveItCanSort by + loom_solve + intro k h₁ h₂ + by_cases h : k = j + · simp [h] + have : j ≠ k - 1 := by grind + have : i ≠ k - 1 := by grind + have : ((A_1.set! i A_1[j]!).set! j A_1[i]!)[j - 1]! = A_1[j - 1]! := by grind + simp at this + rw [this] + have : ((A_1.set! i A_1[j]!).set! j A_1[i]!)[j]! = A_1[i]! := by grind + simp at this + rw [this] + exact invariant_5 (j - 1) (by grind) (by grind) + · grind
• Test.lean
  • @@ -37,4 +37,4 @@ n := n + 1
    return set_option maxHeartbeats 1000000 in prove_correct insertionSort_total by - loom_solve! + loom_solve
• lake-manifest.json
  • @@ -5,37 +5,37 @@ [{"url": "https://github.com/verse-lab/loom",
    "type": "git", "subDir": null, "scope": "verse-lab", - "rev": "2c7dbe712e87fca52517bcab22cef3c5136b6586", + "rev": "bdafc850d4b041eea253baac26dc34d0238e3e8e", "name": "Loom", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "bdafc850d4b041eea253baac26dc34d0238e3e8e", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "36d85bf6372f1a35fb5487325d1ef965b33c6296", + "rev": "e1ef2099e666103b85cd099a1ab5086ede15e7c0", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "e1ef2099e666103b85cd099a1ab5086ede15e7c0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", + "rev": "c98ae54af00eaefe79c51b2b278361ca94e59bfb", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.24.0", + "inputRev": "v4.25.2", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805", + "rev": "0203092c2e5e26edf967000f0e177cf31c72e17a", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -45,7 +45,7 @@ {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -55,7 +55,7 @@ {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d768126816be17600904726ca7976b185786e6b9", + "rev": "3611075024b3529e5798e53c733671039f06f0bd", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -65,17 +65,17 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "556caed0eadb7901e068131d1be208dd907d07a2", + "rev": "45777338ffb69576c945dfe9466665b8023a8b8c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.74", + "inputRev": "v0.0.80+lean-v4.25.2", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50", + "rev": "a2e4d9e9aebdbdce1ce6b6f0a19dd49e0120c990", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -85,7 +85,7 @@ {"url": "https://github.com/leanprover-community/quote4",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c", + "rev": "9bff22d64abde45944c7b1f55bce6c89dd8307e6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master",
  • @@ -95,7 +95,7 @@ {"url": "https://github.com/leanprover-community/batteries",
    "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee", + "rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",
  • @@ -105,10 +105,10 @@ {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git", "subDir": null, "scope": "leanprover", - "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da", + "rev": "cd188c6ecfbf6c00cf639e4d4fb18bf773ce8c2c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.25.1", "inherited": true, "configFile": "lakefile.toml"}], "name": "loomtest",
• lakefile.toml
  • @@ -12,4 +12,4 @@
    [[require]] name = "Loom" scope = "verse-lab" - rev = "master" + rev = "bdafc850d4b041eea253baac26dc34d0238e3e8e"
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.24.0 + leanprover/lean4:v4.25.2