Lean4
/-- Get candidate theorems from the local context for function property `funPropDecl` and
function `funName`. -/
def getLocalTheorems (funPropDecl : FunPropDecl) (funOrigin : Origin) (mainArgs : Array Nat) (appliedArgs : Nat) :
FunPropM (Array FunctionTheorem) := do
let mut thms : Array FunctionTheorem := #[]
let lctx ← getLCtx
for var in lctx do
if (var.kind = Lean.LocalDeclKind.auxDecl) then
continue
let type ← instantiateMVars var.type
let thm? : Option FunctionTheorem ←
forallTelescope type fun _ b => do
let b ← whnfR b
let some (decl, f) ← getFunProp? b |
return none
unless decl.funPropName = funPropDecl.funPropName do
return none
let .data fData ← getFunctionData? f (← unfoldNamePred) |
return none
unless (fData.getFnOrigin == funOrigin) do
return none
unless isOrderedSubsetOf mainArgs fData.mainArgs do
return none
let dec? ← fData.nontrivialDecomposition
let thm : FunctionTheorem :=
{ funPropName := funPropDecl.funPropName
thmOrigin := .fvar var.fvarId
funOrigin := funOrigin
mainArgs := fData.mainArgs
appliedArgs := fData.args.size
priority := eval_prio default
form := if dec?.isSome then .comp else .uncurried }
return some thm
if let some thm := thm? then
thms := thms.push thm
thms :=
thms |>.qsort
(fun t s =>
let dt := (Int.ofNat t.appliedArgs - Int.ofNat appliedArgs).natAbs
let ds := (Int.ofNat s.appliedArgs - Int.ofNat appliedArgs).natAbs
match compare dt ds with
| .lt => true
| .gt => false
| .eq => t.mainArgs.size < s.mainArgs.size)
return thms
