chore: update mathlib nightly 2024-11-21 (#866)

CC: @ineol some theorems (e.g. `Array.mem_push`) exist already, with the same name and a slightly different declaration in `Array/Lemmas`, and this is currently breaking the build. For now I commented the theorems in `ForLean`, but that obviously did not solve the problem. I'm happy to rename the theorems you wrote with a `'` if that's okay for you, but you might want to take a look at the existing theorems and maybe see if they can be useful? --------- Co-authored-by: Léo Stefanesco <[email protected]>
opencompl · Nov 22, 2024 · 64ad96f · 64ad96f
1 parent e347a53
commit 64ad96f
Show file tree

Hide file tree

Showing 5 changed files with 33 additions and 46 deletions.
diff --git a/SSA/Experimental/Bits/AutoStructs/Basic.lean b/SSA/Experimental/Bits/AutoStructs/Basic.lean
@@ -6,6 +6,7 @@ import Std.Data.HashSet
 import Std.Data.HashMap
 import Std.Data.HashMap.Lemmas
 import Batteries.Data.Fin.Basic
+import Batteries.Data.Array.Lemmas
 import Mathlib.Computability.NFA
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Card
@@ -280,7 +281,7 @@ def worklist.St.addOrCreateState (st : worklist.St A S) (final? : Bool) (sa : S)
       intro hc;
       apply st.worklist_incl at hc; simp at hc; apply Std.HashMap.get?_none_not_mem at heq; contradiction
     have worklist_incl : ∀ sa ∈ worklist, sa ∈ map := by
-      simp [worklist, map]; intros sa' hin; apply Array.mem_push at hin; rcases hin with hin | heq
+      simp [worklist, map]; intros sa' hin; rcases hin with hin | heq
       { apply st.worklist_incl at hin; aesop }
       { aesop }
     let st' := { st with m, map, worklist, worklist_nodup, worklist_incl }
@@ -428,10 +429,10 @@ where go (st0 : worklist.St A S) : RawCNFA A :=
         simp [sa?] at heq'
         constructor
         { constructor
-          { apply Array.back?_mem at heq'; apply st0.worklist_incl; assumption }
+          { apply Array.mem_of_back?_eq_some at heq'; apply st0.worklist_incl; assumption }
           { apply Array.not_elem_back_pop at heq' <;> simp_all [Array.pop, wl] } }
         constructor
-        { right; apply Array.back?_mem at heq'; assumption }
+        { right; apply Array.mem_of_back?_eq_some at heq'; assumption }
         rintro sa hh; rcases hh with hnin | hin
         { simp [hnin] }
         right
@@ -490,17 +491,14 @@ lemma addOrCreateElem_visited final? (st : worklist.St A S) sa :
   ext sa'
   split; simp
   simp; constructor <;> simp
-  · rintro ⟨rfl | h⟩ hnin
-    · exfalso; apply hnin; apply Array.mem_push_self
-    · constructor; assumption; intros hin; apply hnin; apply Array.push_incl sa hin
+  · rintro ⟨rfl | h⟩ hnin heq?
+    · simp at heq?
+    · constructor; assumption; simp [hnin]
   · rintro hin hnin; constructor
     · right; assumption
-    · intros hc; apply Array.mem_push at hc
-      rcases hc
-      · simp_all
-      · subst_eqs
-        suffices _ : sa ∉ st.map by simp_all
-        apply Std.HashMap.get?_none_not_mem; assumption
+    · constructor; assumption; rintro rfl
+      suffices _ : sa' ∉ st.map by simp_all
+      apply Std.HashMap.get?_none_not_mem; assumption
 
 omit [LawfulBEq A] [Fintype S] [DecidableEq S] in
 lemma processOneElem_visited (st : worklist.St A S) :
@@ -559,7 +557,7 @@ lemma StInv.mFun_inj' (inv : StInv' T st) : Function.Injective (inv.mFun _ _ _ _
 
 omit [Fintype S] [DecidableEq S] [LawfulBEq A] in
 lemma mFun_mem (inv : StInv' T st) (s : st.m.states) : inv.mFun _ _ _ _ s ∈ st.map :=
-  Std.HashMap.mem_of_get? (inv.mFun_spec _ _ _ _ s)
+  Std.HashMap.mem_of_getElem? (inv.mFun_spec _ _ _ _ s)
 
 omit [LawfulBEq A] [Fintype S] [DecidableEq S] in
 lemma processOneElem_states (st : worklist.St A S) (final : S → Bool) (a : A) (sa : S) (s : State) :
@@ -569,7 +567,7 @@ lemma processOneElem_states (st : worklist.St A S) (final : S → Bool) (a : A)
   split
   next s' heq =>
     dsimp
-    have _ := Std.HashMap.mem_of_get? heq
+    have _ := Std.HashMap.mem_of_getElem? heq
     split_ifs; simp_all
   next heq =>
     dsimp
@@ -621,7 +619,7 @@ lemma processOneElem_finals (st : worklist.St A S) (final : S → Bool) (a : A)
   split
   next s' heq =>
     dsimp
-    have _ := Std.HashMap.mem_of_get? heq
+    have _ := Std.HashMap.mem_of_getElem? heq
     split_ifs <;> simp_all
     simp [RawCNFA.addTrans]
   next heq =>
@@ -648,7 +646,7 @@ lemma processOneElem_trans (st : worklist.St A S) (final : S → Bool) (a b : A)
     split
     next s'' heq =>
       use s''; constructor; assumption
-      have _ := Std.HashMap.mem_of_get? heq
+      have _ := Std.HashMap.mem_of_getElem? heq
       simp [RawCNFA.addTrans]
     next heq =>
       use st.m.stateMax
@@ -765,7 +763,7 @@ def processOneElem_inv {st : worklist.St A S} (s : State) (sa : S) (k : ℕ) :
     split; on_goal 2 => simp_all
     next _ _ heq =>
       simp_all; rw [h2] at *; casesm* _ ∧ _ ; injections; subst_eqs
-      apply Std.HashMap.mem_of_get?; simp_all; rfl }
+      apply Std.HashMap.mem_of_getElem?; simp_all; rfl }
 
 seal GetElem.getElem in
 seal GetElem?.getElem? in
@@ -1002,7 +1000,7 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) :
   | case3 st hnemp sa? sa hsa? wl' st' hc =>
     have h : sa ∈ st.map := by
       apply st.worklist_incl
-      simp_all [sa?, Array.back?_mem]
+      simp_all [sa?, Array.mem_of_back?_eq_some]
     apply Std.HashMap.getElem?_eq_some_getD (fallback := 0) at h
     simp [st'] at hc
     exfalso; apply (hc _); exact h
@@ -1065,7 +1063,7 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) :
           have hmfun : inv.mFun _ _ _ _  = inv'.mFun _ _ _ _ := by simp [StInv.mFun]
           have hfun : inv.fun _ _ _ _ = inv'.fun _ _ _ _ := by simp [StInv.fun, hmfun]
           constructor
-          { simp [worklist.St.visited]; simp_all; exact Std.HashMap.mem_of_get? hmap }
+          { simp [worklist.St.visited]; simp_all; exact Std.HashMap.mem_of_getElem? hmap }
           use inv'; constructor
           { exact hsim.injective }
           { apply hsim.reduced }
@@ -1101,7 +1099,7 @@ def worklistGo_spec {st : worklist.St A S} (inv : StInv' ∅ st) :
           intros hin
           suffices ex : ∃ s, st.map[sa]? = some s by simp_all
           simp_all
-        exfalso; apply hnin; apply st.worklist_incl; exact Array.back_mem st.worklist sa hsome
+        exfalso; apply hnin; apply st.worklist_incl; exact Array.mem_of_back?_eq_some hsome
     next hnone =>
       simp [Array.back?] at *
       have : st.worklist.size = 0 := by omega

diff --git a/SSA/Experimental/Bits/AutoStructs/ForLean.lean b/SSA/Experimental/Bits/AutoStructs/ForLean.lean
@@ -27,34 +27,23 @@ theorem List.dropLast_nodup (l : List X) : l.Nodup → l.dropLast.Nodup := by
 theorem Array.not_elem_back_pop (a : Array X) (x : X) : a.toList.Nodup → a.back? = some x → x ∉ a.pop := by sorry
 
 /- Upstream? -/
-theorem Array.back?_mem (a : Array X) (x : X) : a.back? = some x → x ∈ a := by sorry
-
 theorem Array.not_elem_back_pop_list (a : Array X) (x : X) : a.toList.Nodup → a.back? = some x → x ∉ a.toList.dropLast := by sorry
 
-theorem Array.back_mem (a : Array X) (x : X) : a.back? = some x → x ∈ a := by sorry
-
 /- Upstream? -/
 theorem Array.mem_of_mem_pop (a : Array α) (x : α) : x ∈ a.pop → x ∈ a := by sorry
 
-theorem Array.mem_push (a : Array α) (x y : α) : x ∈ a.push y → x ∈ a ∨ x = y := by sorry
-
 theorem Array.mem_pop_iff (a : Array α) (x : α) : x ∈ a ↔ x ∈ a.pop ∨ a.back? = some x := by sorry
 
-theorem Array.mem_push_self (a : Array α) (x : α) : x ∈ a.push x := by
-  simp [Array.push]
-
 theorem Array.push_incl {a : Array α} {x : α} (y : α) : x ∈ a → x ∈ a.push y := by
   simp [Array.push]
   intros h
   left
   exact h
 
-@[aesop 50% unsafe]
-theorem Array.mem_iff_getElem? {a : Array α} {x : α} :
-     x ∈ a ↔ ∃ (k : Nat), a[k]? = some x := by
-  sorry
-
-theorem Std.HashMap.keys_nodup [BEq K] [Hashable K] (m : Std.HashMap K V) : m.keys.Nodup := by sorry
+theorem Std.HashMap.keys_nodup [BEq K] [LawfulBEq K] [Hashable K] (m : Std.HashMap K V) : m.keys.Nodup := by
+  unfold List.Nodup
+  have x := distinct_keys (m := m)
+  simp_all
 
 @[simp]
 theorem Std.HashMap.mem_keys_iff_mem [BEq K] [Hashable K] (m : Std.HashMap K V) (k : K) : k ∈ m.keys ↔ k ∈ m := by sorry
@@ -77,8 +66,8 @@ theorem Std.HashMap.get?_none_not_mem [BEq K] [LawfulBEq K] [Hashable K] [Lawful
   sorry
 
 @[aesop 50% unsafe]
-theorem Std.HashMap.mem_of_get? [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} :
-    m.get? k = some v → k ∈  m := by
+theorem Std.HashMap.mem_of_getElem? [BEq K] [LawfulBEq K] [Hashable K] [LawfulHashable K] {m : Std.HashMap K V} {k : K} :
+    m[k]? = some v → k ∈  m := by
   sorry
 
 @[aesop 50% unsafe]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "60a189e5bc5c59e67faa3f3445229e76298ce4dc",
+   "rev": "8ce05c99ea86bd5531e5a84a45f04cefa20df502",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-11-19",
+   "inputRev": "nightly-testing-2024-11-21",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0fc755a2a762bd228db724df926de7d3e2306a34",
+   "rev": "a75e35f6cb83e773231f793d1cd8112e41804934",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24d0b61ede545901e80ee866a3609f9e78080034",
+   "rev": "0c995c64c9c8e4186e24f85d5d61bc404b378ba6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "922825a3fa019deafbf4f61ed7c70fbdeebc9206",
+   "rev": "b3935d53ce8dad5665af7ac41f06f0f6de4d942f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "lean-pr-testing-6128",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "SSA",

diff --git a/lakefile.toml b/lakefile.toml
@@ -4,7 +4,7 @@ defaultTargets = ["SSA"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-11-19"
+rev = "nightly-testing-2024-11-21"
 
 [[require]]
 name = "Cli"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-19
+leanprover/lean4:nightly-2024-11-21