From e2ede3b823c8f102e649e3106b8021e83a6f286a Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 21 Nov 2024 14:34:22 +0000 Subject: [PATCH 1/3] started update --- SSA/Experimental/Bits/AutoStructs/ForLean.lean | 12 ++++++------ lake-manifest.json | 12 ++++++------ lakefile.toml | 2 +- lean-toolchain | 2 +- 4 files changed, 14 insertions(+), 14 deletions(-) diff --git a/SSA/Experimental/Bits/AutoStructs/ForLean.lean b/SSA/Experimental/Bits/AutoStructs/ForLean.lean index cea086c71..165a1dca2 100644 --- a/SSA/Experimental/Bits/AutoStructs/ForLean.lean +++ b/SSA/Experimental/Bits/AutoStructs/ForLean.lean @@ -40,8 +40,8 @@ theorem Array.mem_push (a : Array α) (x y : α) : x ∈ a.push y → x ∈ a 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.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] @@ -49,10 +49,10 @@ theorem Array.push_incl {a : Array α} {x : α} (y : α) : x ∈ a → x ∈ a.p left exact h -@[aesop 50% unsafe] -theorem Array.mem_iff_getElem? {a : Array α} {x : α} : - x ∈ a ↔ ∃ (k : Nat), a[k]? = some x := by - sorry +-- @[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 diff --git a/lake-manifest.json b/lake-manifest.json index bba4ca214..0d53f6ecd 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "60a189e5bc5c59e67faa3f3445229e76298ce4dc", + "rev": "33e7503de887ec81d3b24de62cfce9440ffa55a8", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-11-19", + "inputRev": "nightly-testing-2024-11-20", "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,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "922825a3fa019deafbf4f61ed7c70fbdeebc9206", + "rev": "9b9f4d0406d00baaae62d1a717b5aa854a2ae51d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index 91d123032..185c80916 100644 --- 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-20" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index 80611d83b..118d9e578 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-11-19 +leanprover/lean4:nightly-2024-11-20 From e0d04b93c626ed9ddfac8193798104a08e900a72 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 21 Nov 2024 19:28:49 +0000 Subject: [PATCH 2/3] more fixing --- SSA/Experimental/Bits/AutoStructs/Basic.lean | 1 + SSA/Experimental/Bits/AutoStructs/ForLean.lean | 2 +- lake-manifest.json | 8 ++++---- lakefile.toml | 2 +- lean-toolchain | 2 +- 5 files changed, 8 insertions(+), 7 deletions(-) diff --git a/SSA/Experimental/Bits/AutoStructs/Basic.lean b/SSA/Experimental/Bits/AutoStructs/Basic.lean index 38ba048e6..32296fd9c 100644 --- 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 diff --git a/SSA/Experimental/Bits/AutoStructs/ForLean.lean b/SSA/Experimental/Bits/AutoStructs/ForLean.lean index 165a1dca2..28b9cb4f6 100644 --- a/SSA/Experimental/Bits/AutoStructs/ForLean.lean +++ b/SSA/Experimental/Bits/AutoStructs/ForLean.lean @@ -36,7 +36,7 @@ theorem Array.back_mem (a : Array X) (x : X) : a.back? = some x → x ∈ a := b /- 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_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 diff --git a/lake-manifest.json b/lake-manifest.json index 0d53f6ecd..71a25ae5d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "33e7503de887ec81d3b24de62cfce9440ffa55a8", + "rev": "8ce05c99ea86bd5531e5a84a45f04cefa20df502", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-11-20", + "inputRev": "nightly-testing-2024-11-21", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9b9f4d0406d00baaae62d1a717b5aa854a2ae51d", + "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 index 185c80916..077bd9c1b 100644 --- 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-20" +rev = "nightly-testing-2024-11-21" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index 118d9e578..f589f3bf8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-11-20 +leanprover/lean4:nightly-2024-11-21 From fac01b65d409a7501eda103e245271574f408e3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= Date: Fri, 22 Nov 2024 10:57:01 +0100 Subject: [PATCH 3/3] Use new lemmas of the lean standard lib --- SSA/Experimental/Bits/AutoStructs/Basic.lean | 37 +++++++++---------- .../Bits/AutoStructs/ForLean.lean | 23 +++--------- 2 files changed, 23 insertions(+), 37 deletions(-) diff --git a/SSA/Experimental/Bits/AutoStructs/Basic.lean b/SSA/Experimental/Bits/AutoStructs/Basic.lean index 32296fd9c..1462d6865 100644 --- a/SSA/Experimental/Bits/AutoStructs/Basic.lean +++ b/SSA/Experimental/Bits/AutoStructs/Basic.lean @@ -281,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 } @@ -429,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 @@ -491,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) : @@ -560,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) : @@ -570,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 @@ -622,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 => @@ -649,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 @@ -766,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 @@ -1003,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 @@ -1066,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 } @@ -1102,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 index 28b9cb4f6..c5eb54356 100644 --- 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]