fix: module system: remove WellFounded-specific hacks (#9143)

This PR removes a rather ugly hack in the module system, exposing the
bodies of theorems whose type mention `WellFounded`.

The original motivation was that reducing well-founded definitions (e.g.
in `by rfl`) requires reducing proofs, so they need to be available.

But reducing proofs is generally fraught with peril, and we have been
nudging our users away from using it for a while, e.g. in #5182. Since
the module system is opt-in and users will gradually migrate to it, it
may be reasonable to expect them to avoid reducing well-founded
recursion in the process

This way we don't need hacks like this (which, without evidence, I
believe would be incomplete anyways) and we get the nice guarantee that
within the module system, theorems bodies are always private.

src/Init/Data/Array/Find.lean

@@ -387,7 +387,7 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 /-! ### findIdx -/
 
 @[grind =]
-theorem findIdx_empty : findIdx p #[] = 0 := rfl
+theorem findIdx_empty : findIdx p #[] = 0 := by simp
 
 @[grind =]
 theorem findIdx_singleton {a : α} {p : α → Bool} :

src/Init/Data/Fin/Fold.lean

@@ -185,7 +185,9 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
   | zero =>
     rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
     conv => rhs; rw [←bind_pure (f 0 x)]
-    rfl
+    congr
+    funext
+    rw [foldrM_loop_zero]
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..

src/Init/Data/Vector/Lemmas.lean

@@ -1213,7 +1213,7 @@ theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
 instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff contains_iff
 
-@[grind] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := rfl
+@[grind] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := by simp
 
 @[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
     as.contains a = decide (a ∈ as) := by
@@ -2975,7 +2975,7 @@ variable [BEq α]
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by rfl
+@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by simp
 
 @[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
   simp

src/Init/WF.lean

@@ -44,8 +44,7 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
--- `def` for `WellFounded.fix`
-def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
+theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
   h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
@@ -78,8 +77,8 @@ class WellFoundedRelation (α : Sort u) where
   wf  : WellFounded rel
 
 namespace WellFounded
--- `def` for `WellFounded.fix`
-def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
+
+theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
   wf.rec (fun p => p) a
 
 section
@@ -159,15 +158,13 @@ end Subrelation
 namespace InvImage
 variable {α : Sort u} {β : Sort v} {r : β → β → Prop}
 
-def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x :=
+theorem accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x :=
   Acc.recOn ac fun _ _ ih => fun _ e => Acc.intro _ (fun y lt => ih (f y) (e ▸ lt) y rfl)
 
--- `def` for `WellFounded.fix`
-def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
+theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
   accAux f ac a rfl
 
--- `def` for `WellFounded.fix`
-def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
+theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 

src/Lean/AddDecl.lean

@@ -64,12 +64,6 @@ Checks whether the declaration was originally declared as a theorem; see also
 def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
   getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
 
-private def looksLikeRelevantTheoremProofType (type : Expr) : Bool :=
-  if let .forallE _ _ type _ := type then
-    looksLikeRelevantTheoremProofType type
-  else
-    type.isAppOfArity ``WellFounded 2
-
 /-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
 declarations with `sorryAx` generate the "declaration uses 'sorry'" warning. -/
 register_builtin_option warn.sorry : Bool := {
@@ -89,10 +83,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   let mut exportedInfo? := none
   let (name, info, kind) ← match decl with
     | .thmDecl thm =>
-      let exportProof := !(← getEnv).header.isModule ||
-        -- TODO: this is horrible...
-        looksLikeRelevantTheoremProofType thm.type
-      if !exportProof then
+      if (← getEnv).header.isModule then
         exportedInfo? := some <| .axiomInfo { thm with isUnsafe := false }
       pure (thm.name, .thmInfo thm, .thm)
     | .defnDecl defn | .mutualDefnDecl [defn] =>