Initial commit

Changes

16 changed files (+523/-0)

• .gitignore (new)
  • @@ -0,0 +1,1 @@
    + /.lake
• Aristotle.lean (new)
  • @@ -0,0 +1,69 @@
    + import Mathlib + + variable [LE α] [DecidableLE α] [Std.IsLinearOrder α] (xs : List α) + + def ins (a : α) + | [] => [a] + | x :: xs => + if a ≤ x then a :: x :: xs else x :: ins a xs + + def List.insSort : List α → List α + | [] => [] + | x :: xs => ins x xs.insSort + + def Sorted : List α → Prop + | [] | [_] => True + | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs) + + noncomputable section AristotleLemmas + + /- + Inserting an element `x` into a list `xs` results in a permutation of `x :: xs`. + -/ + theorem ins_perm (x : α) (xs : List α) : List.Perm (ins x xs) (x :: xs) := by + -- By definition of `ins`, we know that `ins x [] = [x]`. + have h_base : List.Perm (ins x []) (x :: []) := by + rfl; + induction xs <;> simp_all +decide [ List.Perm ]; + -- By definition of `ins`, we know that `ins x (head :: tail)` is either `x :: head :: tail` or `head :: ins x tail`. + have h_cases : ins x (‹α› :: ‹List α›) = if x ≤ ‹α› then x :: ‹α› :: ‹List α› else ‹α› :: ins x ‹List α› := by + exact?; + split_ifs at h_cases <;> simp_all +decide [ List.Perm.swap ]; + rename_i k hk ih; + exact List.Perm.trans ( List.Perm.cons _ hk ) ( List.Perm.swap .. ) + + /- + Inserting an element into a sorted list preserves sortedness. + -/ + theorem ins_sorted [LE α] [DecidableLE α] [Std.IsLinearOrder α] (x : α) (xs : List α) (h : Sorted xs) : Sorted (ins x xs) := by + revert x xs; + intro x y; + induction y <;> simp_all +decide [ ins ]; + · tauto; + · rename_i k hk ih; + split_ifs with h; + · exact fun h' => ⟨ h, h' ⟩; + · rcases hk with ( _ | ⟨ y, hk ⟩ ) <;> simp_all +decide [ Sorted ]; + · constructor; + · exact?; + · trivial; + · -- Since $k \leq y$ and $y \leq x$, we have $k \leq x$. + have h_kx : k ≤ x := by + exact?; + rcases n : ins x ( y :: hk ) with ( _ | ⟨ z, _ | ⟨ w, l ⟩ ⟩ ) <;> simp_all +decide [ Sorted ]; + · unfold ins at n; aesop; + · unfold ins at n; aesop; + + end AristotleLemmas + + theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by + constructor; + · induction xs <;> simp_all +decide [ List.insSort ]; + · trivial; + · exact?; + · induction xs; + · rfl; + · -- By definition of `ins`, we have `ins head (tail.insSort) = head :: tail.insSort` if `head ≤ tail.insSort`. + have h_insert : List.Perm (ins ‹α› (‹List α›.insSort)) (‹α› :: ‹List α›.insSort) := by + exact?; + exact List.Perm.trans ( List.Perm.cons _ ‹_› ) h_insert.symm
• Beginner.lean (new)
  • @@ -0,0 +1,30 @@
    + import Mathlib + + def ins (a : Nat) (xs : List Nat) : List Nat := + if xs = [] then + [] + else if a <= xs.head! then + [a] ++ xs + else + [xs.head!] ++ ins a xs.tail! + termination_by xs + decreasing_by + simp + simp! + simp? + simp?! + trivial + grind + try? + hint + rfl + simp_all + rw?? + aesop + nlinarith + skip + uninstall lean + uninstall! + uninstall?! + sudo uninstall -- unexpected identifier; expected 'set_option' + sudo set_option uninstall lean -- unsupported option value lean
