Add files using upload-large-folder tool

.gitattributes

@@ -4493,3 +4493,13 @@ backend/core/leanprover--lean4---v4.22.0/lib/lean/Std/Internal/Parsec/ByteArray.
 backend/core/leanprover--lean4---v4.22.0/lib/lean/Std/Data/TreeSet/Basic.olean filter=lfs diff=lfs merge=lfs -text
 backend/core/leanprover--lean4---v4.22.0/lib/lean/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.olean filter=lfs diff=lfs merge=lfs -text
 external/alphageometry/.venv-ag/Lib/site-packages/scipy/special/tests/data/local.npz filter=lfs diff=lfs merge=lfs -text
+external/alphageometry/.venv-ag/Lib/site-packages/scipy/linalg/tests/data/carex_18_data.npz filter=lfs diff=lfs merge=lfs -text
+hfenv/Scripts/python.exe filter=lfs diff=lfs merge=lfs -text
+hfenv/Scripts/pythonw.exe filter=lfs diff=lfs merge=lfs -text
+MyProject/.lake/build/bin/myproject.exe filter=lfs diff=lfs merge=lfs -text
+external/alphageometry/.venv-ag/Lib/site-packages/scipy/stats/tests/data/levy_stable/stable-Z1-pdf-sample-data.npy filter=lfs diff=lfs merge=lfs -text
+external/alphageometry/.venv-ag/Lib/site-packages/numpy/random/lib/npyrandom.lib filter=lfs diff=lfs merge=lfs -text
+external/alphageometry/.venv-ag/Lib/site-packages/matplotlib/mpl-data/fonts/ttf/DejaVuSans-BoldOblique.ttf filter=lfs diff=lfs merge=lfs -text
+external/alphageometry/.venv-ag/Lib/site-packages/matplotlib/mpl-data/fonts/ttf/DejaVuSans.ttf filter=lfs diff=lfs merge=lfs -text
+external/alphageometry/.venv-ag/Lib/site-packages/matplotlib/mpl-data/fonts/ttf/DejaVuSansMono-Bold.ttf filter=lfs diff=lfs merge=lfs -text
+external/alphageometry/.venv-ag/Lib/site-packages/matplotlib/mpl-data/fonts/ttf/DejaVuSansMono-BoldOblique.ttf filter=lfs diff=lfs merge=lfs -text

MyProject/.lake/build/bin/myproject.exe

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:600f5a03635f9f4e2411d2073f2a9b082a0894af45fbfd6eb440074bba0eab51
+size 8729600

MyProject/.lake/build/ir/Main.c.o.noexport.hash

@@ -0,0 +1 @@
+6845279270828235154

MyProject/.lake/build/ir/Main.c.o.noexport.trace

@@ -0,0 +1,17 @@
+{"synthetic": false,
+ "outputs": "6845279270828235154",
+ "log":
+ [{"message":
+   ".> c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\bin\\clang.exe -c -o C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\Main.c.o.noexport C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\Main.c -I c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0 -nostdinc -isystem c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0/include/clang -O3 -DNDEBUG",
+   "level": "trace"}],
+ "inputs":
+ [["Main:c",
+   [["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\Main.c",
+     "2812497700029973126"],
+    ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+     "8739116525927611134"]]],
+  ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+   "8739116525927611134"],
+  ["traceArgs: #[-O3, -DNDEBUG]", "7817036117363455818"],
+  ["x86_64-w64-windows-gnu", "3894966287860160785"]],
+ "depHash": "13981209688990805943"}

MyProject/.lake/build/ir/Main.setup.json

@@ -0,0 +1,6 @@
+{"plugins": [],
+ "options": {},
+ "name": "Main",
+ "isModule": false,
+ "importArts": {},
+ "dynlibs": []}

MyProject/.lake/build/ir/MyProject.c

@@ -0,0 +1,33 @@
+// Lean compiler output
+// Module: MyProject
+// Imports: Init MyProject.Basic
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* initialize_Init(uint8_t builtin, lean_object*);
+lean_object* initialize_MyProject_Basic(uint8_t builtin, lean_object*);
+static bool _G_initialized = false;
+LEAN_EXPORT lean_object* initialize_MyProject(uint8_t builtin, lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = initialize_Init(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_MyProject_Basic(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif

MyProject/.lake/build/ir/MyProject.c.hash

@@ -0,0 +1 @@
+10253638930955786439

MyProject/.lake/build/ir/MyProject.c.o.noexport.hash

@@ -0,0 +1 @@
+1337897845214833469

MyProject/.lake/build/ir/MyProject.c.o.noexport.trace

@@ -0,0 +1,17 @@
+{"synthetic": false,
+ "outputs": "1337897845214833469",
+ "log":
+ [{"message":
+   ".> c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\bin\\clang.exe -c -o C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject.c.o.noexport C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject.c -I c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0 -nostdinc -isystem c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0/include/clang -O3 -DNDEBUG",
+   "level": "trace"}],
+ "inputs":
+ [["MyProject:c",
+   [["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject.c",
+     "10253638930955786439"],
+    ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+     "8739116525927611134"]]],
+  ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+   "8739116525927611134"],
+  ["traceArgs: #[-O3, -DNDEBUG]", "7817036117363455818"],
+  ["x86_64-w64-windows-gnu", "3894966287860160785"]],
+ "depHash": "6185683997854951944"}

MyProject/.lake/build/ir/MyProject.setup.json

@@ -0,0 +1,6 @@
+{"plugins": [],
+ "options": {},
+ "name": "MyProject",
+ "isModule": false,
+ "importArts": {},
+ "dynlibs": []}

MyProject/.lake/build/ir/MyProject/Basic.c

@@ -0,0 +1,51 @@
+// Lean compiler output
+// Module: MyProject.Basic
+// Imports: Init
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+LEAN_EXPORT lean_object* l_hello;
+static lean_object* l_hello___closed__0;
+static lean_object* _init_l_hello___closed__0() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_unchecked("world", 5, 5);
+return x_1;
+}
+}
+static lean_object* _init_l_hello() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_hello___closed__0;
+return x_1;
+}
+}
+lean_object* initialize_Init(uint8_t builtin, lean_object*);
+static bool _G_initialized = false;
+LEAN_EXPORT lean_object* initialize_MyProject_Basic(uint8_t builtin, lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = initialize_Init(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l_hello___closed__0 = _init_l_hello___closed__0();
+lean_mark_persistent(l_hello___closed__0);
+l_hello = _init_l_hello();
+lean_mark_persistent(l_hello);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif

MyProject/.lake/build/ir/MyProject/Basic.c.hash

@@ -0,0 +1 @@
+6640969564603399067

MyProject/.lake/build/ir/MyProject/Basic.c.o.noexport.hash

@@ -0,0 +1 @@
+535684011917836214

MyProject/.lake/build/ir/MyProject/Basic.c.o.noexport.trace

@@ -0,0 +1,17 @@
+{"synthetic": false,
+ "outputs": "535684011917836214",
+ "log":
+ [{"message":
+   ".> c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\bin\\clang.exe -c -o C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject\\Basic.c.o.noexport C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject\\Basic.c -I c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\include -fstack-clash-protection -fwrapv -Wno-unused-command-line-argument --sysroot c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0 -nostdinc -isystem c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0/include/clang -O3 -DNDEBUG",
+   "level": "trace"}],
+ "inputs":
+ [["MyProject.Basic:c",
+   [["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject\\Basic.c",
+     "6640969564603399067"],
+    ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+     "8739116525927611134"]]],
+  ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+   "8739116525927611134"],
+  ["traceArgs: #[-O3, -DNDEBUG]", "7817036117363455818"],
+  ["x86_64-w64-windows-gnu", "3894966287860160785"]],
+ "depHash": "16832078366333324937"}

MyProject/.lake/build/ir/MyProject/Basic.setup.json

@@ -0,0 +1,6 @@
+{"plugins": [],
+ "options": {},
+ "name": "MyProject.Basic",
+ "isModule": false,
+ "importArts": {},
+ "dynlibs": []}

MyProject/.lake/build/lib/lean/Main.ilean

@@ -0,0 +1 @@
+{"version":4,"references":{"{\"c\":{\"n\":\"main\",\"m\":\"Main\"}}":{"usages":[],"definition":[2,4,2,8]},"{\"c\":{\"n\":\"hello\",\"m\":\"MyProject.Basic\"}}":{"usages":[[3,24,3,29,"main",2,0,3,32,2,4,2,8]],"definition":null},"{\"c\":{\"n\":\"Unit\",\"m\":\"Init.Prelude\"}}":{"usages":[[2,14,2,18,"main",2,0,3,32,2,4,2,8]],"definition":null},"{\"c\":{\"n\":\"IO.println\",\"m\":\"Init.System.IO\"}}":{"usages":[[3,2,3,12,"main",2,0,3,32,2,4,2,8]],"definition":null},"{\"c\":{\"n\":\"IO\",\"m\":\"Init.System.IO\"}}":{"usages":[[2,11,2,13,"main",2,0,3,32,2,4,2,8]],"definition":null}},"module":"Main","directImports":[["MyProject",false,false,false]]}

MyProject/.lake/build/lib/lean/Main.ilean.hash

@@ -0,0 +1 @@
+7502200330849018073

MyProject/.lake/build/lib/lean/Main.olean.hash

@@ -0,0 +1 @@
+16614596214648291283

MyProject/.lake/build/lib/lean/Main.trace

@@ -0,0 +1,30 @@
+{"synthetic": false,
+ "outputs":
+ {"o": ["16614596214648291283"],
+  "i": "7502200330849018073",
+  "c": "2812497700029973126"},
+ "log":
+ [{"message":
+   ".> LEAN_PATH=C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\bin\\lean.exe C:\\Users\\marooc\\AXIOVORA X\\MyProject\\Main.lean -o C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\Main.olean -i C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\Main.ilean -c C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\Main.c --setup C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\Main.setup.json --json",
+   "level": "trace"}],
+ "inputs":
+ [["Main:deps",
+   [["deps",
+     [["MyProject/myproject:extraDep", [["@MyProject:extraDep", "1723"]]],
+      ["import oleans",
+       [["MyProject:olean",
+         [["MyProject:deps", "8480390225429029242"],
+          ["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\MyProject.olean",
+           "2826512291163496019"]]]]]]],
+    ["libs",
+     [["import dynlibs", "1723"],
+      ["package external libraries", "1723"],
+      ["module dynlibs", "1723"],
+      ["module plugins", "1723"]]]]],
+  ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+   "8739116525927611134"],
+  ["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\Main.lean",
+   "16909483731186443744"],
+  ["options", "1723"],
+  ["Module.leanArgs: #[]", "1723"]],
+ "depHash": "11749844063866404310"}

MyProject/.lake/build/lib/lean/MyProject.ilean

@@ -0,0 +1 @@
+{"version":4,"references":{},"module":"MyProject","directImports":[["MyProject.Basic",false,false,false]]}

MyProject/.lake/build/lib/lean/MyProject.ilean.hash

@@ -0,0 +1 @@
+1223145565319205264

MyProject/.lake/build/lib/lean/MyProject.olean.hash

@@ -0,0 +1 @@
+2826512291163496019

MyProject/.lake/build/lib/lean/MyProject.trace

@@ -0,0 +1,30 @@
+{"synthetic": false,
+ "outputs":
+ {"o": ["2826512291163496019"],
+  "i": "1223145565319205264",
+  "c": "10253638930955786439"},
+ "log":
+ [{"message":
+   ".> LEAN_PATH=C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\bin\\lean.exe C:\\Users\\marooc\\AXIOVORA X\\MyProject\\MyProject.lean -o C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\MyProject.olean -i C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\MyProject.ilean -c C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject.c --setup C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject.setup.json --json",
+   "level": "trace"}],
+ "inputs":
+ [["MyProject:deps",
+   [["deps",
+     [["MyProject/MyProject:extraDep", [["@MyProject:extraDep", "1723"]]],
+      ["import oleans",
+       [["MyProject.Basic:olean",
+         [["MyProject.Basic:deps", "12720339749678921893"],
+          ["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\MyProject\\Basic.olean",
+           "6875692082518850885"]]]]]]],
+    ["libs",
+     [["import dynlibs", "1723"],
+      ["package external libraries", "1723"],
+      ["module dynlibs", "1723"],
+      ["module plugins", "1723"]]]]],
+  ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+   "8739116525927611134"],
+  ["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\MyProject.lean",
+   "12336320995415267534"],
+  ["options", "1723"],
+  ["Module.leanArgs: #[]", "1723"]],
+ "depHash": "5093461821927556036"}

MyProject/.lake/build/lib/lean/MyProject/Basic.ilean

@@ -0,0 +1 @@
+{"version":4,"references":{"{\"c\":{\"n\":\"hello\",\"m\":\"MyProject.Basic\"}}":{"usages":[],"definition":[0,4,0,9]}},"module":"MyProject.Basic","directImports":[]}

MyProject/.lake/build/lib/lean/MyProject/Basic.ilean.hash

@@ -0,0 +1 @@
+16625990806461164587

MyProject/.lake/build/lib/lean/MyProject/Basic.olean.hash

@@ -0,0 +1 @@
+6875692082518850885

MyProject/.lake/build/lib/lean/MyProject/Basic.trace

@@ -0,0 +1,26 @@
+{"synthetic": false,
+ "outputs":
+ {"o": ["6875692082518850885"],
+  "i": "16625990806461164587",
+  "c": "6640969564603399067"},
+ "log":
+ [{"message":
+   ".> LEAN_PATH=C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean c:\\Users\\marooc\\.elan\\toolchains\\leanprover--lean4---v4.22.0\\bin\\lean.exe C:\\Users\\marooc\\AXIOVORA X\\MyProject\\MyProject\\Basic.lean -o C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\MyProject\\Basic.olean -i C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\lib\\lean\\MyProject\\Basic.ilean -c C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject\\Basic.c --setup C:\\Users\\marooc\\AXIOVORA X\\MyProject\\.lake\\build\\ir\\MyProject\\Basic.setup.json --json",
+   "level": "trace"}],
+ "inputs":
+ [["MyProject.Basic:deps",
+   [["deps",
+     [["MyProject/MyProject:extraDep", [["@MyProject:extraDep", "1723"]]],
+      ["import oleans", "1723"]]],
+    ["libs",
+     [["import dynlibs", "1723"],
+      ["package external libraries", "1723"],
+      ["module dynlibs", "1723"],
+      ["module plugins", "1723"]]]]],
+  ["Lean 4.22.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05",
+   "8739116525927611134"],
+  ["C:\\Users\\marooc\\AXIOVORA X\\MyProject\\MyProject\\Basic.lean",
+   "18126205365334327008"],
+  ["options", "1723"],
+  ["Module.leanArgs: #[]", "1723"]],
+ "depHash": "16222576468637617417"}

