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

@@ -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

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

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

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
 
 

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