From e11b92900c6071eb3f7cd64dd32ab1bb1a59f77e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 18 Nov 2024 11:06:49 +0100 Subject: [PATCH 1/4] fix: handle reordered indices in structural recursion This PR fixes a bug where structural recursion did not work when indices of the recursive argument appeared as function parameters in a different order than in the argument's type's definition. Fixes #6015. --- .../PreDefinition/Structural/FindRecArg.lean | 2 +- .../Structural/IndGroupInfo.lean | 4 ++-- .../PreDefinition/Structural/RecArgInfo.lean | 16 ++++++++------ tests/lean/run/issue6015.lean | 21 +++++++++++++++++++ 4 files changed, 34 insertions(+), 9 deletions(-) create mode 100644 tests/lean/run/issue6015.lean diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index 203e81c5a689..031af71cc690 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean @@ -243,7 +243,7 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr) recArgInfoss := recArgInfoss.push recArgInfos -- Put non-indices first recArgInfoss := recArgInfoss.map nonIndicesFirst - trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}" + 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}" diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean index 10f3c98d40b9..b29ee61438d0 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean @@ -27,7 +27,7 @@ constituents. structure IndGroupInfo where all : Array Name numNested : Nat -deriving BEq, Inhabited +deriving BEq, Inhabited, Repr def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where all := indInfo.all.toArray @@ -56,7 +56,7 @@ mutual structural recursion on such incompatible types. structure IndGroupInst extends IndGroupInfo where levels : List Level params : Array Expr -deriving Inhabited +deriving Inhabited, Repr def IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData := mkAppN (.const igi.all[0]! igi.levels) igi.params diff --git a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean index 0453fa98592e..0c2a5b61c8cd 100644 --- a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean @@ -23,9 +23,9 @@ structure RecArgInfo where fnName : Name /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/ numFixed : Nat - /-- position of the argument (counted including fixed prefix) we are recursing on -/ + /-- position (counted including fixed prefix) of the argument we are recursing on -/ recArgPos : Nat - /-- position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on -/ + /-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/ indicesPos : Array Nat /-- The inductive group (with parameters) of the argument's type -/ indGroupInst : IndGroupInst @@ -34,20 +34,24 @@ structure RecArgInfo where If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion -/ indIdx : Nat -deriving Inhabited +deriving Inhabited, Repr /-- If `xs` are the parameters of the functions (excluding fixed prefix), 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 + let indexMajorPos := info.indicesPos.push info.recArgPos let mut indexMajorArgs := #[] let mut otherArgs := #[] + -- First indices and major arg, using the order they appear in `indexMajorArgs` + for j in indexMajorPos do + assert! info.numFixed ≤ j && j - info.numFixed < xs.size + indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]! + -- Then the other arguments, in the order they appear in `xs` for h : i in [:xs.size] do let j := i + info.numFixed - if j = info.recArgPos || info.indicesPos.contains j then - indexMajorArgs := indexMajorArgs.push xs[i] - else + unless indexMajorPos.contains j do otherArgs := otherArgs.push xs[i] return (indexMajorArgs, otherArgs) diff --git a/tests/lean/run/issue6015.lean b/tests/lean/run/issue6015.lean new file mode 100644 index 000000000000..29a22e0f50c8 --- /dev/null +++ b/tests/lean/run/issue6015.lean @@ -0,0 +1,21 @@ +private axiom test_sorry : ∀ {α}, α + +inductive Tyₛ (l : List Unit): Type +| U : Tyₛ l +open Tyₛ + +inductive Varₚ (d : Unit): List Unit → Type +| vz : Varₚ d [d'] +| vs : Varₚ d l → Varₚ d (Bₛ :: l) + +inductive Tmₛ {l : List Unit}: Tyₛ l → Unit → Type 1 +| arr : (T : Type) → Tmₛ A d → Tmₛ A d +| param : Varₚ d l → Tmₛ A d → Tmₛ (@U l) d + +def TmₛA {l : List Unit} {d : Unit} (nonIndex : Bool) {Aₛ : Tyₛ l} (t : Tmₛ Aₛ d): Type := +match t with + | .arr dom cd => + let cd := TmₛA nonIndex cd + dom → cd + | _ => test_sorry +termination_by structural t From 5bfc1c1861d84ebda3e6b05822c96504042e028f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 18 Nov 2024 11:17:25 +0100 Subject: [PATCH 2/4] Cosmetics --- src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean index 0c2a5b61c8cd..7872c88fbdcc 100644 --- a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean @@ -41,14 +41,14 @@ If `xs` are the parameters of the functions (excluding fixed prefix), partitions into indices and major arguments, and other parameters. -/ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do - let indexMajorPos := info.indicesPos.push info.recArgPos - let mut indexMajorArgs := #[] - let mut otherArgs := #[] -- First indices and major arg, using the order they appear in `indexMajorArgs` + let mut indexMajorArgs := #[] + let indexMajorPos := info.indicesPos.push info.recArgPos for j in indexMajorPos do assert! info.numFixed ≤ j && j - info.numFixed < xs.size indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]! -- Then the other arguments, in the order they appear in `xs` + let mut otherArgs := #[] for h : i in [:xs.size] do let j := i + info.numFixed unless indexMajorPos.contains j do From f72b9d3a2c98d105d4baaf502d13247b3f1fbcef Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 18 Nov 2024 11:17:49 +0100 Subject: [PATCH 3/4] More cosmetics --- src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean index 7872c88fbdcc..520c9713c07f 100644 --- a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean @@ -50,8 +50,7 @@ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array E -- Then the other arguments, in the order they appear in `xs` let mut otherArgs := #[] for h : i in [:xs.size] do - let j := i + info.numFixed - unless indexMajorPos.contains j do + unless indexMajorPos.contains (i + info.numFixed) do otherArgs := otherArgs.push xs[i] return (indexMajorArgs, otherArgs) From 7e50d31233e749fca697acda0bd1809a00d3bee8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 18 Nov 2024 12:12:28 +0100 Subject: [PATCH 4/4] Update src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean --- src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean index 520c9713c07f..874ecbc92151 100644 --- a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean @@ -41,7 +41,7 @@ If `xs` are the parameters of the functions (excluding fixed prefix), partitions into indices and major arguments, and other parameters. -/ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do - -- First indices and major arg, using the order they appear in `indexMajorArgs` + -- 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