From 97aca690d0178103b1c82e265657f335ca922bbb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hagb=20=28Junyu=20Guo=20=E9=83=AD=E4=BF=8A=E4=BD=99=29?=
 <hagbgreen@yahoo.com>
Date: Tue, 8 Jul 2025 22:42:11 +0800
Subject: [PATCH] fix: walk through types of axioms in `collectAxioms` (#8842)

This PR fixes the bug that `collectAxioms` didn't collect axioms
referenced by other axioms. One of the results of this bug is that
axioms collected from a theorem proved by `native_decide` may not
include `Lean.trustCompiler`.

Closes #8840.
---
 src/Lean/Util/CollectAxioms.lean       |  4 ++-
 tests/lean/run/bv_axiom_check.lean     |  2 +-
 tests/lean/run/collectAxioms.lean      | 36 ++++++++++++++++++++++++++
 tests/lean/run/decideNative.lean       |  2 +-
 tests/lean/run/nativeReflBackdoor.lean |  2 +-
 5 files changed, 42 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/collectAxioms.lean

diff --git a/src/Lean/Util/CollectAxioms.lean b/src/Lean/Util/CollectAxioms.lean
index 235e6b1453..163d5bdaa0 100644
--- a/src/Lean/Util/CollectAxioms.lean
+++ b/src/Lean/Util/CollectAxioms.lean
@@ -26,7 +26,9 @@ partial def collect (c : Name) : M Unit := do
     -- We should take the constant from the kernel env, which may differ from the one in the elab
     -- env in case of (async) errors.
     match env.checked.get.find? c with
-    | some (ConstantInfo.axiomInfo _)  => modify fun s => { s with axioms := s.axioms.push c }
+    | some (ConstantInfo.axiomInfo v)  =>
+        modify fun s => { s with axioms := (s.axioms.push c) }
+        collectExpr v.type
     | some (ConstantInfo.defnInfo v)   => collectExpr v.type *> collectExpr v.value
     | some (ConstantInfo.thmInfo v)    => collectExpr v.type *> collectExpr v.value
     | some (ConstantInfo.opaqueInfo v) => collectExpr v.type *> collectExpr v.value
diff --git a/tests/lean/run/bv_axiom_check.lean b/tests/lean/run/bv_axiom_check.lean
index 7e17946821..ae5c09417d 100644
--- a/tests/lean/run/bv_axiom_check.lean
+++ b/tests/lean/run/bv_axiom_check.lean
@@ -5,7 +5,7 @@ open BitVec
 theorem bv_axiomCheck (x y z : BitVec 1) : x < y → y < z → x < z := by bv_decide
 
 /--
-info: 'bv_axiomCheck' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]
+info: 'bv_axiomCheck' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]
 -/
 #guard_msgs in
 #print axioms bv_axiomCheck
diff --git a/tests/lean/run/collectAxioms.lean b/tests/lean/run/collectAxioms.lean
new file mode 100644
index 0000000000..aaea735fd4
--- /dev/null
+++ b/tests/lean/run/collectAxioms.lean
@@ -0,0 +1,36 @@
+import Lean
+
+axiom A0 : Type
+axiom A1 : Type
+
+class C where
+  a0 : A0
+
+axiom A2 (_ : A1) : C
+
+/--
+info: #[`A2, `A1, `A0]
+-/
+#guard_msgs in
+#eval Lean.collectAxioms ``A2
+
+/--
+info: 'A2' depends on axioms: [A0, A1, A2]
+-/
+#guard_msgs in
+#print axioms A2
+
+theorem one_add_one : 1 + 1 = 2 := by
+  native_decide
+
+/--
+info: #[`Lean.ofReduceBool, `Lean.trustCompiler]
+-/
+#guard_msgs in
+#eval Lean.collectAxioms ``one_add_one
+
+/--
+info: 'one_add_one' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler]
+-/
+#guard_msgs in
+#print axioms one_add_one
diff --git a/tests/lean/run/decideNative.lean b/tests/lean/run/decideNative.lean
index a9d89f45e2..91f6d8b8c5 100644
--- a/tests/lean/run/decideNative.lean
+++ b/tests/lean/run/decideNative.lean
@@ -7,7 +7,7 @@ import Lean
 Simplest example.
 -/
 theorem ex1 : True := by native_decide
-/-- info: 'ex1' depends on axioms: [Lean.ofReduceBool] -/
+/-- info: 'ex1' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler] -/
 #guard_msgs in #print axioms ex1
 
 
diff --git a/tests/lean/run/nativeReflBackdoor.lean b/tests/lean/run/nativeReflBackdoor.lean
index 90c83f4a83..636dc49c29 100644
--- a/tests/lean/run/nativeReflBackdoor.lean
+++ b/tests/lean/run/nativeReflBackdoor.lean
@@ -35,6 +35,6 @@ We managed to prove `False` using the unsound annotation `implemented_by` above.
 theorem unsound : False :=
 Bool.noConfusion trueEqFalse
 
-/-- info: 'unsound' depends on axioms: [Lean.ofReduceBool] -/
+/-- info: 'unsound' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler] -/
 #guard_msgs in
 #print axioms unsound