From 154ce7a2fb14ee3f6d894c156d166da564240650 Mon Sep 17 00:00:00 2001 From: Walter Schulze Date: Sun, 29 Oct 2023 19:05:53 +0000 Subject: [PATCH] upgrade to leanv4.2.0-rc4 --- .github/workflows/check_proofs.yml | 2 +- .gitignore | 1 + .gitpod.yml | 2 +- Katydid/Std/Balistic.lean | 13 +++---- Katydid/Std/Lists.lean | 1 - lake-manifest.json | 59 ++++++++++++++++++------------ lean-toolchain | 2 +- 7 files changed, 46 insertions(+), 34 deletions(-) diff --git a/.github/workflows/check_proofs.yml b/.github/workflows/check_proofs.yml index e39b9ef..a8f4042 100644 --- a/.github/workflows/check_proofs.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index 0ffbc0c..579be70 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ lake-packages/* /lake-packages/* !/lake-packages/manifest.json prelude/build/ +/lakefile.olean \ No newline at end of file diff --git a/.gitpod.yml b/.gitpod.yml index 46b13f4..12b92bc 100644 --- a/.gitpod.yml +++ b/.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: diff --git a/Katydid/Std/Balistic.lean b/Katydid/Std/Balistic.lean index 028e56f..7abb285 100644 --- a/Katydid/Std/Balistic.lean +++ b/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 \ No newline at end of file +sorry diff --git a/Katydid/Std/Lists.lean b/Katydid/Std/Lists.lean index cf382d6..b218a8b 100644 --- a/Katydid/Std/Lists.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index 33306e4..7f429b0 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lean-toolchain b/lean-toolchain index 7e1c30c..00004ee 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-07-12 +leanprover/lean4:v4.2.0-rc4 \ No newline at end of file