feat: fun_induction foo (no arguments) (#7101)
This PR implements `fun_induction foo`, which is like `fun_induction foo x y z`, only that it picks the arguments to use from a unique suitable call to `foo` in the goal.
This commit is contained in:
Joachim Breitner
GitHub
parent
9d5f565119
commit
a3b76aa825
5 changed files with 464 additions and 8 deletions
|
|
@ -917,6 +917,14 @@ induction y₁, ... yₘ using f.induct x₁ ... xₙ
|
|||
where the arguments of `f` are used as arguments to `f.induct` or targets of the induction, as
|
||||
appropriate.
|
||||
|
||||
The form
|
||||
```
|
||||
fun_induction f
|
||||
```
|
||||
(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
|
||||
these arguments. An application of `f` is eligible if it is saturated and the arguments that will
|
||||
become targets are free variables.
|
||||
|
||||
The forms `fun_induction f x y generalizing z₁ ... zₙ` and
|
||||
`fun_induction f x y with | case1 => tac₁ | case2 x' ih => tac₂` work like with `induction.`
|
||||
-/
|
||||
|
|
@ -938,6 +946,14 @@ cases y, ... using f.fun_cases x ...
|
|||
where the arguments of `f` are used as arguments to `f.fun_cases` or targets of the case analysis, as
|
||||
appropriate.
|
||||
|
||||
The form
|
||||
```
|
||||
fun_cases f
|
||||
```
|
||||
(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
|
||||
these arguments. An application of `f` is eligible if it is saturated and the arguments that will
|
||||
become targets are free variables.
|
||||
|
||||
The form `fun_cases f x y with | case1 => tac₁ | case2 x' ih => tac₂` works like with `cases`.
|
||||
-/
|
||||
syntax (name := funCases) "fun_cases " term (inductionAlts)? : tactic
|
||||
|
|
|
|||
|
|
@ -13,6 +13,7 @@ import Lean.Meta.Tactic.ElimInfo
|
|||
import Lean.Meta.Tactic.FunIndInfo
|
||||
import Lean.Meta.Tactic.Induction
|
||||
import Lean.Meta.Tactic.Cases
|
||||
import Lean.Meta.Tactic.FunIndCollect
|
||||
import Lean.Meta.GeneralizeVars
|
||||
import Lean.Elab.App
|
||||
import Lean.Elab.Tactic.ElabTerm
|
||||
|
|
@ -819,12 +820,33 @@ def evalInduction : Tactic := fun stx =>
|
|||
let targets ← withMainContext <| addImplicitTargets elimInfo targets
|
||||
evalInductionCore stx elimInfo targets toTag
|
||||
|
||||
|
||||
/--
|
||||
Elaborates the `foo args` of `fun_induction` or `fun_cases`, inferring the args if omitted from the goal
|
||||
-/
|
||||
def elabFunTargetCall (cases : Bool) (stx : Syntax) : TacticM Expr := do
|
||||
match stx with
|
||||
| `($id:ident) =>
|
||||
let fnName ← realizeGlobalConstNoOverload id
|
||||
let some _ ← getFunIndInfo? cases fnName |
|
||||
let theoremKind := if cases then "induction" else "cases"
|
||||
throwError "no functional {theoremKind} theorem for '{.ofConstName fnName}', or function is mutually recursive "
|
||||
let candidates ← FunInd.collect fnName (← getMainGoal)
|
||||
if candidates.isEmpty then
|
||||
throwError "could not find suitable call of '{.ofConstName fnName}' in the goal"
|
||||
if candidates.size > 1 then
|
||||
throwError "found more than one suitable call of '{.ofConstName fnName}' in the goal. \
|
||||
Please include the desired arguments."
|
||||
pure candidates[0]!
|
||||
| _ =>
|
||||
elabTerm stx none
|
||||
|
||||
/--
|
||||
Elaborates the `foo args` of `fun_induction` or `fun_cases`, returning the `ElabInfo` and targets.
|
||||
-/
|
||||
private def elabFunTarget (cases : Bool) (stx : Syntax) : TacticM (ElimInfo × Array Expr) := do
|
||||
withRef stx <| withMainContext do
|
||||
let funCall ← elabTerm stx none
|
||||
let funCall ← elabFunTargetCall cases stx
|
||||
funCall.withApp fun fn funArgs => do
|
||||
let .const fnName fnUs := fn |
|
||||
throwError "expected application headed by a function constant"
|
||||
|
|
|
|||
97
src/Lean/Meta/Tactic/FunIndCollect.lean
Normal file
97
src/Lean/Meta/Tactic/FunIndCollect.lean
Normal file
|
|
@ -0,0 +1,97 @@
|
|||
/-
|
||||
Copyright (c) 2025 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.Tactic.Util
|
||||
import Lean.Meta.Tactic.FunIndInfo
|
||||
|
||||
/-!
|
||||
Support for collecting function calls that could be used for `fun_induction` or `fun_cases`.
|
||||
Used by `fun_induction foo`, and the `Calls` structure is also used by `try?`.
|
||||
-/
|
||||
|
||||
namespace Lean.Meta.FunInd
|
||||
|
||||
structure Call where
|
||||
/- The full function call -/
|
||||
expr : Expr
|
||||
/- Used to avoid adding calls that differ only in dropped arguments -/
|
||||
relevantArgs : Expr
|
||||
deriving Hashable, BEq
|
||||
|
||||
structure SeenCalls where
|
||||
/-- the full calls -/
|
||||
calls : Array Expr
|
||||
/-- only relevant arguments -/
|
||||
seen : Std.HashSet (Array Expr)
|
||||
|
||||
instance : EmptyCollection SeenCalls where
|
||||
emptyCollection := ⟨#[], {}⟩
|
||||
|
||||
def SeenCalls.push (e : Expr) (declName : Name) (args : Array Expr) (calls : SeenCalls) :
|
||||
MetaM SeenCalls := do
|
||||
let some funIndInfo ← getFunIndInfo? (cases := false) declName | return calls
|
||||
if funIndInfo.params.size != args.size then return calls
|
||||
let mut keys := #[]
|
||||
for arg in args, kind in funIndInfo.params do
|
||||
if kind matches .target then
|
||||
if !arg.isFVar then return calls
|
||||
unless kind matches .dropped do
|
||||
keys := keys.push arg
|
||||
if calls.seen.contains keys then return calls
|
||||
return { calls := calls.calls.push e, seen := calls.seen.insert keys }
|
||||
|
||||
namespace Collector
|
||||
|
||||
abbrev M := ReaderT Name <| StateRefT SeenCalls MetaM
|
||||
|
||||
def saveFunInd (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
|
||||
set (← (← get).push e declName args)
|
||||
|
||||
def visitApp (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
|
||||
saveFunInd e declName args
|
||||
|
||||
unsafe abbrev Cache := PtrSet Expr
|
||||
|
||||
unsafe def visit (e : Expr) : StateRefT Cache M Unit := do
|
||||
unless (← get).contains e do
|
||||
modify fun s => s.insert e
|
||||
match e with
|
||||
| .const _ _ => pure ()
|
||||
| .forallE _ d b _ => visit d; visit b
|
||||
| .lam _ d b _ => visit d; visit b
|
||||
| .mdata _ b => visit b
|
||||
| .letE _ t v b _ => visit t; visit v; visit b
|
||||
| .app .. => e.withApp fun f args => do
|
||||
if let .const declName _ := f then
|
||||
if declName = (← read) then
|
||||
unless e.hasLooseBVars do -- TODO: We can allow them in `.dropped` arguments
|
||||
visitApp e declName args
|
||||
else
|
||||
visit f
|
||||
args.forM visit
|
||||
| .proj _ _ b => visit b
|
||||
| _ => return ()
|
||||
|
||||
unsafe def main (needle : Name) (mvarId : MVarId) : MetaM (Array Expr) := mvarId.withContext do
|
||||
let (_, s) ← go |>.run mkPtrSet |>.run needle |>.run {}
|
||||
return s.calls
|
||||
where
|
||||
go : StateRefT Cache M Unit := do
|
||||
for localDecl in (← getLCtx) do
|
||||
unless localDecl.isAuxDecl do
|
||||
if let some val := localDecl.value? then
|
||||
visit val
|
||||
else
|
||||
visit localDecl.type
|
||||
visit (← mvarId.getType)
|
||||
|
||||
end Collector
|
||||
|
||||
def collect (needle : Name) (mvarId : MVarId) : MetaM (Array Expr) := do
|
||||
unsafe Collector.main needle mvarId
|
||||
|
||||
end Lean.Meta.FunInd
|
||||
|
|
@ -168,13 +168,6 @@ error: Expected fully applied application of 'ackermann' with 2 arguments, but f
|
|||
example : P (ackermann n m) := by
|
||||
fun_induction ackermann n
|
||||
|
||||
/--
|
||||
error: Expected fully applied application of 'ackermann' with 2 arguments, but found 0 arguments
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : P (ackermann n m) := by
|
||||
fun_induction ackermann
|
||||
|
||||
end Ex2
|
||||
|
||||
namespace Ex3
|
||||
|
|
|
|||
328
tests/lean/run/funinduction_ident.lean
Normal file
328
tests/lean/run/funinduction_ident.lean
Normal file
|
|
@ -0,0 +1,328 @@
|
|||
namespace ListEx
|
||||
|
||||
theorem map_id (xs : List α) : List.map id xs = xs := by
|
||||
fun_induction List.map <;> simp_all only [List.map, id]
|
||||
|
||||
-- This works because collect ignores `.dropped` arguments
|
||||
|
||||
theorem map_map (f : α → β) (g : β → γ) xs :
|
||||
List.map g (List.map f xs) = List.map (g ∘ f) xs := by
|
||||
fun_induction List.map <;> simp_all only [List.map, Function.comp]
|
||||
|
||||
-- This should genuinely not work, but have a good error message
|
||||
|
||||
/--
|
||||
error: found more than one suitable call of 'List.append' in the goal. Please include the desired arguments.
|
||||
-/
|
||||
#guard_msgs in
|
||||
theorem append_assoc :
|
||||
List.append xs (List.append ys zs) = List.append (List.append xs ys) zs := by
|
||||
fun_induction List.append <;> simp_all only [List.append]
|
||||
|
||||
end ListEx
|
||||
|
||||
namespace Ex1
|
||||
|
||||
variable (P : Nat → Prop)
|
||||
|
||||
def ackermann : (Nat × Nat) → Nat
|
||||
| (0, m) => m + 1
|
||||
| (n+1, 0) => ackermann (n, 1)
|
||||
| (n+1, m+1) => ackermann (n, ackermann (n + 1, m))
|
||||
termination_by p => p
|
||||
|
||||
/--
|
||||
error: tactic 'fail' failed
|
||||
case case1
|
||||
P : Nat → Prop
|
||||
m✝ : Nat
|
||||
⊢ P (ackermann (0, m✝))
|
||||
|
||||
case case2
|
||||
P : Nat → Prop
|
||||
n✝ : Nat
|
||||
ih1✝ : P (ackermann (n✝, 1))
|
||||
⊢ P (ackermann (n✝.succ, 0))
|
||||
|
||||
case case3
|
||||
P : Nat → Prop
|
||||
n✝ m✝ : Nat
|
||||
ih2✝ : P (ackermann (n✝ + 1, m✝))
|
||||
ih1✝ : P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
|
||||
⊢ P (ackermann (n✝.succ, m✝.succ))
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : P (ackermann p) := by
|
||||
fun_induction ackermann
|
||||
fail
|
||||
|
||||
/--
|
||||
error: tactic 'fail' failed
|
||||
case case1
|
||||
P : Nat → Prop
|
||||
m✝ : Nat
|
||||
⊢ P (ackermann (0, m✝))
|
||||
|
||||
case case2
|
||||
P : Nat → Prop
|
||||
n✝ : Nat
|
||||
⊢ P (ackermann (n✝.succ, 0))
|
||||
|
||||
case case3
|
||||
P : Nat → Prop
|
||||
n✝ m✝ : Nat
|
||||
⊢ P (ackermann (n✝.succ, m✝.succ))
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : P (ackermann p) := by
|
||||
fun_cases ackermann
|
||||
fail
|
||||
|
||||
/-- error: could not find suitable call of 'ackermann' in the goal -/
|
||||
#guard_msgs in
|
||||
example : P (ackermann (n, m)) := by
|
||||
fun_induction ackermann
|
||||
|
||||
end Ex1
|
||||
|
||||
namespace Ex2
|
||||
|
||||
variable (P : Nat → Prop)
|
||||
|
||||
def ackermann : Nat → Nat → Nat
|
||||
| 0, m => m + 1
|
||||
| n+1, 0 => ackermann n 1
|
||||
| n+1, m+1 => ackermann n (ackermann (n + 1) m)
|
||||
termination_by n m => (n, m)
|
||||
|
||||
/--
|
||||
error: unsolved goals
|
||||
case case1
|
||||
P : Nat → Prop
|
||||
m✝ : Nat
|
||||
⊢ P (ackermann 0 m✝)
|
||||
|
||||
case case2
|
||||
P : Nat → Prop
|
||||
n✝ : Nat
|
||||
ih1✝ : P (ackermann n✝ 1)
|
||||
⊢ P (ackermann n✝.succ 0)
|
||||
|
||||
case case3
|
||||
P : Nat → Prop
|
||||
n✝ m✝ : Nat
|
||||
ih2✝ : P (ackermann (n✝ + 1) m✝)
|
||||
ih1✝ : P (ackermann n✝ (ackermann (n✝ + 1) m✝))
|
||||
⊢ P (ackermann n✝.succ m✝.succ)
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : P (ackermann n m) := by
|
||||
fun_induction ackermann
|
||||
|
||||
end Ex2
|
||||
|
||||
namespace Ex3
|
||||
|
||||
variable (P : List α → Prop)
|
||||
|
||||
def ackermann {α} (inc : List α) : List α → List α → List α
|
||||
| [], ms => ms ++ inc
|
||||
| _::ns, [] => ackermann inc ns inc
|
||||
| n::ns, _::ms => ackermann inc ns (ackermann inc (n::ns) ms)
|
||||
termination_by ns ms => (ns, ms)
|
||||
|
||||
/--
|
||||
error: unsolved goals
|
||||
case case1
|
||||
α : Type u_1
|
||||
P : List α → Prop
|
||||
inc ms✝ : List α
|
||||
⊢ P (ackermann inc [] ms✝)
|
||||
|
||||
case case2
|
||||
α : Type u_1
|
||||
P : List α → Prop
|
||||
inc : List α
|
||||
head✝ : α
|
||||
ns✝ : List α
|
||||
ih1✝ : P (ackermann inc ns✝ inc)
|
||||
⊢ P (ackermann inc (head✝ :: ns✝) [])
|
||||
|
||||
case case3
|
||||
α : Type u_1
|
||||
P : List α → Prop
|
||||
inc : List α
|
||||
n✝ : α
|
||||
ns✝ : List α
|
||||
head✝ : α
|
||||
ms✝ : List α
|
||||
ih2✝ : P (ackermann inc (n✝ :: ns✝) ms✝)
|
||||
ih1✝ : P (ackermann inc ns✝ (ackermann inc (n✝ :: ns✝) ms✝))
|
||||
⊢ P (ackermann inc (n✝ :: ns✝) (head✝ :: ms✝))
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : P (ackermann inc n m) := by
|
||||
fun_induction ackermann
|
||||
|
||||
end Ex3
|
||||
|
||||
namespace Structural
|
||||
|
||||
variable (P : Nat → Prop)
|
||||
|
||||
def fib : Nat → Nat
|
||||
| 0 => 0
|
||||
| 1 => 1
|
||||
| n+2 => fib n + fib (n+1)
|
||||
termination_by structural x => x
|
||||
|
||||
/--
|
||||
error: tactic 'fail' failed
|
||||
case case1
|
||||
P : Nat → Prop
|
||||
⊢ P (fib 0)
|
||||
|
||||
case case2
|
||||
P : Nat → Prop
|
||||
⊢ P (fib 1)
|
||||
|
||||
case case3
|
||||
P : Nat → Prop
|
||||
n✝ : Nat
|
||||
ih2✝ : P (fib n✝)
|
||||
ih1✝ : P (fib (n✝ + 1))
|
||||
⊢ P (fib n✝.succ.succ)
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : P (fib n) := by
|
||||
fun_induction fib
|
||||
fail
|
||||
|
||||
/-- error: could not find suitable call of 'fib' in the goal -/
|
||||
#guard_msgs in
|
||||
example : n ≤ fib (n + 2) := by
|
||||
fun_induction fib
|
||||
|
||||
end Structural
|
||||
|
||||
namespace StructuralWithOmittedParam
|
||||
|
||||
variable (P : Nat → Prop)
|
||||
|
||||
variable (inc : Nat)
|
||||
def fib : Nat → Nat
|
||||
| 0 => 0
|
||||
| 1 => inc
|
||||
| n+2 => fib n + fib (n+1)
|
||||
termination_by structural x => x
|
||||
|
||||
/--
|
||||
info: StructuralWithOmittedParam.fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
|
||||
(case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check fib.induct -- NB: No inc showing up
|
||||
|
||||
/--
|
||||
error: tactic 'fail' failed
|
||||
case case1
|
||||
P : Nat → Prop
|
||||
inc : Nat
|
||||
⊢ P (fib 2 0)
|
||||
|
||||
case case2
|
||||
P : Nat → Prop
|
||||
inc : Nat
|
||||
⊢ P (fib 2 1)
|
||||
|
||||
case case3
|
||||
P : Nat → Prop
|
||||
inc n✝ : Nat
|
||||
ih2✝ : P (fib 2 n✝)
|
||||
ih1✝ : P (fib 2 (n✝ + 1))
|
||||
⊢ P (fib 2 n✝.succ.succ)
|
||||
-/
|
||||
#guard_msgs in
|
||||
example : P (fib 2 n) := by
|
||||
fun_induction fib
|
||||
fail
|
||||
|
||||
end StructuralWithOmittedParam
|
||||
|
||||
namespace StructuralIndices
|
||||
|
||||
-- Testing recursion on an indexed data type
|
||||
inductive Finn : Nat → Type where
|
||||
| fzero : {n : Nat} → Finn n
|
||||
| fsucc : {n : Nat} → Finn n → Finn (n+1)
|
||||
|
||||
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 i => i
|
||||
|
||||
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 _ j => j
|
||||
|
||||
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
|
||||
|
||||
def Finn.le : Finn n → Finn n → Bool
|
||||
| fzero, _ => true
|
||||
| _, fzero => false
|
||||
| fsucc i, fsucc j => Finn.le i j
|
||||
|
||||
theorem Finn.min_le_right₀ : (Finn.min x m i j).le j := by
|
||||
induction x, m, i, j using @Finn.min.induct <;> simp_all [Finn.min, Finn.le]
|
||||
|
||||
theorem Finn.min_le_right : (Finn.min x m i j).le j := by
|
||||
fun_induction Finn.min <;> simp_all [Finn.min, Finn.le]
|
||||
|
||||
theorem Finn.min_le_right' : (Finn.min' x m i j).le j := by
|
||||
fun_induction Finn.min' <;> simp_all [Finn.min', Finn.le]
|
||||
|
||||
theorem Finn.min_le_right'' : (Finn.min'' x m i j).le j := by
|
||||
fun_induction Finn.min'' <;> simp_all [Finn.min'', Finn.le]
|
||||
|
||||
end StructuralIndices
|
||||
|
||||
namespace Nonrec
|
||||
|
||||
def foo := 1
|
||||
|
||||
/-- error: no functional cases theorem for 'foo', or function is mutually recursive -/
|
||||
#guard_msgs in
|
||||
example : True := by
|
||||
fun_induction foo
|
||||
|
||||
end Nonrec
|
||||
|
||||
namespace Mutual
|
||||
|
||||
inductive Tree (α : Type u) : Type u where
|
||||
| node : α → (Bool → List (Tree α)) → Tree α
|
||||
|
||||
-- Recursion over nested inductive
|
||||
|
||||
mutual
|
||||
def Tree.size : Tree α → Nat
|
||||
| .node _ tsf => 1 + size_aux (tsf true) + size_aux (tsf false)
|
||||
termination_by structural t => t
|
||||
def Tree.size_aux : List (Tree α) → Nat
|
||||
| [] => 0
|
||||
| t :: ts => size t + size_aux ts
|
||||
end
|
||||
|
||||
/-- error: no functional cases theorem for 'Tree.size', or function is mutually recursive -/
|
||||
#guard_msgs in
|
||||
example (t : Tree α) : True := by
|
||||
fun_induction Tree.size
|
||||
|
||||
end Mutual
|
||||
Loading…
Add table
Reference in a new issue