From 8038604d3ec5566309321b9e7d6f1840cbabeabd Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 5 Mar 2024 14:02:05 +0100 Subject: [PATCH] feat: functional induction (#3432) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This adds the concept of **functional induction** to lean. Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is tailored to proofs about that function. For example from: ``` 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) derive_functional_induction ackermann ``` we get ``` ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) (x x : Nat) : motive x x ``` At the moment, the user has to ask for the functional induction principle explicitly using ``` derive_functional_induction ackermann ``` The module docstring of `Lean/Meta/Tactic/FunInd.lean` contains more details on the design and implementation of this command. More convenience around this (e.g. a `functional induction` tactic) will follow eventually. This PR includes a bunch of `PSum`/`PSigma` related functions in the `Lean.Tactic.FunInd` namespace. I plan to move these to `PackArgs`/`PackMutual` afterwards, and do some cleaning up as I do that. --------- Co-authored-by: David Thrane Christiansen Co-authored-by: Leonardo de Moura --- .github/workflows/ci.yml | 3 +- RELEASES.md | 20 + src/Lean/CoreM.lean | 3 + src/Lean/Meta/Basic.lean | 10 + src/Lean/Meta/Match/MatchEqs.lean | 12 +- src/Lean/Meta/Match/MatcherApp/Transform.lean | 255 +++++ src/Lean/Meta/Tactic.lean | 1 + src/Lean/Meta/Tactic/FunInd.lean | 924 ++++++++++++++++++ src/Lean/Parser/Command.lean | 11 + tests/lean/run/funind_demo.lean | 33 + tests/lean/run/funind_expr.lean | 100 ++ tests/lean/run/funind_mutual_dep.lean | 71 ++ tests/lean/run/funind_proof.lean | 67 ++ tests/lean/run/funind_tests.lean | 841 ++++++++++++++++ 14 files changed, 2347 insertions(+), 4 deletions(-) create mode 100644 src/Lean/Meta/Tactic/FunInd.lean create mode 100644 tests/lean/run/funind_demo.lean create mode 100644 tests/lean/run/funind_expr.lean create mode 100644 tests/lean/run/funind_mutual_dep.lean create mode 100644 tests/lean/run/funind_proof.lean create mode 100644 tests/lean/run/funind_tests.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bf69d6d5dd..6c8369e7ae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -140,7 +140,8 @@ jobs: "shell": "msys2 {0}", "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF", // for reasons unknown, interactivetests are flaky on Windows - "CTEST_OPTIONS": "--repeat until-pass:2", + // also, the liasolver test hits “too many exported symbols” + "CTEST_OPTIONS": "--repeat until-pass:2 -E 'leanbenchtest_liasolver.lean'", "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*", "binary-check": "ldd" diff --git a/RELEASES.md b/RELEASES.md index 6b1304f204..18b6753801 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -11,6 +11,26 @@ of each version. v4.8.0 (development in progress) --------- +* New command `derive_functinal_induction`: + + Derived from the definition of a (possibly mutually) recursive function + defined by well-founded recursion, a **functional induction principle** is + tailored to proofs about that function. For example from: + ``` + 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) + derive_functional_induction ackermann + ``` + we get + ``` + ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) + (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) + (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) + (x x : Nat) : motive x x + ``` + v4.7.0 --------- diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 04117326fd..d6d71c5654 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -289,6 +289,9 @@ def Exception.isMaxHeartbeat (ex : Exception) : Bool := def mkArrow (d b : Expr) : CoreM Expr := return Lean.mkForall (← mkFreshUserName `x) BinderInfo.default d b +/-- Iterated `mkArrow`, creates the expression `a₁ → a₂ → … → aₙ → b`. Also see `arrowDomainsN`. -/ +def mkArrowN (ds : Array Expr) (e : Expr) : CoreM Expr := ds.foldrM mkArrow e + def addDecl (decl : Declaration) : CoreM Unit := do profileitM Exception "type checking" (← getOptions) do withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 836f212d00..d21b2f9f96 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1347,6 +1347,16 @@ private def withNewMCtxDepthImp (allowLevelAssignments : Bool) (x : MetaM α) : finally modify fun s => { s with mctx := saved.mctx, postponed := saved.postponed } +/-- +Removes `fvarId` from the local context, and replaces occurrences of it with `e`. +It is the responsibility of the caller to ensure that `e` is well-typed in the context +of any occurrence of `fvarId`. +-/ +def withReplaceFVarId {α} (fvarId : FVarId) (e : Expr) : MetaM α → MetaM α := + withReader fun ctx => { ctx with + lctx := ctx.lctx.replaceFVarId fvarId e + localInstances := ctx.localInstances.erase fvarId } + /-- `withNewMCtxDepth k` executes `k` with a higher metavariable context depth, where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned. diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index f6fa01b87d..782ffd2615 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -110,6 +110,8 @@ def unfoldNamedPattern (e : Expr) : MetaM Expr := do - `type` is the resulting type for `altType`. We use the `mask` to build the splitter proof. See `mkSplitterProof`. + + This can be used to use the alternative of a match expression in its splitter. -/ partial def forallAltTelescope (altType : Expr) (altNumParams numDiscrEqs : Nat) (k : (ys : Array Expr) → (eqs : Array Expr) → (args : Array Expr) → (mask : Array Bool) → (type : Expr) → MetaM α) @@ -132,9 +134,11 @@ where let some k := args.getIdx? lhs | unreachable! let mask := mask.set! k false let args := args.map fun arg => if arg == lhs then rhs else arg - let args := args.push (← mkEqRefl rhs) + let arg ← mkEqRefl rhs let typeNew := typeNew.replaceFVar lhs rhs - return (← go ys eqs args (mask.push false) (i+1) typeNew) + return ← withReplaceFVarId lhs.fvarId! rhs do + withReplaceFVarId y.fvarId! arg do + go ys eqs (args.push arg) (mask.push false) (i+1) typeNew go (ys.push y) eqs (args.push y) (mask.push true) (i+1) typeNew else let arg ← if let some (_, _, rhs) ← matchEq? d then @@ -152,7 +156,9 @@ where they are not eagerly evaluated. -/ if ys.size == 1 then if (← inferType ys[0]!).isConstOf ``Unit && !(← dependsOn type ys[0]!.fvarId!) then - return (← k #[] #[] #[mkConst ``Unit.unit] #[false] type) + let rhs := mkConst ``Unit.unit + return ← withReplaceFVarId ys[0]!.fvarId! rhs do + return (← k #[] #[] #[rhs] #[false] type) k ys eqs args mask type isNamedPatternProof (type : Expr) (h : Expr) : Bool := diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index f44a588264..27790d1f3d 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -156,4 +156,259 @@ def refineThrough? (matcherApp : MatcherApp) (e : Expr) : catch _ => return none + +/-- +Given `n` and a non-dependent function type `α₁ → α₂ → ... → αₙ → Sort u`, returns the +types `α₁, α₂, ..., αₙ`. Throws an error if there are not at least `n` argument types or if a +later argument type depends on a prior one (i.e., it's a dependent function type). + +This can be used to infer the expected type of the alternatives when constructing a `MatcherApp`. +-/ +-- TODO: Which is the natural module for this? +def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do + let mut type := type + let mut ts := #[] + for i in [:n] do + type ← whnfForall type + let Expr.forallE _ α β _ ← pure type | throwError "expected {n} arguments, got {i}" + if β.hasLooseBVars then throwError "unexpected dependent type" + ts := ts.push α + type := β + return ts + +/-- +Performs a possibly type-changing transformation to a `MatcherApp`. + +* `onParams` is run on each parameter and discriminant +* `onMotive` runs on the body of the motive, and is passed the motive parameters + (one for each `MatcherApp.discrs`) +* `onAlt` runs on each alternative, and is passed the expected type of the alternative, + as inferred from the motive +* `onRemaining` runs on the remaining arguments (and may change their number) + +If `useSplitter` is true, the matcher is replaced with the splitter. +NB: Not all operations on `MatcherApp` can handle one `matcherName` is a splitter. + +The array `addEqualities`, if provided, indicates for which of the discriminants an equality +connecting the discriminant to the parameters of the alternative (like in `match h : x with …`) +should be added (if it is isn't already there). + +This function works even if the the type of alternatives do *not* fit the inferred type. This +allows you to post-process the `MatcherApp` with `MatcherApp.inferMatchType`, which will +infer a type, given all the alternatives. +-/ +def transform (matcherApp : MatcherApp) + (useSplitter := false) + (addEqualities : Array Bool := mkArray matcherApp.discrs.size false) + (onParams : Expr → MetaM Expr := pure) + (onMotive : Array Expr → Expr → MetaM Expr := fun _ e => pure e) + (onAlt : Expr → Expr → MetaM Expr := fun _ e => pure e) + (onRemaining : Array Expr → MetaM (Array Expr) := pure) : + MetaM MatcherApp := do + + if addEqualities.size != matcherApp.discrs.size then + throwError "MatcherApp.transform: addEqualities has wrong size" + + -- Do not add equalities when the matcher already does so + let addEqualities := Array.zipWith addEqualities matcherApp.discrInfos fun b di => + if di.hName?.isSome then false else b + + -- We also handle CasesOn applications here, and need to treat them specially in a + -- few places. + -- TODO: Expand MatcherApp with the necessary fields to make this more uniform + -- (in particular, include discrEq and whether there is a splitter) + let isCasesOn := isCasesOnRecursor (← getEnv) matcherApp.matcherName + + let numDiscrEqs ← + if isCasesOn then pure 0 else + match ← getMatcherInfo? matcherApp.matcherName with + | some info => pure info.getNumDiscrEqs + | none => throwError "matcher {matcherApp.matcherName} has no MatchInfo found" + + let params' ← matcherApp.params.mapM onParams + let discrs' ← matcherApp.discrs.mapM onParams + + + let (motive', uElim) ← lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do + unless motiveArgs.size == matcherApp.discrs.size do + throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" + let mut motiveBody' ← onMotive motiveArgs motiveBody + + -- Prepend (x = e) → to the motive when an equality is requested + for arg in motiveArgs, discr in discrs', b in addEqualities do if b then + motiveBody' ← mkArrow (← mkEq discr arg) motiveBody' + + return (← mkLambdaFVars motiveArgs motiveBody', ← getLevel motiveBody') + + let matcherLevels ← match matcherApp.uElimPos? with + | none => pure matcherApp.matcherLevels + | some pos => pure <| matcherApp.matcherLevels.set! pos uElim + + -- We pass `Eq.refl`s for all the equations we added as extra arguments + -- (and count them along the way) + let mut remaining' := #[] + let mut extraEqualities : Nat := 0 + for discr in discrs'.reverse, b in addEqualities.reverse do if b then + remaining' := remaining'.push (← mkEqRefl discr) + extraEqualities := extraEqualities + 1 + + if useSplitter && !isCasesOn then + -- We replace the matcher with the splitter + let matchEqns ← Match.getEquationsFor matcherApp.matcherName + let splitter := matchEqns.splitterName + + let aux1 := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params' + let aux1 := mkApp aux1 motive' + let aux1 := mkAppN aux1 discrs' + unless (← isTypeCorrect aux1) do + logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux1}" + check aux1 + let origAltTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux1) + + let aux2 := mkAppN (mkConst splitter matcherLevels.toList) params' + let aux2 := mkApp aux2 motive' + let aux2 := mkAppN aux2 discrs' + unless (← isTypeCorrect aux2) do + logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux2}" + check aux2 + let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux2) + + let mut alts' := #[] + for alt in matcherApp.alts, + numParams in matcherApp.altNumParams, + splitterNumParams in matchEqns.splitterAltNumParams, + origAltType in origAltTypes, + altType in altTypes do + let alt' ← Match.forallAltTelescope origAltType (numParams - numDiscrEqs) 0 fun ys _eqs args _mask _bodyType => do + let altType ← instantiateForall altType ys + -- The splitter inserts its extra paramters after the first ys.size parameters, before + -- the parameters for the numDiscrEqs + forallBoundedTelescope altType (splitterNumParams - ys.size) fun ys2 altType => do + forallBoundedTelescope altType numDiscrEqs fun ys3 altType => do + forallBoundedTelescope altType extraEqualities fun ys4 altType => do + let alt ← try instantiateLambda alt (args ++ ys3) + catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative" + let alt' ← onAlt altType alt + mkLambdaFVars (ys ++ ys2 ++ ys3 ++ ys4) alt' + alts' := alts'.push alt' + + remaining' := remaining' ++ (← onRemaining matcherApp.remaining) + + return { matcherApp with + matcherName := splitter + matcherLevels := matcherLevels + params := params' + motive := motive' + discrs := discrs' + altNumParams := matchEqns.splitterAltNumParams.map (· + extraEqualities) + alts := alts' + remaining := remaining' + } + else + let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params' + let aux := mkApp aux motive' + let aux := mkAppN aux discrs' + unless (← isTypeCorrect aux) do + -- check aux + logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}" + check aux + let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux) + + let mut alts' := #[] + for alt in matcherApp.alts, + numParams in matcherApp.altNumParams, + altType in altTypes do + let alt' ← forallBoundedTelescope altType numParams fun xs altType => do + forallBoundedTelescope altType extraEqualities fun ys4 altType => do + let alt ← instantiateLambda alt xs + let alt' ← onAlt altType alt + mkLambdaFVars (xs ++ ys4) alt' + alts' := alts'.push alt' + + remaining' := remaining' ++ (← onRemaining matcherApp.remaining) + + return { matcherApp with + matcherLevels := matcherLevels + params := params' + motive := motive' + discrs := discrs' + altNumParams := matcherApp.altNumParams.map (· + extraEqualities) + alts := alts' + remaining := remaining' + } + + + +/-- +Given a `MatcherApp`, replaces the motive with one that is inferred from the actual types of the +alternatives. + +For example, given +``` +(match (motive := Nat → Unit → ?) n with + 0 => 1 + _ => true) () +``` +(for any `?`; the motive’s result type be ignored) will give this type +``` +(match n with + | 0 => Nat + | _ => Bool) +``` + +The given `MatcherApp` must not use a splitter in `matcherName`. +The resulting expression *will* use the splitter corresponding to `matcherName` (this is necessary +for the construction). + +Interally, this needs to reduce the matcher in a given branch; this is done using +`Split.simpMatchTarget`. +-/ +def inferMatchType (matcherApp : MatcherApp) : MetaM MatcherApp := do + -- In matcherApp.motive, replace the (dummy) matcher body with a type + -- derived from the inferred types of the alterantives + let nExtra := matcherApp.remaining.size + matcherApp.transform (useSplitter := true) + (onMotive := fun motiveArgs body => do + let extraParams ← arrowDomainsN nExtra body + let propMotive ← mkLambdaFVars motiveArgs (.sort levelZero) + let propAlts ← matcherApp.alts.mapM fun termAlt => + lambdaTelescope termAlt fun xs termAltBody => do + -- We have alt parameters and parameters corresponding to the extra args + let xs1 := xs[0 : xs.size - nExtra] + let xs2 := xs[xs.size - nExtra : xs.size] + -- logInfo m!"altIH: {xs} => {altIH}" + let altType ← inferType termAltBody + for x in xs2 do + if altType.hasAnyFVar (· == x.fvarId!) then + throwError "Type {altType} of alternative {termAlt} still depends on {x}" + -- logInfo m!"altIH type: {altType}" + mkLambdaFVars xs1 altType + let matcherLevels ← match matcherApp.uElimPos? with + | none => pure matcherApp.matcherLevels + | some pos => pure <| matcherApp.matcherLevels.set! pos levelOne + let typeMatcherApp := { matcherApp with + motive := propMotive + matcherLevels := matcherLevels + discrs := motiveArgs + alts := propAlts + remaining := #[] + } + mkArrowN extraParams typeMatcherApp.toExpr + ) + (onAlt := fun expAltType alt => do + let altType ← inferType alt + let eq ← mkEq expAltType altType + let proof ← mkFreshExprSyntheticOpaqueMVar eq + let goal := proof.mvarId! + -- logInfo m!"Goal: {goal}" + let goal ← Split.simpMatchTarget goal + -- logInfo m!"Goal after splitting: {goal}" + try + goal.refl + catch _ => + logInfo m!"Cannot close goal after splitting: {goal}" + goal.admit + mkEqMPR proof alt + ) + end Lean.Meta.MatcherApp diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index 41fbe22c5f..7f4917dca8 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/src/Lean/Meta/Tactic.lean @@ -37,3 +37,4 @@ import Lean.Meta.Tactic.IndependentOf import Lean.Meta.Tactic.Symm import Lean.Meta.Tactic.Backtrack import Lean.Meta.Tactic.SolveByElim +import Lean.Meta.Tactic.FunInd diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean new file mode 100644 index 0000000000..3e21d32e1c --- /dev/null +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -0,0 +1,924 @@ +/- +Copyright (c) 2024 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.Basic +import Lean.Meta.Match.MatcherApp.Transform +import Lean.Meta.Check +import Lean.Meta.Tactic.Cleanup +import Lean.Meta.Tactic.Subst +import Lean.Meta.Injective -- for elimOptParam +import Lean.Elab.PreDefinition.WF.Eqns +import Lean.Elab.PreDefinition.WF.PackMutual +import Lean.Elab.Command + +/-! +This module contains code to derive, from the definition of a recursive function +(or mutually recursive functions) defined by well-founded recursion, a +**functional induction principle** tailored to proofs about that function(s). For +example from: + +``` +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) +derive_functional_induction ackermann +``` +we get +``` +ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) + (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) + (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) + (x x : Nat) : motive x x +``` + +## Specification + +The functional induction principle takes the same fixed parameters as the function, and +the motive takes the same non-fixed parameters as the original function. + +For each branch of the original function, there is a case in the induction principle. +Here "branch" roughly corresponds to tail-call positions: branches of top-level +`if`-`then`-`else` and of `match` expressions. + +For every recursive call in that branch, an induction hypothesis asserting the +motive for the arguments of the recursive call is provided. +If the recursive call is under binders and it, or its proof of termination, +depend on the the bound values, then these become assumptions of the inductive +hypothesis. + +Additionally, the local context of the branch (e.g. the condition of an +if-then-else; a let-binding, a have-binding) is provided as assumptions in the +corresponding induction case, if they are likely to be useful (as determined +by `MVarId.cleanup`). + +Mutual recursion is supported and results in multiple motives. + + +## Implementation overview + +For a non-mutual, unary function `foo` (or else for the `_unary` function), we + +1. expect its definition, possibly after some `whnf`’ing, to be of the form + ``` + def foo := fun x₁ … xₙ (y : a) => WellFounded.fix (fun y' oldIH => body) y + ``` + where `xᵢ…` are the fixed parameter prefix and `y` is the varying parameter of + the function. + +2. From this structure we derive the type of the motive, and start assembling the induction + principle: + ``` + def foo.induct := fun x₁ … xₙ (motive : (y : a) → Prop) => + fix (fun y' newIH => T[body]) + ``` + +3. The first phase, transformation `T1[body]` (implemented in) `buildInductionBody`, + mirrors the branching structure of `foo`, i.e. replicates `dite` and some matcher applications, + while adjusting their motive. It also unfolds calls to `oldIH` and collects induction hypotheses + in conditions (see below). + + In particular, when translating a `match` it is prepared to recognize the idiom + as introduced by `mkFix` via `Lean.Meta.MatcherApp.addArg?`, which refines the type of `oldIH` + throughout the match. The transformation will replace `oldIH` with `newIH` here. + ``` + T[(match (motive := fun oldIH => …) y with | … => fun oldIH' => body) oldIH] + ==> (match (motive := fun newIH => …) y with | … => fun newIH' => T[body]) newIH + ``` + + In addition, the information gathered from the match is preserved, so that when performing the + proof by induction, the user can reliably enter the right case. To achieve this + + * the matcher is replaced by its splitter, which brings extra assumptions into scope when + patterns are overlapping + * simple discriminants that are mentioned in the goal (i.e plain parameters) are instantiated + in the code. + * for discriminants that are not instantiated that way, equalities connecting the discriminant + to the instantiation are added (just as if the user wrote `match h : x with …`) + +4. When a tail position (no more branching) is found, function `buildInductionCase` assembles the + type of the case: a fresh `MVar` asserts the current goal, unwanted values from the local context + are cleared, and the current `body` is searched for recursive calls using `collectIHs`, + which are then asserted as inductive hyptheses in the `MVar`. + +5. The function `collectIHs` walks the term and collects the induction hypotheses for the current case + (with proofs). When it encounters a saturated application of `oldIH x proof`, it returns + `newIH x proof : motive x`. + + Since `x` and `proof` can contain further recursive calls, it uses + `foldCalls` to replace these with calls to `foo`. This assumes that the + termination proof `proof` works nevertheless. + + Again, `collectIHs` may encounter the `Lean.Meta.Matcherapp.addArg?` idiom, and again it threads `newIH` + through, replacing the extra argument. The resulting type of this induction hypothesis is now + itself a `match` statement (cf. `Lean.Meta.MatcherApp.inferMatchType`) + + The termination proof of `foo` may have abstracted over some proofs; these proofs must be transferred, so + auxillary lemmas are unfolded if needed. + +6. The function `foldCalls` replaces calls to `oldIH` with calls to `foo` that + make sense to the user. + + At the end of this transformation, no mention of `oldIH` must remain. + +7. After this construction, the MVars introduced by `buildInductionCase` are turned into parameters. + +The resulting term then becomes `foo.induct` at its inferred type. + +If `foo` is not unary and/or part of a mutual reduction, then the induction theorem for `foo._unary` +(i.e. the unary non-mutual recursion function produced by the equation compiler) +of the form +``` +foo._unary.induct : {motive : (a ⊗' b) ⊕' c → Prop} → + (case1 : ∀ …, motive (PSum.inl (x,y)) → …) → … → + (x : (a ⊗' b) ⊕' c) → motive x +``` +will first in `unpackMutualInduction` be turned into a joint induction theorem of the form +``` +foo.mutual_induct : {motive1 : a → b → Prop} {motive2 : c → Prop} → + (case1 : ∀ …, motive1 x y → …) → … → + ((x : a) → (y : b) → motive1 x y) ∧ ((z : c) → motive2 z) +``` +where all the `PSum`/`PSigma` encoding has been resolved. This theorem is attached to the +name of the first function in the mutual group, like the `._unary` definition. + +Finally, in `deriveUnpackedInduction`, for each of the funtions in the mutual group, a simple +projection yields the final `foo.induct` theorem: +``` +foo.induct : {motive1 : a → b → Prop} {motive2 : c → Prop} → + (case1 : ∀ …, motive1 x y → …) → … → + (x : a) → (y : b) → motive1 x y +``` + +-/ + +set_option autoImplicit false + +namespace Lean.Tactic.FunInd + +open Lean Elab Meta + +/-- Opens the body of a lambda, _without_ putting the free variable into the local context. +This is used when replacing parameters with different expressions. +This way it will not be picked up by metavariables. +-/ +def removeLamda {α} (e : Expr) (k : FVarId → Expr → MetaM α) : MetaM α := do + let .lam _n _d b _bi := ← whnfD e | throwError "removeLamda: expected lambda, got {e}" + let x ← mkFreshFVarId + let b := b.instantiate1 (.fvar x) + k x b + +/-- Replace calls to oldIH back to calls to the original function. At the end, if `oldIH` occurs, an error is thrown. -/ +partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do + unless e.containsFVar oldIH do + return e + + if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then + let #[arg, _proof] := e.getAppArgs | unreachable! + let arg' ← foldCalls fn oldIH arg + return .app fn arg' + + if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then + if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then + let matcherApp' ← matcherApp.transform + (onParams := foldCalls fn oldIH) + (onMotive := fun _motiveArgs motiveBody => do + let some (_extra, body) := motiveBody.arrow? | throwError "motive not an arrow" + foldCalls fn oldIH body) + (onAlt := fun _altType alt => do + removeLamda alt fun oldIH alt => do + foldCalls fn oldIH alt) + (onRemaining := fun _ => pure #[]) + return matcherApp'.toExpr + + if e.getAppArgs.any (·.isFVarOf oldIH) then + -- Sometimes Fix.lean abstracts over oldIH in a proof definition. + -- So beta-reduce that definition. + + -- Need to look through theorems here! + let e' ← withTransparency .all do whnf e + if e == e' then + throwError "foldCalls: cannot reduce application of {e.getAppFn} in {indentExpr e} " + return ← foldCalls fn oldIH e' + + if let some (n, t, v, b) := e.letFun? then + let t' ← foldCalls fn oldIH t + let v' ← foldCalls fn oldIH v + return ← withLocalDecl n .default t' fun x => do + let b' ← foldCalls fn oldIH (b.instantiate1 x) + mkLetFun x v' b' + + match e with + | .app e1 e2 => + return .app (← foldCalls fn oldIH e1) (← foldCalls fn oldIH e2) + + | .lam n t body bi => + let t' ← foldCalls fn oldIH t + return ← withLocalDecl n bi t' fun x => do + let body' ← foldCalls fn oldIH (body.instantiate1 x) + mkLambdaFVars #[x] body' + + | .forallE n t body bi => + let t' ← foldCalls fn oldIH t + return ← withLocalDecl n bi t' fun x => do + let body' ← foldCalls fn oldIH (body.instantiate1 x) + mkForallFVars #[x] body' + + | .letE n t v b _ => + let t' ← foldCalls fn oldIH t + let v' ← foldCalls fn oldIH v + return ← withLetDecl n t' v' fun x => do + let b' ← foldCalls fn oldIH (b.instantiate1 x) + mkLetFVars #[x] b' + + | .mdata m b => + return .mdata m (← foldCalls fn oldIH b) + + | .proj t i e => + return .proj t i (← foldCalls fn oldIH e) + + | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. => + unreachable! -- cannot contain free variables, so early exit above kicks in + + | .fvar .. => + throwError m!"collectIHs: cannot eliminate unsaturated call to induction hypothesis" + + +/-- +Given proofs of `P₁`, …, `Pₙ`, returns a proof of `P₁ ∧ … ∧ Pₙ`. +If `n = 0` returns a proof of `True`. +If `n = 1` returns the proof of `P₁`. +-/ +def mkAndIntroN : Array Expr → MetaM Expr +| #[] => return mkConst ``True.intro [] +| #[e] => return e +| es => es.foldrM (start := es.size - 1) (fun a b => mkAppM ``And.intro #[a,b]) es.back + +/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ`, return the proof of `Pᵢ` -/ +def mkProjAndN (n i : Nat) (e : Expr) : Expr := Id.run do + let mut value := e + for _ in [:i] do + value := mkProj ``And 1 value + if i + 1 < n then + value := mkProj ``And 0 value + return value + + +-- Non-tail-positions: Collect induction hypotheses +-- (TODO: Worth folding with `foldCalls`, like before?) +-- (TODO: Accumulated with a left fold) +partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Array Expr) := do + unless e.containsFVar oldIH do + return #[] + + if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then + let #[arg, proof] := e.getAppArgs | unreachable! + + let arg' ← foldCalls fn oldIH arg + let proof' ← foldCalls fn oldIH proof + let ihs ← collectIHs fn oldIH newIH arg + + return ihs.push (mkApp2 (.fvar newIH) arg' proof') + + if let some (n, t, v, b) := e.letFun? then + let ihs1 ← collectIHs fn oldIH newIH v + let v' ← foldCalls fn oldIH v + return ← withLetDecl n t v' fun x => do + let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x) + let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·) + return ihs1 ++ ihs2 + + if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then + if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then + + let matcherApp' ← matcherApp.transform + (onParams := foldCalls fn oldIH) + (onMotive := fun xs _body => do + -- Remove the old IH that was added in mkFix + let eType ← newIH.getType + let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i eTypeAbst => do + let motiveArg := xs[i]! + let discr := matcherApp.discrs[i]! + let eTypeAbst ← kabstract eTypeAbst discr + return eTypeAbst.instantiate1 motiveArg + + -- Will later be overriden with a type that’s itself a match + -- statement and the infered alt types + let dummyGoal := mkConst ``True [] + mkArrow eTypeAbst dummyGoal) + (onAlt := fun altType alt => do + removeLamda alt fun oldIH' alt => do + forallBoundedTelescope altType (some 1) fun newIH' _goal' => do + let #[newIH'] := newIH' | unreachable! + let altIHs ← collectIHs fn oldIH' newIH'.fvarId! alt + let altIH ← mkAndIntroN altIHs + mkLambdaFVars #[newIH'] altIH) + (onRemaining := fun _ => pure #[mkFVar newIH]) + let matcherApp'' ← matcherApp'.inferMatchType + + return #[ matcherApp''.toExpr ] + + if e.getAppArgs.any (·.isFVarOf oldIH) then + -- Sometimes Fix.lean abstracts over oldIH in a proof definition. + -- So beta-reduce that definition. + + -- Need to look through theorems here! + let e' ← withTransparency .all do whnf e + if e == e' then + throwError "collectIHs: cannot reduce application of {e.getAppFn} in {indentExpr e} " + return ← collectIHs fn oldIH newIH e' + + if e.getAppArgs.any (·.isFVarOf oldIH) then + throwError "collectIHs: could not collect recursive calls from call {indentExpr e}" + + match e with + | .letE n t v b _ => + let ihs1 ← collectIHs fn oldIH newIH v + let v' ← foldCalls fn oldIH v + return ← withLetDecl n t v' fun x => do + let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x) + let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·) + return ihs1 ++ ihs2 + + | .app e1 e2 => + return (← collectIHs fn oldIH newIH e1) ++ (← collectIHs fn oldIH newIH e2) + + | .proj _ _ e => + return ← collectIHs fn oldIH newIH e + + | .forallE n t body bi => + let t' ← foldCalls fn oldIH t + return ← withLocalDecl n bi t' fun x => do + let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x) + ihs.mapM (mkLambdaFVars (usedOnly := true) #[x]) + + | .lam n t body bi => + let t' ← foldCalls fn oldIH t + return ← withLocalDecl n bi t' fun x => do + let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x) + ihs.mapM (mkLambdaFVars (usedOnly := true) #[x]) + + | .mdata _m b => + return ← collectIHs fn oldIH newIH b + + | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. => + unreachable! -- cannot contain free variables, so early exit above kicks in + + | .fvar _ => + throwError "collectIHs: could not collect recursive calls, unsaturated application of old induction hypothesis" + +-- Because of term duplications we might encounter the same IH multiple times. +-- We deduplicate them (by type, not proof term) here. +-- This could be improved and catch cases where the same IH is used in different contexts. +-- (Cf. `assignSubsumed` in `WF.Fix`) +def deduplicateIHs (vals : Array Expr) : MetaM (Array Expr) := do + let mut vals' := #[] + let mut types := #[] + for v in vals do + let t ← inferType v + unless types.contains t do + vals' := vals'.push v + types := types.push t + return vals' + +def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do + let mut mvarid := mvarid + for v in vals.reverse, i in [0:vals.size] do + mvarid ← mvarid.assert s!"ih{i+1}" (← inferType v) v + return mvarid + +/-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis. -/ +def buildInductionCase (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve : Array FVarId) + (goal : Expr) (IHs : Array Expr) (e : Expr) : MetaM Expr := do + let IHs := IHs ++ (← collectIHs fn oldIH newIH e) + let IHs ← deduplicateIHs IHs + + let mvar ← mkFreshExprSyntheticOpaqueMVar goal (tag := `hyp) + let mut mvarId := mvar.mvarId! + mvarId ← assertIHs IHs mvarId + for fvarId in toClear do + mvarId ← mvarId.clear fvarId + mvarId ← mvarId.cleanup (toPreserve := toPreserve) + mvarId ← substVars mvarId + let mvar ← instantiateMVars mvar + pure mvar + +/-- +Like `mkLambdaFVars (usedOnly := true)`, but + + * silently skips expression in `xs` that are not `.isFVar` + * returns a mask (same size as `xs`) indicating which variables have been abstracted + (`true` means was abstracted). + +The result `r` can be applied with `r.beta (maskArray mask args)`. + +We use this when generating the functional induction principle to refine the goal through a `match`, +here `xs` are the discriminans of the `match`. +We do not expect non-trivial discriminants to appear in the goal (and if they do, the user will +get a helpful equality into the context). +-/ +def mkLambdaFVarsMasked (xs : Array Expr) (e : Expr) : MetaM (Array Bool × Expr) := do + let mut e := e + let mut xs := xs + let mut mask := #[] + while ! xs.isEmpty do + let discr := xs.back + if discr.isFVar && e.containsFVar discr.fvarId! then + e ← mkLambdaFVars #[discr] e + mask := mask.push true + else + mask := mask.push false + xs := xs.pop + return (mask.reverse, e) + +/-- `maskArray mask xs` keeps those `x` where the corresponding entry in `mask` is `true` -/ +def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do + let mut ys := #[] + for b in mask, x in xs do + if b then ys := ys.push x + return ys + +partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId) + (goal : Expr) (oldIH newIH : FVarId) (IHs : Array Expr) (e : Expr) : MetaM Expr := do + + if e.isDIte then + let #[_α, c, h, t, f] := e.getAppArgs | unreachable! + let IHs := IHs ++ (← collectIHs fn oldIH newIH c) + let c' ← foldCalls fn oldIH c + let h' ← foldCalls fn oldIH h + let t' ← withLocalDecl `h .default c' fun h => do + let t ← instantiateLambda t #[h] + let t' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t + mkLambdaFVars #[h] t' + let f' ← withLocalDecl `h .default (mkNot c') fun h => do + let f ← instantiateLambda f #[h] + let f' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f + mkLambdaFVars #[h] f' + let u ← getLevel goal + return mkApp5 (mkConst ``dite [u]) goal c' h' t' f' + + if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then + -- Collect IHs from the parameters and discrs of the matcher + let paramsAndDiscrs := matcherApp.params ++ matcherApp.discrs + let IHs := IHs ++ (← paramsAndDiscrs.concatMapM (collectIHs fn oldIH newIH)) + + -- Calculate motive + let eType ← newIH.getType + let motiveBody ← mkArrow eType goal + let (mask, absMotiveBody) ← mkLambdaFVarsMasked matcherApp.discrs motiveBody + + -- A match that refines the parameter has been modified by `Fix.lean` to refine the IH, + -- so we need to replace that IH + if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then + let matcherApp' ← matcherApp.transform (useSplitter := true) + (addEqualities := mask.map not) + (onParams := foldCalls fn oldIH) + (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs))) + (onAlt := fun expAltType alt => do + removeLamda alt fun oldIH' alt => do + forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do + let #[newIH'] := newIH' | unreachable! + let alt' ← buildInductionBody fn (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! IHs alt + mkLambdaFVars #[newIH'] alt') + (onRemaining := fun _ => pure #[.fvar newIH]) + return matcherApp'.toExpr + + -- A match that does not refine the parameter, but that we still want to split into separate + -- cases + if matcherApp.remaining.isEmpty then + -- Calculate motive + let (mask, absMotiveBody) ← mkLambdaFVarsMasked matcherApp.discrs goal + + let matcherApp' ← matcherApp.transform (useSplitter := true) + (addEqualities := mask.map not) + (onParams := foldCalls fn oldIH) + (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs))) + (onAlt := fun expAltType alt => do + buildInductionBody fn toClear toPreserve expAltType oldIH newIH IHs alt) + return matcherApp'.toExpr + + if let .letE n t v b _ := e then + let IHs := IHs ++ (← collectIHs fn oldIH newIH v) + let t' ← foldCalls fn oldIH t + let v' ← foldCalls fn oldIH v + return ← withLetDecl n t' v' fun x => do + let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x) + mkLetFVars #[x] b' + + if let some (n, t, v, b) := e.letFun? then + let IHs := IHs ++ (← collectIHs fn oldIH newIH v) + let t' ← foldCalls fn oldIH t + let v' ← foldCalls fn oldIH v + return ← withLocalDecl n .default t' fun x => do + let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x) + mkLetFun x v' b' + + buildInductionCase fn oldIH newIH toClear toPreserve goal IHs e + +partial def findFixF {α} (name : Name) (e : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do + lambdaTelescope e fun params body => do + if body.isAppOf ``WellFounded.fixF then + k params body + else if body.isAppOf ``WellFounded.fix then + findFixF name (← unfoldDefinition body) fun args e' => k (params ++ args) e' + else + throwError m!"Function {name} does not look like a function defined by well-founded " ++ + m!"recursion.\nNB: If {name} is not itself recursive, but contains an inner recursive " ++ + m!"function (via `let rec` or `where`), try `{name}.go` where `go` is name of the inner " ++ + "function." + +/-- +Given a definition `foo` defined via `WellFounded.fixF`, derive a suitable induction principle +`foo.induct` for it. See module doc for details. + -/ +def deriveUnaryInduction (name : Name) : MetaM Name := do + let inductName := .append name `induct + if ← hasConst inductName then return inductName + + let info ← getConstInfoDefn name + findFixF name info.value fun params body => body.withApp fun f fixArgs => do + -- logInfo f!"{fixArgs}" + unless params.size > 0 do + throwError "Value of {name} is not a lambda application" + unless f.isConstOf ``WellFounded.fixF do + throwError "Term isn’t application of {``WellFounded.fixF}, but of {f}" + let #[argType, rel, _motive, body, arg, acc] := fixArgs | + throwError "Application of WellFounded.fixF has wrong arity {fixArgs.size}" + unless ← isDefEq arg params.back do + throwError "fixF application argument {arg} is not function argument " + let [argLevel, _motiveLevel] := f.constLevels! | unreachable! + + let motiveType ← mkArrow argType (.sort levelZero) + withLocalDecl `motive .default motiveType fun motive => do + + let e' := mkApp3 (.const ``WellFounded.fixF [argLevel, levelZero]) argType rel motive + let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) params.pop + let body' ← forallTelescope (← inferType e').bindingDomain! fun xs _ => do + let #[param, genIH] := xs | unreachable! + -- open body with the same arg + let body ← instantiateLambda body #[param] + removeLamda body fun oldIH body => do + let body' ← buildInductionBody fn #[genIH.fvarId!] #[] (.app motive param) oldIH genIH.fvarId! #[] body + if body'.containsFVar oldIH then + throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}" + mkLambdaFVars #[param, genIH] body' + + let e' := mkApp3 e' body' arg acc + + let e' ← mkLambdaFVars #[params.back] e' + let mvars ← getMVarsNoDelayed e' + let mvars ← mvars.mapM fun mvar => do + let (_, mvar) ← mvar.revertAfter motive.fvarId! + pure mvar + -- Using `mkLambdaFVars` on mvars directly does not reliably replace + -- the mvars with the parameter, in the presence of delayed assignemnts. + -- Also `abstractMVars` does not handle delayed assignments correctly (as of now). + -- So instead we bring suitable fvars into scope and use `assign`; this handles + -- delayed assignemnts correctly. + -- NB: This idiom only works because + -- * we know that the `MVars` have the right local context (thanks to `mvarId.revertAfter`) + -- * the MVars are independent (so we don’t need to reorder them) + -- * we do no need the mvars in their unassigned form later + let e' ← Meta.withLocalDecls + (mvars.mapIdx (fun i mvar => (s!"case{i.val+1}", .default, (fun _ => mvar.getType)))) + fun xs => do + for mvar in mvars, x in xs do + mvar.assign x + let e' ← instantiateMVars e' + mkLambdaFVars xs e' + + -- We could pass (usedOnly := true) below, and get nicer induction principles that + -- do do not mention odd unused parameters. + -- But the downside is that automatic instantiation of the principle (e.g. in a tactic + -- that derives them from an function application in the goal) is harder, as + -- one would have to infer or keep track of which parameters to pass. + -- So for now lets just keep them around. + let e' ← mkLambdaFVars (binderInfoForMVars := .default) (params.pop ++ #[motive]) e' + let e' ← instantiateMVars e' + + let eTyp ← inferType e' + let eTyp ← elimOptParam eTyp + -- logInfo m!"eTyp: {eTyp}" + unless (← isTypeCorrect e') do + logError m!"failed to derive induction priciple:{indentExpr e'}" + check e' + + addDecl <| Declaration.thmDecl + { name := inductName, levelParams := info.levelParams, type := eTyp, value := e' } + return inductName + +/-- +In the type of `value`, reduces +* Beta-redexes +* `PSigma.casesOn (PSigma.mk a b) (fun x y => k x y) --> k a b` +* `PSum.casesOn (PSum.inl x) k₁ k₂ --> k₁ x` +* `foo._unary (PSum.inl (PSigma.mk a b)) --> foo a b` +and then wraps `value` in an appropriate type hint. +-/ +def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do + -- TODO: Make arities (or varnames) part of eqnInfo + let arities ← eqnInfo.declNames.mapM fun name => do + let ci ← getConstInfoDefn name + lambdaTelescope ci.value fun xs _body => return xs.size - eqnInfo.fixedPrefixSize + + let t ← Meta.transform (← inferType value) (skipConstInApp := true) (pre := fun e => do + -- Need to beta-reduce first + let e' := e.headBeta + if e' != e then + return .visit e' + -- Look for PSigma redexes + if e.isAppOf ``PSigma.casesOn then + let args := e.getAppArgs + if 5 ≤ args.size then + let scrut := args[3]! + let k := args[4]! + let extra := args[5:] + if scrut.isAppOfArity ``PSigma.mk 4 then + let #[_, _, x, y] := scrut.getAppArgs | unreachable! + let e' := (k.beta #[x, y]).beta extra + return .visit e' + -- Look for PSum redexes + if e.isAppOf ``PSum.casesOn then + let args := e.getAppArgs + if 6 ≤ args.size then + let scrut := args[3]! + let k₁ := args[4]! + let k₂ := args[5]! + let extra := args[6:] + if scrut.isAppOfArity ``PSum.inl 3 then + let e' := (k₁.beta #[scrut.appArg!]).beta extra + return .visit e' + if scrut.isAppOfArity ``PSum.inr 3 then + let e' := (k₂.beta #[scrut.appArg!]).beta extra + return .visit e' + -- Look for _unary redexes + if e.isAppOf eqnInfo.declNameNonRec then + let args := e.getAppArgs + if eqnInfo.fixedPrefixSize + 1 ≤ args.size then + let packedArg := args.back + let (i, unpackedArgs) ← WF.unpackArg arities packedArg + let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels! + let e' := mkAppN e' args.pop + let e' := mkAppN e' unpackedArgs + let e' := mkAppN e' args[eqnInfo.fixedPrefixSize+1:] + return .continue e' + + return .continue e) + mkExpectedTypeHint value t + +/-- Given type `A ⊕' B ⊕' … ⊕' D`, return `[A, B, …, D]` -/ +partial def unpackPSum (type : Expr) : List Expr := + if type.isAppOfArity ``PSum 2 then + if let #[a, b] := type.getAppArgs then + a :: unpackPSum b + else unreachable! + else + [type] + +/-- Given `A ⊗' B ⊗' … ⊗' D` and `R`, return `A → B → … → D → R` -/ +partial def uncurryPSumArrow (domain : Expr) (codomain : Expr) : MetaM Expr := do + if domain.isAppOfArity ``PSigma 2 then + let #[a, b] := domain.getAppArgs | unreachable! + withLocalDecl `x .default a fun x => do + mkForallFVars #[x] (← uncurryPSumArrow (b.beta #[x]) codomain) + else + mkArrow domain codomain + +/-- +Given expression `e` with type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]` +return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]` +-/ +partial def uncurryPSigma (e : Expr) : MetaM Expr := do + let packedDomain := (← inferType e).bindingDomain! + go packedDomain packedDomain #[] +where + go (packedDomain domain : Expr) args : MetaM Expr := do + if domain.isAppOfArity ``PSigma 2 then + let #[a, b] := domain.getAppArgs | unreachable! + withLocalDecl `x .default a fun x => do + mkLambdaFVars #[x] (← go packedDomain (b.beta #[x]) (args.push x)) + else + withLocalDecl `x .default domain fun x => do + let args := args.push x + let packedArg ← WF.mkUnaryArg packedDomain args + mkLambdaFVars #[x] (e.beta #[packedArg]) + +/-- +Iterated `PSigma.casesOn`: Given `y : a ⊗' b ⊗' …` and a type `codomain`, +and `alt : (x : a) → (y : b) → codomain`, uses `PSigma.casesOn` to invoke `alt` on `y`. + +This very is similar to `Lean.Predefinition.WF.mkPSigmaCasesOn`, but takes a lambda rather than +free variables. +-/ +partial def mkPSigmaNCasesOn (y : FVarId) (codomain : Expr) (alt : Expr) : MetaM Expr := do + let mvar ← mkFreshExprSyntheticOpaqueMVar codomain + let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := mvarId.withContext do + if (← inferType (mkFVar y)).isAppOfArity ``PSigma 2 then + let #[s] ← mvarId.cases y | unreachable! + go s.mvarId s.fields[1]!.fvarId! (ys.push s.fields[0]!) + else + let ys := ys.push (mkFVar y) + mvarId.assign (alt.beta ys) + go mvar.mvarId! y #[] + instantiateMVars mvar + +/-- +Given expression `e` with type `(x : A) → (y : B[x]) → … → (z : D[x,y]) → R` +returns an expression of type `(x : A ⊗' B ⊗' … ⊗' D) → R`. +-/ +partial def curryPSigma (e : Expr) : MetaM Expr := do + let (d, codomain) ← forallTelescope (← inferType e) fun xs codomain => do + if xs.any (codomain.containsFVar ·.fvarId!) then + throwError "curryPSum: codomain depends on domain variables" + let mut d ← inferType xs.back + for x in xs.pop.reverse do + d ← mkLambdaFVars #[x] d + d ← mkAppOptM ``PSigma #[some (← inferType x), some d] + return (d, codomain) + withLocalDecl `x .default d fun x => do + let value ← mkPSigmaNCasesOn x.fvarId! codomain e + mkLambdaFVars #[x] value + +/-- +Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e` +into scope as fresh local declarations and passes their FVars to the continuation `k`. +The `name` is used to form the variable names; uses `name1`, `name2`, … if there are multiple. +-/ +def withCurriedDecl {α} (name : String) (type : Expr) (k : Array Expr → MetaM α) : MetaM α := do + let some (d,c) := type.arrow? | throwError "withCurriedDecl: Expected arrow" + let motiveTypes ← (unpackPSum d).mapM (uncurryPSumArrow · c) + if let [t] := motiveTypes then + -- If a singleton, do not number the names. + withLocalDecl name .default t fun x => do k #[x] + else + go motiveTypes #[] +where + go : List Expr → Array Expr → MetaM α + | [], acc => k acc + | t::ts, acc => do + let name := s!"{name}{acc.size+1}" + withLocalDecl name .default t fun x => do + go ts (acc.push x) + + +/-- +Given expression `e` of type `(x : a ⊗' b ⊕' c ⊗' d) → e[x]`, wraps that expression +to produce an expression of the isomorphic type +``` +((x: a) → (y : b) → e[.inl (x,y)]) ∧ ((x : c) → (y : d) → e[.inr (x,y)]) +``` +-/ +def deMorganPSumPSigma (e : Expr) : MetaM Expr := do + let packedDomain := (← inferType e).bindingDomain! + let unaryTypes := unpackPSum packedDomain + shareIf (unaryTypes.length > 1) e fun e => do + let mut es := #[] + for unaryType in unaryTypes, i in [:unaryTypes.length] do + -- unary : (x : a ⊗ b) → e[inl x] + let unary ← withLocalDecl `x .default unaryType fun x => do + let packedArg ← WF.mkMutualArg unaryTypes.length packedDomain i x + mkLambdaFVars #[x] (e.beta #[packedArg]) + -- nary : (x : a) → (y : b) → e[inl (x,y)] + let nary ← uncurryPSigma unary + es := es.push nary + mkAndIntroN es + where + shareIf (b : Bool) (e : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do + if b then + withLetDecl `packed (← inferType e) e fun e => do mkLetFVars #[e] (← k e) + else + k e + + +-- Adapted from PackMutual: TODO: Compare and unify +/-- + Combine/pack the values of the different definitions in a single value + `x` is `PSum`, and we use `PSum.casesOn` to select the appropriate `preDefs.value`. + See: `packMutual`. + + Remark: this method does not replace the nested recursive `preDefValues` applications. + This step is performed by `transform` with the following `post` method. + -/ +private def packValues (x : Expr) (codomain : Expr) (preDefValues : Array Expr) : MetaM Expr := do + let varNames := preDefValues.map fun val => + if val.isLambda then val.bindingName! else `x + let mvar ← mkFreshExprSyntheticOpaqueMVar codomain + let rec go (mvarId : MVarId) (x : FVarId) (i : Nat) : MetaM Unit := do + if i < preDefValues.size - 1 then + /- + Names for the `cases` tactics. The names are important to preserve the user provided names (unary functions). + -/ + let givenNames : Array AltVarNames := + if i == preDefValues.size - 2 then + #[{ varNames := [varNames[i]!] }, { varNames := [varNames[i+1]!] }] + else + #[{ varNames := [varNames[i]!] }] + let #[s₁, s₂] ← mvarId.cases x (givenNames := givenNames) | unreachable! + s₁.mvarId.assign (mkApp preDefValues[i]! s₁.fields[0]!).headBeta + go s₂.mvarId s₂.fields[0]!.fvarId! (i+1) + else + mvarId.assign (mkApp preDefValues[i]! (mkFVar x)).headBeta + termination_by preDefValues.size - 1 - i + go mvar.mvarId! x.fvarId! 0 + instantiateMVars mvar + + +/-- +Takes an induction principle where the motive is a `PSigma`/`PSum` type and +unpacks it into a n-ary and (possibly) joint induction principle. +-/ +def unpackMutualInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name) : MetaM Name := do + let inductName := if eqnInfo.declNames.size > 1 then + .append eqnInfo.declNames[0]! `mutual_induct + else + -- If there is no mutual recursion, generate the `foo.induct` directly. + .append eqnInfo.declNames[0]! `induct + if ← hasConst inductName then return inductName + + let ci ← getConstInfo unaryInductName + let us := ci.levelParams + let value := .const ci.name (us.map mkLevelParam) + let motivePos ← forallTelescope ci.type fun xs concl => concl.withApp fun motive targets => do + unless motive.isFVar && targets.size = 1 && targets.all (·.isFVar) do + throwError "conclusion {concl} does not look like a packed motive application" + let packedTarget := targets[0]! + unless xs.back == packedTarget do + throwError "packed target not last argument to {unaryInductName}" + let some motivePos := xs.findIdx? (· == motive) + | throwError "could not find motive {motive} in {xs}" + pure motivePos + let value ← forallBoundedTelescope ci.type motivePos fun params type => do + let value := mkAppN value params + -- Next parameter is the motive (motive : a ⊗' b ⊕' c ⊗' d → Prop). + let packedMotiveType := type.bindingDomain! + -- Bring unpacked motives (motive1 : a → b → Prop and motive2 : c → d → Prop) into scope + withCurriedDecl "motive" packedMotiveType fun motives => do + -- Combine them into a packed motive (motive : a ⊗' b ⊕' c ⊗' d → Prop), and use that + let motive ← forallBoundedTelescope packedMotiveType (some 1) fun xs motiveCodomain => do + let #[x] := xs | throwError "packedMotiveType is not a forall: {packedMotiveType}" + let packedMotives ← motives.mapM curryPSigma + let motiveBody ← packValues x motiveCodomain packedMotives + mkLambdaFVars xs motiveBody + let type ← instantiateForall type #[motive] + let value := mkApp value motive + -- Bring the rest into scope + forallTelescope type fun xs _concl => do + let alts := xs.pop + let value := mkAppN value alts + let value ← deMorganPSumPSigma value + let value ← mkLambdaFVars alts value + let value ← mkLambdaFVars motives value + let value ← mkLambdaFVars params value + check value + let value ← cleanPackedArgs eqnInfo value + return value + + unless ← isTypeCorrect value do + logError m!"failed to unpack induction priciple:{indentExpr value}" + check value + let type ← inferType value + let type ← elimOptParam type + + addDecl <| Declaration.thmDecl + { name := inductName, levelParams := ci.levelParams, type, value } + return inductName + +/-- Given `foo._unary.induct`, define `foo.mutual_induct` and then `foo.induct`, `bar.induct`, … -/ +def deriveUnpackedInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name): MetaM Unit := do + let unpackedInductName ← unpackMutualInduction eqnInfo unaryInductName + let ci ← getConstInfo unpackedInductName + let levelParams := ci.levelParams + + for name in eqnInfo.declNames, idx in [:eqnInfo.declNames.size] do + let inductName := .append name `induct + unless ← hasConst inductName do + let value ← forallTelescope ci.type fun xs _body => do + let value := .const ci.name (levelParams.map mkLevelParam) + let value := mkAppN value xs + let value := mkProjAndN eqnInfo.declNames.size idx value + mkLambdaFVars xs value + let type ← inferType value + addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value } + +/-- +Given a recursively defined function `foo`, derives `foo.induct`. See the module doc for details. +-/ +def deriveInduction (name : Name) : MetaM Unit := do + if let some eqnInfo := WF.eqnInfoExt.find? (← getEnv) name then + let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec + unless eqnInfo.declNameNonRec = name do + deriveUnpackedInduction eqnInfo unaryInductName + else + _ ← deriveUnaryInduction name + +@[builtin_command_elab Parser.Command.deriveInduction] +def elabDeriveInduction : Command.CommandElab := fun stx => Command.runTermElabM fun _xs => do + let ident := stx[1] + let name ← resolveGlobalConstNoOverloadWithInfo ident + deriveInduction name + +end Lean.Tactic.FunInd diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 4363d91583..1558d097d8 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -281,6 +281,17 @@ def initializeKeyword := leading_parser @[builtin_command_parser] def addDocString := leading_parser docComment >> "add_decl_doc " >> ident +/-- +`derive_functional_induction foo`, where `foo` is the name of a function defined using well-founded recursion, +will define a theorem `foo.induct` which provides an induction principle that follows the branching +and recursion pattern of `foo`. + +If `foo` is part of a mutual recursion group, this defines such `.induct`-theorems for all functions +in the group. +-/ +@[builtin_command_parser] def deriveInduction := leading_parser + "derive_functional_induction " >> Parser.ident + /-- This is an auxiliary command for generation constructor injectivity theorems for inductive types defined at `Prelude.lean`. diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean new file mode 100644 index 0000000000..e7ea42bfb0 --- /dev/null +++ b/tests/lean/run/funind_demo.lean @@ -0,0 +1,33 @@ +set_option autoImplicit false + +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) +derive_functional_induction ackermann + +/-- +info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) + (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) + (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) + (x x : Nat) : motive x x +-/ +#guard_msgs in +#check ackermann.induct + +-- TODO: Remove when `List.attach` is upstreamed from std +def List.attach {α} : (l : List α) → List {x // x ∈ l} +| [] => [] +| x::xs => ⟨x, List.mem_cons_self _ _⟩ :: xs.attach.map (fun ⟨y, hy⟩ => ⟨y, mem_cons_of_mem _ hy⟩) + +inductive Tree | node : List Tree → Tree +def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ => t.rev) |>.reverse) + +derive_functional_induction Tree.rev + +/-- +info: Tree.rev.induct (motive : Tree → Prop) + (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (x : Tree) : motive x +-/ +#guard_msgs in +#check Tree.rev.induct diff --git a/tests/lean/run/funind_expr.lean b/tests/lean/run/funind_expr.lean new file mode 100644 index 0000000000..d15fe1bd03 --- /dev/null +++ b/tests/lean/run/funind_expr.lean @@ -0,0 +1,100 @@ +import Lean.Elab.Tactic.Guard + +inductive Expr where + | nat : Nat → Expr + | plus : Expr → Expr → Expr + | bool : Bool → Expr + | and : Expr → Expr → Expr + +inductive Ty where + | nat + | bool + deriving DecidableEq + +inductive HasType : Expr → Ty → Prop + | nat : HasType (.nat v) .nat + | plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat + | bool : HasType (.bool v) .bool + | and : HasType a .bool → HasType b .bool → HasType (.and a b) .bool + +theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by + cases h₁ <;> cases h₂ <;> rfl + +inductive Maybe (p : α → Prop) where + | found : (a : α) → p a → Maybe p + | unknown + +notation "{{ " x " | " p " }}" => Maybe (fun x => p) + +def Expr.typeCheck (e : Expr) : {{ ty | HasType e ty }} := + match e with + | nat .. => .found .nat .nat + | bool .. => .found .bool .bool + | plus a b => + match a.typeCheck, b.typeCheck with + | .found .nat h₁, .found .nat h₂ => .found .nat (.plus h₁ h₂) + | _, _ => .unknown + | and a b => + match a.typeCheck, b.typeCheck with + | .found .bool h₁, .found .bool h₂ => .found .bool (.and h₁ h₂) + | _, _ => .unknown +termination_by e + +theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .unknown) + : e.typeCheck = .found ty h := by + revert h₂ + cases typeCheck e with + | found ty' h' => intro; have := HasType.det h₁ h'; subst this; rfl + | unknown => intros; contradiction + +derive_functional_induction Expr.typeCheck + +/-- +info: Expr.typeCheck.induct (motive : Expr → Prop) (case1 : ∀ (a : Nat), motive (Expr.nat a)) + (case2 : ∀ (a : Bool), motive (Expr.bool a)) + (case3 : + ∀ (a b : Expr) (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), + Expr.typeCheck b = Maybe.found Ty.nat h₂ → + Expr.typeCheck a = Maybe.found Ty.nat h₁ → motive a → motive b → motive (Expr.plus a b)) + (case4 : + ∀ (a b : Expr), + (∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), + Expr.typeCheck a = Maybe.found Ty.nat h₁ → Expr.typeCheck b = Maybe.found Ty.nat h₂ → False) → + motive a → motive b → motive (Expr.plus a b)) + (case5 : + ∀ (a b : Expr) (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), + Expr.typeCheck b = Maybe.found Ty.bool h₂ → + Expr.typeCheck a = Maybe.found Ty.bool h₁ → motive a → motive b → motive (Expr.and a b)) + (case6 : + ∀ (a b : Expr), + (∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), + Expr.typeCheck a = Maybe.found Ty.bool h₁ → Expr.typeCheck b = Maybe.found Ty.bool h₂ → False) → + motive a → motive b → motive (Expr.and a b)) + (x : Expr) : motive x +-/ +#guard_msgs in +#check Expr.typeCheck.induct + +/- +This no longer works after splitting non-refining tail-call matches, +as we now have different number of variables + +theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by + apply Expr.typeCheck.induct (motive := fun e => e.typeCheck = .unknown → ¬ HasType e ty) + <;> simp [typeCheck] + <;> { + intro _ _ a b iha ihb + split <;> simp [*] + intro ht; cases ht + next hnp h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂)) + } +-/ + +-- The same, using the induction tactic +theorem Expr.typeCheck_complete' {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by + induction e using Expr.typeCheck.induct + all_goals simp [typeCheck] + case case3 | case5 => simp [*] + case case4 iha ihb | case6 iha ihb => + intro ht; cases ht + next hnp h₁ h₂ => exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂)) diff --git a/tests/lean/run/funind_mutual_dep.lean b/tests/lean/run/funind_mutual_dep.lean new file mode 100644 index 0000000000..e503e181c2 --- /dev/null +++ b/tests/lean/run/funind_mutual_dep.lean @@ -0,0 +1,71 @@ +-- Testing functional induction derivation with mutual recursion + dependent types +inductive Finite where + | unit : Finite + | bool : Finite + | pair : Finite → Finite → Finite + | arr : Finite → Finite → Finite + +abbrev Finite.asType : Finite → Type + | .unit => Unit + | .bool => Bool + | .pair t1 t2 => asType t1 × asType t2 + | .arr t1 t2 => asType t1 → asType t2 + +def List.product (xs : List α) (ys : List β) : List (α × β) := Id.run do + let mut out : List (α × β) := [] + for x in xs do + for y in ys do + out := (x, y) :: out + pure out.reverse + +mutual +def Finite.enumerate (t : Finite) : List t.asType := + match t with + | .unit => [()] + | .bool => [true, false] + | .pair t1 t2 => t1.enumerate.product t2.enumerate + | .arr t1 t2 => t1.functions t2.enumerate + +def Finite.functions (t : Finite) (results : List α) : List (t.asType → α) := + match t with + | .unit => results.map fun r => fun () => r + | .bool => + (results.product results).map fun (r1, r2) => + fun + | true => r1 + | false => r2 + | .pair t1 t2 => + let f1s := t1.functions <| t2.functions results + f1s.map fun f => fun (x, y) => f x y + | .arr t1 t2 => + let args := t1.enumerate + let base := results.map fun r => fun _ => r + args.foldr (init := base) fun arg rest => + (t2.functions rest).map fun (more : t2.asType → (t1.asType → t2.asType) → α) => + fun (f : t1.asType → t2.asType) => more (f arg) f +end + +derive_functional_induction Finite.functions + +/-- +info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (x : Type) → Finite → List x → Prop) + (case1 : motive1 Finite.unit) (case2 : motive1 Finite.bool) + (case3 : ∀ (t1 t2 : Finite), motive1 t1 → motive1 t2 → motive1 (Finite.pair t1 t2)) + (case4 : + ∀ (t1 t2 : Finite), motive1 t2 → motive2 (Finite.asType t2) t1 (Finite.enumerate t2) → motive1 (Finite.arr t1 t2)) + (case5 : ∀ (fst : Type) (snd : List fst), motive2 fst Finite.unit snd) + (case6 : ∀ (fst : Type) (snd : List fst), motive2 fst Finite.bool snd) + (case7 : + ∀ (fst : Type) (snd : List fst) (t1 t2 : Finite), + motive2 fst t2 snd → + motive2 (Finite.asType t2 → fst) t1 (Finite.functions t2 snd) → motive2 fst (Finite.pair t1 t2) snd) + (case8 : + ∀ (fst : Type) (snd : List fst) (t1 t2 : Finite), + motive1 t1 → + (∀ (rest : List (Finite.asType (Finite.arr t1 t2) → fst)), + motive2 (Finite.asType (Finite.arr t1 t2) → fst) t2 rest) → + motive2 fst (Finite.arr t1 t2) snd) + (x : Type) (x : Finite) (x : List x) : motive2 x x x +-/ +#guard_msgs in +#check Finite.functions.induct diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean new file mode 100644 index 0000000000..cc33203077 --- /dev/null +++ b/tests/lean/run/funind_proof.lean @@ -0,0 +1,67 @@ +inductive Term where + | const : String → Term + | app : String → List Term → Term + +namespace Term + +mutual + def numConsts : Term → Nat + | const _ => 1 + | app _ cs => numConstsLst cs + + def numConstsLst : List Term → Nat + | [] => 0 + | c :: cs => numConsts c + numConstsLst cs +end + +mutual + def replaceConst (a b : String) : Term → Term + | const c => if a == c then const b else const c + | app f cs => app f (replaceConstLst a b cs) + + def replaceConstLst (a b : String) : List Term → List Term + | [] => [] + | c :: cs => replaceConst a b c :: replaceConstLst a b cs +end + +derive_functional_induction replaceConst + +/-- +info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2 : List Term → Prop) (case1 : motive2 []) + (case2 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1)) + (case3 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1)) + (case4 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) + (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) (x : Term) : motive1 x +-/ +#guard_msgs in +#check replaceConst.induct + +theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by + apply replaceConst.induct + (motive1 := fun e => numConsts (replaceConst a b e) = numConsts e) + (motive2 := fun es => numConstsLst (replaceConstLst a b es) = numConstsLst es) + case case1 => simp [replaceConstLst, numConstsLst, *] + case case2 => intro c h; guard_hyp h :ₛ (a == c) = true; simp [replaceConst, numConsts, *] + case case3 => intro c h; guard_hyp h :ₛ ¬(a == c) = true; simp [replaceConst, numConsts, *] + case case4 => + intros f cs ih + guard_hyp ih :ₛnumConstsLst (replaceConstLst a b cs) = numConstsLst cs + simp [replaceConst, numConsts, *] + case case5 => + intro c cs ih₁ ih₂ + guard_hyp ih₁ :ₛ numConsts (replaceConst a b c) = numConsts c + guard_hyp ih₂ :ₛ numConstsLst (replaceConstLst a b cs) = numConstsLst cs + simp [replaceConstLst, numConstsLst, *] + +theorem numConsts_replaceConst' (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by + apply replaceConst.induct + (motive1 := fun e => numConsts (replaceConst a b e) = numConsts e) + (motive2 := fun es => numConstsLst (replaceConstLst a b es) = numConstsLst es) + <;> intros <;> simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *] + +theorem numConsts_replaceConst'' (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by + induction e using replaceConst.induct (a := a) (b := b) + (motive2 := fun es => numConstsLst (replaceConstLst a b es) = numConstsLst es) <;> + simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *] + +end Term diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean new file mode 100644 index 0000000000..9c9fc43611 --- /dev/null +++ b/tests/lean/run/funind_tests.lean @@ -0,0 +1,841 @@ +namespace Unary + +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 + +derive_functional_induction ackermann + +/-- +info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m)) + (case2 : ∀ (n : Nat), motive (n, 1) → motive (Nat.succ n, 0)) + (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (Nat.succ n, Nat.succ m)) + (x : Nat × Nat) : motive x +-/ +#guard_msgs in +#check ackermann.induct + +end Unary + +namespace Binary + +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) +derive_functional_induction ackermann + +/-- +info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) + (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) + (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) + (x x : Nat) : motive x x +-/ +#guard_msgs in +#check ackermann.induct + +end Binary + +universe u +opaque _root_.List.attach : {α : Type u} → (l : List α) → List { x // x ∈ l } + +inductive Tree | node : List Tree → Tree +def Tree.rev : Tree → Tree + | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ => t.rev) |>.reverse) +derive_functional_induction Tree.rev + +/-- +info: Tree.rev.induct (motive : Tree → Prop) + (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (x : Tree) : motive x +-/ +#guard_msgs in +#check Tree.rev.induct + + +def fib : Nat → Nat + | 0 => 1 + | 1 => 1 + | n+2 => fib n + fib (n+1) +termination_by n => n + +derive_functional_induction fib +/-- +info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) + (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive (Nat.succ (Nat.succ n))) (x : Nat) : motive x +-/ +#guard_msgs in +#check fib.induct + +set_option linter.unusedVariables false in +def have_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + have h2 : n < n+1 := Nat.lt_succ_self n + have_tailrec n +termination_by n => n +derive_functional_induction have_tailrec + +/-- +info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) + (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive (Nat.succ n)) (x : Nat) : motive x +-/ +#guard_msgs in +#check have_tailrec.induct + +set_option linter.unusedVariables false in +def have_non_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + Nat.succ <| + have h2 : n < n+1 := Nat.lt_succ_self n + have_non_tailrec n +termination_by n => n +derive_functional_induction have_non_tailrec + +/-- +info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) + (x : Nat) : motive x +-/ +#guard_msgs in +#check have_non_tailrec.induct + +set_option linter.unusedVariables false in +def let_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + let h2 : n < n+1 := Nat.lt_succ_self n + let_tailrec n +termination_by n => n +derive_functional_induction let_tailrec + +/-- +info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) + (case2 : + ∀ (n : Nat), + let h2 := ⋯; + motive n → motive (Nat.succ n)) + (x : Nat) : motive x +-/ +#guard_msgs in +#check let_tailrec.induct + +set_option linter.unusedVariables false in +def let_non_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + Nat.succ <| + let h2 : n < n+1 := Nat.lt_succ_self n + let_non_tailrec n +termination_by n => n +derive_functional_induction let_non_tailrec + +/-- +info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) + (x : Nat) : motive x +-/ +#guard_msgs in +#check let_non_tailrec.induct + + +set_option linter.unusedVariables false in +def with_ite_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + if n % 2 = 0 then + with_ite_tailrec n + else + with_ite_tailrec n +termination_by n => n +derive_functional_induction with_ite_tailrec + +/-- +info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) + (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive (Nat.succ n)) + (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive (Nat.succ n)) (x : Nat) : motive x +-/ +#guard_msgs in +#check with_ite_tailrec.induct + + +set_option linter.unusedVariables false in +def with_ite_non_tailrec : Nat → Nat + | 0 => 0 + | 1 => 1 + | n+2 => + Nat.succ <| + if n % 2 = 0 then + with_ite_non_tailrec (n+1) + else + with_ite_non_tailrec n +termination_by n => n +derive_functional_induction with_ite_non_tailrec + +/-- +info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) + (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive (Nat.succ (Nat.succ n))) (x : Nat) : motive x +-/ +#guard_msgs in +#check with_ite_non_tailrec.induct + +set_option linter.unusedVariables false in +def with_dite_non_tailrec (n : Nat) : Nat := + Nat.succ <| + if h : n - 1 < n then + with_dite_non_tailrec (n-1) + else + 0 +termination_by n +derive_functional_induction with_dite_non_tailrec + +/-- +info: with_dite_non_tailrec.induct (motive : Nat → Prop) +(case1 : ∀ (x : Nat), (x - 1 < x → motive (x - 1)) → motive x) + (x : Nat) : motive x +-/ +#guard_msgs in +#check with_dite_non_tailrec.induct + +set_option linter.unusedVariables false in +def with_dite_tailrec (n : Nat) : Nat := + if h : n - 1 < n then + with_dite_tailrec (n-1) + else + 0 +termination_by n +derive_functional_induction with_dite_tailrec + +/-- +info: with_dite_tailrec.induct (motive : Nat → Prop) +(case1 : ∀ (x : Nat), x - 1 < x → motive (x - 1) → motive x) + (case2 : ∀ (x : Nat), ¬x - 1 < x → motive x) (x : Nat) : motive x +-/ +#guard_msgs in +#check with_dite_tailrec.induct + +set_option linter.unusedVariables false in +def with_match_refining_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + match n with + | 0 => with_match_refining_tailrec 0 + | m => with_match_refining_tailrec m +termination_by n => n +derive_functional_induction with_match_refining_tailrec + +/-- +info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0)) + (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive (Nat.succ m)) (x : Nat) : motive x +-/ +#guard_msgs in +#check with_match_refining_tailrec.induct + + + +def with_arg_refining_match1 (i : Nat) : Nat → Nat + | 0 => 0 + | n+1 => + if h : i = 0 then 0 else with_arg_refining_match1 (i - 1) n +termination_by i +derive_functional_induction with_arg_refining_match1 + +/-- +info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (fst : Nat), motive fst 0) + (case2 : ∀ (n : Nat), motive 0 (Nat.succ n)) + (case3 : ∀ (fst n : Nat), ¬fst = 0 → motive (fst - 1) n → motive fst (Nat.succ n)) (x x : Nat) : motive x x +-/ +#guard_msgs in +#check with_arg_refining_match1.induct + +def with_arg_refining_match2 (i : Nat) (n : Nat) : Nat := + if i = 0 then 0 else match n with + | 0 => 0 + | n+1 => with_arg_refining_match2 (i - 1) n +termination_by i +derive_functional_induction with_arg_refining_match2 + +/-- +info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (snd : Nat), motive 0 snd) + (case2 : ∀ (fst : Nat), ¬fst = 0 → motive fst 0) + (case3 : ∀ (fst : Nat), ¬fst = 0 → ∀ (n : Nat), motive (fst - 1) n → motive fst (Nat.succ n)) (x x : Nat) : motive x x +-/ +#guard_msgs in +#check with_arg_refining_match2.induct + + +set_option linter.unusedVariables false in +def with_other_match_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + match n % 2 with + | 0 => with_other_match_tailrec n + | _ => with_other_match_tailrec n +termination_by n => n +derive_functional_induction with_other_match_tailrec + +/-- +info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) + (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive (Nat.succ n)) + (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive (Nat.succ n)) (x : Nat) : motive x +-/ +#guard_msgs in +#check with_other_match_tailrec.induct + +set_option linter.unusedVariables false in +def with_mixed_match_tailrec : Nat → Nat → Nat → Nat → Nat := fun a b c d => + match a, h: b, c % 2, h : d % 2 with + | 0, _, _, _ => 0 + | a+1, x, y, z => with_mixed_match_tailrec a x y z +termination_by n => n +derive_functional_induction with_mixed_match_tailrec + +/-- +info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) + (case1 : ∀ (fst snd x : Nat), motive 0 x fst snd) + (case2 : ∀ (fst snd a x : Nat), motive a x (fst % 2) (snd % 2) → motive (Nat.succ a) x fst snd) (x x x x : Nat) : + motive x x x x +-/ +#guard_msgs in +#check with_mixed_match_tailrec.induct + +set_option linter.unusedVariables false in +def with_mixed_match_tailrec2 : Nat → Nat → Nat → Nat → Nat → Nat := fun n a b c d => + match n with + | 0 => 0 + | n+1 => + match a, h: b, c % 2, h : d % 2 with + | 0, _, _, _ => 0 + | a+1, x, y, z => with_mixed_match_tailrec2 n a x y z +termination_by n => n +derive_functional_induction with_mixed_match_tailrec2 + +/-- +info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop) + (case1 : ∀ (fst fst_1 fst_2 snd : Nat), motive 0 fst fst_1 fst_2 snd) + (case2 : ∀ (fst snd n x : Nat), motive (Nat.succ n) 0 x fst snd) + (case3 : ∀ (fst snd n a x : Nat), motive n a x (fst % 2) (snd % 2) → motive (Nat.succ n) (Nat.succ a) x fst snd) + (x x x x x : Nat) : motive x x x x x +-/ +#guard_msgs in +#check with_mixed_match_tailrec2.induct + +set_option linter.unusedVariables false in +def with_match_non_tailrec : Nat → Nat + | 0 => 0 + | n+1 => + Nat.succ <| + match n % 2 with + | 0 => with_match_non_tailrec n + | _ => with_match_non_tailrec n +termination_by n => n +derive_functional_induction with_match_non_tailrec + +/-- +info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) + (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) (x : Nat) : motive x +-/ +#guard_msgs in +#check with_match_non_tailrec.induct + +set_option linter.unusedVariables false in +def with_match_non_tailrec_refining : Nat → Nat + | 0 => 0 + | n+1 => + Nat.succ <| + match n with + | 0 => with_match_non_tailrec_refining 0 + | m => with_match_non_tailrec_refining m +termination_by n => n +derive_functional_induction with_match_non_tailrec_refining + +/-- +info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : motive 0) + (case2 : + ∀ (n : Nat), + (match n with + | 0 => motive 0 + | m => motive m) → + motive (Nat.succ n)) + (x : Nat) : motive x +-/ +#guard_msgs in +#check with_match_non_tailrec_refining.induct + + +def with_overlap : Nat → Nat + | 0 => 0 + | 1 => 1 + | 2 => 2 + | 3 => 3 + | n+1 => with_overlap n +termination_by n => n +derive_functional_induction with_overlap + +/-- +info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3) + (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive (Nat.succ n)) + (x : Nat) : motive x +-/ +#guard_msgs in +#check with_overlap.induct + +namespace UnusedExtraParams + +-- This test how unused fixed function parameters are handled. +-- See comment in the code + +def unary (base : Nat) : Nat → Nat + | 0 => base + | n+1 => unary base n +termination_by n => n +derive_functional_induction unary + +/-- +info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0) + (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) (x : Nat) : motive x +-/ +#guard_msgs in +#check unary.induct + +def binary (base : Nat) : Nat → Nat → Nat + | 0, m => base + m + | n+1, m => binary base n m +termination_by n => n +derive_functional_induction binary + +/-- +info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) + (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) (x x : Nat) : motive x x +-/ +#guard_msgs in +#check binary.induct + +end UnusedExtraParams + +namespace NonTailrecMatch + +def match_non_tail (n : Nat ) : Bool := + n = 42 || match n with + | 0 => true + | 1 => true + | n+2 => match_non_tail n && match_non_tail (n+1) +termination_by n + +def match_non_tail_induct + {motive : Nat → Prop} + (case1 : forall n, (IH : match n with | 0 => True | n+1 => motive n) → motive n) + (n : Nat) : motive n := + WellFounded.fix Nat.lt_wfRel.wf (fun n IH => + match n with + | 0 => case1 0 True.intro + | n+1 => + case1 (n+1) (IH n (Nat.lt_succ_self _)) + ) n + +derive_functional_induction match_non_tail + +/-- +info: NonTailrecMatch.match_non_tail.induct (motive : Nat → Prop) + (case1 : + ∀ (x : Nat), + (match x with + | 0 => True + | 1 => True + | Nat.succ (Nat.succ n) => motive n ∧ motive (n + 1)) → + motive x) + (x : Nat) : motive x +-/ +#guard_msgs in +#check match_non_tail.induct + + +theorem match_non_tail_eq_true (n : Nat) : match_non_tail n = true := by + induction n using match_non_tail.induct + case case1 n IH => + unfold match_non_tail + split <;> dsimp at IH <;> simp [IH] + +end NonTailrecMatch + + +namespace AsPattern + +def foo (n : Nat) := + match n with + | 0 => 0 + | x@(n+1) => x + foo n +termination_by n +derive_functional_induction foo + +/-- +info: AsPattern.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) + (x : Nat) : motive x +-/ +#guard_msgs in +#check foo.induct + + + +def bar (n : Nat) := + 1 + + match n with + | 0 => 0 + | x@(n+1) => x + bar n +termination_by n +derive_functional_induction bar + +/-- +info: AsPattern.bar.induct (motive : Nat → Prop) + (case1 : + ∀ (x : Nat), + (match x with + | 0 => True + | x@h:(Nat.succ n) => motive n) → + motive x) + (x : Nat) : motive x +-/ +#guard_msgs in +#check bar.induct + +end AsPattern + +namespace GramSchmidt + +-- this tried to repoduce a problem with gramSchmidt, +-- with more proofs from `simp` abstracting over the IH. +-- I couldn't quite reproduce it, but let's keep it. + +def below (n i : Nat) := i < n + +@[simp] +def below_lt (n i : Nat) (h : below n i) : i < n := h + +def sum_below (n : Nat) (f : (i : Nat) → below n i → Nat) := + match n with + | 0 => 0 + | n+1 => sum_below n (fun i hi => f i (Nat.lt_succ_of_le (Nat.le_of_lt hi))) + + f n (Nat.lt_succ_self n) + +def foo (n : Nat) := + 1 + sum_below n (fun i _ => foo i) +termination_by n +decreasing_by + simp_wf + simp [below_lt, *] + +derive_functional_induction foo +/-- +info: GramSchmidt.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (i : Nat), below x i → motive i) → motive x) + (x : Nat) : motive x +-/ +#guard_msgs in +#check foo.induct + +end GramSchmidt + +namespace LetFun + +def foo {α} (x : α) : List α → Nat + | .nil => 0 + | .cons _y ys => + let this := foo x ys + this +termination_by xs => xs +derive_functional_induction foo +/-- +info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive []) + (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (x : List α) : motive x +-/ +#guard_msgs in +#check foo.induct + + +def bar {α} (x : α) : List α → Nat + | .nil => 0 + | .cons _y ys => + have this := bar x ys + this +termination_by xs => xs + +derive_functional_induction bar +/-- +info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive []) + (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (x : List α) : motive x +-/ +#guard_msgs in +#check bar.induct + +end LetFun + + +namespace RecCallInDisrs + +def foo : Nat → Nat + | 0 => 0 + | n+1 => if foo n = 0 then 1 else 0 +termination_by n => n +derive_functional_induction foo + +/-- +info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0) + (case2 : ∀ (n : Nat), foo n = 0 → motive n → motive (Nat.succ n)) + (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive (Nat.succ n)) (x : Nat) : motive x +-/ +#guard_msgs in +#check foo.induct + + +def bar : Nat → Nat + | 0 => 0 + | n+1 => match h₁ : n, bar n with + | 0, 0 => 0 + | 0, _ => 1 + | m+1, _ => bar m +termination_by n => n +derive_functional_induction bar + +/-- +info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0)) + (case3 : (bar 0 = 0 → False) → motive 0 → motive (Nat.succ 0)) + (case4 : ∀ (m : Nat), motive (Nat.succ m) → motive m → motive (Nat.succ (Nat.succ m))) (x : Nat) : motive x +-/ +#guard_msgs in +#check bar.induct + +end RecCallInDisrs + +namespace EvenOdd + +mutual +def even : Nat → Bool + | 0 => true + | n+1 => odd n +termination_by n => n +def odd : Nat → Bool + | 0 => false + | n+1 => even n +termination_by n => n +end +derive_functional_induction even + +/-- +info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0) + (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) + (x : Nat) : motive1 x +-/ +#guard_msgs in +#check even.induct + +/-- +info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0) + (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) + (x : Nat) : motive2 x +-/ +#guard_msgs in +#check odd.induct + +end EvenOdd + +namespace Tree + +inductive Tree : Type + | node : List Tree → Tree + +mutual +def Tree.map (f : Tree → Tree) : Tree → Tree + | Tree.node ts => Tree.node (map_forest f ts) + +def Tree.map_forest (f : Tree → Tree) (ts : List Tree) : List Tree := + ts.attach.map (fun ⟨t, _ht⟩ => Tree.map f t) +end +derive_functional_induction Tree.map + +/-- +info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) + (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) + (case2 : ∀ (val : List Tree), (∀ (t : Tree), t ∈ val → motive1 t) → motive2 val) (x : Tree) : motive1 x +-/ +#guard_msgs in +#check Tree.map.induct + +/-- +info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) + (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) + (case2 : ∀ (val : List Tree), (∀ (t : Tree), t ∈ val → motive1 t) → motive2 val) (x : List Tree) : motive2 x +-/ +#guard_msgs in +#check Tree.map_forest.induct + +end Tree + +namespace DefaultArgument + +-- Default arguments should not be copied over + +def unary (fixed : Bool := false) (n : Nat := 0) : Nat := + match n with + | 0 => 0 + | n+1 => unary fixed n +termination_by n +derive_functional_induction unary + +/-- +info: DefaultArgument.unary.induct (fixed : Bool) (motive : Nat → Prop) (case1 : motive 0) + (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) (x : Nat) : motive x +-/ +#guard_msgs in +#check unary.induct + +def foo (fixed : Bool := false) (n : Nat) (m : Nat := 0) : Nat := + match n with + | 0 => m + | n+1 => foo fixed n m +termination_by n +derive_functional_induction foo + +/-- +info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (snd : Nat), motive 0 snd) + (case2 : ∀ (snd n : Nat), motive n snd → motive (Nat.succ n) snd) (x x : Nat) : motive x x +-/ +#guard_msgs in +#check foo.induct + +end DefaultArgument + +namespace Nary + +def foo : Nat → Nat → (k : Nat) → Fin k → Nat + | 0, _, _, _ => 0 + | _, 0, _, _ => 0 + | _, _, 0, _ => 0 + | _, _, 1, _ => 0 + | n+1, m+1, k+2, _ => foo n m (k+1) ⟨0, Nat.zero_lt_succ _⟩ +termination_by n => n +derive_functional_induction foo + +/-- +info: Nary.foo.induct (motive : Nat → Nat → (x : Nat) → Fin x → Prop) + (case1 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), motive 0 x x_1 x_2) + (case2 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), (x = 0 → False) → motive x 0 x_1 x_2) + (case3 : ∀ (x x_1 : Nat) (x_2 : Fin 0), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 0 x_2) + (case4 : ∀ (x x_1 : Nat) (x_2 : Fin 1), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 1 x_2) + (case5 : + ∀ (n m k : Nat) (x : Fin (k + 2)), + motive n m (k + 1) { val := 0, isLt := ⋯ } → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x) + (x x x : Nat) (x : Fin x) : motive x x x x +-/ +#guard_msgs in +#check foo.induct + +end Nary + +namespace Dite + +def foo (n : Nat) : Nat := + let j := n - 1 + if _h : j < n then + foo j + else + 42 +derive_functional_induction foo + +/-- +info: Dite.foo.induct (motive : Nat → Prop) + (case1 : + ∀ (x : Nat), + let j := x - 1; + j < x → motive j → motive x) + (case2 : + ∀ (x : Nat), + let j := x - 1; + ¬j < x → motive x) + (x : Nat) : motive x +-/ +#guard_msgs in +#check foo.induct + +end Dite + +namespace CommandIdempotence + +-- This checks that the `derive_functional_induction` command gracefully handles being called twice + +mutual +def even : Nat → Bool + | 0 => true + | n+1 => odd n +termination_by n => n +def odd : Nat → Bool + | 0 => false + | n+1 => even n +termination_by n => n +end + +derive_functional_induction even._mutual + +/-- +info: CommandIdempotence.even._mutual.induct (motive : Nat ⊕' Nat → Prop) (case1 : motive (PSum.inl 0)) + (case2 : motive (PSum.inr 0)) (case3 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl (Nat.succ n))) + (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr (Nat.succ n))) (x : Nat ⊕' Nat) : motive x +-/ +#guard_msgs in +#check even._mutual.induct + +/-- error: unknown constant 'CommandIdempotence.even.induct' -/ +#guard_msgs in +#check even.induct + +derive_functional_induction even + +/-- +info: CommandIdempotence.even._mutual.induct (motive : Nat ⊕' Nat → Prop) (case1 : motive (PSum.inl 0)) + (case2 : motive (PSum.inr 0)) (case3 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl (Nat.succ n))) + (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr (Nat.succ n))) (x : Nat ⊕' Nat) : motive x +-/ +#guard_msgs in +#check even._mutual.induct + +/-- +info: CommandIdempotence.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0) + (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) + (x : Nat) : motive1 x +-/ +#guard_msgs in +#check even.induct + +derive_functional_induction even + +end CommandIdempotence + +namespace Errors + +/-- error: unknown constant 'doesNotExist' -/ +#guard_msgs in +derive_functional_induction doesNotExist + +def takeWhile (p : α → Bool) (as : Array α) : Array α := + foo 0 #[] +where + foo (i : Nat) (r : Array α) : Array α := + if h : i < as.size then + let a := as.get ⟨i, h⟩ + if p a then + foo (i+1) (r.push a) + else + r + else + r + termination_by as.size - i + +/-- +error: Function Errors.takeWhile does not look like a function defined by well-founded recursion. +NB: If Errors.takeWhile is not itself recursive, but contains an inner recursive function (via `let rec` or `where`), try `Errors.takeWhile.go` where `go` is name of the inner function. +-/ +#guard_msgs in +derive_functional_induction takeWhile -- Cryptic error message + +derive_functional_induction takeWhile.foo + +end Errors