chore: rename ProofBelow to below.

src/Lean/Elab/Inductive.lean

@@ -9,7 +9,7 @@ import Lean.Util.CollectLevelParams
 import Lean.Util.Constructions
 import Lean.Meta.CollectFVars
 import Lean.Meta.SizeOf
-import Lean.Meta.ProofBelow
+import Lean.Meta.IndPredBelow
 import Lean.Elab.Command
 import Lean.Elab.DefView
 import Lean.Elab.DeclUtil
@@ -518,7 +518,7 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
   runTermElabM view0.declName fun vars => withRef ref do
     mkInductiveDecl vars views
     mkSizeOfInstances view0.declName
-    mkProofBelow view0.declName
+    Lean.Meta.IndPredBelow.mkBelow view0.declName
   applyDerivingHandlers views
 
 end Lean.Elab.Command

src/Lean/Meta.lean

@@ -29,7 +29,7 @@ import Lean.Meta.PPGoal
 import Lean.Meta.UnificationHint
 import Lean.Meta.Inductive
 import Lean.Meta.SizeOf
-import Lean.Meta.ProofBelow
+import Lean.Meta.IndPredBelow
 import Lean.Meta.Coe
 import Lean.Meta.SortLocalDecls
 import Lean.Meta.CollectFVars

src/Lean/Meta/IndPredBelow.lean

@@ -8,23 +8,21 @@ import Lean.Util.Constructions
 import Lean.Meta.Transform
 import Lean.Meta.Tactic
 
-namespace Lean.Meta
-
-namespace ProofBelow
+namespace Lean.Meta.IndPredBelow
 
 /--
-  The context used in the creation of the `ProofBelow` scheme for inductive predicates.
+  The context used in the creation of the `below` scheme for inductive predicates.
 -/  
 structure Context where
   motives : Array (Name × Expr)
   typeInfos : Array InductiveVal
-  proofBelowNames : Array Name
+  belowNames : Array Name
   headers : Array Expr
   numParams : Nat
 
 /--
   Collection of variables used to keep track of the positions of binders in the construction
-  of `ProofBelow` motives and constructors.
+  of `below` motives and constructors.
 -/
 structure Variables where
   target : Array Expr
@@ -57,7 +55,7 @@ def mkContext (declName : Name) : MetaM Context := do
     typeInfos := typeInfos
     numParams := indVal.numParams
     headers := ←headers