• Conventional.lean (new)
  • @@ -0,0 +1,20 @@
    + def Array.insSort (A : Array Int32) := Id.run do + let N := A.size + let mut A := A + for i in [:N] do + for j in [:i] do + -- Screw bounds checking + -- I'm not afraid of segfaults + if A[i - j]'(by sorry) < A[i - j - 1]'(by sorry) then + A := A.swap (i - j - 1) (i - j) (by sorry) (by sorry) + else + break + return A + + -- Obviously that code is correct + theorem insSortCorrect : True := .intro + + -- Actually let's test it just in case + #guard let A := #[69, 420, 1, 1, 13, 1, 65536] + A.insSort = A.qsort + -- Yay it passed, so it must be correct
• Evil.lean (new)
  • @@ -0,0 +1,36 @@
    + import Mathlib + import Lean + + variable [LinearOrder α] (xs : List α) + + def ins (a : α) + | [] => [a] + | x :: xs => + if a ≤ x then a :: x :: xs else x :: ins a xs + + def List.insSort : List α → List α + | [] => [] + | x :: xs => ins x xs.insSort + + def Sorted : List α → Prop + | [] | [_] => True + | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs) + + open Lean Environment + + def emptDecl : Declaration := + .thmDecl { name := `empt + levelParams := [] + type := .const ``Empty [] + value := .lit (.strVal "😈") } + + elab "add_empt" : command => do + let env' := addDeclCore (← get).env 0 emptDecl none 0 + match env' with + | .error _ => throwError "@" + | .ok e => modifyEnv (fun _ ↦ e) + + add_empt + + theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := + Empty.elim empt
• Experienced.lean (new)
  • @@ -0,0 +1,20 @@
    + import Mathlib.Order.Lattice + + variable [LinearOrder α] (xs : List α) + + @[grind] + def ins (a : α) + | [] => [a] + | x :: xs => if a ≤ x then a :: x :: xs else x :: ins a xs + + abbrev List.insSort := xs.foldr ins [] + + abbrev Sorted := xs.IsChain (· ≤ ·) + + theorem insCorrect x : (Sorted xs → Sorted (ins x xs)) ∧ (x :: xs).Perm (ins x xs) := by + induction xs with + | nil => grind + | cons _ xs => cases xs <;> grind + + theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by + induction xs <;> grind [insCorrect]
• Golf.lean (new)
  • @@ -0,0 +1,1 @@
    + variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α)@[grind]def I(n:α)|[]=>[n]|h::t=>ite (n≤h) (n::h::t) (h::I n t)@[grind]def S:List α→List α|[]=>[]|h::t=>I h<|S t@[grind]def D:List α→Prop|[]|[_]=>True|h::h'::t=>h≤h'∧D (h'::t)theorem A(n):(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with|nil=>grind|cons _ t=>cases t<;>grind example:D (S l)∧l.Perm (S l):=by induction l with|nil=>grind|cons h t=>grind[A (S t) h]
• Imperative.lean (new)
  • @@ -0,0 +1,69 @@
    + import Std.Tactic.Do + import Mathlib.Algebra.Order.Group.Nat + + variable [LinearOrder α] (A : Array α) + + def Array.insSort := Id.run do + let N := A.size + let mut A := A.toVector + for hi : i in [:N] do + for hj : j in [:i] do + have := Membership.get_elem_helper hi rfl + if A[i - j] < A[i - j - 1] then + A := A.swap (i - j - 1) (i - j) + else + break + return A.toArray + + open Std.Do + + theorem insSortPerm : A.insSort.Perm A := by + generalize h : A.insSort = x + apply Id.of_wp_run_eq h + mvcgen invariants + · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝ + · ⇓⟨_, A'⟩ => ⌜A.Perm A'.toArray⌝ + with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm] + + abbrev Sorted := ∀ i (_ : 0 ≤ i ∧ i < A.size - 1), A[i] ≤ A[i + 1] + + abbrev SortedRange (l r : ℕ) (_ : l ≤ A.size) (_ : r ≤ A.size) := + ∀ i (_ : l ≤ i ∧ i < r - 1), A[i] ≤ A[i + 1] + + theorem insSortSorted : Sorted A.insSort := by + generalize h : A.insSort = x + apply Id.of_wp_run_eq h + mvcgen <;> expose_names + case inv1 => exact ⇓⟨xs, A'⟩ => ⌜SortedRange A'.toArray 0 xs.pos (by grind) (by grind [List.length_append, xs.property])⌝ + case inv2 => + exact ⇓⟨xs, A'⟩ => ⌜SortedRange A'.toArray 0 (cur - xs.pos) (by grind) (by grind) + ∧ SortedRange A'.toArray (cur - xs.pos) (cur + 1) (by grind) (by grind) + ∧ ((_ : 0 < xs.pos ∧ xs.pos < cur) → A'[cur - xs.pos - 1]'(by grind) ≤ A'[cur - xs.pos + 1]'(by grind))⌝ + case vc1.step.isTrue => + simp at h_5 ⊢ + and_intros + · grind + · intro i hi + by_cases i = cur - cur_1 - 1 ∨ i = cur - cur_1 + · grind + · grind [h_5.2.1 i (by grind)] + · intro _ + grind [h_5.1 (cur - cur_1 - 2) (by grind)] + case vc2.step.isFalse => + simp_all + and_intros + · grind + · intro i hi + by_cases i < cur - cur_1 - 1 + · exact h_5.1 i (by grind) + · by_cases cur - cur_1 ≤ i + · exact h_5.2.1 i (by grind) + · grind + · grind + case vc4.step.post.success => + simp at h_3 ⊢ + grind + all_goals grind + + theorem insSortCorrect : A.insSort.Perm A ∧ Sorted A.insSort := + ⟨insSortPerm A, insSortSorted A⟩
• Intermediate.lean (new)
  • @@ -0,0 +1,37 @@
    + import Mathlib + + variable [LinearOrder α] + + def ins (a : α) + | [] => [a] + | x :: xs => + if a ≤ x then + a :: x :: xs + else + x :: ins a xs + + def List.insSort : List α → List α + | [] => [] + | x :: xs => ins x xs.insSort + + inductive Sorted : List α → Prop where + | nil : Sorted [] + | single x : Sorted [x] + | cons_cons x x' xs : x ≤ x' → Sorted (x' :: xs) → Sorted (x :: x' :: xs) + + theorem insCorrect x (xs : List α) : (Sorted xs → Sorted (ins x xs)) ∧ (x :: xs).Perm (ins x xs) := by + constructor + · intro h + unfold ins + grind + induction xs <;> grind + try? + hint + sorry + · sorry + + -- WARNING: This will uninstall Lean! + -- #eval do + -- IO.FS.removeDirAll + -- <| .mk <$> (← IO.getEnv "ELAN_HOME") |>.getD + -- <| (← Std.Internal.IO.Async.System.getHomeDir) / ".elan"
• Lazy.lean (new)
  • @@ -0,0 +1,3 @@
    + import Curl + + open Curl
• Long.lean (new)
  • @@ -0,0 +1,77 @@
    + import Mathlib.Order.Lattice + + variable [LinearOrder α] + + def ins (a : α) : List α → List α + | [] => [a] + | x :: xs => + if a ≤ x then + a :: x :: xs + else + x :: ins a xs + + def List.insSort : List α → List α + | [] => [] + | x :: xs => ins x xs.insSort + + def Sorted : List α → Prop + | [] | [_] => True + | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs) + + theorem insSorted (a : α) (xs : List α) : + Sorted xs → Sorted (ins a xs) := by + induction xs + case nil => simp [Sorted, ins] + case cons x xs ih => + cases xs + case nil => + by_cases h₁ : a ≤ x + · simp [ins, h₁, Sorted] + · simp only [Sorted, ins, h₁, ↓reduceIte, and_true, forall_const] + exact le_of_lt <| lt_of_not_ge h₁ + case cons x' t => + by_cases h₁ : a ≤ x + · simp [ins, h₁, Sorted] + · by_cases h₂ : a ≤ x' + · simp only [Sorted, ins, h₁, ↓reduceIte, h₂, true_and, and_imp] + intro h₃ h₄ + constructor + · exact le_of_lt <| lt_of_not_ge h₁ + · exact h₄ + · simp only [Sorted, ins, h₁, ↓reduceIte, h₂, and_imp] + intro h₃ h₄ + constructor + · exact h₃ + · have ih₂ := ih h₄ + simp only [ins, h₂, ↓reduceIte] at ih₂ + exact ih₂ + + theorem insSortSorted (xs : List α) : + Sorted xs.insSort := by + induction xs + case nil => simp [List.insSort, Sorted] + case cons x xs ih => + rw [List.insSort] + exact (insSorted x xs.insSort) ih + + theorem insPerm (xs : List α) (a : α) : + List.Perm (a :: xs) (ins a xs) := by + induction xs + case nil => rw [ins] + case _ x xs ih => + rw [ins] + by_cases h₁ : a ≤ x + · simp [h₁] + · simp only [h₁] + exact .trans (.swap x a xs) (.cons x ih) + + theorem insSortPerm (xs : List α) : + List.Perm xs xs.insSort := by + induction xs + case nil => rw [List.insSort] + case cons h t ih => + rw [List.insSort] + exact .trans (.cons h ih) (insPerm t.insSort h) + + theorem insSortCorrect (xs : List α) : Sorted xs.insSort ∧ xs.Perm xs.insSort := + ⟨insSortSorted xs, insSortPerm xs⟩
• Mathematician.lean (new)
  • @@ -0,0 +1,23 @@
    + import Mathlib + + variable [LinearOrder α] (xs : List α) + + inductive Sorted' : List α → Prop where + | nil : Sorted' [] + | single x : Sorted' [x] + | cons_cons x x' xs : x ≤ x' → Sorted' (x' :: xs) → Sorted' (x :: x' :: xs) + + -- open Classical in + -- noncomputable def List.insSort : List α := by + -- have blah' : ∃ ys : List α, Sorted' ys ∧ ys.Perm xs := by + -- sorry + -- have blah : ∃ n, 3 + n = 4 := by + -- use 1 + -- obtain ⟨x, hx⟩ := blah + -- exact ys + + + + + theorem insSortCorrect : ∃ ys, Sorted' ys ∧ xs.Perm ys := by + have : xs.permutations
• README.md (new)
  • @@ -0,0 +1,13 @@
    + # evolution + + ## GitHub configuration + + To set up your new GitHub repository, follow these steps: + + * Under your repository name, click **Settings**. + * In the **Actions** section of the sidebar, click "General". + * Check the box **Allow GitHub Actions to create and approve pull requests**. + * Click the **Pages** section of the settings sidebar. + * In the **Source** dropdown menu, select "GitHub Actions". + + After following the steps above, you can remove this section from the README file.
• lake-manifest.json (new)
  • @@ -0,0 +1,105 @@
    + {"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/bergmannjg/leanCurl", + "type": "git", + "subDir": null, + "scope": "bergmannjg", + "rev": "5ef9a480e51eaa082784a73c1aa574584d09990f", + "name": "Curl", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "32d24245c7a12ded17325299fd41d412022cd3fe", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0-rc1", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "19e5f5cc9c21199be466ef99489e3acab370f079", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ef8377f31b5535430b6753a974d685b0019d0681", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.84", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "fb12f5535c80e40119286d9575c9393562252d21", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "evolution", + "lakeDir": ".lake"}
• lakefile.toml (new)
  • @@ -0,0 +1,18 @@
    + name = "evolution" + version = "0.1.0" + moreLinkArgs = ["/nix/store/0apq92vpf3f3kll8vl9nhjq1gaaffibk-curl-8.17.0/lib/libcurl.so.4"] + + [leanOptions] + pp.unicode.fun = true # pretty-prints `fun a ↦ b` + relaxedAutoImplicit = false + weak.linter.mathlibStandardSet = true + maxSynthPendingDepth = 3 + + [[require]] + name = "mathlib" + scope = "leanprover-community" + rev = "v4.27.0-rc1" + + [[require]] + name = "Curl" + scope = "bergmannjg"
• lean-toolchain (new)
  • @@ -0,0 +1,1 @@
    + leanprover/lean4:v4.27.0-rc1