From 61a5bc0ed725737de913f60604d3cabfb653f550 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 25 Jul 2024 17:06:02 +0200 Subject: [PATCH] fix: structural recursion: do not check for brecOn too early Due to nested recursion, we do two passes of `getRecArgInfo`: One on each argument in isolation, to see which inductive types are around (e.g. `Tree` and `List`), and then we later refine/replace this result with the data for the nested type former (the implicit `ListTree`). If we have nested recursion through a non-recursive data type like `Array` or `Prod` then arguemnts of these types should survive the first phase, so that we can still use them when looking for, say, `Array Tree`. This was helpfully reported by @arthur-adjedj. --- .../PreDefinition/Structural/FindRecArg.lean | 9 ++- .../Structural/IndGroupInfo.lean | 22 +++--- tests/lean/guessLexFailures.lean.expected.out | 3 +- tests/lean/run/structuralMutual.lean | 71 ++++++++++++++++++- tests/lean/run/terminationByStructurally.lean | 27 +++++++ 5 files changed, 117 insertions(+), 15 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index 63289c8dec42..5199cd977451 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean @@ -68,9 +68,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : 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 - if !(← hasConst (mkBRecOnName indInfo.name)) then - throwError "its type {indInfo.name} does not have a recursor" - else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then + if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then throwError "its type {indInfo.name} is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate" else let indArgs : Array Expr := xType.getAppArgs @@ -263,6 +261,11 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr) 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 false 0)) do + throwError "the type {group} does not have a `.brecOn` recursor" -- TODO: Here we used to save and restore the state. But should the `try`-`catch` -- not suffice? let r ← k comb diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean index 2490faaacac1..78354fa8170b 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean @@ -36,6 +36,16 @@ def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where def IndGroupInfo.numMotives (group : IndGroupInfo) : Nat := group.all.size + group.numNested +/-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index, +including universe parameters and fixed prefix. -/ +partial def IndGroupInfo.brecOnName (info : IndGroupInfo) (ind : Bool) (idx : Nat) : Name := + if let .some n := info.all[idx]? then + if ind then mkBInductionOnName n + else mkBRecOnName n + else + let j := idx - info.all.size + 1 + info.brecOnName ind 0 |>.appendIndexAfter j + /-- An instance of an mutually inductive group of inductives, identified by the `all` array and the level and expressions parameters. @@ -65,15 +75,9 @@ def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do /-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index, including universe parameters and fixed prefix. -/ def IndGroupInst.brecOn (group : IndGroupInst) (ind : Bool) (lvl : Level) (idx : Nat) : Expr := - let e := if let .some n := group.all[idx]? then - if ind then .const (mkBInductionOnName n) group.levels - else .const (mkBRecOnName n) (lvl :: group.levels) - else - let n := group.all[0]! - let j := idx - group.all.size + 1 - if ind then .const (mkBInductionOnName n |>.appendIndexAfter j) group.levels - else .const (mkBRecOnName n |>.appendIndexAfter j) (lvl :: group.levels) - mkAppN e group.params + let n := group.brecOnName ind idx + let us := if ind then group.levels else lvl :: group.levels + mkAppN (.const n us) group.params /-- Figures out the nested type formers of an inductive group, with parameters instantiated diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out index f1e02e1e1cb8..e159fd9263a1 100644 --- a/tests/lean/guessLexFailures.lean.expected.out +++ b/tests/lean/guessLexFailures.lean.expected.out @@ -72,11 +72,10 @@ Not considering parameter fixed of Mutual.f: it is unchanged in the recursive calls Not considering parameter fixed of Mutual.g: it is unchanged in the recursive calls -Not considering parameter H of Mutual.g: - its type True does not have a recursor Not considering parameter fixed of Mutual.h: it is unchanged in the recursive calls Too many possible combinations of parameters of type Nat (or please indicate the recursive argument explicitly using `termination_by structural`). +Skipping arguments of type True, as Mutual.f has no compatible argument. Could not find a decreasing measure. diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index f3bdec673e17..6d227e8e50a1 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -575,6 +575,53 @@ end end ManyCombinations +namespace WithTuple + +inductive Tree (α : Type) where + | node : α → (Tree α × Tree α) → Tree α + +mutual + +def Tree.map (f : α → β) (x : Tree α): Tree β := + match x with + | node x arrs => node (f x) $ Tree.map_tup f arrs +termination_by structural x + +def Tree.map_tup (f : α → β) (x : Tree α × Tree α): (Tree β × Tree β) := + match x with + | (t₁,t₂) => (Tree.map f t₁, Tree.map f t₂) +termination_by structural x + +end + +end WithTuple + +namespace WithArray + +inductive Tree (α : Type) where + | node : α → Array (Tree α) → Tree α + +mutual + +def Tree.map (f : α → β) (x : Tree α): Tree β := + match x with + | node x arr₁ => node (f x) $ Tree.map_arr f arr₁ +termination_by structural x + +def Tree.map_arr (f : α → β) (x : Array (Tree α)): Array (Tree β) := + match x with + | .mk arr₁ => .mk (Tree.map_list f arr₁) +termination_by structural x + +def Tree.map_list (f : α → β) (x : List (Tree α)): List (Tree β) := + match x with + | [] => [] + | h₁::t₁ => (Tree.map f h₁)::Tree.map_list f t₁ +termination_by structural x +end + +end WithArray + namespace FunIndTests -- FunInd does not handle mutual structural recursion yet, so make sure we error @@ -632,6 +679,28 @@ info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1 (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a : Nat), motive_1 a -/ #guard_msgs in -#check EvenOdd.isEven.induct -- TODO: This error message can be improved +#check EvenOdd.isEven.induct + +/-- +info: WithTuple.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithTuple.Tree α → Prop) + (motive_2 : WithTuple.Tree α × WithTuple.Tree α → Prop) + (case1 : + ∀ (x : α) (arrs : WithTuple.Tree α × WithTuple.Tree α), motive_2 arrs → motive_1 (WithTuple.Tree.node x arrs)) + (case2 : ∀ (t₁ t₂ : WithTuple.Tree α), motive_1 t₁ → motive_1 t₂ → motive_2 (t₁, t₂)) (x : WithTuple.Tree α) : + motive_1 x +-/ +#guard_msgs in +#check WithTuple.Tree.map.induct + +/-- +info: WithArray.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithArray.Tree α → Prop) + (motive_2 : Array (WithArray.Tree α) → Prop) (motive_3 : List (WithArray.Tree α) → Prop) + (case1 : ∀ (x : α) (arr₁ : Array (WithArray.Tree α)), motive_2 arr₁ → motive_1 (WithArray.Tree.node x arr₁)) + (case2 : ∀ (arr₁ : List (WithArray.Tree α)), motive_3 arr₁ → motive_2 { data := arr₁ }) (case3 : motive_3 []) + (case4 : ∀ (h₁ : WithArray.Tree α) (t₁ : List (WithArray.Tree α)), motive_1 h₁ → motive_3 t₁ → motive_3 (h₁ :: t₁)) + (x : WithArray.Tree α) : motive_1 x +-/ +#guard_msgs in +#check WithArray.Tree.map.induct end FunIndTests diff --git a/tests/lean/run/terminationByStructurally.lean b/tests/lean/run/terminationByStructurally.lean index 2137a7b5de0a..2b34bccd6548 100644 --- a/tests/lean/run/terminationByStructurally.lean +++ b/tests/lean/run/terminationByStructurally.lean @@ -83,5 +83,32 @@ def foo4 (n : Nat) : Nat → Nat := match n with | n+1 => foo4 n termination_by structural id n + 1 +/-- +error: failed to infer structural recursion: +Cannot use parameter #2: + the type Nat × Nat does not have a `.brecOn` recursor +-/ +#guard_msgs in +def foo5 : Nat → (Nat × Nat) → Nat + | 0, _ => 0 + | n+1, t => foo5 n t +termination_by structural n t => t + +/-- +error: failed to infer structural recursion: +Cannot use parameters #2 of Errors.foo6 and #2 of Errors.bar6: + the type Nat × Nat does not have a `.brecOn` recursor +-/ +#guard_msgs in +mutual +def foo6 : Nat → (Nat × Nat) → Nat + | 0, _ => 0 + | n+1, t => bar6 n t +termination_by structural n t => t +def bar6 : Nat → (Nat × Nat) → Nat + | 0, _ => 0 + | n+1, t => foo6 n t +termination_by structural n t => t +end end Errors