diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index 85a26b679a..9f9c1164ac 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -17,6 +17,11 @@ import Lean.Util.HasConstCache namespace Lean.Elab.WF open Meta +register_builtin_option debug.definition.wf.replaceRecApps : Bool := { + defValue := false + descr := "Type check every step of the well-founded definition translation" + } + /- Creates a subgoal for a recursive call, as an unsolved `MVar`. The goal is cleaned up, and the current syntax reference is stored in the `MVar`’s type as a `RecApp` marker, for @@ -32,11 +37,13 @@ private def mkDecreasingProof (decreasingProp : Expr) : TermElabM Expr := do private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (F : Expr) (e : Expr) : TermElabM Expr := do trace[Elab.definition.wf] "replaceRecApps:{indentExpr e}" - trace[Elab.definition.wf] "{F} : {← inferType F}" - loop F e |>.run' {} + trace[Elab.definition.wf] "type of functorial {F} is{indentExpr (← inferType F)}" + let e ← loop F e |>.run' {} + return e where processRec (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do if e.getAppNumArgs < fixedPrefixSize + 1 then + trace[Elab.definition.wf] "replaceRecApp: eta-expanding{indentExpr e}" loop F (← etaExpand e) else let args := e.getAppArgs @@ -55,6 +62,19 @@ where modifyGet (·.contains e) loop (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do + let e' ← loopGo F e + if (debug.definition.wf.replaceRecApps.get (← getOptions)) then + withTransparency .all do withNewMCtxDepth do + unless (← isTypeCorrect e') do + throwError "Type error introduced when transforming{indentExpr e}\nto{indentExpr e'}" + let t1 ← inferType e + let t2 ← inferType e' + unless (← isDefEq t1 t2) do + let (t1, t2) ← addPPExplicitToExposeDiff t1 t2 + throwError "Type not preserved transforming{indentExpr e}\nto{indentExpr e'}\nType was{indentExpr t1}\nand now is{indentExpr t2}" + return e' + + loopGo (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do if !(← containsRecFn e) then return e match e with @@ -83,7 +103,8 @@ where unless xs.size = numParams do throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}" let FAlt := xs[numParams - 1]! - mkLambdaFVars xs (← loop FAlt altBody) + let altBody' ← loop FAlt altBody + mkLambdaFVars xs altBody' return { matcherApp with alts := altsNew, discrs := (← matcherApp.discrs.mapM (loop F)) }.toExpr else processApp F e diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index 9af30b1273..23f4df8519 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -37,21 +37,27 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu else throwError "failed to add argument to matcher application, argument type was not refined by `casesOn`" -/-- Given - - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - - expression `e : B[discrs]`, - Construct the term - `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`. +/-- +Given +- matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and +- expression `e : B[discrs]`, +Construct the term +`match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`. - We use `kabstract` to abstract the discriminants from `B[discrs]`. +We only abstract discriminants that are fvars. We used to use `kabstract` to abstract all +discriminants from `B[discrs]`, but that changes the type of the arg in ways that make it no +longer compatible with the original recursive function (issue #7322). - This method assumes - - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` - - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` +If this is still not great, then we could try to use `kabstract`, but only on the last paramter +of the `arg` (the termination proof obligation). - This is used in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to - the argument provided by `fix` to refine type of the local variable used for recursive calls, - which may mention `major`. See there for how to use this function. +This method assumes +- the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` +- each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` + +This is used in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to +the argument provided by `fix` to refine type of the local variable used for recursive calls, +which may mention `major`. See there for how to use this function. -/ def addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do @@ -59,11 +65,13 @@ def addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" let eType ← inferType e - let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i _ eTypeAbst => do - let motiveArg := motiveArgs[i]! + let eTypeAbst := matcherApp.discrs.size.foldRev (init := eType) fun i _ eTypeAbst => let discr := matcherApp.discrs[i] - let eTypeAbst ← kabstract eTypeAbst discr - return eTypeAbst.instantiate1 motiveArg + if discr.isFVar then + let motiveArg := motiveArgs[i]! + eTypeAbst.replaceFVar discr motiveArg + else + eTypeAbst let motiveBody ← mkArrow eTypeAbst motiveBody let matcherLevels ← match matcherApp.uElimPos? with | none => pure matcherApp.matcherLevels diff --git a/tests/lean/run/issue7322.lean b/tests/lean/run/issue7322.lean new file mode 100644 index 0000000000..688c26d991 --- /dev/null +++ b/tests/lean/run/issue7322.lean @@ -0,0 +1,62 @@ +-- set_option trace.Elab.definition.fixedParams true in +-- set_option debug.skipKernelTC true +-- set_option debug.definition.wf.replaceRecApps true +-- set_option trace.Elab.definition.wf true +set_option pp.proofs true + +/-! +This test case show a tricky issue, originally shown in +`Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_denote_eq` +where type of `fix`’s induction hypothese change when being refined +in a way that makes the resulting proof term type incorrect. +-/ + +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +theorem demo (distance : Nat) (idx : Nat) (a : Fin distance) (fuel : Nat) : + a = if hidx : idx < distance then Fin.mk idx hidx else a := by + cases fuel + · sorry + next fuel => + split + · rw [demo distance idx a fuel] + sorry + · rfl +termination_by fuel +decreasing_by sorry + +structure Ev (p : Prop) : Type where + isTrue : p + +/-- +warning: declaration uses 'sorry' +--- +warning: declaration uses 'sorry' +--- +warning: declaration uses 'sorry' +--- +warning: declaration uses 'sorry' +-/ +#guard_msgs in +def bar (distance : Nat) (idx : Nat) (a : Fin distance) (fuel : Nat) : + Ev (a = if hidx : idx < distance then Fin.mk idx hidx else a) := by + cases fuel + · sorry + next fuel => + split + · rw [(bar distance idx a fuel).isTrue] + sorry + · apply Ev.mk + rfl +termination_by fuel +decreasing_by sorry + +set_option Elab.async false -- for stable message ordering in guard_msgs + +/-- +warning: declaration uses 'sorry' +--- +info: bar.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (n : Nat), motive n) → motive x) (fuel : Nat) : motive fuel +-/ +#guard_msgs in +#check bar.induct