update Lean to version 4.14.0

Author: awalterschulze

Katydid/Std/Lists.lean

@@ -44,21 +44,12 @@ theorem nat_pred_le_succ' : {n m : Nat} -> Nat.le n (succ m) -> Nat.le (pred n)
       have h_n_le_succ_n := Nat.le_succ n
       exact (Nat.le_trans h_n_le_succ_n h)
 
-theorem nat_min_zero {n: Nat}: min 0 n = 0 := by
-  unfold min
-  unfold instMinNat
-  unfold minOfLe
-  simp
 
-theorem nat_zero_min {n: Nat}: min n 0 = 0 := by
-  cases n with
-  | zero =>
-    simp
-  | succ n =>
-    unfold min
-    unfold instMinNat
-    unfold minOfLe
-    simp only [nonpos_iff_eq_zero, ite_false]
+theorem nat_min_zero {n: Nat}: min 0 n = 0 :=
+  Nat.min_eq_left (Nat.zero_le _)
+
+theorem nat_zero_min {n: Nat}: min n 0 = 0 :=
+  Nat.min_eq_right (Nat.zero_le _)
 
 theorem nat_add_succ_is_succ_add (n m: Nat): succ n + m = succ (n + m) := by
   cases n with
@@ -116,7 +107,8 @@ theorem list_length_zero_is_empty (xs: List α):
   · intro _
     rfl
   · intro h'
-    simp only [length, add_eq_zero, and_false] at h'
+    -- simp? at h'
+    simp only [length_cons, AddLeftCancelMonoid.add_eq_zero, length_eq_zero, one_ne_zero, and_false] at h'
 
 theorem list_app_nil_l (xs: List α):
   [] ++ xs = xs := by
@@ -231,7 +223,8 @@ theorem list_app_inj_tail {xs ys: List α} {x y: α}:
     cases ys with
     | nil =>
       intro h'
-      simp only [cons_append, nil_append, cons.injEq, append_eq_nil, and_false] at h'
+      -- simp? at h'
+      simp only [cons_append, nil_append, cons.injEq, append_eq_nil, cons_ne_self, and_false] at h'
     | cons heady taily =>
       intro h'
       simp only [cons_append, cons.injEq] at h'
@@ -319,7 +312,8 @@ theorem list_rev_empty (xs : List α) :
   | cons head tail =>
     intro h
     have h' : (reverse (reverse (head :: tail)) = []) := congrArg reverse h
-    simp only [reverse_cons, reverse_append, reverse_nil, nil_append, reverse_reverse, singleton_append] at h'
+    -- simp? at h'
+    simp only [reverse_cons, reverse_append, reverse_nil, nil_append, reverse_reverse, singleton_append, reduceCtorEq] at h'
 
 theorem list_rev_empty2 :
   reverse ([] : List α) = [] := by trivial
@@ -470,20 +464,22 @@ theorem list_take_take (n: Nat) (xs: List α):
   revert m xs
   induction n with
   | zero =>
-    intro m xs
-    rw [nat_min_zero]
-    repeat rw [take]
-  | succ n ihn =>
+        simp
+      | succ n ihn =>
     intro m xs
     cases m with
     | zero =>
       unfold min
+      unfold instMin_mathlib
+      unfold inferInstance
       unfold instMinNat
       unfold minOfLe
       rw [take]
       simp only [take]
     | succ m =>
       unfold min
+      unfold instMin_mathlib
+      unfold inferInstance
       unfold instMinNat
       unfold minOfLe
       simp only
@@ -498,6 +494,8 @@ theorem list_take_take (n: Nat) (xs: List α):
           apply (congrArg (cons x))
           have hmin : min n m = n := by
             unfold min
+            unfold instMin_mathlib
+            unfold inferInstance
             unfold instMinNat
             unfold minOfLe
             simp only [ite_eq_left_iff, not_le]
@@ -517,6 +515,8 @@ theorem list_take_take (n: Nat) (xs: List α):
           apply (congrArg (cons x))
           have hmin : min n m = m := by
             unfold min
+            unfold instMin_mathlib
+            unfold inferInstance
             unfold instMinNat
             unfold minOfLe
             simp only [ite_eq_right_iff]
@@ -683,6 +683,8 @@ theorem list_take_large_length {n: Nat} {xs: List α}:
 theorem list_take_length (n: Nat) (xs: List α):
   length (take n xs) = min n (length xs) := by
   unfold min
+  unfold instMin_mathlib
+  unfold inferInstance
   unfold instMinNat
   unfold minOfLe
   simp only [length_take, ge_iff_le]
@@ -904,7 +906,8 @@ theorem list_prefix_is_not_empty_with_index_gt_zero: ∀ (xs: List α) (n: Nat)
       | nil =>
         contradiction
       | cons x xs =>
-        simp only [succ_pos', take] at *
+        -- simp? at *
+        simp only [lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true, take_succ_cons, reduceCtorEq] at *
 
 theorem list_app_uncons: ∀ {x: α} {xs ys zs: List α},
   ys ++ zs = x :: xs ->

lake-manifest.json

@@ -1,75 +1,95 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0",
-   "name": "batteries",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
-   "name": "Qq",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
-   "name": "aesop",
+   "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "68280daef58803f68368eb2e53046dabcd270c9d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.47",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
-   "name": "importGraph",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "cae1b27ace5330f372b57f1051e228fe9b264d57",
-   "name": "mathlib",
+   "scope": "leanprover",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "katydid",
  "lakeDir": ".lake"}

lakefile.lean

@@ -7,5 +7,4 @@ package katydid
 lean_lib Katydid
 
 -- dependencies std4, quote4 are obtained transitively through mathlib4
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.14.0"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc2
+leanprover/lean4:v4.14.0