From 325fab1c1db791101a71610160d1359dced5719e Mon Sep 17 00:00:00 2001
From: Arthur Adjedj <aarthuur01@gmail.com>
Date: Thu, 21 Sep 2023 06:24:37 +0200
Subject: [PATCH] fix: don't try to generate `below` for nested predicates.
 (#2390)

* fix: don't try to generate `below` for nested predicates.

* doc : document test #2389

* doc : document `mkBelow`

* test: extend `2389.lean`

* style: fix comments in `IndPredBelow.lean` and `2389.lean`
---
 src/Lean/Meta/IndPredBelow.lean       |  7 ++++--
 tests/lean/run/2389.lean              | 35 +++++++++++++++++++++++++++
 tests/lean/run/2389.lean.expected.out |  1 +
 3 files changed, 41 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/2389.lean
 create mode 100644 tests/lean/run/2389.lean.expected.out

diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index 3145f29d311c..7118a320582c 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -571,10 +571,13 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
     else pure none
   | _, _ => pure none
 
+/-- Generates the auxiliary lemmas `below` and `brecOn` for a recursive inductive predicate.
+The current generator doesn't support nested predicates, but pattern-matching on them still works
+thanks to well-founded recursion. -/
 def mkBelow (declName : Name) : MetaM Unit := do
   if (← isInductivePredicate declName) then
     let x ← getConstInfoInduct declName
-    if x.isRec then
+    if x.isRec && !x.isNested then
       let ctx ← IndPredBelow.mkContext declName
       let decl ← IndPredBelow.mkBelowDecl ctx
       addDecl decl
@@ -585,7 +588,7 @@ def mkBelow (declName : Name) : MetaM Unit := do
           let decl ← IndPredBelow.mkBrecOnDecl ctx i
           addDecl decl
         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] "Nested or not recursive"
   else trace[Meta.IndPredBelow] "Not inductive predicate"
 
 builtin_initialize
diff --git a/tests/lean/run/2389.lean b/tests/lean/run/2389.lean
new file mode 100644
index 000000000000..6923e6c5e612
--- /dev/null
+++ b/tests/lean/run/2389.lean
@@ -0,0 +1,35 @@
+/-!
+# Verify that nested predicates don't trigger the generation of `below` lemmas
+Since the case of nested predicates is not currently handled by `mkBelow` (in `src/Lean/Meta/IndPredBelow.lean`),
+trying to generate `OnlyZeros.below` triggers an error upon defining the inductive type.
+-/
+
+inductive Forall (P : α → Prop) : List α → Prop
+  | nil : Forall P []
+  | cons : {x : α} → P x → Forall P l → Forall P (x::l)
+
+inductive Tree : Type :=
+  | leaf : Nat → Tree
+  | node : List Tree → Tree
+
+set_option trace.Meta.IndPredBelow true in
+
+/-- Despite not having `.below` and `.brecOn`,
+the type is still usable thanks to well-founded recursion. -/
+inductive OnlyZeros : Tree → Prop :=
+  | leaf : OnlyZeros (.leaf 0)
+  | node (l : List Tree): Forall OnlyZeros l → OnlyZeros (.node l)
+
+/-- Equivalent definition of `OnlyZeros`, defined by a function instead of an inductive type. -/
+def onlyZeros : Tree → Prop
+  | .leaf n => n = 0
+  | .node [] => True
+  | .node (x::s) => onlyZeros x ∧ onlyZeros (.node s)
+
+/-- Pattern-matching on `OnlyZeros` works despite `below` and `brecOn` not being generated. -/
+def toFixPoint : OnlyZeros t → onlyZeros t
+  | .leaf => rfl
+  | .node [] _ => True.intro
+  | .node (x::s) (.cons h p) => by
+    rw [onlyZeros] -- necessary because `onlyZeros` isn't structurally recursive
+    exact And.intro (toFixPoint h) (toFixPoint (.node s p))
diff --git a/tests/lean/run/2389.lean.expected.out b/tests/lean/run/2389.lean.expected.out
new file mode 100644
index 000000000000..635fa04e07e2
--- /dev/null
+++ b/tests/lean/run/2389.lean.expected.out
@@ -0,0 +1 @@
+[Meta.IndPredBelow] Nested or not recursive