From b42a7780e2f284dc53956ada763bd1ba575ef670 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 5 Aug 2025 13:41:28 +0200 Subject: [PATCH] feat: default `let rec` and `where` decls to private under the module system (#9666) This PR addresses an outstanding feature in the module system to automatically mark `let rec` and `where` helper declarations as private unless they are defined in a public context such as under `@[expose]`. --- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Array/Lemmas.lean | 13 +++++++------ src/Init/Data/Fin/Fold.lean | 24 ++++++++++++------------ src/Init/Data/Fin/Lemmas.lean | 2 +- src/Init/Data/List/Impl.lean | 4 ++-- src/Init/Data/List/Sort/Impl.lean | 10 +++++----- src/Init/Data/List/ToArray.lean | 10 +++++----- src/Init/Data/Nat/Fold.lean | 6 +++--- src/Init/Data/Vector/Lemmas.lean | 2 +- src/Init/Grind/Ordered/Linarith.lean | 4 ++-- src/Lean/DeclarationRange.lean | 6 +++++- src/Lean/Elab/LetRec.lean | 5 ++++- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 2 +- src/Std/Data/DHashMap/Internal/WF.lean | 6 +++--- src/Std/Sat/AIG/CNF.lean | 12 ++++++------ tests/pkg/module/Module/ImportedAll.lean | 6 +++++- 16 files changed, 63 insertions(+), 51 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 0a52edefce..025b884a1f 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -1285,7 +1285,7 @@ def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as decreasing_by simp_wf; decreasing_trivial_pre_omega loop 0 -theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} : +private theorem findIdx?_loop_eq_map_findFinIdx?_loop_val {xs : Array α} {p : α → Bool} {j} : findIdx?.loop p xs j = (findFinIdx?.loop p xs j).map (·.val) := by unfold findIdx?.loop unfold findFinIdx?.loop diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index e40c96e1e6..aca79c93ac 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -8,19 +8,20 @@ module prelude public import Init.Data.Nat.Lemmas public import Init.Data.List.Range -public import all Init.Data.List.Control public import Init.Data.List.Nat.TakeDrop public import Init.Data.List.Nat.Modify public import Init.Data.List.Nat.Basic public import Init.Data.List.Monadic public import Init.Data.List.OfFn -public import all Init.Data.Array.Bootstrap public import Init.Data.Array.Mem public import Init.Data.Array.DecidableEq public import Init.Data.Array.Lex.Basic public import Init.Data.Range.Lemmas public import Init.TacticsExtra public import Init.Data.List.ToArray +import all Init.Data.List.Control +import all Init.Data.Array.Basic +import all Init.Data.Array.Bootstrap public section @@ -2995,14 +2996,14 @@ theorem take_size {xs : Array α} : xs.take xs.size = xs := by /-! ### shrink -/ -@[simp] theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by +@[simp] private theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by induction n generalizing xs with | zero => simp [shrink.loop] | succ n ih => simp [shrink.loop, ih] omega -@[simp] theorem getElem_shrink_loop {xs : Array α} {n i : Nat} (h : i < (shrink.loop n xs).size) : +@[simp] private theorem getElem_shrink_loop {xs : Array α} {n i : Nat} (h : i < (shrink.loop n xs).size) : (shrink.loop n xs)[i] = xs[i]'(by simp at h; omega) := by induction n generalizing xs i with | zero => simp [shrink.loop] @@ -4278,7 +4279,7 @@ Examples: /-! ### Preliminaries about `ofFn` -/ -@[simp] theorem size_ofFn_go {n} {f : Fin n → α} {i acc h} : +@[simp] private theorem size_ofFn_go {n} {f : Fin n → α} {i acc h} : (ofFn.go f acc i h).size = acc.size + i := by induction i generalizing acc with | zero => simp [ofFn.go] @@ -4288,7 +4289,7 @@ Examples: @[simp] theorem size_ofFn {n : Nat} {f : Fin n → α} : (ofFn f).size = n := by simp [ofFn] -- Recall `ofFn.go f acc i h = acc ++ #[f (n - i), ..., f(n - 1)]` -theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁ : k < acc.size + i) : +private theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁ : k < acc.size + i) : (ofFn.go f acc i h)[k]'(by simpa using w₁) = if w₂ : k < acc.size then acc[k] else f ⟨n - i + k - acc.size, by omega⟩ := by induction i generalizing acc k with diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index fbd4904045..1b6b9722f1 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -107,14 +107,14 @@ Fin.foldrM n f xₙ = do subst w rfl -theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) : +private theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) : foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by rw [foldlM.loop, dif_pos h] -theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x := by +private theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x := by rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)] -theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) : +private theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) : foldlM.loop (n+1) f x i = f x ⟨i, h⟩ >>= (foldlM.loop n (fun x j => f x j.succ) . i) := by if h' : i < n then rw [foldlM_loop_lt _ _ h] @@ -170,15 +170,15 @@ theorem foldlM_add [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) : subst w rfl -theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) : +private theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) : foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by rw [foldrM.loop] -theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) : +private theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) : foldrM.loop n f ⟨i+1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, Nat.le_of_lt h⟩ := by rw [foldrM.loop] -theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) : +private theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) : foldrM.loop (n+1) f ⟨i+1, h⟩ x = foldrM.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x >>= f 0 := by induction i generalizing x with @@ -228,14 +228,14 @@ theorem foldrM_add [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) : subst w rfl -theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) : +private theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) : foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by rw [foldl.loop, dif_pos h] -theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by +private theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by rw [foldl.loop, dif_neg (Nat.lt_irrefl _)] -theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : i < n+1) : +private theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : i < n+1) : foldl.loop (n+1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i := by if h' : i < n then rw [foldl_loop_lt _ _ h] @@ -285,15 +285,15 @@ theorem foldlM_pure [Monad m] [LawfulMonad m] {n} {f : α → Fin n → α} : subst w rfl -theorem foldr_loop_zero (f : Fin n → α → α) (x) : +private theorem foldr_loop_zero (f : Fin n → α → α) (x) : foldr.loop n f 0 (Nat.zero_le _) x = x := by rw [foldr.loop] -theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) : +private theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) : foldr.loop n f (i+1) h x = foldr.loop n f i (Nat.le_of_lt h) (f ⟨i, h⟩ x) := by rw [foldr.loop] -theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) : +private theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) : foldr.loop (n+1) f (i+1) h x = f 0 (foldr.loop n (fun j => f j.succ) i (Nat.le_of_succ_le_succ h) x) := by induction i generalizing x with diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 70352acdac..ca064d7f9d 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -938,7 +938,7 @@ For the induction: (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by rw [reverseInduction, reverseInduction.go]; simp -@[simp] theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) → Sort _} {succ} +private theorem reverseInduction_castSucc_aux {n : Nat} {motive : Fin (n + 1) → Sort _} {succ} (i : Fin n) (j : Nat) (h) (h2 : i.1 < j) (zero : motive ⟨j, h⟩) : reverseInduction.go (motive := motive) succ i.castSucc j h (Nat.le_of_lt h2) zero = succ i (reverseInduction.go succ i.succ j h h2 zero) := by diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index 4183198f2a..3ce106e32a 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -367,7 +367,7 @@ def modifyTR (l : List α) (i : Nat) (f : α → α) : List α := go l i #[] whe | a :: l, 0, acc => acc.toListAppend (f a :: l) | a :: l, i+1, acc => go l i (acc.push a) -theorem modifyTR_go_eq : ∀ l i, modifyTR.go f l i acc = acc.toList ++ modify l i f +private theorem modifyTR_go_eq : ∀ l i, modifyTR.go f l i acc = acc.toList ++ modify l i f | [], i => by cases i <;> simp [modifyTR.go, modify] | a :: l, 0 => by simp [modifyTR.go, modify] | a :: l, i+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l] @@ -399,7 +399,7 @@ Examples: | _, [], acc => acc.toList | n+1, a :: l, acc => go n l (acc.push a) -theorem insertIdxTR_go_eq : ∀ i l, insertIdxTR.go a i l acc = acc.toList ++ insertIdx l i a +private theorem insertIdxTR_go_eq : ∀ i l, insertIdxTR.go a i l acc = acc.toList ++ insertIdx l i a | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx] | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l] diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean index 09601968d6..0533a079d9 100644 --- a/src/Init/Data/List/Sort/Impl.lean +++ b/src/Init/Data/List/Sort/Impl.lean @@ -57,7 +57,7 @@ where go : List α → List α → List α → List α else go (x :: xs) ys (y :: acc) -theorem mergeTR_go_eq : mergeTR.go le l₁ l₂ acc = acc.reverse ++ merge l₁ l₂ le := by +private theorem mergeTR_go_eq : mergeTR.go le l₁ l₂ acc = acc.reverse ++ merge l₁ l₂ le := by induction l₁ generalizing l₂ acc with | nil => simp [mergeTR.go, reverseAux_eq] | cons x l₁ ih₁ => @@ -84,7 +84,7 @@ def splitRevAt (n : Nat) (l : List α) : List α × List α := go l n [] where | x :: xs, n+1, acc => go xs n (x :: acc) | xs, _, acc => (acc, xs) -theorem splitRevAt_go (xs : List α) (i : Nat) (acc : List α) : +private theorem splitRevAt_go (xs : List α) (i : Nat) (acc : List α) : splitRevAt.go xs i acc = ((take i xs).reverse ++ acc, drop i xs) := by induction xs generalizing i acc with | nil => simp [splitRevAt.go] @@ -172,7 +172,7 @@ theorem splitRevInTwo_snd (l : { l : List α // l.length = n }) : (splitRevInTwo l).2 = ⟨(splitInTwo l).2.1, by simp; omega⟩ := by simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_snd] -theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR.run le l = mergeSort l.1 le +private theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR.run le l = mergeSort l.1 le | 0, ⟨[], _⟩ | 1, ⟨[a], _⟩ => by simp [mergeSortTR.run] | n+2, ⟨a :: b :: l, h⟩ => by @@ -189,7 +189,7 @@ theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by -- This mutual block is unfortunately quite slow to elaborate. set_option maxHeartbeats 400000 in mutual -theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR₂.run le l = mergeSort l.1 le +private theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR₂.run le l = mergeSort l.1 le | 0, ⟨[], _⟩ | 1, ⟨[a], _⟩ => by simp [mergeSortTR₂.run] | n+2, ⟨a :: b :: l, h⟩ => by @@ -201,7 +201,7 @@ theorem mergeSortTR₂_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l. rw [reverse_reverse] termination_by n => n -theorem mergeSortTR₂_run'_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → (w : l' = l.1.reverse) → mergeSortTR₂.run' le l = mergeSort l' le +private theorem mergeSortTR₂_run'_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → (w : l' = l.1.reverse) → mergeSortTR₂.run' le l = mergeSort l' le | 0, ⟨[], _⟩, w | 1, ⟨[a], _⟩, w => by simp_all [mergeSortTR₂.run'] | n+2, ⟨a :: b :: l, h⟩, w => by diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index a45da00f7c..843ce04bdb 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -222,11 +222,11 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) : congr ext1 (_|_) <;> simp [ih] -theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) +private theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) (i : Nat) (h) : findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by induction i generalizing l with - | zero => simp [Array.findSomeRevM?.find.eq_def] + | zero => simp [Array.findSomeRevM?.find] | succ i ih => rw [size_toArray] at h rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)] @@ -437,7 +437,7 @@ theorem zipWithMAux_toArray_zero {m : Type u → Type v} [Monad m] [LawfulMonad Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by simp [Array.zip, zipWith_toArray, zip] -theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (xs : Array γ) : +private theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (xs : Array γ) : zipWithAll.go f as.toArray bs.toArray i xs = xs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by unfold zipWithAll.go split <;> rename_i h @@ -489,7 +489,7 @@ theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → O apply ext' simp -theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) : +private theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) : takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by rw [takeWhile.go, takeWhile.go] simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, @@ -498,7 +498,7 @@ theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) : rw [takeWhile_go_succ] rfl -theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) : +private theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) : Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by induction l generalizing i r with | nil => simp [takeWhile.go] diff --git a/src/Init/Data/Nat/Fold.lean b/src/Init/Data/Nat/Fold.lean index de1c4478ac..240d5311de 100644 --- a/src/Init/Data/Nat/Fold.lean +++ b/src/Init/Data/Nat/Fold.lean @@ -128,7 +128,7 @@ theorem fold_congr {α : Type u} {n m : Nat} (w : n = m) subst m rfl -theorem foldTR_loop_congr {α : Type u} {n m : Nat} (w : n = m) +private theorem foldTR_loop_congr {α : Type u} {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → α → α) (j : Nat) (h : j ≤ n) (init : α) : foldTR.loop n f j h init = foldTR.loop m (fun i h => f i (by omega)) j (by omega) init := by subst m @@ -154,7 +154,7 @@ theorem any_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) : a subst m rfl -theorem anyTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) : +private theorem anyTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) : anyTR.loop n f j h = anyTR.loop m (fun i h => f i (by omega)) j (by omega) := by subst m rfl @@ -179,7 +179,7 @@ theorem all_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) : a subst m rfl -theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) : allTR.loop n f j h = allTR.loop m (fun i h => f i (by omega)) j (by omega) := by +private theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) : allTR.loop n f j h = allTR.loop m (fun i h => f i (by omega)) j (by omega) := by subst m rfl diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index 458cee79ad..d5907096ee 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -321,7 +321,7 @@ abbrev toArray_mkEmpty := @toArray_emptyWithCapacity xs.toArray.mapFinIdx (fun i a h => f i a (by simpa [xs.size_toArray] using h)) := rfl -theorem toArray_mapM_go [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} {i} (h) {acc} : +private theorem toArray_mapM_go [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} {i} (h) {acc} : toArray <$> mapM.go f xs i h acc = Array.mapM.map f xs.toArray i acc.toArray := by unfold mapM.go unfold Array.mapM.map diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean index 9836778a8f..5dfc9cfe00 100644 --- a/src/Init/Grind/Ordered/Linarith.lean +++ b/src/Init/Grind/Ordered/Linarith.lean @@ -80,7 +80,7 @@ local instance {α} [IntModule α] : Std.Associative (· + · : α → α → α local instance {α} [IntModule α] : Std.Commutative (· + · : α → α → α) where comm := AddCommMonoid.add_comm -theorem Poly.denote'_go_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) (r : α) : denote'.go ctx r p = p.denote ctx + r := by +private theorem Poly.denote'_go_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) (r : α) : denote'.go ctx r p = p.denote ctx + r := by induction r, p using denote'.go.induct ctx <;> simp [denote'.go, denote] next ih => rw [ih]; ac_rfl next ih => rw [ih]; ac_rfl @@ -214,7 +214,7 @@ theorem Poly.denote_combine {α} [IntModule α] (ctx : Context α) (p₁ p₂ : attribute [local simp] Poly.denote_combine -theorem Expr.denote_toPoly'_go {α} [IntModule α] {k p} (ctx : Context α) (e : Expr) +private theorem Expr.denote_toPoly'_go {α} [IntModule α] {k p} (ctx : Context α) (e : Expr) : (toPoly'.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by induction k, e using Expr.toPoly'.go.induct generalizing p <;> simp [toPoly'.go, denote, Poly.denote, *, zsmul_add] next => ac_rfl diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean index 7402fe0a39..45694f30cf 100644 --- a/src/Lean/DeclarationRange.lean +++ b/src/Lean/DeclarationRange.lean @@ -34,7 +34,11 @@ def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges : modifyEnv fun env => declRangeExt.insert env declName declRanges def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) := - return declRangeExt.find? (level := .server) (← getEnv) declName + -- In the case of private definitions imported via `import all`, looking in `.olean.server` is not + -- sufficient, so we look in the actual environment as well via `exported` (TODO: rethink + -- parameter naming). + return declRangeExt.find? (level := .exported) (← getEnv) declName <|> + declRangeExt.find? (level := .server) (← getEnv) declName def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do let env ← getEnv diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index fe70a98353..cc66f79441 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -115,12 +115,15 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array let toLift ← views.mapIdxM fun i view => do let value := values[i]! let termination := view.termination.rememberExtraParams view.binderIds.size value + let env ← getEnv pure { ref := view.ref fvarId := fvars[i]!.fvarId! attrs := view.attrs shortDeclName := view.shortDeclName - declName := view.declName + declName := + if env.isExporting || !env.header.isModule then view.declName + else mkPrivateName env view.declName parentName? := view.parentName? lctx localInstances diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 07eb40f422..2056ce5cf8 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -67,7 +67,7 @@ def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do withTraceNode `ReservedNameAction (pure m!"{exceptOptionEmoji ·} copyPrivateUnfoldTheorem running for {declName}") do let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix if let some mod ← findModuleOf? declName then - let unfoldName' := mkPrivateNameCore mod (.str declName unfoldThmSuffix) + let unfoldName' := mkPrivateNameCore mod (.str (privateToUserName declName) unfoldThmSuffix) if let some (.thmInfo info) := (← getEnv).find? unfoldName' then realizeConst declName name do addDecl <| Declaration.thmDecl { diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index de985cad3c..a9cee5789a 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -280,20 +280,20 @@ theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α refine (ih _).trans ?_ refine ((toListModel_reinsertAux _ _ _).append_left _).trans perm_middle -theorem expand.go_pos [Hashable α] {i : Nat} {source : Array (AssocList α β)} +private theorem expand.go_pos [Hashable α] {i : Nat} {source : Array (AssocList α β)} {target : { d : Array (AssocList α β) // 0 < d.size }} (h : i < source.size) : expand.go i source target = go (i + 1) (source.set i .nil) ((source[i]).foldl (reinsertAux hash) target) := by rw [expand.go] simp only [h, dite_true] -theorem expand.go_neg [Hashable α] {i : Nat} {source : Array (AssocList α β)} +private theorem expand.go_neg [Hashable α] {i : Nat} {source : Array (AssocList α β)} {target : { d : Array (AssocList α β) // 0 < d.size}} (h : ¬i < source.size) : expand.go i source target = target := by rw [expand.go] simp only [h, dite_false] -theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array (AssocList α β)) +private theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array (AssocList α β)) (target : {d : Array (AssocList α β) // 0 < d.size}) : expand.go 0 source target = (toListModel source).foldl (fun acc p => reinsertAux hash acc p.1 p.2) target := by suffices ∀ i, expand.go i source target = diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean index d38766a8da..11e15f329d 100644 --- a/src/Std/Sat/AIG/CNF.lean +++ b/src/Std/Sat/AIG/CNF.lean @@ -595,7 +595,7 @@ where The function we use to convert from CNF with explicit auxiliary variables to just `Nat` variables in `toCNF` is an injection. -/ -theorem toCNF.inj_is_injection {aig : AIG Nat} (a b : CNFVar aig) : +private theorem toCNF.inj_is_injection {aig : AIG Nat} (a b : CNFVar aig) : toCNF.inj a = toCNF.inj b → a = b := by intro h cases a with @@ -623,21 +623,21 @@ theorem toCNF.inj_is_injection {aig : AIG Nat} (a b : CNFVar aig) : /-- The node that we started CNF conversion at will always be marked as visited in the CNF cache. -/ -theorem toCNF.go_marks : +private theorem toCNF.go_marks : (go aig start h state).val.cache.marks[start]'(by have := (go aig start h state).val.cache.hmarks; omega) = true := (go aig start h state).property.trueAt /-- The CNF returned by `go` will always be SAT at `cnfSatAssignment`. -/ -theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) +private theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) (state : toCNF.State aig) : (go aig start h1 state).val.Sat (cnfSatAssignment aig assign1) := by have := (go aig start h1 state).val.inv assign1 rw [State.sat_iff] simp [this] -theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (inv) (h1) (assign1) : +private theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (inv) (h1) (assign1) : ⟦aig, ⟨start, inv, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1) := by have := go_sat aig start h1 assign1 (.empty aig) simp only [State.Sat, CNF.sat_def] at this @@ -646,7 +646,7 @@ theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (inv) (h1) (assign1) : /-- Connect SAT results about the CNF to SAT results about the AIG. -/ -theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) : +private theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) : ((⟦aig, ⟨start, inv, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?) → (⟦aig, ⟨start, inv, h1⟩, assign1⟧ = sat?) := by @@ -656,7 +656,7 @@ theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) : /-- Connect SAT results about the AIG to SAT results about the CNF. -/ -theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool} : +private theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool} : (⟦aig, ⟨start, inv, h1⟩, projectLeftAssign assign⟧ = false) → CNF.eval assign (([(.inr ⟨start, h1⟩, !inv)] :: (go aig start h1 (.empty aig)).val.cnf)) = false := by diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index 877e11cd30..c02e054980 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/tests/pkg/module/Module/ImportedAll.lean @@ -1,7 +1,7 @@ module -prelude public import all Module.Basic +import Lean.CoreM /-! `import all` should import private information, privately. -/ @@ -12,6 +12,10 @@ testSorry #guard_msgs in #print t +/-- info: true -/ +#guard_msgs in +#eval (return (← Lean.findDeclarationRanges? ``t).isSome : Lean.CoreM _) + /-- error: Type mismatch y