-    proofBelowNames := ←indVal.all.toArray.mapM (·.appendAfter "ProofBelow") }
+    belowNames := ←indVal.all.toArray.map (· ++ `below) }
 where 
   motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name := 
     if motiveTypes.size > 1 
@@ -89,7 +87,7 @@ where
     
 partial def mkCtorType 
     (ctx : Context) 
-    (proofBelowIdx : Nat) 
+    (belowIdx : Nat) 
     (originalCtor : ConstructorVal) : MetaM Expr := 
   forallTelescope originalCtor.type fun xs t => addHeaderVars 
     { innerType := t
@@ -101,7 +99,7 @@ partial def mkCtorType
 where
   addHeaderVars (vars : Variables) := do
     let headersWithNames ← ctx.headers.mapIdxM fun idx header =>
-      (ctx.proofBelowNames[idx], fun _ => pure header)
+      (ctx.belowNames[idx], fun _ => pure header)
 
     withLocalDeclsD headersWithNames fun xs =>
       addMotives { vars with indVal := xs } 
@@ -118,7 +116,7 @@ where
       let binder := vars.args[i]
       let binderType ←inferType binder
       if ←checkCount binderType then
-        mkProofBelowBinder vars binder binderType fun indValIdx x =>
+        mkBelowBinder vars binder binderType fun indValIdx x =>
           mkMotiveBinder vars indValIdx binder binderType fun y =>
             modifyBinders { vars with target := vars.target ++ #[binder, x, y]} i.succ
       else modifyBinders { vars with target := vars.target.push binder } i.succ
@@ -130,7 +128,7 @@ where
         mkAppN 
           (mkConst originalCtor.name $ ctx.typeInfos[0].levelParams.map mkLevelParam)
           (vars.params ++ vars.args)
-      let innerType := mkAppN vars.indVal[proofBelowIdx] $
+      let innerType := mkAppN vars.indVal[belowIdx] $
         vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
       let x ← mkForallFVars vars.target innerType 
       replaceTempVars vars x
@@ -139,7 +137,7 @@ where
     let levelParams := 
       ctx.typeInfos[0].levelParams.map mkLevelParam
 
-    ctor.replaceFVars vars.indVal $ ctx.proofBelowNames.map fun indVal =>
+    ctor.replaceFVars vars.indVal $ ctx.belowNames.map fun indVal =>
       mkConst indVal levelParams
   
   checkCount (domain : Expr) : MetaM Bool := do
@@ -156,7 +154,7 @@ where
     
     return cnt == 1
   
-  mkProofBelowBinder 
+  mkBelowBinder 
       (vars : Variables) 
       (binder : Expr) 
       (domain : Expr) 
@@ -200,7 +198,7 @@ where
 
 def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor := do
   let ctorInfo ← getConstInfoCtor ctor
-  let name := ctor.updatePrefix ctx.proofBelowNames[i]
+  let name := ctor.updatePrefix ctx.belowNames[i]
   let type ← mkCtorType ctx i ctorInfo
   return { 
     name := name
@@ -211,11 +209,11 @@ def mkInductiveType
     (i : Fin ctx.typeInfos.size) 
     (indVal : InductiveVal) : MetaM InductiveType := do
   return {
-    name := ctx.proofBelowNames[i]
+    name := ctx.belowNames[i]
     type := ctx.headers[i]
     ctors := ←indVal.ctors.mapM (mkConstructor ctx i) }
 
-def mkProofBelowDecl (ctx : Context) : MetaM Declaration := do
+def mkBelowDecl (ctx : Context) : MetaM Declaration := do
   let lparams := ctx.typeInfos[0].levelParams
   Declaration.inductDecl 
     lparams 
@@ -254,7 +252,7 @@ where
     let motives ← ctx.motives.mapIdxM fun idx (_, motive) => do
       let motive ← instantiateForall motive params
       forallTelescope motive fun xs _ => do
-      mkLambdaFVars xs $ mkAppN (mkConst ctx.proofBelowNames[idx] levelParams) $ (params ++ motives ++ xs)
+      mkLambdaFVars xs $ mkAppN (mkConst ctx.belowNames[idx] levelParams) $ (params ++ motives ++ xs)
     withMVarContext m do
     let recursorInfo ← getConstInfo $ mkRecName indVal.name
     let recLevels := 
@@ -267,11 +265,11 @@ where
   applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
     let mss ← ms.toArray.mapIdxM fun idx m => do
       let m ← introNPRec m 
-      (←getMVarType m).withApp fun proofBelow args =>
+      (←getMVarType m).withApp fun below args =>
       args.back.withApp fun ctor args =>
-      let ctor := ctor.constName!.updatePrefix proofBelow.constName!
+      let ctor := ctor.constName!.updatePrefix below.constName!
       withMVarContext m do
-      let ctor := mkConst ctor proofBelow.constLevels!
+      let ctor := mkConst ctor below.constLevels!
       apply m ctor 
     return mss.foldr List.append []
 
@@ -334,32 +332,31 @@ where
         let args := params ++ motives ++ ys
         let premise :=
           mkAppN 
-            (mkConst ctx.proofBelowNames[idx.val] levels) args
+            (mkConst ctx.belowNames[idx.val] levels) args
         let conclusion :=
           mkAppN motives[idx] ys
         mkForallFVars ys (←mkArrow premise conclusion)
     (←name, mkDomain)
 
-end ProofBelow
 
-def mkProofBelow (declName : Name) : MetaM Unit := do
+def mkBelow (declName : Name) : MetaM Unit := do
   if (←isInductivePredicate declName) then
     let x ← getConstInfoInduct declName
     if x.isRec then
-      let ctx ← ProofBelow.mkContext declName
-      let decl ← ProofBelow.mkProofBelowDecl ctx
+      let ctx ← IndPredBelow.mkContext declName
+      let decl ← IndPredBelow.mkBelowDecl ctx
       addDecl decl
-      trace[Meta.ProofBelow] "added {ctx.proofBelowNames}"
-      ctx.proofBelowNames.forM Lean.mkCasesOn
+      trace[Meta.IndPredBelow] "added {ctx.belowNames}"
+      ctx.belowNames.forM Lean.mkCasesOn
       for i in [:ctx.typeInfos.size] do
         try
-          let decl ← ProofBelow.mkBrecOnDecl ctx i
+          let decl ← IndPredBelow.mkBrecOnDecl ctx i
           addDecl decl
-        catch e => trace[Meta.ProofBelow] "failed to prove brecOn for {ctx.proofBelowNames[i]}\n{e.toMessageData}"
-    else trace[Meta.ProofBelow] "Not recursive"
-  else trace[Meta.ProofBelow] "Not inductive predicate"
+        catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]}\n{e.toMessageData}"
+    else trace[Meta.IndPredBelow] "Not recursive"
+  else trace[Meta.IndPredBelow] "Not inductive predicate"
 
 builtin_initialize
-  registerTraceClass `Meta.ProofBelow
+  registerTraceClass `Meta.IndPredBelow
 
-end Lean.Meta
+end Lean.Meta.IndPredBelow

tests/lean/run/inductive_pred.lean

@@ -7,7 +7,7 @@ def typeOf {α : Sort u} (a : α) := α
 
 theorem LE_brecOn : typeOf @LE.brecOn = 
 ∀ {motive : (a a_1 : Nat) → LE a a_1 → Prop} {a a_1 : Nat} (x : LE a a_1),
-  (∀ (a a_2 : Nat) (x : LE a a_2), @LEProofBelow motive a a_2 x → motive a a_2 x) → motive a a_1 x := rfl
+  (∀ (a a_2 : Nat) (x : LE a a_2), @LE.below motive a a_2 x → motive a a_2 x) → motive a a_1 x := rfl
 
 theorem LE.trans : LE m n → LE n o → LE m o := by
   intro h1 h2
@@ -24,7 +24,7 @@ inductive Even : Nat → Prop
   | ss   : Even n → Even n.succ.succ
 
 theorem Even_brecOn : typeOf @Even.brecOn = ∀ {motive : (a : Nat) → Even a → Prop} {a : Nat} (x : Even a),
-  (∀ (a : Nat) (x : Even a), @EvenProofBelow motive a x → motive a x) → motive a x := rfl
+  (∀ (a : Nat) (x : Even a), @Even.below motive a x → motive a x) → motive a x := rfl
 
 theorem Even.add : Even n → Even m → Even (n+m) := by
   intro h1 h2
@@ -44,7 +44,7 @@ inductive Power2 : Nat → Prop
   | ind  : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
   
 theorem Power2_brecOn : typeOf @Power2.brecOn = ∀ {motive : (a : Nat) → Power2 a → Prop} {a : Nat} (x : Power2 a),
-  (∀ (a : Nat) (x : Power2 a), @Power2ProofBelow motive a x → motive a x) → motive a x := rfl
+  (∀ (a : Nat) (x : Power2 a), @Power2.below motive a x → motive a x) → motive a x := rfl
 
 theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
   intro h1 h2
@@ -82,11 +82,11 @@ def deterministic {X : Type} (R : X → X → Prop) :=
 theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ => 
   @step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ => 
     match hy₁, hy₂ with
-    | stepProofBelow.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl
-    | stepProofBelow.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw ←ih t₁'; assumption
-    | stepProofBelow.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁
-    | stepProofBelow.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw ←ih t₂; assumption
-    | stepProofBelow.ST_Plus2 _ _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁
+    | step.below.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl
+    | step.below.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw ←ih t₁'; assumption
+    | step.below.ST_Plus1 _ _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁
+    | step.below.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw ←ih t₂; assumption
+    | step.below.ST_Plus2 _ _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁
     ) y₂ hy₂ 
 
 section NestedRecursion
@@ -111,9 +111,9 @@ axiom FS {n : Nat} : P n → P (f (f n))
 theorem foo' : ∀ {n}, is_nat n → P n := fun h => 
   @is_nat.brecOn (fun n hn => P n) _ h fun n h ih => 
   match ih with
-  | is_natProofBelow.Z => F0 
-  | is_natProofBelow.S _ is_natProofBelow.Z _ => F1
-  | is_natProofBelow.S _ (is_natProofBelow.S a b hx) h₂ => FS hx
+  | is_nat.below.Z => F0 
+  | is_nat.below.S _ is_nat.below.Z _ => F1
+  | is_nat.below.S _ (is_nat.below.S a b hx) h₂ => FS hx
 
 end NestedRecursion
 

tests/lean/run/reflectiveIndPred.lean

@@ -8,5 +8,5 @@ inductive Pos : Expr → Prop
   | add  : Pos e₁ → Pos e₂ → Pos (Expr.add e₁ e₂)
   | fn   : ((n : Nat) → Pos (f n)) → Pos (Expr.fn f)
 
-#print PosProofBelow
+#print Pos.below
 #print Pos.brecOn