From e32f3e8140f497899190aad557379ba2e7befbfa Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 19 Jul 2024 12:20:50 +0200 Subject: [PATCH] refactor: IndGroupInst.brecOn (#4787) this logic fits nicely within `IndGroupInst`. Also makes `isAuxRecursorWithSuffix` recognize `brecOn_`. --- src/Lean/AuxRecursor.lean | 2 +- src/Lean/Elab/PreDefinition/Structural/BRecOn.lean | 13 +------------ .../Elab/PreDefinition/Structural/IndGroupInfo.lean | 13 +++++++++++++ tests/lean/run/funind_structural.lean | 12 +++++++----- tests/lean/run/structuralMutual.lean | 6 ++++-- 5 files changed, 26 insertions(+), 20 deletions(-) diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean index b68aa5019d..c49a369828 100644 --- a/src/Lean/AuxRecursor.lean +++ b/src/Lean/AuxRecursor.lean @@ -37,7 +37,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool := def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool := match declName with - | .str _ s => s == suffix && isAuxRecursor env declName + | .str _ s => (s == suffix || s.startsWith s!"{suffix}_") && isAuxRecursor env declName | _ => false def isCasesOnRecursor (env : Environment) (declName : Name) : Bool := diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 9d2fb74eb6..96f742b747 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -245,18 +245,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions) decLevel brecOnUniv else pure brecOnUniv - let brecOnCons := fun idx => - let brecOn := - if let .some n := indGroup.all[idx]? then - if useBInductionOn then .const (mkBInductionOnName n) indGroup.levels - else .const (mkBRecOnName n) (brecOnUniv :: indGroup.levels) - else - let n := indGroup.all[0]! - let j := idx - indGroup.all.size + 1 - if useBInductionOn then .const (mkBInductionOnName n |>.appendIndexAfter j) indGroup.levels - else .const (mkBRecOnName n |>.appendIndexAfter j) (brecOnUniv :: indGroup.levels) - mkAppN brecOn indGroup.params - + let brecOnCons := fun idx => indGroup.brecOn useBInductionOn brecOnUniv idx -- Pick one as a prototype let brecOnAux := brecOnCons 0 -- Infer the type of the packed motive arguments diff --git a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean index f9c9dc29fe..2490faaaca 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean @@ -62,6 +62,19 @@ def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do unless (← (igi1.params.zip igi2.params).allM (fun (e₁, e₂) => Meta.isDefEqGuarded e₁ e₂)) do return false return true +/-- 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 + /-- Figures out the nested type formers of an inductive group, with parameters instantiated and indices still forall-abstracted. diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean index 08bb7db9f2..0e57adc3b9 100644 --- a/tests/lean/run/funind_structural.lean +++ b/tests/lean/run/funind_structural.lean @@ -1,6 +1,3 @@ -import Lean.Elab.Command -import Lean.Elab.PreDefinition.Structural.Eqns - /-! This module tests functional induction principles on *structurally* recursive functions. -/ @@ -8,6 +5,7 @@ This module tests functional induction principles on *structurally* recursive fu def fib : Nat → Nat | 0 | 1 => 0 | n+2 => fib n + fib (n+1) +termination_by structural x => x /-- info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) @@ -20,6 +18,7 @@ info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) def binary : Nat → Nat → Nat | 0, acc | 1, acc => 1 + acc | n+2, acc => binary n (binary (n+1) acc) +termination_by structural x => x /-- info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc) @@ -34,6 +33,7 @@ info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), mo def binary' : Bool → Nat → Bool | acc, 0 | acc , 1 => not acc | acc, n+2 => binary' (binary' acc (n+1)) n +termination_by structural _ x => x /-- info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0) @@ -48,6 +48,7 @@ def zip {α β} : List α → List β → List (α × β) | [], _ => [] | _, [] => [] | x::xs, y::ys => (x, y) :: zip xs ys +termination_by structural x => x /-- info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop) @@ -84,6 +85,7 @@ def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n | fzero, _ => fzero | _, fzero => fzero | fsucc i, fsucc j => fsucc (Finn.min (not x) (m + 1) i j) +termination_by structural n /-- info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop) @@ -95,8 +97,6 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n #guard_msgs in #check Finn.min.induct - - namespace TreeExample inductive Tree (β : Type v) where @@ -113,6 +113,7 @@ def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β := node left key value (right.insert k v) else node left k v right +termination_by structural t /-- info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop) @@ -174,6 +175,7 @@ def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote | .app f a, env => f.denote env (a.denote env) | .lam b, env => fun x => b.denote (.cons x env) | .let a b, env => b.denote (.cons (a.denote env) env) +termination_by structural x => x /-- info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop) diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index 6b18532e12..5adc7e81aa 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -215,6 +215,8 @@ namespace EvenOdd -- Mutual structural recursion over a non-mutual inductive type +-- (The functions don't actually implement even/odd, but that isn't the point here.) + mutual def Even : Nat → Prop | 0 => True @@ -518,13 +520,13 @@ Too many possible combinations of parameters of type Nattish (or please indicate Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) -Call from ManyCombinations.f to ManyCombinations.g at 550:15-29: +Call from ManyCombinations.f to ManyCombinations.g at 552:15-29: #1 #2 #3 #4 #5 ? ? ? ? #6 ? = ? ? #7 ? ? = ? #8 ? ? ? = -Call from ManyCombinations.g to ManyCombinations.f at 553:15-29: +Call from ManyCombinations.g to ManyCombinations.f at 555:15-29: #5 #6 #7 #8 #1 _ _ _ _ #2 _ = _ _