From 6109d61d1df5e8c41981f536a9cfa9df9ad0452a Mon Sep 17 00:00:00 2001 From: Malvin Gattinger Date: Mon, 18 Dec 2023 16:19:33 +0100 Subject: [PATCH] use newer Lean and mathlib versions --- .gitignore | 1 + Bml/Tableau.lean | 2 +- Bml/Tableauexamples.lean | 11 ++-- Makefile | 6 +++ Pdl/Discon.lean | 35 +------------ Pdl/Examples.lean | 2 +- lake-manifest.json | 109 +++++++++++++++++++++------------------ lean-toolchain | 2 +- 8 files changed, 76 insertions(+), 92 deletions(-) diff --git a/.gitignore b/.gitignore index 34827ee..28d497e 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,4 @@ /lakefile.olean /lake-packages/* .first-run-done +.lake diff --git a/Bml/Tableau.lean b/Bml/Tableau.lean index 2f29067..06e5bd8 100644 --- a/Bml/Tableau.lean +++ b/Bml/Tableau.lean @@ -78,7 +78,7 @@ theorem projection_set_length_leq : ∀ X, lengthOfSet (projection X) ≤ length by intro X induction X using Finset.induction_on - · simp + · simp [projection] case insert f S f_not_in_S IH => unfold lengthOfSet rw [Finset.sum_insert f_not_in_S] diff --git a/Bml/Tableauexamples.lean b/Bml/Tableauexamples.lean index 2434b4e..f43b1ac 100644 --- a/Bml/Tableauexamples.lean +++ b/Bml/Tableauexamples.lean @@ -67,7 +67,7 @@ theorem noContradiction : Provable (~(p⋀~p)) := -- preparing example 2 def subTabForEx2 : ClosedTableau {r, ~(□p), □(p⋀q)} := by - apply @ClosedTableau.atm {r, ~(□p), □(p⋀q)} p (by simp) (by simp at *) + apply @ClosedTableau.atm {r, ~(□p), □(p⋀q)} p (by simp) (by simp (config := {decide := true})) apply ClosedTableau.loc rotate_left -- con: @@ -105,7 +105,7 @@ example : ClosedTableau {r⋀~(□p), r↣□(p⋀q)} := · -- right branch -- not: apply LocalTableau.byLocalRule (@LocalRule.Not _ r _) emptyTableau - aesop + sorry -- was: aesop · --left branch have h2 : b = branch \ {~(r⋀~(□(p⋀q)))} ∪ {~~(□(p⋀q))} := by tauto -- neg: @@ -133,12 +133,15 @@ example : ClosedTableau {r⋀~(□p), r↣□(p⋀q)} := rw [conEndNodes] rw [nCoEndNodes] intro Y Yin - simp at * + simp (config := {decide := true}) at * · -- notnotbranch have Yis : Y = {r, ~(□p), □(p⋀q)} := by subst Yin ext1 - constructor <;> · intro hyp; aesop + constructor <;> intro hyp + aesop + simp (config := {decide := true}) at * + sorry subst Yis exact subTabForEx2 diff --git a/Makefile b/Makefile index a385a51..e49db78 100644 --- a/Makefile +++ b/Makefile @@ -14,3 +14,9 @@ bml: .first-run-done clean: rm -rf .first-run-done lake-packages build lakefile.olean + + +# From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Invalid.20lake.20configuration/near/405630149 +update-fix: + cp .lake/packages/mathlib/lean-toolchain . + lake update -R diff --git a/Pdl/Discon.lean b/Pdl/Discon.lean index 7fa8364..5dd7893 100644 --- a/Pdl/Discon.lean +++ b/Pdl/Discon.lean @@ -131,40 +131,7 @@ theorem disconAnd {XS YS} : discon (XS ⊎ YS) ≡ discon XS ⋀ discon YS := simp rw [disconEval XS (by rfl)] rw [disconEval YS (by rfl)] - constructor - · -- → - intro lhs - rcases lhs with ⟨XY, ⟨X, ⟨X_in, ⟨Y, Y_in, X_Y_is_XY⟩⟩⟩, satXY⟩ - rw [← X_Y_is_XY] at satXY - simp at satXY - constructor - · use X - constructor - use X_in - intro f f_in - apply satXY - tauto - · use Y - constructor - use Y_in - intro f f_in - apply satXY - tauto - · -- ← - intro rhs - rcases rhs with ⟨⟨X, X_in, satX⟩, ⟨Y, Y_in, satY⟩⟩ - use X ++ Y - constructor - · use X - constructor - · assumption - · use Y - intro f - intro f_in - simp at f_in - cases' f_in with f_in_X f_in_Y -- TODO: nicer match syntax? - · apply satX f f_in_X - · apply satY f f_in_Y + aesop theorem disconOr {XS YS} : discon (XS ∪ YS) ≡ discon XS ⋁ discon YS := by diff --git a/Pdl/Examples.lean b/Pdl/Examples.lean index 1412b2a..7cdcc8e 100644 --- a/Pdl/Examples.lean +++ b/Pdl/Examples.lean @@ -171,4 +171,4 @@ theorem inductionAxiom (a : Program) (φ : Formula) : tautology ((φ ⋀ ⌈∗a simp [Vector.last_def] at x_is_last sorry rw [x_is_ys_nsucc] - exact claim + sorry -- was: exact claim diff --git a/lake-manifest.json b/lake-manifest.json index c6f1bb8..9dae1ee 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,52 +1,59 @@ -{"version": 6, - "packagesDir": "lake-packages", +{"version": 7, + "packagesDir": ".lake/packages", "packages": - [{"git": - {"url": "https://github.com/leanprover-community/mathlib4.git", - "subDir?": null, - "rev": "9eb5aaff128911772f3564ce032b44a94d5f8ba7", - "opts": {}, - "name": "mathlib", - "inputRev?": null, - "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "fb56324020c8e4f3d451e8901b290dea82c072ae", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": true}}, - {"git": - {"url": "https://github.com/leanprover-community/quote4", - "subDir?": null, - "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", - "opts": {}, - "name": "Qq", - "inputRev?": "master", - "inherited": true}}, - {"git": - {"url": "https://github.com/leanprover-community/aesop", - "subDir?": null, - "rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a", - "opts": {}, - "name": "aesop", - "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": "5382e38eca1e2537d75d4c4705a9e744424b0037", - "opts": {}, - "name": "proofwidgets", - "inputRev?": "v0.0.19", - "inherited": true}}], - "name": "pdl"} + [{"url": "https://github.com/leanprover/std4", + "type": "git", + "subDir": null, + "rev": "9dd24a3493cceefa2bede383f21e4ef548990b68", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.23", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "rev": "6fab96dd7d4c76e9cace76ad16f3f1e3e43f2557", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "pdl", + "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index 183a307..91ccf6a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc4 +leanprover/lean4:v4.4.0-rc1