upgrade to leanv4.2.0-rc4

.github/workflows/check_proofs.yml

@@ -22,7 +22,7 @@ jobs:
         run: |
           curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
           chmod u+x elan-init.sh
-          ./elan-init.sh -y --default-toolchain leanprover/lean4:nightly-2023-03-09
+          ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.2.0-rc4
           echo "Adding location $HOME/.elan/bin to PATH..."
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 

.gitignore

@@ -8,3 +8,4 @@ lake-packages/*
 /lake-packages/*
 !/lake-packages/manifest.json
 prelude/build/
+/lakefile.olean

.gitpod.yml

@@ -2,7 +2,7 @@
 tasks:
   - name: Install Lean
     command: |
-      curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly-2023-03-09 -y
+      curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:v4.2.0-rc4 -y
       echo 'export PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.bashrc
       echo '### You can now close this terminal and use use File/Open folder to open the sample you want to play with.'
 vscode:

Katydid/Std/Balistic.lean

@@ -395,11 +395,11 @@ local elab "balistic" : tactic => newTactic do
     | list_single
     | list_app_uncons
     | wreck_conj
-  ) <;> try simp
-    <;> try assumption
-    <;> try exact ⟨rfl, rfl⟩
+  ) <;> (try assumption)
     <;> subst_vars
-    <;> try contradiction
+    <;> (try simp)
+    <;> (try exact ⟨rfl, rfl⟩)
+    <;> (try contradiction)
   )
 
 example: ∀ (x y: List α) (a: α),
@@ -467,6 +467,7 @@ example: ∀ (x y z: α),
 intro x y z
 balistic
 
+
 example: ∀ (x y: α) (xs ys zs xs': List α),
   x ≠ y ->
   xs ++ ys ++ zs = xs' ++ [x] ->
@@ -486,8 +487,6 @@ example:
   xs ++ [x] ++ [y] ≠ [y] ++ [x] := by
 intro x y xy xs H
 balistic
-have xy' := Eq.symm HRight -- TODO: contradiction should be smarter
-contradiction
 
 example:
   ∀ (x y: α) (xy: x ≠ y) (xs: List α),
@@ -500,4 +499,4 @@ example:
 intro x y xy xs H
 balistic
 -- TODO: balistic should be able to do this with list_cons_neq
-sorry
+sorry

Katydid/Std/Lists.lean

@@ -881,7 +881,6 @@ theorem list_prefix_is_not_empty_with_index_gt_zero: ∀ (xs: List α) (n: Nat)
     | zero =>
       contradiction
     | succ n =>
-      simp only at *
       cases xs with
       | nil =>
         contradiction

lake-manifest.json

@@ -1,39 +1,52 @@
-{"version": 4,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.11"}},
-  {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
-    "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
-    "name": "Cli",
-    "inputRev?": "nightly"}},
-  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "f8c1566ccfded661bfcb7b64f01a88be3a9d87dc",
+    "rev": "3a9b57c42ffba439bff1c6de6c350fb12b858f82",
+    "opts": {},
     "name": "mathlib",
-    "inputRev?": null}},
+    "inputRev?": null,
+    "inherited": false}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "ae84bd82cca324dc958583d6f1ae08429877dcb0",
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
     "name": "Qq",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
+    "rev": "5e016236e9e699691aaa9872fa380df12cd7f677",
+    "opts": {},
     "name": "aesop",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/lean4-cli",
+    "subDir?": null,
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.21",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "rev": "0da0e81a141cd26364f8799fb31ae7866ec43fb7",
+    "opts": {},
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main",
+    "inherited": true}}],
+ "name": "katydid"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-12
+leanprover/lean4:v4.2.0-rc4