toolchain updated

siddhartha-gadgil · Jun 23, 2024 · 3811a9d · 3811a9d
1 parent ddcebe3
commit 3811a9d
Show file tree

Hide file tree

Showing 9 changed files with 53 additions and 75 deletions.
diff --git a/Saturn/Containment.lean b/Saturn/Containment.lean
@@ -386,8 +386,19 @@ def simplifiedContainment{num_clauses n : Nat}: (clauses : Vector (Clause n) num
                               Containment clauses :=
                     match num_clauses with
                     |zero => fun _ _ _ =>
-                      ⟨zero, Vector.nil, Vector.nil, fun _ jw => nomatch jw, fun _ jw => nomatch jw,
-                        Vector.nil, fun _ jw => nomatch jw, fun _ jw => nomatch jw⟩
+                      {
+                        num_reducedClauses := 0,
+                        reducedClauses := Vector.nil,
+                        forwardVec := Vector.nil,
+                        forwardBound := by simp,
+                        forwardEq := by
+                          intro _ jw
+                          simp at jw,
+                        reverseVec := Vector.nil,
+                        reverseBound := by simp,
+                        reverseEq := fun _ jw => nomatch jw
+                        }
+                      -- ⟨zero, Vector.nil, Vector.nil, fun _ jw => nomatch jw, fun _ jw => nomatch jw, Vector.nil, fun _ jw => nomatch jw, fun _ jw => nomatch jw⟩
                     | m + 1 => fun clauses posCount negCount =>
                         simplifyNonEmptyContainment (m + 1) clauses
                             posCount negCount (Containment.identity clauses)
diff --git a/Saturn/Core.lean b/Saturn/Core.lean
@@ -1,4 +1,4 @@
-import Mathlib.Data.Vector
+import Mathlib.Data.Vector.Basic
 open Nat
 /-!
 ## SATurn Core

diff --git a/Saturn/DPLL.lean b/Saturn/DPLL.lean
@@ -98,9 +98,14 @@ def restrictionData{num_clauses n: Nat}(branch: Bool)(focus: Nat)(focusLt : focu
         ReductionData branch focus focusLt clauses :=
         fun clauses =>
           let rc : ReductionClauses branch focus focusLt Vector.nil :=
-              ⟨0, Vector.nil, Vector.nil,
-                fun ⟨k, w⟩ => nomatch w,
-                Vector.nil, fun ⟨k, w⟩ => nomatch w⟩
+          {
+            num_reducedClauses := 0,
+            restClauses := Vector.nil,
+            forwardVec := Vector.nil,
+            forwardWit := by simp,
+            reverseVec := Vector.nil,
+            reverseWit := by simp
+            }
           let rd : ReductionData branch focus focusLt Vector.nil := ⟨rc,
             ⟨fun k w => nomatch w⟩,
             ⟨fun k w => nomatch w⟩,

diff --git a/Saturn/LiftSolution.lean b/Saturn/LiftSolution.lean
@@ -112,7 +112,7 @@ def liftResolutionTriple{n : Nat} (bf : Bool) (leftFoc rightFoc : Option Bool)
           apply witness_independent
           assumption
         rw [leftLem, rightLem, topLem]
-        simp [insert_at_focus]
+        simp [leftN, rightN, topN, insert_at_focus]
         exact focJoin
       else
         let i := skipInverse k jj jj_eq_k

diff --git a/Saturn/PrependClause.lean b/Saturn/PrependClause.lean
@@ -282,7 +282,7 @@ theorem revrelAux (v : Vector Nat num_reducedClauses)(clauses: Vector (Clause (n
               apply Nat.succ_lt_succ
               exact bd
           ⟩  := by
-            apply Fin.eq_of_veq
+            apply Fin.eq_of_val_eq
             simp
             symm
             exact lem
@@ -302,29 +302,26 @@ def reverseRelation{num_clauses n: Nat}(branch: Bool)(focus: Nat)(focusLt : focu
           let codomN := rcN.num_reducedClauses
           let clausesN := head +: clauses
           have relationN : (k : Nat) → (w: k < codomN) →
-                 (rcN.restClauses.get' k w).get' =
+                 (rcN.restClauses.get ⟨k, w⟩).get' =
                   delete focus focusLt
                       (clausesN.get' (rcN.reverse k w)
                       (rcN.reverseWit ⟨ k, w⟩ )).get' :=
                     by
-                    intro k
-                    match k with
-                    | zero =>
-                      intro w
+                    intro k w
+                    match k, w with
+                    | zero, _ =>
                       simp [Vector.get', Vector.of_Fn'_get]
                       rw [restClauses_prependClause]
                       simp [reverseVec_prependClause]
                       apply Vector.of_Fn'_get'
-                    | l + 1 =>
-                      intro w
-                      let lem2 := rrc.relation l (le_of_succ_le_succ w)
+                    | l + 1, w =>
+                      let w' := (le_of_succ_le_succ w)
+                      let lem2 := rrc.relation l w'
                       simp [Vector.get', ReverseRelation.relation]
                       rw [Vector.get'] at lem2
                       rw [restClauses_prependClause]
-                      simp [reverseVec_prependClause]
-                      have s : { val := l + 1, isLt := w } =
-                        Fin.succ ⟨l, le_of_succ_le_succ w⟩ := by rfl
-                      rw [s]
+                      simp [rcN, reverseVec_prependClause]
+                      show get' ((ofFn' (delete focus focusLt (get' head))+:rc.restClauses).get (⟨l, w'⟩ : Fin _).succ) = _
                       rw [Vector.get_cons_succ]
                       rw [lem2]
                       simp [ReductionClauses.reverse]
@@ -345,6 +342,7 @@ def reverseRelation{num_clauses n: Nat}(branch: Bool)(focus: Nat)(focusLt : focu
                         revrelAux v clauses head l (Nat.le_of_succ_le_succ w)
           ⟨relationN⟩
 
+#check Vector.get_cons_succ
 
 def pureReverse{num_clauses n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1)
     (clauses: Vector (Clause (n + 1)) num_clauses):

diff --git a/Saturn/Vector.lean b/Saturn/Vector.lean
@@ -58,7 +58,7 @@ theorem cons_commutes{α : Type}{n : Nat} (head : α) (tail : Vector α n) :
               rfl
 
 theorem Vector.get'_of_Fn' {α : Type}{n : Nat} (f : (k : Nat) → k < n → α) (k : Nat) (kw : k < n) :
-      (Vector.ofFn' f).get' k kw = f k kw :=
+      Vector.get' (Vector.ofFn' f) k kw = f k kw :=
       by
       let lem := Vector.of_Fn'_get' f
       let lem' := congrFun lem k

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,19 +1,19 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
-   "name": "std",
+   "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,25 +22,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "ae76973be902b1da1589b28d10648c4e57333cad",
+   "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.1",
+   "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.29",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,55 +49,19 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
+   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "5bb630b0e53879b30dc48637d83822677a64065b",
+   "rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.1",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-   "name": "CMark",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "5b096942260d7805cc90bacf4ea4a0f8e9700ccb",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "rev": "780bbec107cba79d18ec55ac2be3907a77f27f98",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.8.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "saturn",

diff --git a/lakefile.lean b/lakefile.lean
@@ -9,7 +9,7 @@ package saturn where
   ]
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.6.1"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0"
 
 
 @[default_target]
@@ -18,4 +18,4 @@ lean_lib Saturn
 lean_exe nqueens
 
 meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "c7f4ac8"
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.8.0