use newer Lean and mathlib versions

m4lvin · Dec 18, 2023 · 6109d61 · 6109d61
1 parent cc9880c
commit 6109d61
Show file tree

Hide file tree

Showing 8 changed files with 76 additions and 92 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.4.0-rc1