MyProject/MyProject/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Split
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Eqns
+import Lean.Meta.ArgsPacker.Basic
+import Init.Data.Array.Basic
+
+namespace Lean.Elab.Nonrec
+open Meta
+open Eqns
+
+/--
+Simple, coarse-grained equation theorem for nonrecursive definitions.
+-/
+private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
+  if let some (.defnInfo info) := (← getEnv).find? declName then
+    let name := mkEqLikeNameFor (← getEnv) declName eqn1ThmSuffix
+    trace[Elab.definition.eqns] "mkSimpleEqnThm: {name}"
+    realizeConst declName name (doRealize name info)
+    return some name
+  else
+    return none
+where
+  doRealize name info :=
+    lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
+      let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
+      let type  ← mkForallFVars xs (← mkEq lhs body)
+      let value ← mkLambdaFVars xs (← mkEqRefl lhs)
+      addDecl <| .thmDecl {
+        name, type, value
+        levelParams := info.levelParams
+      }
+      inferDefEqAttr name
+
+def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
+  if (← isRecursiveDefinition declName) then
+    return none
+  if (← getEnv).contains declName then
+    if backward.eqns.nonrecursive.get (← getOptions) then
+      mkEqns declName #[]
+    else
+      let o ← mkSimpleEqThm declName
+      return o.map (#[·])
+  else
+    return none
+
+builtin_initialize
+  registerGetEqnsFn getEqnsFor?
+
+end Lean.Elab.Nonrec

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Elab.Tactic.Conv
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Split
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Eqns
+import Lean.Elab.PreDefinition.FixedParams
+import Lean.Meta.ArgsPacker.Basic
+import Init.Data.Array.Basic
+import Init.Internal.Order.Basic
+
+namespace Lean.Elab.PartialFixpoint
+open Meta
+open Eqns
+
+structure EqnInfo extends EqnInfoCore where
+  declNames       : Array Name
+  declNameNonRec  : Name
+  fixedParamPerms : FixedParamPerms
+  fixpointType    : Array PartialFixpointType
+  deriving Inhabited
+
+builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
+
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name)
+    (fixedParamPerms : FixedParamPerms) (fixpointType : Array PartialFixpointType): MetaM Unit := do
+  preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
+  unless preDefs.all fun p => p.kind.isTheorem do
+    unless (← preDefs.allM fun p => isProp p.type) do
+      let declNames := preDefs.map (·.declName)
+      modifyEnv fun env =>
+        preDefs.foldl (init := env) fun env preDef =>
+          eqnInfoExt.insert env preDef.declName { preDef with
+            declNames, declNameNonRec, fixedParamPerms, fixpointType }
+
+private def deltaLHSUntilFix (declName declNameNonRec : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
+  let lhs' ← deltaExpand lhs fun n => n == declName || n == declNameNonRec
+  mvarId.replaceTargetDefEq (← mkEq lhs' rhs)
+
+partial def rwFixUnder (lhs : Expr) : MetaM Expr := do
+  if lhs.isAppOfArity ``Order.fix 4 then
+    return mkAppN (mkConst ``Order.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
+  else if lhs.isAppOfArity ``Order.lfp_monotone 4 then
+    return mkAppN (mkConst ``Order.lfp_monotone_fix lhs.getAppFn.constLevels!) lhs.getAppArgs
+  else if lhs.isApp then
+    let h ← rwFixUnder lhs.appFn!
+    mkAppM ``congrFun #[h, lhs.appArg!]
+  else if lhs.isProj then
+    let f := mkLambda `p .default (← inferType lhs.projExpr!) (lhs.updateProj! (.bvar 0))
+    let h ← rwFixUnder lhs.projExpr!
+    mkAppM ``congrArg #[f, h]
+  else
+    throwError "rwFixUnder: unexpected expression {lhs}"
+
+private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  let mut mvarId := mvarId
+  let target ← mvarId.getType'
+  let some (_, lhs, rhs) := target.eq? | unreachable!
+  let h ← rwFixUnder lhs
+  let some (_, _, lhsNew) := (← inferType h).eq? | unreachable!
+  let targetNew ← mkEq lhsNew rhs
+  let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew
+  mvarId.assign (← mkEqTrans h mvarNew)
+  return mvarNew.mvarId!
+
+/-- Generate the "unfold" lemma for `declName`. -/
+def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+  realizeConst declName name (doRealize name)
+  return name
+where
+  doRealize name := withOptions (tactic.hygienic.set · false) do
+    lambdaTelescope info.value fun xs body => do
+      let us := info.levelParams.map mkLevelParam
+      let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
+      let goal ← withNewMCtxDepth do
+        try
+          let goal ← mkFreshExprSyntheticOpaqueMVar type
+          let mvarId := goal.mvarId!
+          trace[Elab.definition.partialFixpoint] "mkUnfoldEq start:{mvarId}"
+          let mvarId ← deltaLHSUntilFix declName info.declNameNonRec mvarId
+          trace[Elab.definition.partialFixpoint] "mkUnfoldEq after deltaLHS:{mvarId}"
+          let mvarId ← rwFixEq mvarId
+          trace[Elab.definition.partialFixpoint] "mkUnfoldEq after rwFixEq:{mvarId}"
+          withAtLeastTransparency .all <|
+            withOptions (smartUnfolding.set · false) <|
+              mvarId.refl
+          trace[Elab.definition.partialFixpoint] "mkUnfoldEq rfl succeeded"
+          instantiateMVars goal
+        catch e =>
+          throwError "failed to generate unfold theorem for '{declName}':\n{e.toMessageData}"
+      let type ← mkForallFVars xs type
+      let type ← letToHave type
+      let value ← mkLambdaFVars xs goal
+      addDecl <| Declaration.thmDecl {
+        name, type, value
+        levelParams := info.levelParams
+      }
+
+def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+  let env ← getEnv
+  if env.contains name then return name
+  let some info := eqnInfoExt.find? env declName | return none
+  return some (← mkUnfoldEq declName info)
+
+def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
+  if let some info := eqnInfoExt.find? (← getEnv) declName then
+    mkEqns declName info.declNames
+  else
+    return none
+
+builtin_initialize
+  registerGetEqnsFn getEqnsFor?
+  registerGetUnfoldEqnFn getUnfoldFor?
+
+end Lean.Elab.PartialFixpoint

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean

@@ -0,0 +1,402 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Meta.Basic
+import Lean.Meta.Match.MatcherApp.Transform
+import Lean.Meta.Check
+import Lean.Meta.Tactic.Subst
+import Lean.Meta.Injective -- for elimOptParam
+import Lean.Meta.ArgsPacker
+import Lean.Meta.PProdN
+import Lean.Meta.Tactic.Apply
+import Lean.Elab.PreDefinition.PartialFixpoint.Eqns
+import Lean.Elab.Command
+import Lean.Meta.Tactic.ElimInfo
+
+namespace Lean.Elab.PartialFixpoint
+
+open Lean Elab Meta
+
+open Lean.Order
+
+def mkAdmAnd (α instα adm₁ adm₂ : Expr) : MetaM Expr :=
+  mkAppOptM ``admissible_and #[α, instα, none, none, adm₁, adm₂]
+
+partial def mkAdmProj (packedInst : Expr) (i : Nat) (e : Expr) : MetaM Expr := do
+  if let some inst ← whnfUntil packedInst ``instCCPOPProd then
+    let_expr instCCPOPProd α β instα instβ := inst | throwError "mkAdmProj: unexpected instance {inst}"
+    if i == 0 then
+      mkAppOptM ``admissible_pprod_fst #[α, β, instα, instβ, none, e]
+    else
+      let e ← mkAdmProj instβ (i - 1) e
+      mkAppOptM ``admissible_pprod_snd #[α, β, instα, instβ, none, e]
+  else
+    assert! i == 0
+    return e
+
+def CCPOProdProjs (n : Nat) (inst : Expr) : Array Expr := Id.run do
+  let mut insts := #[inst]
+  while insts.size < n do
+    let inst := insts.back!
+    let_expr Lean.Order.instCCPOPProd _ _ inst₁ inst₂ := inst
+      | panic! s!"isOptionFixpoint: unexpected CCPO instance {inst}"
+    insts := insts.pop
+    insts := insts.push inst₁
+    insts := insts.push inst₂
+  return insts
+
+/--
+Unfolds an appropriate `PartialOrder` instance on predicates to quantifications and implications.
+I.e. `ImplicationOrder.instPartialOrder.rel P Q` becomes
+`∀ x y, P x y → Q x y`.
+In the premise of the Park induction principle (`lfp_le_of_le_monotone`) we use a monotone map defining the predicate in the eta expanded form. In such a case, besides desugaring the predicate, we need to perform a weak head reduction.
+The optional parameter `reduceConclusion` (false by default) indicates whether we need to perform this reduction.
+-/
+def unfoldPredRel (predType : Expr) (body : Expr) (fixpointType : PartialFixpointType) (reduceConclusion : Bool := false) : MetaM Expr := do
+  match fixpointType with
+  | .partialFixpoint => throwError "Trying to apply lattice induction to a non-lattice fixpoint. Please report this issue."
+  | .inductiveFixpoint | .coinductiveFixpoint =>
+    unless body.isAppOfArity ``PartialOrder.rel 4 do
+      throwError "{body} is not an application of partial order"
+    let lhsTypes ← forallTelescope predType fun ts _ =>  ts.mapM inferType
+    let names ← lhsTypes.mapM fun _ => mkFreshUserName `x
+    let bodyArgs := body.getAppArgs
+    withLocalDeclsDND (names.zip lhsTypes) fun exprs => do
+      let mut applied  := match fixpointType with
+        | .inductiveFixpoint => (bodyArgs[2]!, bodyArgs[3]!)
+        | .coinductiveFixpoint => (bodyArgs[3]!, bodyArgs[2]!)
+        | .partialFixpoint => panic! "Cannot apply lattice induction to a non-lattice fixpoint"
+      for e in exprs do
+        applied := (mkApp applied.1 e, mkApp applied.2 e)
+      if reduceConclusion then
+        match fixpointType with
+        | .inductiveFixpoint => applied := ((←whnf applied.1), applied.2)
+        | .coinductiveFixpoint => applied := (applied.1, (←whnf applied.2))
+        | .partialFixpoint => throwError "Cannot apply lattice induction to a non-lattice fixpoint"
+      mkForallFVars exprs (←mkArrow applied.1 applied.2)
+
+/-- `maskArray mask xs` keeps those `x` where the corresponding entry in `mask` is `true` -/
+-- Worth having in the standard library?
+private def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do
+  let mut ys := #[]
+  for b in mask, x in xs do
+    if b then ys := ys.push x
+  return ys
+
+/-- Appends `_1` etc to `base` unless `n == 1` -/
+private def numberNames (n : Nat) (base : String) : Array Name :=
+  .ofFn (n := n) fun ⟨i, _⟩ =>
+    if n == 1 then .mkSimple base else .mkSimple s!"{base}_{i+1}"
+
+def getInductionPrinciplePostfix (name : Name) : MetaM Name := do
+  let some eqnInfo := eqnInfoExt.find? (← getEnv) name | throwError "{name} is not defined by partial_fixpoint, inductive_fixpoint, nor coinductive_fixpoint"
+  let idx := eqnInfo.declNames.idxOf name
+  let some res := eqnInfo.fixpointType[idx]? | throwError "Cannot get fixpoint type for {name}"
+  match res with
+  | .partialFixpoint => return `fixpoint_induct
+  | .inductiveFixpoint => return `induct
+  | .coinductiveFixpoint => return `coinduct
+
+def deriveInduction (name : Name) : MetaM Unit := do
+  let postFix ← getInductionPrinciplePostfix name
+  let inductName := name ++ postFix
+  realizeConst name inductName do
+  trace[Elab.definition.partialFixpoint] "Called deriveInduction for {inductName}"
+  prependError m!"Cannot derive fixpoint induction principle (please report this issue)" do
+    let some eqnInfo := eqnInfoExt.find? (← getEnv) name |
+      throwError "{name} is not defined by partial_fixpoint"
+    let infos ← eqnInfo.declNames.mapM getConstInfoDefn
+    let e' ← eqnInfo.fixedParamPerms.perms[0]!.forallTelescope infos[0]!.type fun xs => do
+      -- Now look at the body of an arbitrary of the functions (they are essentially the same
+      -- up to the final projections)
+      let body ← eqnInfo.fixedParamPerms.perms[0]!.instantiateLambda infos[0]!.value xs
+
+      -- The body should now be of the form of the form (fix … ).2.2.1
+      -- We strip the projections (if present)
+      let body' := PProdN.stripProjs body.eta -- TODO: Eta more carefully?
+      if eqnInfo.fixpointType.all isLatticeTheoretic then
+        unless eqnInfo.declNames.size == 1 do
+          throwError "Mutual lattice (co)induction is not supported yet"
+
+        -- We strip it until we reach an application of `lfp_montotone`
+        let some fixApp ← whnfUntil body' ``lfp_monotone
+          | throwError "Unexpected function body {body}, could not whnfUntil lfp_monotone"
+        let_expr lfp_monotone α instcomplete_lattice F hmono := fixApp
+          | throwError "Unexpected function body {body}, not an application of lfp_monotone"
+        let e' ← mkAppOptM ``lfp_le_of_le_monotone #[α, instcomplete_lattice, F, hmono]
+
+        -- We get the type of the induction principle
+        let eTyp ← inferType e'
+        let f ← mkConstWithLevelParams infos[0]!.name
+        let fEtaExpanded ← lambdaTelescope infos[0]!.value fun ys _ =>
+            mkLambdaFVars ys (mkAppN f ys)
+        let fInst ← eqnInfo.fixedParamPerms.perms[0]!.instantiateLambda fEtaExpanded xs
+        let fInst := fInst.eta
+
+        -- Then, we change the conclusion so it doesn't mention the `lfp_monotone`, but rather the actual predicate.
+        let newTyp ← forallTelescope eTyp fun args econc =>
+          if econc.isAppOfArity ``PartialOrder.rel 4 then
+            let oldArgs := econc.getAppArgs
+            let newArgs := oldArgs.set! 2 fInst
+            let newBody := mkAppN econc.getAppFn newArgs
+            mkForallFVars args newBody
+          else
+            throwError "Unexpected conclusion of the fixpoint induction principle: {econc}"
+
+        -- Desugar partial order on predicates in premises and conclusion
+        let newTyp ← forallTelescope newTyp fun args conclusion => do
+          let predicate := args[0]!
+          let predicateType ← inferType predicate
+          let premise := args[1]!
+          let premiseType ← inferType premise
+          -- Besides unfolding the predicate, we need to perform a weak head reduction in the premise,
+          -- where the monotone map defining the fixpoint is in the eta expanded form.
+          -- We do this by setting the optional parameter `reduceConclusion` to true.
+          let premiseType ← unfoldPredRel predicateType premiseType eqnInfo.fixpointType[0]! (reduceConclusion := true)
+          let newConclusion ← unfoldPredRel predicateType conclusion eqnInfo.fixpointType[0]!
+          let abstracedNewConclusion ← mkForallFVars args newConclusion
+          withLocalDecl `y BinderInfo.default premiseType fun newPremise => do
+            let typeHint ← mkExpectedTypeHint newPremise premiseType
+            let argsForInst := args.set! 1 typeHint
+            let argsWithNewPremise := args.set! 1 newPremise
+            let instantiated ← instantiateForall abstracedNewConclusion argsForInst
+            mkForallFVars argsWithNewPremise instantiated
+
+        let e' ← mkExpectedTypeHint e' newTyp
+        let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) xs e'
+
+        trace[Elab.definition.partialFixpoint.induction] "Complete body of (lattice-theoretic) fixpoint induction principle:{indentExpr e'}"
+
+        pure e'
+      else
+        let some fixApp ← whnfUntil body' ``fix
+          | throwError "Unexpected function body {body}, could not whnfUntil fix"
+        let_expr fix α instCCPOα F hmono := fixApp
+          | throwError "Unexpected function body {body'}, not an application of fix"
+
+        let instCCPOs := CCPOProdProjs infos.size instCCPOα
+        let types ← infos.mapIdxM (eqnInfo.fixedParamPerms.perms[·]!.instantiateForall ·.type xs)
+        let packedType ← PProdN.pack 0 types
+        let motiveTypes ← types.mapM (mkArrow · (.sort 0))
+        let motiveNames := numberNames motiveTypes.size "motive"
+        withLocalDeclsDND (motiveNames.zip motiveTypes) fun motives => do
+          let packedMotive ←
+            withLocalDeclD (← mkFreshUserName `x) packedType fun x => do
+              mkLambdaFVars #[x] <| ← PProdN.pack 0 <|
+                motives.mapIdx fun idx motive =>
+                  mkApp motive (PProdN.proj motives.size idx packedType x)
+
+          let admTypes ← motives.mapIdxM fun i motive => do
+            mkAppOptM ``admissible #[types[i]!, instCCPOs[i]!, some motive]
+          let admNames := numberNames admTypes.size "adm"
+          withLocalDeclsDND (admNames.zip admTypes) fun adms => do
+            let adms' ← adms.mapIdxM fun i adm => mkAdmProj instCCPOα i adm
+            let packedAdm ← PProdN.genMk (mkAdmAnd α instCCPOα) adms'
+            let hNames := numberNames infos.size "h"
+            let hTypes_hmask : Array (Expr × Array Bool) ← infos.mapIdxM fun i _info => do
+              let approxNames := infos.map fun info =>
+                match info.name with
+                  | .str _ n => .mkSimple n
+                  | _ => `f
+              withLocalDeclsDND (approxNames.zip types) fun approxs => do
+                let ihTypes := approxs.mapIdx fun j approx => mkApp motives[j]! approx
+                withLocalDeclsDND (ihTypes.map (⟨`ih, ·⟩)) fun ihs => do
+                  let f ← PProdN.mk 0 approxs
+                  let Ff := F.beta #[f]
+                  let Ffi := PProdN.proj motives.size i packedType Ff
+                  let t := mkApp motives[i]! Ffi
+                  let t ← PProdN.reduceProjs t
+                  let mask := approxs.map fun approx => t.containsFVar approx.fvarId!
+                  let t ← mkForallFVars (maskArray mask approxs ++ maskArray mask ihs) t
+                  pure (t, mask)
+            let (hTypes, masks) := hTypes_hmask.unzip
+            withLocalDeclsDND (hNames.zip hTypes) fun hs => do
+              let packedH ←
+                withLocalDeclD `approx packedType fun approx =>
+                  let packedIHType := packedMotive.beta #[approx]
+                  withLocalDeclD `ih packedIHType fun ih => do
+                    let approxs := PProdN.projs motives.size packedType approx
+                    let ihs := PProdN.projs motives.size packedIHType ih
+                    let e ← PProdN.mk 0 <| hs.mapIdx fun i h =>
+                      let mask := masks[i]!
+                      mkAppN h (maskArray mask approxs ++ maskArray mask ihs)
+                    mkLambdaFVars #[approx, ih] e
+              let e' ← mkAppOptM ``fix_induct #[α, instCCPOα, F, hmono, packedMotive, packedAdm, packedH]
+              -- Should be the type of e', but with the function definitions folded
+              let packedConclusion ← PProdN.pack 0 <| ←
+                motives.mapIdxM fun i motive => do
+                  let f ← mkConstWithLevelParams infos[i]!.name
+                  let fEtaExpanded ← lambdaTelescope infos[i]!.value fun ys _ =>
+                    mkLambdaFVars ys (mkAppN f ys)
+                  let fInst ← eqnInfo.fixedParamPerms.perms[i]!.instantiateLambda fEtaExpanded xs
+                  let fInst := fInst.eta
+                  return mkApp motive fInst
+              let e' ← mkExpectedTypeHint e' packedConclusion
+              let e' ← mkLambdaFVars hs e'
+              let e' ← mkLambdaFVars adms e'
+              let e' ← mkLambdaFVars motives e'
+              let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) xs e'
+              let e' ← instantiateMVars e'
+              trace[Elab.definition.partialFixpoint.induction] "complete body of fixpoint induction principle:{indentExpr e'}"
+              pure e'
+
+    let eTyp ← inferType e'
+    let eTyp ← elimOptParam eTyp
+    -- logInfo m!"eTyp: {eTyp}"
+    let params := (collectLevelParams {} eTyp).params
+    -- Prune unused level parameters, preserving the original order
+    let us := infos[0]!.levelParams.filter (params.contains ·)
+
+    addDecl <| Declaration.thmDecl
+      { name := inductName, levelParams := us, type := eTyp, value := e' }
+
+def isInductName (env : Environment) (name : Name) : Bool := Id.run do
+  let .str p s := name | return false
+  match s with
+  | "fixpoint_induct" =>
+    if let some eqnInfo := eqnInfoExt.find? env p then
+      return p == eqnInfo.declNames[0]! && isPartialFixpoint (eqnInfo.fixpointType[0]!)
+    return false
+  | "coinduct" =>
+    if let some eqnInfo := eqnInfoExt.find? env p then
+      let idx := eqnInfo.declNames.idxOf p
+      return isCoinductiveFixpoint eqnInfo.fixpointType[idx]!
+    return false
+  | "induct" =>
+    if let some eqnInfo := eqnInfoExt.find? env p then
+      let idx := eqnInfo.declNames.idxOf p
+      return isInductiveFixpoint eqnInfo.fixpointType[idx]!
+    return false
+  | _ => return false
+
+builtin_initialize
+  registerReservedNamePredicate isInductName
+
+  registerReservedNameAction fun name => do
+    if isInductName (← getEnv) name then
+      let .str p _ := name | return false
+      MetaM.run' <| deriveInduction p
+      return true
+    return false
+
+/--
+Returns true if `name` defined by `partial_fixpoint`, the first in its mutual group,
+and all functions are defined using the `CCPO` instance for `Option`.
+-/
+def isOptionFixpoint (env : Environment) (name : Name) : Bool := Option.isSome do
+  let eqnInfo ← eqnInfoExt.find? env name
+  guard <| name == eqnInfo.declNames[0]!
+  let defnInfo ← env.find? eqnInfo.declNameNonRec
+  assert! defnInfo.hasValue
+  let mut value := defnInfo.value!
+  while value.isLambda do value := value.bindingBody!
+  let_expr Lean.Order.fix _ inst _ _ := value | panic! s!"isOptionFixpoint: unexpected value {value}"
+  let insts := CCPOProdProjs eqnInfo.declNames.size inst
+  insts.forM fun inst => do
+    let mut inst := inst
+    while inst.isAppOfArity ``instCCPOPi 3 do
+      guard inst.appArg!.isLambda
+      inst := inst.appArg!.bindingBody!
+    guard <| inst.isAppOfArity ``instCCPOOption 1
+
+def isPartialCorrectnessName (env : Environment) (name : Name) : Bool := Id.run do
+  let .str p s := name | return false
+  unless s == "partial_correctness" do return false
+  return isOptionFixpoint env p
+
+/--
+Given `motive : α → β → γ → Prop`, construct a proof of
+`admissible (fun f => ∀ x y r, f x y = r → motive x y r)`
+-/
+def mkOptionAdm (motive : Expr) : MetaM Expr := do
+  let type ← inferType motive
+  forallTelescope type fun ysr _ => do
+    let P := mkAppN motive ysr
+    let ys := ysr.pop
+    let r := ysr.back!
+    let mut inst ← mkAppM ``Option.admissible_eq_some #[P, r]
+    inst ← mkLambdaFVars #[r] inst
+    inst ← mkAppOptM ``admissible_pi #[none, none, none, none, inst]
+    for y in ys.reverse do
+      inst ← mkLambdaFVars #[y] inst
+      inst ← mkAppOptM ``admissible_pi_apply #[none, none, none, none, inst]
+    pure inst
+
+def derivePartialCorrectness (name : Name) : MetaM Unit := do
+  let inductName := name ++ `partial_correctness
+  realizeConst name inductName do
+  let fixpointInductThm := name ++ `fixpoint_induct
+  unless (← getEnv).contains fixpointInductThm do
+    deriveInduction name
+
+  prependError m!"Cannot derive partial correctness theorem (please report this issue)" do
+    let some eqnInfo := eqnInfoExt.find? (← getEnv) name |
+      throwError "{name} is not defined by partial_fixpoint"
+
+    let infos ← eqnInfo.declNames.mapM getConstInfoDefn
+    let fixedParamPerm0 := eqnInfo.fixedParamPerms.perms[0]!
+    -- First open up the fixed parameters everywhere
+    let e' ← fixedParamPerm0.forallTelescope infos[0]!.type fun xs => do
+      let types ← infos.mapIdxM (eqnInfo.fixedParamPerms.perms[·]!.instantiateForall ·.type xs)
+
+      -- for `f : α → β → Option γ`, we expect a `motive : α → β → γ → Prop`
+      let motiveTypes ← types.mapM fun type =>
+        forallTelescopeReducing type fun ys type => do
+          let type ← whnf type
+          let_expr Option γ := type | throwError "Expected `Option`, got:{indentExpr type}"
+          withLocalDeclD (← mkFreshUserName `r) γ fun r =>
+            mkForallFVars (ys.push r) (.sort 0)
+      let motiveDecls ← motiveTypes.mapIdxM fun i motiveType => do
+        let n := if infos.size = 1 then .mkSimple "motive"
+                                   else .mkSimple s!"motive_{i+1}"
+        pure (n, fun _ => pure motiveType)
+      withLocalDeclsD motiveDecls fun motives => do
+        -- the motives, as expected by `f.fixpoint_induct`:
+        -- fun f => ∀ x y r, f x y = some r → motive x y r
+        let motives' ← motives.mapIdxM fun i motive => do
+          withLocalDeclD (← mkFreshUserName `f) types[i]! fun f => do
+            forallTelescope (← inferType motive) fun ysr _ => do
+              let ys := ysr.pop
+              let r := ysr.back!
+              let heq ← mkEq (mkAppN f ys) (← mkAppM ``some #[r])
+              let motive' ← mkArrow heq (mkAppN motive ysr)
+              let motive' ← mkForallFVars ysr motive'
+              mkLambdaFVars #[f] motive'
+
+        let e' ← mkAppOptM fixpointInductThm <| (xs ++ motives').map some
+        let adms ← motives.mapM mkOptionAdm
+        let e' := mkAppN e' adms
+        let e' ← mkLambdaFVars motives e'
+        let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) xs e'
+        let e' ← instantiateMVars e'
+        trace[Elab.definition.partialFixpoint.induction] "complete body of partial correctness principle:{indentExpr e'}"
+        pure e'
+
+    let eTyp ← inferType e'
+    let eTyp ← elimOptParam eTyp
+    let eTyp ← Core.betaReduce eTyp
+    -- logInfo m!"eTyp: {eTyp}"
+    let params := (collectLevelParams {} eTyp).params
+    -- Prune unused level parameters, preserving the original order
+    let us := infos[0]!.levelParams.filter (params.contains ·)
+
+    addDecl <| Declaration.thmDecl
+      { name := inductName, levelParams := us, type := eTyp, value := e' }
+
+builtin_initialize
+  registerReservedNamePredicate isPartialCorrectnessName
+
+  registerReservedNameAction fun name => do
+    let .str p s := name | return false
+    unless s == "partial_correctness" do return false
+    unless isOptionFixpoint (← getEnv) p do return false
+    MetaM.run' <| derivePartialCorrectness p
+    return false
+
+end Lean.Elab.PartialFixpoint
+
+builtin_initialize Lean.registerTraceClass `Elab.definition.partialFixpoint.induction

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean

@@ -0,0 +1,224 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Lean.Elab.PreDefinition.MkInhabitant
+import Lean.Elab.PreDefinition.Mutual
+import Lean.Elab.PreDefinition.PartialFixpoint.Eqns
+import Lean.Elab.Tactic.Monotonicity
+import Init.Internal.Order.Basic
+import Lean.Meta.PProdN
+import Lean.Meta.Order
+
+namespace Lean.Elab
+
+open Meta
+open Monotonicity
+
+open Lean.Order
+
+private def replaceRecApps (recFnNames : Array Name) (fixedParamPerms : FixedParamPerms) (f : Expr) (e : Expr) : MetaM Expr := do
+  assert! recFnNames.size = fixedParamPerms.perms.size
+  let t ← inferType f
+  return e.replace fun e => do
+    let fn := e.getAppFn
+    guard fn.isConst
+    let idx ← recFnNames.idxOf? fn.constName!
+    let args := e.getAppArgs
+    let varying := fixedParamPerms.perms[idx]!.pickVarying args
+    return mkAppN (PProdN.proj recFnNames.size idx t f) varying
+
+/--
+For pretty error messages:
+Takes `F : (fun f => e)`, where `f` is the packed function, and replaces `f` in `e` with the user-visible
+constants, which are added to the environment temporarily.
+-/
+private def unReplaceRecApps {α} (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr)
+    (F : Expr) (k : Expr → MetaM α) : MetaM α := do
+  unless F.isLambda do throwError "Expected lambda:{indentExpr F}"
+  withoutModifyingEnv do
+    preDefs.forM addAsAxiom
+    let fns ← preDefs.mapIdxM fun funIdx preDef => do
+      let value ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs
+      lambdaTelescope value fun xs _ =>
+        let args := fixedParamPerms.perms[funIdx]!.buildArgs fixedArgs xs
+        let call := mkAppN (.const preDef.declName (preDef.levelParams.map mkLevelParam)) args
+        mkLambdaFVars (etaReduce := true) xs call
+    let packedFn ← PProdN.mk 0 fns
+    let e ← lambdaBoundedTelescope F 1 fun f e => do
+      let f := f[0]!
+      -- Replace f with calls to the constants
+      let e := e.replace fun e => do
+        if e == f then return packedFn else none
+      -- And reduce projection and beta redexes
+      -- (This is a bit blunt; we could try harder to only replace the projection and beta-redexes
+      -- introduced above)
+      let e ← PProdN.reduceProjs e
+      let e ← Core.betaReduce e
+      pure e
+    k e
+
+/--
+Given two type-proof pairs for `monotone f` and `monotone g`, constructs a type-proof pair for `monotone fun x => ⟨f x, g x⟩`.
+-/
+private def mkMonoPProd : (hmono₁ hmono₂ : Expr × Expr) → MetaM (Expr × Expr)
+  | (hmono1Type, hmono1Proof), (hmono2Type, hmono2Proof) => do
+  -- mkAppM does not support the equivalent of (cfg := { synthAssignedInstances := false}),
+  -- so this is a bit more pedestrian
+  let_expr monotone _ inst _ inst₁ _ := hmono1Type
+    | throwError "mkMonoPProd: unexpected type of{indentExpr hmono1Proof}"
+  let_expr monotone _ _ _ inst₂ _ := hmono2Type
+    | throwError "mkMonoPProd: unexpected type of{indentExpr hmono2Proof}"
+  let hmonoProof ← mkAppOptM ``PProd.monotone_mk #[none, none, none, inst₁, inst₂, inst, none, none, hmono1Proof, hmono2Proof]
+  return (← inferType hmonoProof, hmonoProof)
+
+def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
+  -- We expect all functions in the clique to have `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` syntax
+  let hints := preDefs.filterMap (·.termination.partialFixpoint?)
+  assert! preDefs.size = hints.size
+  -- We check if any fixpoints were defined lattice-theoretically
+  if hints.any fun x => isLatticeTheoretic x.fixpointType then
+    -- If yes, then we expect all of them to be defined using lattice theory
+    assert! hints.all fun x => isLatticeTheoretic x.fixpointType
+
+  -- For every function of type `∀ x y, r x y`, an CCPO instance
+  -- ∀ x y, CCPO (r x y), but crucially constructed using `instCCPOPi`
+  let insts ← preDefs.mapIdxM fun i preDef => withRef hints[i]!.ref do
+    lambdaTelescope preDef.value fun xs _body => do
+      let type ← instantiateForall preDef.type xs
+      let inst ←
+        match hints[i]!.fixpointType with
+        | .coinductiveFixpoint =>
+          unless type.isProp do
+            throwError "`coinductive_fixpoint` can be only used to define predicates"
+          pure (mkConst ``ReverseImplicationOrder.instCompleteLattice)
+        | .inductiveFixpoint =>
+          unless type.isProp do
+            throwError "`inductive_fixpoint` can be only used to define predicates"
+          pure (mkConst ``ImplicationOrder.instCompleteLattice)
+        | .partialFixpoint => try
+            synthInstance (← mkAppM ``CCPO #[type])
+          catch _ =>
+            trace[Elab.definition.partialFixpoint] "No CCPO instance found for {preDef.declName}, trying inhabitation"
+            let msg := m!"failed to compile definition '{preDef.declName}' using `partial_fixpoint`"
+            let w ← mkInhabitantFor msg #[] preDef.type
+            let instNonempty ← mkAppM ``Nonempty.intro #[mkAppN w xs]
+            let classicalWitness ← mkAppOptM ``Classical.ofNonempty #[none, instNonempty]
+            mkAppOptM ``FlatOrder.instCCPO #[none, classicalWitness]
+      mkLambdaFVars xs inst
+
+  let declNames := preDefs.map (·.declName)
+  let fixedParamPerms ← getFixedParamPerms preDefs
+  fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun fixedArgs => do
+    -- Either: ∀ x y, CCPO (rᵢ x y)
+    -- Or:     ∀ x y, CompleteLattice (rᵢ x y)
+    let insts ← insts.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda · fixedArgs)
+    let types ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateForall ·.type fixedArgs)
+
+    -- (∀ x y, r₁ x y) ×' (∀ x y, r₂ x y)
+    let packedType ← PProdN.pack 0 types
+
+    -- Either: CCPO (∀ x y, rᵢ x y)
+    -- Or:     CompleteLattice (∀ x y, rᵢ x y)
+    let insts' ← insts.mapM fun inst =>
+      lambdaTelescope inst fun xs inst => do
+        let mut inst := inst
+        for x in xs.reverse do
+          inst ← mkInstPiOfInstForall x inst
+        pure inst
+
+    -- Either: CCPO ((∀ x y, r₁ x y) ×' (∀ x y, r₂ x y))
+    -- Or:     CompleteLattice ((∀ x y, r₁ x y) ×' (∀ x y, r₂ x y))
+    let packedInst ← mkPackedPPRodInstance insts'
+    -- Order ((∀ x y, r₁ x y) ×' (∀ x y, r₂ x y))
+    let packedPartialOrderInst ← toPartialOrder packedInst
+
+    -- Error reporting hook, presenting monotonicity errors in terms of recursive functions
+    let failK {α} f (monoThms : Array Name) : MetaM α := do
+      unReplaceRecApps preDefs fixedParamPerms fixedArgs f fun t => do
+        let extraMsg := if monoThms.isEmpty then m!"" else
+          m!"Tried to apply {.andList (monoThms.toList.map (m!"'{.ofConstName ·}'"))}, but failed.\n\
+             Possible cause: A missing `{.ofConstName ``MonoBind}` instance.\n\
+             Use `set_option trace.Elab.Tactic.monotonicity true` to debug."
+        if let some recApp := t.find? hasRecAppSyntax then
+          let some syn := getRecAppSyntax? recApp | panic! "getRecAppSyntax? failed"
+          withRef syn <|
+            throwError "Cannot eliminate recursive call `{syn}` enclosed in{indentExpr t}\n{extraMsg}"
+        else
+          throwError "Cannot eliminate recursive call in{indentExpr t}\n{extraMsg}"
+
+    -- Adjust the body of each function to take the other functions as a
+    -- (packed) parameter
+    let Fs ← preDefs.mapIdxM fun funIdx preDef => do
+      let body ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs
+      withLocalDeclD (← mkFreshUserName `f) packedType fun f => do
+        let body' ← withoutModifyingEnv do
+          -- replaceRecApps needs the constants in the env to typecheck things
+          preDefs.forM (addAsAxiom ·)
+          replaceRecApps declNames fixedParamPerms f body
+        mkLambdaFVars #[f] body'
+
+    -- Construct and solve monotonicity goals for each function separately
+    -- This way we preserve the user's parameter names as much as possible
+    -- and can (later) use the user-specified per-function tactic
+    let hmonos ← preDefs.mapIdxM fun i preDef => do
+      let type := types[i]!
+      let F := Fs[i]!
+      let inst ← toPartialOrder insts'[i]! type
+      let goal ← mkAppOptM ``monotone #[packedType, packedPartialOrderInst, type, inst, F]
+      if let some term := hints[i]!.term? then
+        let hmono ← Term.withSynthesize <| Term.elabTermEnsuringType term goal
+        let hmono ← instantiateMVars hmono
+        let mvars ← getMVars hmono
+        if mvars.isEmpty then
+          pure (goal, hmono)
+        else
+          discard <| Term.logUnassignedUsingErrorInfos mvars
+          pure (goal, ← mkSorry goal (synthetic := true))
+      else
+        let hmono ← mkFreshExprSyntheticOpaqueMVar goal
+        prependError m!"Could not prove '{preDef.declName}' to be monotone in its recursive calls:" do
+          solveMono failK hmono.mvarId!
+        trace[Elab.definition.partialFixpoint] "monotonicity proof for {preDef.declName}: {hmono}"
+        pure (goal, ← instantiateMVars hmono)
+    let (_, hmono) ← PProdN.genMk mkMonoPProd hmonos
+
+    let packedValue ← mkFixOfMonFun packedType packedInst hmono
+
+    trace[Elab.definition.partialFixpoint] "packedValue: {packedValue}"
+
+    let declName :=
+      if preDefs.size = 1 && fixedParamPerms.fixedArePrefix then
+        preDefs[0]!.declName
+      else
+        preDefs[0]!.declName ++ `mutual
+    let packedType' ← mkForallFVars fixedArgs packedType
+    let packedValue' ← mkLambdaFVars fixedArgs packedValue
+    let preDefNonRec := { preDefs[0]! with
+      declName := declName
+      type := packedType'
+      value := packedValue'}
+
+    let preDefsNonrec ← preDefs.mapIdxM fun fidx preDef => do
+      forallBoundedTelescope preDef.type fixedParamPerms.perms[fidx]!.size fun params _ => do
+        let fixed := fixedParamPerms.perms[fidx]!.pickFixed params
+        let varying := fixedParamPerms.perms[fidx]!.pickVarying params
+        let us := preDefNonRec.levelParams.map mkLevelParam
+        let value := mkConst preDefNonRec.declName us
+        let value := mkAppN value fixed
+        let value := PProdN.proj preDefs.size fidx packedType value
+        let value := mkAppN value varying
+        let value ← mkLambdaFVars (etaReduce := true) params value
+        pure { preDef with value }
+
+    Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec
+    addAndCompilePartialRec preDefs
+    let preDefs ← preDefs.mapM (Mutual.cleanPreDef ·)
+    PartialFixpoint.registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms (hints.map (·.fixpointType))
+    Mutual.addPreDefAttributes preDefs
+
+end Lean.Elab
+
+builtin_initialize Lean.registerTraceClass `Elab.definition.partialFixpoint

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -0,0 +1,293 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Util.HasConstCache
+import Lean.Meta.PProdN
+import Lean.Meta.Match.MatcherApp.Transform
+import Lean.Elab.RecAppSyntax
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Elab.PreDefinition.Structural.RecArgInfo
+
+namespace Lean.Elab.Structural
+open Meta
+
+private def throwToBelowFailed : MetaM α :=
+  throwError "toBelow failed"
+
+partial def searchPProd (e : Expr) (F : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
+  match (← whnf e) with
+  | .app (.app (.const `PProd _) d1) d2 =>
+        (do searchPProd d1 (.proj ``PProd 0 F) k)
+    <|> (do searchPProd d2 (.proj ``PProd 1 F) k)
+  | .app (.app (.const `And _) d1) d2 =>
+        (do searchPProd d1 (.proj `And 0 F) k)
+    <|> (do searchPProd d2 (.proj `And 1 F) k)
+  | .const `PUnit _
+  | .const `True _ => throwToBelowFailed
+  | _ => k e F
+
+/-- See `toBelow` -/
+private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : Expr) : MetaM Expr := do
+  trace[Elab.definition.structural] "belowDict start:{indentExpr belowDict}\narg:{indentExpr arg}"
+  -- First search through the PProd packing of the different `brecOn` motives
+  searchPProd belowDict F fun belowDict F => do
+    trace[Elab.definition.structural] "belowDict step 1:{indentExpr belowDict}"
+    -- Then instantiate parameters of a reflexive type, if needed
+    forallTelescopeReducing belowDict fun xs belowDict => do
+      let arg ← zetaReduce arg
+      let argArgs := arg.getAppArgs
+      unless argArgs.size >= xs.size do throwToBelowFailed
+      let n := argArgs.size
+      let argTailArgs := argArgs.extract (n - xs.size) n
+      let belowDict := belowDict.replaceFVars xs argTailArgs
+      -- And again search through the PProd packing due to multiple functions recursing on the
+      -- same inductive data type
+      -- (We could use the funIdx and the `positions` array to replace this search with more
+      -- targeted indexing.)
+      searchPProd belowDict (mkAppN F argTailArgs) fun belowDict F => do
+        trace[Elab.definition.structural] "belowDict step 2:{indentExpr belowDict}"
+        match belowDict with
+        | .app belowDictFun belowDictArg =>
+          unless belowDictFun.getAppFn == C do throwToBelowFailed
+          unless ← isDefEq belowDictArg arg do throwToBelowFailed
+          pure F
+        | _ =>
+          trace[Elab.definition.structural] "belowDict not an app:{indentExpr belowDict}"
+          throwToBelowFailed
+
+/-- See `toBelow` -/
+private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
+    (positions : Positions) (k : Array Expr → Expr → MetaM α) : MetaM α := do
+  let numTypeFormers := positions.size
+  let belowType ← inferType below
+  trace[Elab.definition.structural] "belowType: {belowType}"
+  unless (← isTypeCorrect below) do
+    trace[Elab.definition.structural] "not type correct!"
+  belowType.withApp fun f args => do
+    unless numIndParams + numTypeFormers < args.size do
+      trace[Elab.definition.structural] "unexpected 'below' type{indentExpr belowType}"
+      throwToBelowFailed
+    let params := args[*...numIndParams]
+    let finalArgs := args[(numIndParams+numTypeFormers)...*]
+    let pre := mkAppN f params
+    let motiveTypes ← inferArgumentTypesN numTypeFormers pre
+    let numMotives : Nat := positions.numIndices
+    trace[Elab.definition.structural] "numMotives: {numMotives}"
+    let mut CTypes := Array.replicate numMotives (.sort 37) -- dummy value
+    for poss in positions, motiveType in motiveTypes do
+      for pos in poss do
+        CTypes := CTypes.set! pos motiveType
+    let CDecls : Array (Name × (Array Expr → MetaM Expr)) ← CTypes.mapM fun t => do
+        return ((← mkFreshUserName `C), fun _ => pure t)
+    withLocalDeclsD CDecls fun Cs => do
+      -- We have to pack these canary motives like we packed the real motives
+      let packedCs ← positions.mapMwith PProdN.packLambdas motiveTypes Cs
+      let belowDict := mkAppN pre packedCs
+      let belowDict := mkAppN belowDict finalArgs
+      trace[Elab.definition.structural] "initial belowDict for {Cs}:{indentExpr belowDict}"
+      unless (← isTypeCorrect belowDict) do
+        trace[Elab.definition.structural] "not type correct!"
+      k Cs belowDict
+
+/--
+  `below` is a free variable with type of the form `I.below indParams motive indices major`,
+  where `I` is the name of an inductive datatype.
+
+  For example, when trying to show that the following function terminates using structural recursion
+  ```lean
+  def addAdjacent : List Nat → List Nat
+  | []       => []
+  | [a]      => [a]
+  | a::b::as => (a+b) :: addAdjacent as
+  ```
+  when we are visiting `addAdjacent as` at `replaceRecApps`, `below` has type
+  `@List.below Nat (fun (x : List Nat) => List Nat) (a::b::as)`
+  The motive `fun (x : List Nat) => List Nat` depends on the actual function we are trying to compute.
+  So, we first replace it with a fresh variable `C` at `withBelowDict`.
+  Recall that `brecOn` implements course-of-values recursion, and `below` can be viewed as a dictionary
+  of the "previous values".
+  We search this dictionary using the auxiliary function `toBelowAux`.
+  The dictionary is built using the `PProd` (`And` for inductive predicates).
+  We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`.  -/
+private partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr := do
+  withTraceNode `Elab.definition.structural (return m!"{exceptEmoji ·} searching IH for {recArg} in {←inferType below}") do
+    withBelowDict below numIndParams positions fun Cs belowDict =>
+      toBelowAux Cs[fnIndex]! belowDict recArg below
+
+private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
+    (below : Expr) (e : Expr) : M Expr :=
+  let recFnNames := recArgInfos.map (·.fnName)
+  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) M Bool :=
+    modifyGet (·.contains e)
+  let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
+    if !(← containsRecFn e) then
+      return e
+    match e with
+    | Expr.lam n d b c =>
+      withLocalDecl n c (← loop below d) fun x => do
+        mkLambdaFVars #[x] (← loop below (b.instantiate1 x))
+    | Expr.forallE n d b c =>
+      withLocalDecl n c (← loop below d) fun x => do
+        mkForallFVars #[x] (← loop below (b.instantiate1 x))
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do
+        loop below (body.instantiate1 x)
+    | Expr.mdata d b =>
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop below b
+      else
+        return mkMData d (← loop below b)
+    | Expr.proj n i e => return mkProj n i (← loop below e)
+    | Expr.app _ _ =>
+      let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr :=
+        e.withApp fun f args => do
+          if let .some fnIdx := recArgInfos.findFinIdx? (f.isConstOf ·.fnName) then
+            let recArgInfo := recArgInfos[fnIdx]
+            let some recArg := args[recArgInfo.recArgPos]?
+              | throwError "insufficient number of parameters at recursive application {indentExpr e}"
+            -- For reflexive type, we may have nested recursive applications in recArg
+            let recArg ← loop below recArg
+            let f ←
+              try toBelow below recArgInfo.indGroupInst.params.size positions fnIdx recArg
+              catch _ => throwError "failed to eliminate recursive application{indentExpr e}"
+            -- We don't pass the fixed parameters, the indices and the major arg to `f`, only the rest
+            let ys := recArgInfo.fixedParamPerm.pickVarying args
+            let (_, fArgs) := recArgInfo.pickIndicesMajor ys
+            let fArgs ← fArgs.mapM (replaceRecApps recArgInfos positions below ·)
+            return mkAppN f fArgs
+          else
+            return mkAppN (← loop below f) (← args.mapM (loop below))
+      match (← matchMatcherApp? (alsoCasesOn := true) e) with
+      | some matcherApp =>
+        if recArgInfos.all (fun recArgInfo => !recArgHasLooseBVarsAt recArgInfo.fnName recArgInfo.recArgPos e) then
+          processApp e
+        else
+          /- Here is an example we currently do not handle
+             ```
+             def g (xs : List Nat) : Nat :=
+             match xs with
+             | [] => 0
+             | y::ys =>
+               match ys with
+               | []       => 1
+               | _::_::zs => g zs + 1
+               | zs       => g ys + 2
+             ```
+             We are matching on `ys`, but still using `ys` in the third alternative.
+             If we push the `below` argument over the dependent match it will be able to eliminate recursive call using `zs`.
+             To make it work, users have to write the third alternative as `| zs => g zs + 2`
+             If this is too annoying in practice, we may replace `ys` with the matching term, but
+             this may generate weird error messages, when it doesn't work. -/
+          trace[Elab.definition.structural] "below before matcherApp.addArg: {below} : {← inferType below}"
+          if let some matcherApp ← matcherApp.addArg? below then
+            let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
+              lambdaBoundedTelescope alt numParams fun xs altBody => do
+                trace[Elab.definition.structural] "altNumParams: {numParams}, xs: {xs}"
+                unless xs.size = numParams do
+                  throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
+                let belowForAlt := xs[numParams - 1]!
+                mkLambdaFVars xs (← loop belowForAlt altBody)
+            pure { matcherApp with alts := altsNew }.toExpr
+          else
+            processApp e
+      | none => processApp e
+    | e =>
+      ensureNoRecFn recFnNames e
+      pure e
+  loop below e |>.run' {}
+
+/--
+Calculates the `.brecOn` motive corresponding to one structural recursive function.
+The `value` is the function with (only) the fixed parameters moved into the context.
+-/
+def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
+  lambdaTelescope value fun xs value => do
+    let type  := (← inferType value).headBeta
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let motive ← mkForallFVars otherArgs type
+    mkLambdaFVars indexMajorArgs motive
+
+/--
+Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
+The `value` is the function with (only) the fixed parameters moved into the context,
+The `FType` is the expected type of the argument.
+The `recArgInfos` is used to transform the body of the function to replace recursive calls with
+uses of the `below` induction hypothesis.
+-/
+def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
+    (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
+  lambdaTelescope value fun xs value => do
+    let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let FType ← instantiateForall FType indicesMajorArgs
+    forallBoundedTelescope FType (some 1) fun below _ => do
+      -- TODO: `below` user name is `f`, and it will make a global `f` to be pretty printed as `_root_.f` in error messages.
+      -- We should add an option to `forallBoundedTelescope` to ensure fresh names are used.
+      let below := below[0]!
+      let valueNew ← replaceRecApps recArgInfos positions below value
+      mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
+
+/--
+Given the `motives`, pass the right universe levels, the parameters, and the motives.
+It was already checked earlier in `checkCodomainsLevel` that the functions live in the same universe.
+-/
+def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
+   (motives : Array Expr) : MetaM (Nat → Expr) := do
+  let indGroup := recArgInfos[0]!.indGroupInst
+  let motive := motives[0]!
+  let brecOnUniv ← lambdaTelescope motive fun _ type => getLevel type
+  let brecOnCons := fun idx => indGroup.brecOn brecOnUniv idx
+  -- Pick one as a prototype
+  let brecOnAux := brecOnCons 0
+  -- Infer the type of the packed motive arguments
+  let packedMotiveTypes ← inferArgumentTypesN indGroup.numMotives brecOnAux
+  let packedMotives ← positions.mapMwith PProdN.packLambdas packedMotiveTypes motives
+
+  return fun n => mkAppN (brecOnCons n) packedMotives
+
+/--
+Given the `recArgInfos` and the `motives`, infer the types of the `F` arguments to the `.brecOn`
+combinators. This assumes that all `.brecOn` functions of a mutual inductive have the same structure.
+
+It also undoes the permutation and packing done by `packMotives`
+-/
+def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
+    (brecOnConst : Nat → Expr) : MetaM (Array Expr) := do
+  let numTypeFormers := positions.size
+  let recArgInfo := recArgInfos[0]! -- pick an arbitrary one
+  let brecOn := brecOnConst recArgInfo.indIdx
+  check brecOn
+  let brecOnType ← inferType brecOn
+  -- Skip the indices and major argument
+  let packedFTypes ← forallBoundedTelescope brecOnType (some (recArgInfo.indicesPos.size + 1)) fun _ brecOnType =>
+    -- And return the types of the next arguments
+    arrowDomainsN numTypeFormers brecOnType
+
+  let mut FTypes := Array.replicate positions.numIndices (Expr.sort 0)
+  for packedFType in packedFTypes, poss in positions do
+    for pos in poss do
+      FTypes := FTypes.set! pos packedFType
+  return FTypes
+
+/--
+Completes the `.brecOn` for the given function.
+The `value` is the function with (only) the fixed parameters moved into the context.
+-/
+def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Expr)
+    (FArgs : Array Expr) (recArgInfo : RecArgInfo) (value : Expr) : MetaM Expr := do
+  lambdaTelescope value fun ys _value => do
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor ys
+    let brecOn := brecOnConst recArgInfo.indIdx
+    let brecOn := mkAppN brecOn indexMajorArgs
+    let packedFTypes ← inferArgumentTypesN positions.size brecOn
+    let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
+    let brecOn := mkAppN brecOn packedFArgs
+    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.finIdxOf? fnIdx
+      | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
+    let brecOn ← PProdN.projM size idx brecOn
+    mkLambdaFVars ys (mkAppN brecOn otherArgs)
+
+end Lean.Elab.Structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/Basic.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Meta.Basic
+import Lean.Meta.ForEachExpr
+
+namespace Lean.Elab.Structural
+
+structure State where
+  /-- As part of the inductive predicates case, we keep adding more and more discriminants from the
+     local context and build up a bigger matcher application until we reach a fixed point.
+     As a side-effect, this creates matchers. Here we capture all these side-effects, because
+     the construction rolls back any changes done to the environment and the side-effects
+     need to be replayed. -/
+  addMatchers : Array (MetaM Unit) := #[]
+
+abbrev M := StateRefT State MetaM
+
+instance : Inhabited (M α) where
+  default := throwError "failed"
+
+def run (x : M α) (s : State := {}) : MetaM (α × State) :=
+  StateRefT'.run x s
+
+/--
+  Return true iff `e` contains an application `recFnName .. t ..` where the term `t` is
+  the argument we are trying to recurse on, and it contains loose bound variables.
+
+  We use this test to decide whether we should process a matcher-application as a regular
+  application or not. That is, whether we should push the `below` argument should be affected by the matcher or not.
+  If `e` does not contain an application of the form `recFnName .. t ..`, then we know
+  the recursion doesn't depend on any pattern variable in this matcher.
+-/
+def recArgHasLooseBVarsAt (recFnName : Name) (recArgPos : Nat) (e : Expr) : Bool :=
+  let app?   := e.find? fun e =>
+     e.isAppOf recFnName && e.getAppNumArgs > recArgPos && (e.getArg! recArgPos).hasLooseBVars
+  app?.isSome
+
+
+/--
+Lets say we have `n` mutually recursive functions whose recursive arguments are from a group
+of `m` mutually inductive data types. This mapping does not have to be one-to-one: for one type
+there can be zero, one or more functions. We use the logic in the `FunPacker` modules to combine
+the bodies (and motives) of multiple such functions.
+
+Therefore we have to take the `n` functions, group them by their recursive argument's type,
+and for each such type, keep track of the order of the functions.
+
+We represent these positions as an `Array (Array Nat)`. We have that
+
+* `positions.size = indInfo.numTypeFormers`
+* `positions.flatten` is a permutation of `[0:n]`, so each of the `n` functions has exactly one
+  position, and each position refers to one of the `n` functions.
+* if `k ∈ positions[i]` then the recursive argument of function `k` is has type `indInfo.all[i]`
+  (or corresponding nested inductive type)
+
+-/
+abbrev Positions := Array (Array Nat)
+
+/--
+The number of indices in the array.
+-/
+def Positions.numIndices (positions : Positions) : Nat :=
+    positions.foldl (fun s poss => s + poss.size) 0
+
+/--
+`positions.inverse[k] = i` means that function `i` has type k
+-/
+def Positions.inverse (positions : Positions) : Array Nat := Id.run do
+  let mut r := .replicate positions.numIndices 0
+  for _h : i in [:positions.size] do
+    for k in positions[i] do
+      r := r.set! k i
+  return r
+
+/--
+Groups the `xs` by their `f` value, and puts these groups into the order given by `ys`.
+-/
+def Positions.groupAndSort {α β} [Inhabited α] [DecidableEq β]
+    (f : α → β) (xs : Array α) (ys : Array β) : Positions :=
+  let positions := ys.map fun y => (Array.range xs.size).filter fun i => f xs[i]! = y
+  -- Sanity check: is this really a grouped permutation of all the indices?
+  assert! Array.range xs.size == positions.flatten.qsort Nat.blt
+  positions
+
+/--
+Let `positions.size = ys.size` and `positions.numIndices = xs.size`. Maps `f` over each `y` in `ys`,
+also passing in those elements `xs` that belong to that are those elements of `xs` that belong to
+`y` according to `positions`.
+-/
+def Positions.mapMwith {α β m} [Monad m] [Inhabited β] (f : α → Array β → m γ)
+    (positions : Positions) (ys : Array α) (xs : Array β) : m (Array γ) := do
+  assert! positions.size = ys.size
+  assert! positions.numIndices = xs.size
+  (Array.zip ys positions).mapM fun ⟨y, poss⟩ => f y (poss.map (xs[·]!))
+
+end Lean.Elab.Structural
+
+builtin_initialize
+  Lean.registerTraceClass `Elab.definition.structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Eqns
+import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.Simp.Main
+import Lean.Meta.Tactic.Apply
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Eqns
+import Lean.Elab.PreDefinition.FixedParams
+import Lean.Elab.PreDefinition.Structural.Basic
+
+namespace Lean.Elab
+open Meta
+open Eqns
+
+namespace Structural
+
+structure EqnInfo extends EqnInfoCore where
+  recArgPos : Nat
+  declNames : Array Name
+  fixedParamPerms : FixedParamPerms
+  deriving Inhabited
+
+private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
+  withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
+    withNewMCtxDepth do
+      let main ← mkFreshExprSyntheticOpaqueMVar type
+      let (_, mvarId) ← main.mvarId!.intros
+      unless (← tryURefl mvarId) do -- catch easy cases
+        go (← deltaLHS mvarId)
+      instantiateMVars main
+where
+  go (mvarId : MVarId) : MetaM Unit := do
+    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
+      if (← tryURefl mvarId) then
+        trace[Elab.definition.structural.eqns] "tryURefl succeeded"
+        return ()
+      else if (← tryContradiction mvarId) then
+        trace[Elab.definition.structural.eqns] "tryContadiction succeeded"
+        return ()
+      else if let some mvarId ← whnfReducibleLHS? mvarId then
+        trace[Elab.definition.structural.eqns] "whnfReducibleLHS succeeded"
+        go mvarId
+      else if let some mvarId ← simpMatch? mvarId then
+        trace[Elab.definition.structural.eqns] "simpMatch? succeeded"
+        go mvarId
+      else if let some mvarId ← simpIf? mvarId then
+        trace[Elab.definition.structural.eqns] "simpIf? succeeded"
+        go mvarId
+      else
+        let ctx ← Simp.mkContext
+        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+        | TacticResultCNM.closed =>
+          trace[Elab.definition.structural.eqns] "simpTargetStar closed the goal"
+        | TacticResultCNM.modified mvarId =>
+          trace[Elab.definition.structural.eqns] "simpTargetStar modified the goal"
+          go mvarId
+        | TacticResultCNM.noChange =>
+          if let some mvarId ← deltaRHS? mvarId declName then
+            trace[Elab.definition.structural.eqns] "deltaRHS? succeeded"
+            go mvarId
+          else if let some mvarIds ← casesOnStuckLHS? mvarId then
+            trace[Elab.definition.structural.eqns] "casesOnStuckLHS? succeeded"
+            mvarIds.forM go
+          else if let some mvarIds ← splitTarget? mvarId then
+            trace[Elab.definition.structural.eqns] "splitTarget? succeeded"
+            mvarIds.forM go
+          else
+            throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+
+def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
+  withOptions (tactic.hygienic.set · false) do
+  let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
+    let us := info.levelParams.map mkLevelParam
+    let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
+    let goal ← mkFreshExprSyntheticOpaqueMVar target
+    mkEqnTypes info.declNames goal.mvarId!
+  let mut thmNames := #[]
+  for h : i in [: eqnTypes.size] do
+    let type := eqnTypes[i]
+    trace[Elab.definition.structural.eqns] "eqnType {i+1}: {type}"
+    let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}"
+    thmNames := thmNames.push name
+    -- determinism: `type` should be independent of the environment changes since `baseName` was
+    -- added
+    realizeConst info.declNames[0]! name (doRealize name type)
+  return thmNames
+where
+  doRealize name type := withOptions (tactic.hygienic.set · false) do
+    let value ← mkProof info.declName type
+    let (type, value) ← removeUnusedEqnHypotheses type value
+    let type ← letToHave type
+    addDecl <| Declaration.thmDecl {
+      name, type, value
+      levelParams := info.levelParams
+    }
+    inferDefEqAttr name
+
+builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
+
+def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
+    (fixedParamPerms : FixedParamPerms) : CoreM Unit := do
+  ensureEqnReservedNamesAvailable preDef.declName
+  modifyEnv fun env => eqnInfoExt.insert env preDef.declName
+    { preDef with recArgPos, declNames, fixedParamPerms }
+
+def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
+  if let some info := eqnInfoExt.find? (← getEnv) declName then
+    mkEqns info
+  else
+    return none
+
+/-- Generate the "unfold" lemma for `declName`. -/
+def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
+  let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
+  realizeConst info.declNames[0]! name (doRealize name)
+  return name
+where
+  doRealize name := withOptions (tactic.hygienic.set · false) do
+    lambdaTelescope info.value fun xs body => do
+      let us := info.levelParams.map mkLevelParam
+      let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
+      let goal ← mkFreshExprSyntheticOpaqueMVar type
+      mkUnfoldProof declName goal.mvarId!
+      let type ← mkForallFVars xs type
+      let type ← letToHave type
+      let value ← mkLambdaFVars xs (← instantiateMVars goal)
+      addDecl <| Declaration.thmDecl {
+        name, type, value
+        levelParams := info.levelParams
+      }
+      inferDefEqAttr name
+
+def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
+  if let some info := eqnInfoExt.find? (← getEnv) declName then
+    return some (← mkUnfoldEq declName info)
+  else
+    return none
+
+@[export lean_get_structural_rec_arg_pos]
+def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
+  let some info := eqnInfoExt.find? (← getEnv) declName | return none
+  return some info.recArgPos
+
+builtin_initialize
+  registerGetEqnsFn getEqnsFor?
+  registerGetUnfoldEqnFn getUnfoldFor?
+  registerTraceClass `Elab.definition.structural.eqns
+
+end Structural
+end Lean.Elab

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -0,0 +1,281 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Elab.PreDefinition.TerminationMeasure
+import Lean.Elab.PreDefinition.FixedParams
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Elab.PreDefinition.Structural.RecArgInfo
+
+namespace Lean.Elab.Structural
+open Meta
+
+def prettyParam (xs : Array Expr) (i : Nat) : MetaM MessageData := do
+  let x := xs[i]!
+  let n ← x.fvarId!.getUserName
+  addMessageContextFull <| if n.hasMacroScopes then m!"#{i+1}" else m!"{x}"
+
+def prettyRecArg (xs : Array Expr) (value : Expr) (recArgInfo : RecArgInfo) : MetaM MessageData := do
+  lambdaTelescope value fun ys _ => prettyParam (xs ++ ys) recArgInfo.recArgPos
+
+def prettyParameterSet (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
+    (recArgInfos : Array RecArgInfo) : MetaM MessageData := do
+  if fnNames.size = 1 then
+    return m!"parameter " ++ (← prettyRecArg xs values[0]! recArgInfos[0]!)
+  else
+    let mut l := #[]
+    for fnName in fnNames, value in values, recArgInfo in recArgInfos do
+      l := l.push m!"{(← prettyRecArg xs value recArgInfo)} of {fnName}"
+    return m!"parameters " ++ .andList l.toList
+
+private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := Id.run do
+  let mut minPos := xs.size
+  for index in indices do
+    match xs.idxOf? index with
+    | some pos => if pos < minPos then minPos := pos
+    | _        => pure ()
+  return minPos
+
+-- Indices can only depend on other indices
+private def hasBadIndexDep? (ys : Array Expr) (indices : Array Expr) : MetaM (Option (Expr × Expr)) := do
+  for index in indices do
+    let indexType ← inferType index
+    for y in ys do
+      if !indices.contains y && (← dependsOn indexType y.fvarId!) then
+        return some (index, y)
+  return none
+
+-- Inductive datatype parameters cannot depend on ys
+private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (Option (Expr × Expr)) := do
+  for p in indParams do
+    for y in ys do
+      if ← dependsOn p y.fvarId! then
+        return some (p, y)
+  return none
+
+/--
+Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
+various sanity checks on the parameter (is it even of inductive type etc).
+-/
+def getRecArgInfo (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do
+  assert! fixedParamPerm.size = xs.size
+  if h : i < xs.size then
+    if fixedParamPerm.isFixed i then
+      throwError "it is unchanged in the recursive calls"
+    let x := xs[i]
+    let localDecl ← getFVarLocalDecl x
+    if localDecl.isLet then
+      throwError "it is a let-binding"
+    let xType ← whnfD localDecl.type
+    matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
+    let indArgs    : Array Expr := xType.getAppArgs
+    let indParams  : Array Expr := indArgs[*...indInfo.numParams]
+    let indIndices : Array Expr := indArgs[indInfo.numParams...*]
+    if !indIndices.all Expr.isFVar then
+      throwError "its type {indInfo.name} is an inductive family and indices are not variables{indentExpr xType}"
+    else if !indIndices.allDiff then
+      throwError "its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+    else
+      let ys := fixedParamPerm.pickVarying xs
+      match (← hasBadIndexDep? ys indIndices) with
+      | some (index, y) =>
+        throwError "its type {indInfo.name} is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
+      | none =>
+        match (← hasBadParamDep? ys indParams) with
+        | some (indParam, y) =>
+          throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich is not fixed."
+        | none =>
+          let indAll := indInfo.all.toArray
+          let .some indIdx := indAll.idxOf? indInfo.name | panic! "{indInfo.name} not in {indInfo.all}"
+          let indicesPos := indIndices.map fun index => match xs.idxOf? index with | some i => i | none => unreachable!
+          let indGroupInst := {
+            IndGroupInfo.ofInductiveVal indInfo with
+            levels := us
+            params := indParams }
+          return { fnName       := fnName
+                   fixedParamPerm := fixedParamPerm
+                   recArgPos    := i
+                   indicesPos   := indicesPos
+                   indGroupInst := indGroupInst
+                   indIdx       := indIdx }
+  else
+    throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
+
+/--
+Collects the `RecArgInfos` for one function, and returns a report for why the others were not
+considered.
+
+The `xs` are the fixed parameters, `value` the body with the fixed prefix instantiated.
+
+Takes the optional user annotation into account (`termMeasure?`). If this is given and the measure
+is unsuitable, throw an error.
+-/
+def getRecArgInfos (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr)
+    (value : Expr) (termMeasure? : Option TerminationMeasure) : MetaM (Array RecArgInfo × MessageData) := do
+  lambdaTelescope value fun ys _ => do
+    if let .some termMeasure := termMeasure? then
+      -- User explicitly asked to use a certain measure, so throw errors eagerly
+      let recArgInfo ← withRef termMeasure.ref do
+        prependError m!"cannot use specified measure for structural recursion:" do
+          let args := fixedParamPerm.buildArgs xs ys
+          getRecArgInfo fnName fixedParamPerm args (← termMeasure.structuralArg)
+      return (#[recArgInfo], m!"")
+    else
+      let args := fixedParamPerm.buildArgs xs ys
+      let mut recArgInfos := #[]
+      let mut report : MessageData := m!""
+      -- No `termination_by`, so try all, and remember the errors
+      for idx in [:args.size] do
+        try
+          let recArgInfo ← getRecArgInfo fnName fixedParamPerm args idx
+          recArgInfos := recArgInfos.push recArgInfo
+        catch e =>
+          report := report ++ (m!"Not considering parameter {← prettyParam args idx} of {fnName}:" ++
+            indentD e.toMessageData) ++ "\n"
+      trace[Elab.definition.structural] "getRecArgInfos report: {report}"
+      return (recArgInfos, report)
+
+
+/--
+Reorders the `RecArgInfos` of one function to put arguments that are indices of other arguments
+last.
+See issue #837 for an example where we can show termination using the index of an inductive family, but
+we don't get the desired definitional equalities.
+-/
+def nonIndicesFirst (recArgInfos : Array RecArgInfo) : Array RecArgInfo := Id.run do
+  let mut indicesPos : Std.HashSet Nat := {}
+  for recArgInfo in recArgInfos do
+    for pos in recArgInfo.indicesPos do
+      indicesPos := indicesPos.insert pos
+  let (indices,nonIndices) := recArgInfos.partition (indicesPos.contains ·.recArgPos)
+  return nonIndices ++ indices
+
+private def dedup [Monad m] (eq : α → α → m Bool) (xs : Array α) : m (Array α) := do
+  let mut ret := #[]
+  for x in xs do
+    unless (← ret.anyM (eq · x)) do
+      ret := ret.push x
+  return ret
+
+/--
+Given the `RecArgInfo`s of all the recursive functions, find the inductive groups to consider.
+-/
+def inductiveGroups (recArgInfos : Array RecArgInfo) : MetaM (Array IndGroupInst) :=
+  dedup IndGroupInst.isDefEq (recArgInfos.map (·.indGroupInst))
+
+/--
+Filters the `recArgInfos` by those that describe an argument that's part of the recursive inductive
+group `group`.
+
+Because of nested inductives this function has the ability to change the `recArgInfo`.
+Consider
+```
+inductive Tree where | node : List Tree → Tree
+```
+then when we look for arguments whose type is part of the group `Tree`, we want to also consider
+the argument of type `List Tree`, even though that argument’s `RecArgInfo` refers to initially to
+`List`.
+-/
+def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr)
+    (recArgInfos : Array RecArgInfo) : MetaM (Array RecArgInfo) := do
+
+  let nestedTypeFormers ← group.nestedTypeFormers
+
+  recArgInfos.filterMapM fun recArgInfo => do
+    -- Is this argument from the same mutual group of inductives?
+    if (← group.isDefEq recArgInfo.indGroupInst) then
+      return (.some recArgInfo)
+
+    -- Can this argument be understood as the auxiliary type former of a nested inductive?
+    if nestedTypeFormers.isEmpty then return .none
+    lambdaTelescope value fun ys _ => do
+      let x := (xs++ys)[recArgInfo.recArgPos]!
+      for nestedTypeFormer in nestedTypeFormers, indIdx in [group.all.size : group.numMotives] do
+        let xType ← whnfD (← inferType x)
+        let (indIndices, _, type) ← forallMetaTelescope nestedTypeFormer
+        if (← isDefEqGuarded type xType) then
+          let indIndices ← indIndices.mapM instantiateMVars
+          if !indIndices.all Expr.isFVar then
+            -- throwError "indices are not variables{indentExpr xType}"
+            continue
+          if !indIndices.allDiff then
+            -- throwError "indices are not pairwise distinct{indentExpr xType}"
+            continue
+          -- TODO: Do we have to worry about the indices ending up in the fixed prefix here?
+          if let some (_index, _y) ← hasBadIndexDep? ys indIndices then
+            -- throwError "its type {indInfo.name} is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
+            continue
+          let indicesPos := indIndices.map fun index => match (xs++ys).idxOf? index with | some i => i | none => unreachable!
+          return .some
+            { fnName       := recArgInfo.fnName
+              fixedParamPerm  := recArgInfo.fixedParamPerm
+              recArgPos    := recArgInfo.recArgPos
+              indicesPos   := indicesPos
+              indGroupInst := group
+              indIdx       := indIdx }
+      return .none
+
+def maxCombinationSize : Nat := 10
+
+def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
+  if xss.foldl (· * ·.size) 1 > maxCombinationSize then
+    none
+  else
+    let rec go i acc : Array (Array α):=
+      if h : i < xss.size then
+        xss[i].flatMap fun x => go (i + 1) (acc.push x)
+      else
+        #[acc]
+    some (go 0 #[])
+
+
+def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
+   (values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do
+  let mut report := m!""
+  -- Gather information on all possible recursive arguments
+  let mut recArgInfoss := #[]
+  for fnName in fnNames, value in values, termMeasure? in termMeasure?s, fixedParamPerm in fixedParamPerms.perms do
+    let (recArgInfos, thisReport) ← getRecArgInfos fnName fixedParamPerm xs value termMeasure?
+    report := report ++ thisReport
+    recArgInfoss := recArgInfoss.push recArgInfos
+  -- Put non-indices first
+  recArgInfoss := recArgInfoss.map nonIndicesFirst
+  trace[Elab.definition.structural] "recArgInfos:{indentD (.joinSep (recArgInfoss.flatten.toList.map (repr ·)) Format.line)}"
+  -- Inductive groups to consider
+  let groups ← inductiveGroups recArgInfoss.flatten
+  trace[Elab.definition.structural] "inductive groups: {groups}"
+  if groups.isEmpty then
+    report := report ++ "no parameters suitable for structural recursion"
+  -- Consider each group
+  for group in groups do
+    -- Select those RecArgInfos that are compatible with this inductive group
+    let mut recArgInfoss' := #[]
+    for value in values, recArgInfos in recArgInfoss do
+      recArgInfoss' := recArgInfoss'.push (← argsInGroup group xs value recArgInfos)
+    if let some idx := recArgInfoss'.findIdx? (·.isEmpty) then
+      report := report ++ m!"Skipping arguments of type {group}, as {fnNames[idx]!} has no compatible argument.\n"
+      continue
+    if let some combs := allCombinations recArgInfoss' then
+      for comb in combs do
+        try
+          -- Check that the group actually has a brecOn (we used to check this in getRecArgInfo,
+          -- but in the first phase we do not want to rule-out non-recursive types like `Array`, which
+          -- are ok in a nested group. This logic can maybe simplified)
+          unless (← hasConst (group.brecOnName 0)) do
+            throwError "the type {group} does not have a `.brecOn` recursor"
+          let r ← k comb
+          trace[Elab.definition.structural] "tryAllArgs report:\n{report}"
+          return r
+        catch e =>
+          let m ← prettyParameterSet fnNames xs values comb
+          report := report ++ m!"Cannot use {m}:{indentD e.toMessageData}\n"
+    else
+          report := report ++ m!"Too many possible combinations of parameters of type {group} (or " ++
+            m!"please indicate the recursive argument explicitly using `termination_by structural`).\n"
+  report := m!"failed to infer structural recursion:\n" ++ report
+  trace[Elab.definition.structural] "tryAllArgs:\n{report}"
+  throwError report
+
+end Lean.Elab.Structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Lean.Meta.InferType
+
+/-!
+This module contains the types
+* `IndGroupInfo`, a variant of `InductiveVal` with information that
+   applies to a whole group of mutual inductives and
+* `IndGroupInst` which extends `IndGroupInfo` with levels and parameters
+   to indicate a instantiation of the group.
+
+One purpose of this abstraction is to make it clear when a function operates on a group as
+a whole, rather than a specific inductive within the group.
+-/
+
+namespace Lean.Elab.Structural
+open Lean Meta
+
+/--
+A mutually inductive group, identified by the `all` array of the `InductiveVal` of its
+constituents.
+-/
+structure IndGroupInfo where
+  all       : Array Name
+  numNested : Nat
+deriving BEq, Inhabited, Repr
+
+def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
+  all       := indInfo.all.toArray
+  numNested := indInfo.numNested
+
+def IndGroupInfo.numMotives (group : IndGroupInfo) : Nat :=
+  group.all.size + group.numNested
+
+/-- Instantiates the right `.brecOn` for the given type former index,
+including universe parameters and fixed prefix.  -/
+partial def IndGroupInfo.brecOnName (info : IndGroupInfo) (idx : Nat) : Name :=
+  if let .some n := info.all[idx]? then
+      mkBRecOnName n
+    else
+      let j := idx - info.all.size + 1
+      info.brecOnName 0 |>.appendIndexAfter j
+
+/--
+An instance of an mutually inductive group of inductives, identified by the `all` array
+and the level and expressions parameters.
+
+For example this distinguishes between `List α` and `List β` so that we will not even attempt
+mutual structural recursion on such incompatible types.
+-/
+structure IndGroupInst extends IndGroupInfo where
+  levels    : List Level
+  params    : Array Expr
+deriving Inhabited, Repr
+
+def IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData :=
+  mkAppN (.const igi.all[0]! igi.levels) igi.params
+
+instance : ToMessageData IndGroupInst where
+  toMessageData := IndGroupInst.toMessageData
+
+def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do
+  unless igi1.toIndGroupInfo == igi2.toIndGroupInfo do return false
+  unless igi1.levels.length = igi2.levels.length do return false
+  unless (igi1.levels.zip igi2.levels).all (fun (l₁, l₂) => Level.isEquiv l₁ l₂) do return false
+  unless igi1.params.size = igi2.params.size do return false
+  unless (← (igi1.params.zip igi2.params).allM (fun (e₁, e₂) => Meta.isDefEqGuarded e₁ e₂)) do return false
+  return true
+
+/-- Instantiates the right `.brecOn` for the given type former index,
+including universe parameters and fixed prefix.  -/
+def IndGroupInst.brecOn (group : IndGroupInst) (lvl : Level) (idx : Nat) : Expr :=
+  let n := group.brecOnName idx
+  let us := lvl :: group.levels
+  mkAppN (.const n us) group.params
+
+/--
+Figures out the nested type formers of an inductive group, with parameters instantiated
+and indices still forall-abstracted.
+
+For example given a nested inductive
+```
+inductive Tree α where | node : α → Vector (Tree α) n → Tree α
+```
+(where `n` is an index of `Vector`) and the instantiation `Tree Int` it will return
+```
+#[(n : Nat) → Vector (Tree Int) n]
+```
+
+-/
+def IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr) := do
+  if igi.numNested = 0 then return #[]
+  -- We extract this information from the motives of the recursor
+  let recName := mkRecName igi.all[0]!
+  let recInfo ← getConstInfoRec recName
+  assert! recInfo.numMotives = igi.numMotives
+  let aux := mkAppN (.const recName (0 :: igi.levels)) igi.params
+  let motives ← inferArgumentTypesN recInfo.numMotives aux
+  let auxMotives : Array Expr := motives[igi.all.size...*]
+  auxMotives.mapM fun motive =>
+    forallTelescopeReducing motive fun xs _ => do
+      assert! xs.size > 0
+      mkForallFVars xs.pop (← inferType xs.back!)
+
+end Lean.Elab.Structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/IndPred.lean

@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dany Fabian
+-/
+prelude
+import Lean.Meta.IndPredBelow
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Elab.PreDefinition.Structural.RecArgInfo
+
+namespace Lean.Elab.Structural
+open Meta
+
+private def replaceIndPredRecApp (fixedParamPerm : FixedParamPerm) (funType : Expr) (e : Expr) : M Expr := do
+  withoutProofIrrelevance do
+  withTraceNode `Elab.definition.structural (fun _ => pure m!"eliminating recursive call {e}") do
+    -- We want to replace `e` with an expression of the same type
+    let main ← mkFreshExprSyntheticOpaqueMVar (← inferType e)
+    let args : Array Expr := e.getAppArgs
+    let ys := fixedParamPerm.pickVarying args
+    let lctx ← getLCtx
+    let r ← lctx.anyM fun localDecl => do
+      if localDecl.isAuxDecl then return false
+      let (mvars, _, t) ← forallMetaTelescope localDecl.type -- NB: do not reduce, we want to see the `funType`
+      unless t.getAppFn == funType do return false
+      withTraceNodeBefore `Elab.definition.structural (do pure m!"trying {mkFVar localDecl.fvarId} : {localDecl.type}") do
+        if ys.size < t.getAppNumArgs then
+          trace[Elab.definition.structural] "too few arguments, expected {t.getAppNumArgs}, found {ys.size}. Underapplied recursive call?"
+          return false
+        if (← (t.getAppArgs.zip ys).allM (fun (t,s) => isDefEq t s)) then
+          main.mvarId!.assign (mkAppN (mkAppN localDecl.toExpr mvars) ys[t.getAppNumArgs...*])
+          return ← mvars.allM fun v => do
+            unless (← v.mvarId!.isAssigned) do
+              trace[Elab.definition.structural] "Cannot use {mkFVar localDecl.fvarId}: parameter {v} remains unassigned"
+              return false
+            return true
+        trace[Elab.definition.structural] "Arguments do not match"
+        return false
+    unless r do
+      throwError "Could not eliminate recursive call {e}"
+    instantiateMVars main
+
+private partial def replaceIndPredRecApps (recArgInfo : RecArgInfo) (funType : Expr) (motive : Expr) (e : Expr) : M Expr := do
+  let rec loop (e : Expr) : M Expr := do
+    match e with
+    | Expr.lam n d b c =>
+      withLocalDecl n c (← loop d) fun x => do
+        mkLambdaFVars #[x] (← loop (b.instantiate1 x))
+    | Expr.forallE n d b c =>
+      withLocalDecl n c (← loop d) fun x => do
+        mkForallFVars #[x] (← loop (b.instantiate1 x))
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n (← loop type) (← loop val) (nondep := nondep) fun x => do
+        loop (body.instantiate1 x)
+    | Expr.mdata d b => do
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop b
+      else
+        return mkMData d (← loop b)
+    | Expr.proj n i e    => return mkProj n i (← loop e)
+    | Expr.app _ _ =>
+      let processApp (e : Expr) : M Expr := do
+        e.withApp fun f args => do
+          if f.isConstOf recArgInfo.fnName then
+            replaceIndPredRecApp recArgInfo.fixedParamPerm funType e
+          else
+            return mkAppN (← loop f) (← args.mapM loop)
+      match (← matchMatcherApp? e) with
+      | some matcherApp =>
+        if !recArgHasLooseBVarsAt recArgInfo.fnName recArgInfo.recArgPos e then
+          processApp e
+        else
+          trace[Elab.definition.structural] "matcherApp before adding below transformation:\n{matcherApp.toExpr}"
+          let rec addBelow (matcherApp : MatcherApp) : M Expr := do
+            if let some (t, idx) ← IndPredBelow.findBelowIdx matcherApp.discrs motive then
+              let (newApp, addMatcher) ← IndPredBelow.mkBelowMatcher matcherApp motive t idx
+              modify fun s => { s with addMatchers := s.addMatchers.push addMatcher }
+              let some newApp ← matchMatcherApp? newApp | throwError "not a matcherApp: {newApp}"
+              addBelow newApp
+            else pure matcherApp.toExpr
+
+          let newApp ← addBelow matcherApp
+          if newApp == matcherApp.toExpr then
+            throwError "could not add below discriminant"
+          else
+            trace[Elab.definition.structural] "modified matcher:\n{newApp}"
+            processApp newApp
+      | none => processApp e
+    | e =>
+      ensureNoRecFn #[recArgInfo.fnName] e
+      pure e
+  loop e
+
+/--
+Transform the body of a recursive function into a non-recursive one.
+
+The `value` is the function with (only) the fixed parameters instantiated.
+-/
+def mkIndPredBRecOn (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
+  lambdaTelescope value fun ys value => do
+    let type  := (← inferType value).headBeta
+    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor ys
+    trace[Elab.definition.structural] "indexMajorArgs: {indexMajorArgs}, otherArgs: {otherArgs}"
+    let funType ← mkLambdaFVars ys type
+    withLetDecl `funType (← inferType funType) funType fun funType => do
+      let motive ← mkForallFVars otherArgs (mkAppN funType ys)
+      let motive ← mkLambdaFVars indexMajorArgs motive
+      trace[Elab.definition.structural] "brecOn motive: {motive}"
+      let brecOn := Lean.mkConst (mkBRecOnName recArgInfo.indName!) recArgInfo.indGroupInst.levels
+      let brecOn := mkAppN brecOn recArgInfo.indGroupInst.params
+      let brecOn := mkApp brecOn motive
+      let brecOn := mkAppN brecOn indexMajorArgs
+      check brecOn
+      let brecOnType ← inferType brecOn
+      trace[Elab.definition.structural] "brecOn     {brecOn}"
+      trace[Elab.definition.structural] "brecOnType {brecOnType}"
+      -- we need to close the telescope here, because the local context is used:
+      -- The root cause was, that this copied code puts an ih : FType into the
+      -- local context and later, when we use the local context to build the recursive
+      -- call, it uses this ih. But that ih doesn't exist in the actual brecOn call.
+      -- That's why it must go.
+      let FType ← forallBoundedTelescope brecOnType (some 1) fun F _ => do
+        let F := F[0]!
+        let FType ← inferType F
+        trace[Elab.definition.structural] "FType: {FType}"
+        instantiateForall FType indexMajorArgs
+      forallBoundedTelescope FType (some 1) fun below _ => do
+        let below := below[0]!
+        let valueNew     ← replaceIndPredRecApps recArgInfo funType motive value
+        let Farg         ← mkLambdaFVars (indexMajorArgs ++ #[below] ++ otherArgs) valueNew
+        let brecOn       := mkApp brecOn Farg
+        let brecOn       := mkAppN brecOn otherArgs
+        let brecOn       ← mkLetFVars #[funType] brecOn
+        mkLambdaFVars ys brecOn
+
+end Lean.Elab.Structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Elab.PreDefinition.TerminationMeasure
+import Lean.Elab.PreDefinition.Mutual
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Elab.PreDefinition.Structural.FindRecArg
+import Lean.Elab.PreDefinition.Structural.Preprocess
+import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Elab.PreDefinition.Structural.IndPred
+import Lean.Elab.PreDefinition.Structural.Eqns
+import Lean.Elab.PreDefinition.Structural.SmartUnfolding
+import Lean.Meta.Tactic.TryThis
+
+namespace Lean.Elab
+namespace Structural
+open Meta
+
+private def getFixedPrefix (declName : Name) (xs : Array Expr) (value : Expr) : MetaM Nat := do
+  let numFixedRef ← IO.mkRef xs.size
+  forEachExpr' value fun e => do
+    if e.isAppOf declName then
+      let args := e.getAppArgs
+      numFixedRef.modify fun numFixed => if args.size < numFixed then args.size else numFixed
+      for arg in args, x in xs do
+        /- We should not use structural equality here. For example, given the definition
+           ```
+           def V.map {α β} f x x_1 :=
+             @V.map.match_1.{1} α (fun x x_2 => V β x) x x_1
+               (fun x x_2 => @V.mk₁ β x (f Bool.true x_2))
+               (fun e => @V.mk₂ β (V.map (fun b => α b) (fun b => β b) f Bool.false e))
+           ```
+           The first three arguments at `V.map (fun b => α b) (fun b => β b) f Bool.false e` are "fixed"
+           modulo definitional equality.
+
+           We disable to proof irrelevance to be able to use structural recursion on inductive predicates.
+           For example, consider the example
+           ```
+           inductive PList (α : Type) : Prop
+           | nil
+           | cons : α → PList α → PList α
+
+           infixr:67 " ::: " => PList.cons
+
+           set_option trace.Elab.definition.structural true in
+           def pmap {α β} (f : α → β) : PList α → PList β
+             | PList.nil => PList.nil
+             | a:::as => f a ::: pmap f as
+           ```
+          The "Fixed" prefix would be 4 since all elements of type `PList α` are definitionally equal.
+        -/
+        if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then
+          -- We continue searching if e's arguments are not a prefix of `xs`
+          return true
+      return false
+    else
+      return true
+  numFixedRef.get
+
+partial def withCommonTelescope (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → M α) : M α :=
+  go #[] (preDefs.map (·.value))
+where
+  go (fvars : Array Expr) (vals : Array Expr) : M α := do
+    if !(vals.all fun val => val.isLambda) then
+      k fvars vals
+    else if !(← vals.allM fun val=> isDefEq val.bindingDomain! vals[0]!.bindingDomain!) then
+      k fvars vals
+    else
+      withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>
+        go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x)
+
+private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
+    (xs : Array Expr) (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do
+  let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
+  let indInfo ← getConstInfoInduct recArgInfos[0]!.indGroupInst.all[0]!
+  if ← isInductivePredicate indInfo.name then
+    -- Here we branch off to the IndPred construction, but only for non-mutual functions
+    unless preDefs.size = 1 do
+      throwError "structural mutual recursion over inductive predicates is not supported"
+    trace[Elab.definition.structural] "Using mkIndPred construction"
+    let preDef := preDefs[0]!
+    let recArgInfo := recArgInfos[0]!
+    let value := values[0]!
+    let valueNew ← mkIndPredBRecOn recArgInfo value
+    let valueNew ← lambdaTelescope value fun ys _ => do
+      mkLambdaFVars (etaReduce := true) (fixedParamPerms.perms[0]!.buildArgs xs ys) (mkAppN valueNew ys)
+    trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}"
+    check valueNew
+    return #[{ preDef with value := valueNew }]
+
+  -- Groups the (indices of the) definitions by their position in indInfo.all
+  let positions : Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers)
+  trace[Elab.definition.structural] "assignments of type formers of {indInfo.name} to functions: {positions}"
+
+  -- Construct the common `.brecOn` arguments
+  let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
+  trace[Elab.definition.structural] "motives: {motives}"
+  let brecOnConst ← mkBRecOnConst recArgInfos positions motives
+  let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
+  trace[Elab.definition.structural] "FTypes: {FTypes}"
+  let FArgs ← (recArgInfos.zip (values.zip FTypes)).mapM fun (r, (v, t)) =>
+    mkBRecOnF recArgInfos positions r v t
+  trace[Elab.definition.structural] "FArgs: {FArgs}"
+  -- Assemble the individual `.brecOn` applications
+  let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) =>
+    mkBrecOnApp positions i brecOnConst FArgs r v
+  -- Abstract over the fixed prefixed, preserving the original parameter order
+  let valuesNew ← (values.zip valuesNew).mapIdxM fun i ⟨value, valueNew⟩ =>
+    lambdaTelescope value fun ys _ => do
+      -- NB: Do not eta-contract here, other code (e.g. FunInd) expects this to have the
+      -- same number of head lambdas as the original definition
+      mkLambdaFVars (fixedParamPerms.perms[i]!.buildArgs xs ys) (valueNew.beta ys)
+  return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
+
+private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) :
+    M (Array Nat × (Array PreDefinition) × FixedParamPerms) := do
+  withoutModifyingEnv do
+    preDefs.forM (addAsAxiom ·)
+    let fnNames := preDefs.map (·.declName)
+    let preDefs ← preDefs.mapM fun preDef =>
+      return { preDef with value := (← preprocess preDef.value fnNames) }
+
+    -- The syntactically fixed arguments
+    let fixedParamPerms ← getFixedParamPerms preDefs
+
+    fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun xs => do
+      let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
+
+      tryAllArgs fnNames fixedParamPerms xs values termMeasure?s fun recArgInfos => do
+        let recArgPoss := recArgInfos.map (·.recArgPos)
+        trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
+        let (fixedParamPerms', xs', toErase) := fixedParamPerms.erase xs (recArgInfos.map (·.indicesAndRecArgPos))
+        -- We may have to turn some fixed parameters into varying parameters
+        let recArgInfos := recArgInfos.mapIdx fun i recArgInfo =>
+          {recArgInfo with fixedParamPerm := fixedParamPerms'.perms[i]!}
+        if xs'.size != xs.size then
+          trace[Elab.definition.structural] "Reduced fixed params from {xs} to {xs'}, erasing {toErase.map mkFVar}"
+          trace[Elab.definition.structural] "New recArgInfos {repr recArgInfos}"
+        -- Check that the parameters of the IndGroupInsts are still fine
+          for recArgInfo in recArgInfos do
+            for indParam in recArgInfo.indGroupInst.params do
+              for y in toErase do
+                if (← dependsOn indParam y) then
+                  if indParam.isFVarOf y then
+                    throwError "its type is an inductive datatype and the datatype parameter\
+                      {indentExpr indParam}\n\
+                      which cannot be fixed as it is an index or depends on an index, and indices \
+                      cannot be fixed parameters when using structural recursion."
+                  else
+                    throwError "its type is an inductive datatype and the datatype parameter\
+                      {indentExpr indParam}\ndepends on the function parameter{indentExpr (mkFVar y)}\n\
+                      which cannot be fixed as it is an index or depends on an index, and indices \
+                      cannot be fixed parameters when using structural recursion."
+        withErasedFVars toErase do
+          let preDefs' ← elimMutualRecursion preDefs fixedParamPerms' xs' recArgInfos
+          return (recArgPoss, preDefs', fixedParamPerms')
+
+def reporttermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
+  if let some ref := preDef.termination.terminationBy?? then
+    let fn ← lambdaTelescope preDef.value fun xs _ => mkLambdaFVars xs xs[recArgPos]!
+    let termMeasure : TerminationMeasure:= {ref := .missing, structural := true, fn}
+    let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
+    let stx ← termMeasure.delab arity (extraParams := preDef.termination.extraParams)
+    Tactic.TryThis.addSuggestion ref stx
+
+
+def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do
+  let names := preDefs.map (·.declName)
+  let ((recArgPoss, preDefsNonRec, fixedParamPerms), state) ← run <| inferRecArgPos preDefs termMeasure?s
+  for recArgPos in recArgPoss, preDef in preDefs do
+    reporttermMeasure preDef recArgPos
+  state.addMatchers.forM liftM
+  preDefsNonRec.forM fun preDefNonRec => do
+    let preDefNonRec ← eraseRecAppSyntax preDefNonRec
+    prependError m!"structural recursion failed, produced type incorrect term" do
+      -- We create the `_unsafe_rec` before we abstract nested proofs.
+      -- Reason: the nested proofs may be referring to the _unsafe_rec.
+      addNonRec preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList)
+  let preDefs ← preDefs.mapM (eraseRecAppSyntax ·)
+  addAndCompilePartialRec preDefs
+  for preDef in preDefs, recArgPos in recArgPoss do
+    let mut preDef := preDef
+    unless preDef.kind.isTheorem do
+      unless (← isProp preDef.type) do
+        preDef ← abstractNestedProofs preDef
+        /-
+        Don't save predefinition info for equation generator
+        for theorems and definitions that are propositions.
+        See issue #2327
+        -/
+        registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
+    addSmartUnfoldingDef preDef recArgPos
+    markAsRecursive preDef.declName
+  for preDef in preDefs do
+    -- must happen in separate loop so realizations can see eqnInfos of all other preDefs
+    enableRealizationsForConst preDef.declName
+    -- must happen after `enableRealizationsForConst`
+    generateEagerEqns preDef.declName
+  applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation
+
+
+end Structural
+
+export Structural (structuralRecursion)
+
+end Lean.Elab

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/Preprocess.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Transform
+import Lean.Elab.RecAppSyntax
+
+namespace Lean.Elab.Structural
+open Meta
+
+private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
+  if e.isHeadBetaTarget then
+    e.getAppFn.find? (fun e => e.isConst && recFnNames.contains e.constName!) |>.isSome
+  else
+    false
+
+/--
+Preprocesses the expressions to improve the effectiveness of `elimRecursion`.
+
+* Beta reduce terms where the recursive function occurs in the lambda term.
+  Example:
+  ```
+  def f : Nat → Nat
+    | 0 => 1
+    | i+1 => (fun x => f x) i
+  ```
+
+* Floats out the RecApp markers.
+  Example:
+  ```
+  def f : Nat → Nat
+    | 0 => 1
+    | i+1 => (f x) i
+  ```
+-/
+def preprocess (e : Expr) (recFnNames : Array Name) : CoreM Expr :=
+  Core.transform e
+    (pre := fun e =>
+      if shouldBetaReduce e recFnNames then
+        return .visit e.headBeta
+      else
+        return .continue)
+    (post := fun e => do
+      if e.isApp && e.getAppFn.isMData then
+        let .mdata m f := e.getAppFn | unreachable!
+        if m.isRecApp then
+          return .done (.mdata m (f.beta e.getAppArgs))
+      return .continue)
+
+
+end Lean.Elab.Structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Meta.Basic
+import Lean.Meta.ForEachExpr
+import Lean.Elab.PreDefinition.FixedParams
+import Lean.Elab.PreDefinition.Structural.IndGroupInfo
+
+namespace Lean.Elab.Structural
+
+
+/--
+Information about the argument of interest of a structurally recursive function.
+
+The `Expr`s in this data structure expect the fixed parameters to be in scope, but not the other
+parameters of the function. This ensures that this data structure makes sense in the other functions
+of a mutually recursive group.
+-/
+structure RecArgInfo where
+  /-- the name of the recursive function -/
+  fnName       : Name
+  /-- Information which arguments are fixed -/
+  fixedParamPerm : FixedParamPerm
+  /-- position of the argument we are recursing on, among all parameters -/
+  recArgPos    : Nat
+  /-- position of the indices of the inductive datatype we are recursing on, among all parameters -/
+  indicesPos   : Array Nat
+  /-- The inductive group (with parameters) of the argument's type -/
+  indGroupInst : IndGroupInst
+  /--
+  index of the inductive datatype of the argument we are recursing on.
+  If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
+  -/
+  indIdx       : Nat
+deriving Inhabited, Repr
+
+  /-- position of the argument and its indices we are recursing on, among all parameters -/
+def RecArgInfo.indicesAndRecArgPos (info : RecArgInfo) : Array Nat :=
+  info.indicesPos.push info.recArgPos
+
+/--
+If `xs` are the varying parameters of the functions, partitions them into indices and major
+arguments, and other parameters.
+-/
+def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
+  -- To simplify the index calculation, pad xs with dummy values where fixed parameters are
+  let xs := info.fixedParamPerm.buildArgs (.replicate info.fixedParamPerm.numFixed (mkSort 0)) xs
+  -- First indices and major arg, using the order they appear in `info.indicesPos`
+  let mut indexMajorArgs := #[]
+  let indexMajorPos := info.indicesPos.push info.recArgPos
+  for j in indexMajorPos do
+    indexMajorArgs := indexMajorArgs.push xs[j]!
+  -- Then the other arguments, in the order they appear in `xs`
+  let mut otherVaryingArgs := #[]
+  for h : i in [:xs.size] do
+    unless indexMajorPos.contains i do
+      unless info.fixedParamPerm.isFixed i do
+        otherVaryingArgs := otherVaryingArgs.push xs[i]
+  return (indexMajorArgs, otherVaryingArgs)
+
+/--
+Name of the recursive data type. Assumes that it is not one of the auxiliary ones.
+-/
+def RecArgInfo.indName! (info : RecArgInfo) : Name :=
+  info.indGroupInst.all[info.indIdx]!
+
+end Lean.Elab.Structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Meta.Match.MatcherApp.Basic
+
+namespace Lean.Elab.Structural
+open Meta
+
+partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) : MetaM PreDefinition := do
+  return { preDef with
+    declName  := mkSmartUnfoldingNameFor preDef.declName
+    value     := (← visit preDef.value)
+    modifiers := default
+  }
+where
+  /--
+     Auxiliary method for annotating `match`-alternatives with `markSmartUnfoldingMatch` and `markSmartUnfoldingMatchAlt`.
+
+     It uses the following approach:
+     - Whenever it finds a `match` application `e` s.t. `recArgHasLooseBVarsAt preDef.declName recArgPos e`,
+       it marks the `match` with `markSmartUnfoldingMatch`, and each alternative that does not contain a nested marked `match`
+       is marked with `markSmartUnfoldingMatchAlt`.
+
+     Recall that the condition `recArgHasLooseBVarsAt preDef.declName recArgPos e` is the one used at `mkBRecOn`.
+  -/
+  visit (e : Expr) : MetaM Expr := do
+    match e with
+    | Expr.lam ..     => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
+    | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
+    | Expr.letE n type val body nondep =>
+      mapLetDecl n type (← visit val) (nondep := nondep) fun x => do
+        visit (body.instantiate1 x)
+    | Expr.mdata d b     => return mkMData d (← visit b)
+    | Expr.proj n i s    => return mkProj n i (← visit s)
+    | Expr.app .. =>
+      let processApp (e : Expr) : MetaM Expr :=
+        e.withApp fun f args =>
+          return mkAppN (← visit f) (← args.mapM visit)
+      match (← matchMatcherApp? e) with
+      | some matcherApp =>
+        if !recArgHasLooseBVarsAt preDef.declName recArgPos e then
+          processApp e
+        else
+          let mut altsNew := #[]
+          for alt in matcherApp.alts, numParams in matcherApp.altNumParams do
+            let altNew ← lambdaBoundedTelescope alt numParams fun xs altBody => do
+              unless xs.size = numParams do
+                throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
+              let altBody ← visit altBody
+              let containsSUnfoldMatch := Option.isSome <| altBody.find? fun e => smartUnfoldingMatch? e |>.isSome
+              let altBody := if !containsSUnfoldMatch then markSmartUnfoldingMatchAlt altBody else altBody
+              mkLambdaFVars xs altBody
+            altsNew := altsNew.push altNew
+          return markSmartUnfoldingMatch { matcherApp with alts := altsNew }.toExpr
+      | _ => processApp e
+    | _ => return e
+
+partial def addSmartUnfoldingDef (preDef : PreDefinition) (recArgPos : Nat) : TermElabM Unit := do
+  if (← isProp preDef.type) then
+    return ()
+  else
+    withEnableInfoTree false do
+      let preDefSUnfold ← addSmartUnfoldingDefAux preDef recArgPos
+      addNonRec preDefSUnfold (cleanupValue := true)
+
+end Lean.Elab.Structural

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/WF/Basic.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.WF
+
+register_builtin_option debug.rawDecreasingByGoal : Bool := {
+  defValue := false
+  descr    := "Shows the raw `decreasing_by` goal including internal implementation detail \
+               instead of cleaning it up with the `clean_wf` tactic. Can be enabled for debugging \
+               purposes. Please report an issue if you have to use this option for other reasons."
+}
+
+open Lean Elab Tactic
+
+def applyCleanWfTactic : TacticM Unit := do
+  unless debug.rawDecreasingByGoal.get (← getOptions) do
+    Tactic.evalTactic (← `(tactic| all_goals clean_wf))
+
+end Lean.Elab.WF

backend/core/leanprover--lean4---v4.22.0/src/lean/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Split
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Eqns
+import Lean.Meta.ArgsPacker.Basic
+import Lean.Elab.PreDefinition.WF.Unfold
+import Lean.Elab.PreDefinition.FixedParams
+import Init.Data.Array.Basic
+
+namespace Lean.Elab.WF
+open Meta
+open Eqns
+
+structure EqnInfo extends EqnInfoCore where
+  declNames       : Array Name
+  declNameNonRec  : Name
+  argsPacker      : ArgsPacker
+  fixedParamPerms : FixedParamPerms
+  deriving Inhabited
+
+builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
+
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
+    (argsPacker : ArgsPacker) : MetaM Unit := do
+  preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
+  /-
+  See issue #2327.
+  Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare
+  combination, and we would have add support for it in the equation generator. I did not check which assumptions are made there.
+  -/
+  unless preDefs.all fun p => p.kind.isTheorem do
+    unless (← preDefs.allM fun p => isProp p.type) do
+      let declNames := preDefs.map (·.declName)
+      modifyEnv fun env =>
+        preDefs.foldl (init := env) fun env preDef =>
+          eqnInfoExt.insert env preDef.declName { preDef with
+            declNames, declNameNonRec, argsPacker, fixedParamPerms }
+
+def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
+  if let some info := eqnInfoExt.find? (← getEnv) declName then
+    mkEqns declName info.declNames (tryRefl := false)
+  else
+    return none
+
+builtin_initialize
+  registerGetEqnsFn getEqnsFor?
+
+
+/--
+This is a hack to fix fallout from #8519, where a non-exposed wfrec definition `foo`
+in a module would cause `foo.eq_def` to be defined eagerly and privately,
+but it should still be visible from non-mudule files.
+
+So we create a unfold equation generator that aliases an existing private `eq_def` to
+wherever the current module expects it.
+-/
+def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do
+  withTraceNode `ReservedNameAction (pure m!"{exceptOptionEmoji ·} copyPrivateUnfoldTheorem running for {declName}") do
+  let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
+  if let some mod ← findModuleOf? declName then
+    let unfoldName' := mkPrivateNameCore mod (.str declName unfoldThmSuffix)
+    if let some (.thmInfo info) := (← getEnv).find? unfoldName' then
+      realizeConst declName name do
+        addDecl <| Declaration.thmDecl {
+          name,
+          type := info.type,
+          value := .const unfoldName' (info.levelParams.map mkLevelParam),
+          levelParams := info.levelParams
+        }
+      return name
+  return none
+
+builtin_initialize
+  registerGetUnfoldEqnFn copyPrivateUnfoldTheorem
+
+end Lean.Elab.WF