diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 497df8c35249..7a793406e367 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1023,11 +1023,25 @@ theorem of_decide_eq_true [inst : Decidable p] : Eq (decide p) true → p := fun | isTrue h₁ => h₁ | isFalse h₁ => absurd h (Bool.ne_true_of_eq_false (decide_eq_false h₁)) +/-- +Variant of `of_decide_eq_true` that takes `Decidable` as an implicit argument, intended for +forward reasoning. +-/ +theorem of_decide_eq_true_forward {inst : Decidable p} : Eq (decide p) true → p := + of_decide_eq_true + theorem of_decide_eq_false [inst : Decidable p] : Eq (decide p) false → Not p := fun h => match (generalizing := false) inst with | isTrue h₁ => absurd h (Bool.ne_false_of_eq_true (decide_eq_true h₁)) | isFalse h₁ => h₁ +/-- +Variant of `of_decide_eq_false` that takes `Decidable` as an implicit argument, intended for +forward reasoning. +-/ +theorem of_decide_eq_false_forward {inst : Decidable p} : Eq (decide p) false → Not p := + of_decide_eq_false + theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true := match (generalizing := false) inst a a with | isTrue _ => rfl diff --git a/src/Init/WF.lean b/src/Init/WF.lean index 1d0216ed49d1..87ae4267a137 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -523,7 +523,7 @@ The `wfParam` gadget is used internally during the construction of recursive fun wellfounded recursion, to keep track of the parameter for which the automatic introduction of `List.attach` (or similar) is plausible. -/ -@[implicit_reducible] def wfParam {α : Sort u} (a : α) : α := a +@[instance_reducible] def wfParam {α : Sort u} (a : α) : α := a /-- Reverse direction of `dite_eq_ite`. Used by the well-founded definition preprocessor to extend the diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index 79b457a08230..cec936893e2b 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura module prelude public import Lean.Attributes +public import Lean.ScopedEnvExtension import Lean.Util.CollectLevelParams public section namespace Lean @@ -174,6 +175,48 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme let outLevelParams := computeOutLevelParams decl.type outParams decl.levelParams return classExtension.addEntry env { name := clsName, outParams, outLevelParams } +/-- +Classes marked `@[lax_instance_defeq]` are exempt from the strict instance-argument discipline of +`backward.isDefEq.respectTransparency.instances`: a value assigned to an instance metavariable of +such a class is not required to have a type that matches the metavariable's type at `.instances` +transparency. The instance-argument check of `simp`/`dsimp` (`dsimp.resynthInstances`) and the +`linter.tacticCheckInstances` linter skip these classes as well. +-/ +builtin_initialize laxInstanceDefeqExt : SimpleScopedEnvExtension Name NameSet ← + registerSimpleScopedEnvExtension { + initial := {} + addEntry := fun s n => s.insert n + } + +builtin_initialize + registerBuiltinAttribute { + name := `lax_instance_defeq + descr := "exempt instances of a class from the strict defeq check at `.instances` \ + transparency (see `backward.isDefEq.respectTransparency.instances`)" + add := fun declName stx kind => do + Attribute.Builtin.ensureNoArgs stx + unless isClass (← getEnv) declName do + throwError "invalid `lax_instance_defeq`, `{.ofConstName declName}` is not a class" + laxInstanceDefeqExt.add declName kind + } + +/-- Whether a class type's result sort is `Prop`. -/ +private def isPropValued : Expr → Bool + | .forallE _ _ b _ => isPropValued b + | .sort u => u == .zero + | _ => false + +/-- +Return `true` if instances of class `className` are exempt from the strict defeq check at +`.instances` transparency: the class is marked `@[lax_instance_defeq]`, or it is propositional +(proof irrelevance makes a stale instance argument harmless there). See `laxInstanceDefeqExt`. +-/ +def isLaxInstanceDefeqClass (env : Environment) (className : Name) : Bool := + (laxInstanceDefeqExt.getState env).contains className || + match env.find? className with + | some info => isPropValued info.type + | none => false + /-- Registers an inductive type or structure as a type class. Using `class` or `class inductive` is generally preferred over using `@[class] structure` or `@[class] inductive` directly. diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 32906b9bc869..3a16c592efdc 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -349,6 +349,42 @@ private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do let args := mvars ++ args.drop mvars.size instantiateMVars (mkAppN fn args) +/-- +Best-effort unification of the user-supplied `type` against the `expectedType` to resolve +user-placed `_` placeholders. We decompose both sides as applications of a common head and +unify arguments position-by-position, skipping instance-implicit positions. + +Instance-implicit arguments of `type` are fresh synthetic class metavariables introduced by +`elabType` that will be discarded by `resynthInstImplicitArgs`. Routing them through `isDefEq` +serves no purpose and can spuriously fail: assigning a synthetic class metavariable triggers +a transparency cap at `.instances` in the type-equality check (see +`backward.isDefEq.respectTransparency.instances`), which prevents non-`[reducible]` definitions +from unfolding — so, e.g., `Neg (Nat ⧸ n) =?= Neg (Zmod n)` fails even though `Zmod` reduces +to `Nat ⧸ n` at `.default` transparency. The outer `isDefEq` then fails and rolls back the +useful assignments made to user `_` placeholders. + +When the two sides do not share a common-shape head, we fall back to a plain `isDefEq`. +Per-argument `isDefEq` calls are best-effort: a failure at one position does not roll back +successes at others. +-/ +private def unifyTypeForInferInstanceAs (type expectedType : Expr) : TermElabM Unit := do + let typeFn := type.getAppFn + let expectedFn := expectedType.getAppFn + let typeArgs := type.getAppArgs + let expectedArgs := expectedType.getAppArgs + unless typeFn.isConst && expectedFn.isConst + && typeFn.constName! == expectedFn.constName! + && typeArgs.size == expectedArgs.size do + discard <| isDefEq type expectedType + return + unless (← isDefEq typeFn expectedFn) do + return + let (_, bis, _) ← forallMetaTelescope (← inferType typeFn) + for i in [:typeArgs.size] do + if i < bis.size && bis[i]!.isInstImplicit then + continue + discard <| isDefEq typeArgs[i]! expectedArgs[i]! + @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`) let typeStx := stx[stx.getNumArgs - 1]! @@ -363,7 +399,7 @@ private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do let type ← withSynthesize do let type ← elabType typeStx -- Unify with expected type to resolve metavariables (e.g., `_` placeholders) - discard <| isDefEq type expectedType + unifyTypeForInferInstanceAs type expectedType return type -- Re-infer instance-implicit args, so that synthesis is not influenced by the expected type's -- instance choices. diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 7acba898530b..03f938f66bf1 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -2327,7 +2327,8 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) ( let numPublicConsts := modules.foldl (init := 0) fun numPublicConsts mod => Id.run do if !mod.isExported then numPublicConsts else let some data := mod.publicModule? | numPublicConsts - numPublicConsts + data.constants.size + -- binop issue: can't synthesize `HAdd Nat Nat (Id Nat)`; solved using `pure` + pure <| numPublicConsts + data.constants.size let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numExtraConsts) let mut privateConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts) let mut publicConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPublicConsts) diff --git a/src/Lean/Linter/TacticTypeCheck.lean b/src/Lean/Linter/TacticTypeCheck.lean index c1e0228870ad..7fe9d1ba588c 100644 --- a/src/Lean/Linter/TacticTypeCheck.lean +++ b/src/Lean/Linter/TacticTypeCheck.lean @@ -17,16 +17,19 @@ open Lean Elab Command open Lean.Linter (logLint) /-- -Warn when the goal target is not type-correct at `.implicit` transparency. -This can happen when e.g. `unfold` leaves hypotheses whose types still refer to -the pre-unfolded definition, preventing `rw`/`simp` from matching patterns. +Whether a `linter.tacticCheckInstances` warning has already been logged for this command, e.g. by +`simp` checking its own intermediate results while the command was elaborated. -/ -register_builtin_option linter.tacticCheckInstances : Bool := { - defValue := false - descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency" -} +private def alreadyReported : CommandElabM Bool := do + -- `Command.State.messages` is reset per command, but by the time linters run its messages have + -- been marked reported, which `MessageLog.toList` does not return. + return (← get).messages.reportedPlusUnreported.any + (·.data.hasTag (· == linter.tacticCheckInstances.name)) -/-- A linter that runs `Meta.check _ .implicit` on every tactic goal. -/ +/-- +A linter that runs `Meta.check _ .implicit` and `Meta.findInstanceArgMismatch?` on every tactic +goal. +-/ def tacticCheckInstances : Linter where run _cmdStx := do -- Do *not* check `linter.all` here, this linter is purely for debugging @@ -35,8 +38,10 @@ def tacticCheckInstances : Linter where let infoTrees := (← get).infoState.trees.toArray -- Once any tactic step in this command has produced a warning, suppress -- all further checks: a bad lctx typically persists across many tactic - -- steps - let warned : IO.Ref Bool ← IO.mkRef false + -- steps. `simp` runs the same instance-argument check on its intermediate + -- results during elaboration, so start out suppressed if it already + -- reported one. + let warned : IO.Ref Bool ← IO.mkRef (← alreadyReported) for tree in infoTrees do -- `postNode` so children are visited before parents: leaf tactic infos -- (the actual user-written `unfold`, `rw`, ...) fire before the @@ -56,7 +61,8 @@ def tacticCheckInstances : Linter where -- `.implicit` check fails, the defs unfolded at `.default` but not at -- `.implicit` are the candidates for `@[implicit_reducible]` and get -- reported to the user. The pattern mirrors `mkUnfoldAxiomsNote` in - -- `Lean.Meta.Check`. + -- `Lean.Meta.Check`. If it succeeds, we look for instance arguments + -- that stop matching one transparency level down. -- `kind` selects the wording of the warning: -- * "initial" — the failure is in `goalsBefore` of the first tactic -- (i.e. the `by` block started with a bad goal). @@ -74,30 +80,37 @@ def tacticCheckInstances : Linter where let counterDefault := (← get).diag.unfoldCounter -- Reset and try at `.implicit`. modify ({ · with diag := origDiag }) - try - Meta.check target .implicit + let implicitError? : Option Exception ← + try Meta.check target .implicit; pure none catch e => pure (some e) + let some e := implicitError? | do + -- Type-correct at `.implicit`, but `simp`/`rw` unify instance-implicit arguments at + -- `.instances`, where an argument left behind by an earlier rewrite may no longer + -- match. + let some msg ← Meta.findInstanceArgMismatch? target | return none + return some m!"The {kind} tactic goal has an instance argument whose type does not \ + match at `.instances` transparency. `simp` and `rw` unify instance-implicit \ + arguments at that transparency. Lemmas that mention this instance do not \ + apply:{indentD msg}" + let counterInst := (← get).diag.unfoldCounter + let diff := Meta.subCounters counterDefault counterInst + let env ← getEnv + let candidates : List MessageData := + diff.toList.filterMap fun (n, count) => do + guard <| count > 0 + guard <| getReducibilityStatusCore env n matches .semireducible + guard <| !Meta.isInstanceCore env n + return m!"{.ofConstName n}" + if candidates.isEmpty then return none - catch e => - let counterInst := (← get).diag.unfoldCounter - let diff := Meta.subCounters counterDefault counterInst - let env ← getEnv - let candidates : List MessageData := - diff.toList.filterMap fun (n, count) => do - guard <| count > 0 - guard <| getReducibilityStatusCore env n matches .semireducible - guard <| !Meta.isInstanceCore env n - return m!"{.ofConstName n}" - if candidates.isEmpty then - return none - let remedy : MessageData := match kind with - | "initial" => "consider rephrasing the goal or marking" - | _ => "consider using propositional rewriting or marking" - return some m!"{kind} tactic goal is not type-correct at \ - `.implicit` transparency; {remedy} some of the following as \ - `@[implicit_reducible]`:\ - {indentD (.joinSep candidates Format.line)}\n\ - Full error:\ - {indentD e.toMessageData}" + let remedy : MessageData := match kind with + | "initial" => "consider rephrasing the goal or marking" + | _ => "consider using propositional rewriting or marking" + return some m!"{kind} tactic goal is not type-correct at \ + `.implicit` transparency; {remedy} some of the following as \ + `@[implicit_reducible]`:\ + {indentD (.joinSep candidates Format.line)}\n\ + Full error:\ + {indentD e.toMessageData}" -- Always restore the original diagnostics snapshot. modify ({ · with diag := origDiag }) return result diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean index 3796de18422b..ec27311284c1 100644 --- a/src/Lean/Meta/Check.lean +++ b/src/Lean/Meta/Check.lean @@ -17,6 +17,28 @@ This is not the Kernel type checker, but an auxiliary method for checking whether terms produced by tactics and `isDefEq` are type correct. -/ +namespace Lean.Linter + +/-- +Warn when the goal target is not type-correct at `.implicit` transparency, or when it contains an +instance argument that only has the expected type above `.instances` transparency. + +The former happens when e.g. `unfold` leaves hypotheses whose types still refer to the pre-unfolded +definition, preventing `rw`/`simp` from matching patterns. The latter happens when e.g. an `rfl` +lemma rewrites a value without updating the instances mentioning it, preventing `rw`/`simp` from +unifying the instance argument. + +The option lives here rather than next to the linter in `Lean.Linter.TacticTypeCheck` because +`simp` reads it too, to run `findInstanceArgMismatch?` on its intermediate results. +-/ +register_builtin_option linter.tacticCheckInstances : Bool := { + defValue := false + descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency and \ + checks its instance arguments at `.instances` transparency" +} + +end Lean.Linter + namespace Lean.Meta private def ensureType (e : Expr) : MetaM Unit := do @@ -337,6 +359,65 @@ def check (e : Expr) (transparency : TransparencyMode := .all) : MetaM Unit := trace[Meta.check] ex.toMessageData throw ex +/-- +Describes the first application in `e` whose instance-implicit argument has the expected type at +`.implicit` transparency but not at `.instances`, if there is one. + +`check e .implicit` accepts such an application, but `simp` and `rw` unify instance-implicit +arguments at `.instances`, so a lemma mentioning the instance still fails to apply. This state +typically arises when an `rfl` lemma rewrites a value without updating the instances mentioning it. +-/ +partial def findInstanceArgMismatch? (e : Expr) : MetaM (Option MessageData) := + withDefault <| visit e |>.run +where + visit (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) := + checkCache { val := e : ExprStructEq } fun _ => do + match e with + | .forallE .. => visitForall e + | .lam .. => visitLambdaLet e + | .letE .. => visitLambdaLet e + | .app f a => + if let some msg ← visit f then return some msg + if let some msg ← visit a then return some msg + visitApp f a + | .mdata _ e => visit e + | .proj _ _ e => visit e + | _ => return none + + visitApp (f a : Expr) : MetaM (Option MessageData) := do + let (expectedType, binfo) ← try getFunctionDomain f catch _ => return none + unless binfo.isInstImplicit do return none + if let some className ← isClass? expectedType then + if isLaxInstanceDefeqClass (← getEnv) className then return none + let aType ← try inferType a catch _ => return none + let defEqAt (transparency : TransparencyMode) : MetaM Bool := + withoutModifyingState <| withTransparency transparency <| isDefEqGuarded expectedType aType + if (← defEqAt .instances) then return none + -- A mismatch that persists at `.implicit` is an outright type error, which `check e .implicit` + -- reports with more context. + unless (← defEqAt .implicit) do return none + let app := (mkApp f a).setAppPPExplicit + addMessageContext m!"The instance argument{indentExpr a}\n\ + {← mkHasTypeButIsExpectedMsg aType expectedType + (trailing? := m!"in the application{indentExpr app}") (trailingExprs := #[app])}" + + visitLambdaLet (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) := + lambdaLetTelescope e fun xs b => do + for x in xs do + match ← getFVarLocalDecl x with + | .cdecl (type := t) .. => + if let some msg ← visit t then return some msg + | .ldecl (type := t) (value := v) .. => + if let some msg ← visit t then return some msg + if let some msg ← visit v then return some msg + visit b + + visitForall (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) := + forallTelescope e fun xs b => do + for x in xs do + if let some msg ← visit (← getFVarLocalDecl x).type then return some msg + visit b + /-- Runs `x` and, on any error, lazily checks whether `e` is type-correct at `instances` transparency. If not, appends an explanatory note to the error message. diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 6a8b7ce3e962..bbd50292d94d 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -60,6 +60,19 @@ register_builtin_option backward.isDefEq.respectTransparency.types : Bool := { when checking whether the type of a metavariable matches the type of the term being assigned to it." } +/-- +Controls whether, when checking the type of an assignment to an instance-implicit (`[..]`) +metavariable, the transparency is capped at `.instances` so an ambient `.default`/`.all` +does not let semireducible definitions be unfolded. + +This option only has an effect when `backward.isDefEq.respectTransparency.types` is `true`. +-/ +register_builtin_option backward.isDefEq.respectTransparency.instances : Bool := { + defValue := true + descr := "if true (the default), cap transparency at `.instances` when checking the type \ + of an assignment to an instance-implicit metavariable" +} + /-- Controls whether non-instance implicit arguments get their transparency bumped to `TransparencyMode.implicit` during `isDefEq`. @@ -553,11 +566,31 @@ abbrev respectTransparencyAtTypes : CoreM Bool := do let opts ← getOptions return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts +/-- +Returns `true` if `mvarId` is an instance metavariable — created for an instance-implicit (`[..]`) +parameter, identified by `.synthetic` kind together with a class type. + +Assignments to these are checked at exactly `.instances` transparency, so an ambient +`.default`/`.all` does not let semireducible definitions be unfolded while checking the type of an +instance assignment. This intentionally does not apply to ordinary implicit (`{..}`) metavariables +that happen to have a class type, which are created with `.natural` kind, nor to classes exempted +by `isLaxInstanceDefeqClass` (marked `@[lax_instance_defeq]`, or propositional). +-/ +private def isInstanceMVar (mvarId : MVarId) : MetaM Bool := do + unless backward.isDefEq.respectTransparency.instances.get (← getOptions) do + return false + unless (← mvarId.getKind) matches .synthetic do return false + let some className ← isClass? (← mvarId.getDecl).type | return false + return !isLaxInstanceDefeqClass (← getEnv) className + /-- Returns `true` if all metavariables whose types influence the type of `e`, a value assigned to an -instance-typed metavariable unter `backward.isDefEq.respectTransparency.instanceSearchTypes`, are admissible. Admissible are: +instance-typed metavariable unter `backward.isDefEq.respectTransparency.instanceSearchTypes`, are +admissible. Admissible are: -* instance-typed metavariables: their own assignments are subject to the same restriction; +* metavariables whose own assignments are subject to the same restriction: instance-typed ones + (spawned by instance search, see `backward.isDefEq.respectTransparency.instanceSearchTypes`) and + instance metavariables (see `isInstanceMVar`); * metavariables `isDefEq` cannot assign (from an outer `MetavarContext` depth, or synthetic opaque): the current instance search cannot commit them to a wrong-typed value, and their eventual assignment is governed by whoever created them. @@ -587,8 +620,12 @@ where | .mvar mvarId => if let some d ← getDelayedMVarAssignment? mvarId then go (mkMVar d.mvarIdPending) + else if (← mvarId.isReadOnlyOrSyntheticOpaque) then + return true + else if (← mvarId.isInstanceTyped) then + return backward.isDefEq.respectTransparency.instanceSearchTypes.get (← getOptions) else - mvarId.isInstanceTyped <||> mvarId.isReadOnlyOrSyntheticOpaque + isInstanceMVar mvarId | .app f _ => go f | .lam _ _ b _ => go b | .letE _ _ v b _ => go v <&&> go b @@ -673,16 +710,36 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool := -- must check whether types are definitionally equal or not, before assigning and returning true let mvarType ← inferType mvar let vType ← inferType v - if (← respectTransparencyAtTypes) then - withImplicitConfig do - if (← Meta.isExprDefEqAux mvarType vType) then + if (← isInstanceMVar mvar.mvarId!) then + if (← spineMVarsAdmissible v) then + if (← checkTypesForInstanceTypedMVarAssignment mvarType vType v) then mvar.mvarId!.assign v return true - else - if (← isDiagnosticsEnabled) then withInferTypeConfig do - if (← Meta.isExprDefEqAux mvarType vType) then - trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.implicit` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`" - return false + synthInstanceTypedMVarAndUnify mvar v + else if (← respectTransparencyAtTypes) then + withImplicitConfig do + if (← Meta.isExprDefEqAux mvarType vType) then + mvar.mvarId!.assign v + return true + else + if (← isDiagnosticsEnabled) then withInferTypeConfig do + if (← Meta.isExprDefEqAux mvarType vType) then + trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.implicit` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`" + return false + -- let withCorrectTransparency (x : MetaM Bool) : MetaM Bool := + -- if isInstance then withExactInstancesConfig x else withImplicitConfig x + -- -- withCorrectTransparency do + -- if (← withCorrectTransparency <| Meta.isExprDefEqAux mvarType vType) then + -- mvar.mvarId!.assign v + -- return true + -- else + -- if isInstance then + -- synthInstanceTypedMVarAndUnify mvar v + -- else + -- if (← isDiagnosticsEnabled) then withInferTypeConfig do + -- if (← Meta.isExprDefEqAux mvarType vType) then + -- trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.implicit` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`" + -- return false else withInferTypeConfig do if (← Meta.isExprDefEqAux mvarType vType) then @@ -972,8 +1029,9 @@ where how many metavariable arguments are representing dependencies. -/ -def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (numScopeArgs : Nat := 0) : MetaM Expr := do - mkFreshExprMVarAt lctx localInsts type MetavarKind.natural Name.anonymous numScopeArgs +def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (numScopeArgs : Nat := 0) + (kind : MetavarKind := .natural) : MetaM Expr := do + mkFreshExprMVarAt lctx localInsts type kind Name.anonymous numScopeArgs namespace CheckAssignment @@ -1108,7 +1166,10 @@ mutual /- Compute new set of local instances. -/ let localInsts := mvarDecl.localInstances.filter fun localInst => !toErase.contains localInst.fvar.fvarId! let mvarType ← check mvarDecl.type - let newMVar ← mkAuxMVar lctx localInsts mvarType mvarDecl.numScopeArgs + -- `newMVar` stands for `mvarId`, so restrictions on its assignments must carry over + let newMVar ← mkAuxMVar lctx localInsts mvarType mvarDecl.numScopeArgs (kind := mvarDecl.kind) + if (← mvarId.isInstanceTyped) then + newMVar.mvarId!.markInstanceTyped mvarId.assign newMVar return newMVar @@ -1150,6 +1211,9 @@ mutual Note that `mvarType` may be different from `eType`. -/ let ctx ← read let newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType + (kind := (← f.mvarId!.getDecl).kind) + if (← f.mvarId!.isInstanceTyped) then + newMVar.mvarId!.markInstanceTyped if (← assignToConstFun f args.size newMVar) then pure newMVar else @@ -1974,7 +2038,10 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM let mvarDecl ← mvarId.getDecl if mvarDecl.numScopeArgs == args₁.size || cfg.constApprox then let type ← inferType (mkAppN mvar args₁) - let auxMVar ← mkAuxMVar mvarDecl.lctx mvarDecl.localInstances type + -- `auxMVar` stands for `mvarId`, so restrictions on its assignments must carry over + let auxMVar ← mkAuxMVar mvarDecl.lctx mvarDecl.localInstances type (kind := mvarDecl.kind) + if (← mvarId.isInstanceTyped) then + auxMVar.mvarId!.markInstanceTyped assignConst mvar args₁.size auxMVar else pure false diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 6a03f9943177..1e0983ac4f9a 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -32,6 +32,28 @@ register_builtin_option backward.synthInstance.canonInstances : Bool := { descr := "use optimization that relies on 'morally canonical' instances during type class resolution" } +/-- +Controls the transparency used by the post-synthesis check that unifies the original goal type +with the synthesized result's type when the class has `outParam`s. + +When `true` (the default), the check uses `.instances` transparency, matching the transparency +used by the rest of typeclass resolution. This means a non-reducible `def Bar := Nat` is *not* +unfolded, so e.g. `#synth Foo Nat Bar` cannot be satisfied by `instance : Foo Nat Nat`. + +When `false`, the check bumps transparency to `.default`, which unfolds semireducible +definitions. This was the historical behavior, retained because patterns like Mathlib's +`def OrderDual (α : Type) : Type := α` rely on `OrderDual α` and `α` being defEq at `.default` +during the outParam check. + +See `assignOutParams` for the implementation. +-/ +register_builtin_option backward.isDefEq.respectTransparency.outParams : Bool := { + defValue := false + descr := "if true (the default), do not bump transparency to `.default` \ + when checking that a synthesized instance's type matches the original goal type \ + for classes with `outParam`s" +} + namespace SynthInstance def getMaxHeartbeats (opts : Options) : Nat := @@ -842,8 +864,14 @@ private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do ``` Mathlib developers are currently trying to refactor the `OrderDual` declaration, but it will take time. We will try to remove the `withDefault` again after the refactoring. + + The `backward.isDefEq.respectTransparency.outParams` option (defaulting to `true`) keeps the + check at `.instances` transparency. Setting it to `false` restores the historical `withDefault` + behavior. -/ - let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType + let bumpTransparency := !backward.isDefEq.respectTransparency.outParams.get (← getOptions) + let defEq ← (if bumpTransparency then withDefault else id) <| + withAssignableSyntheticOpaque <| isDefEq type resultType unless defEq do trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}" return defEq diff --git a/src/Lean/Meta/Tactic/Simp.lean b/src/Lean/Meta/Tactic/Simp.lean index 7faa9f28c5a0..84e0f8194202 100644 --- a/src/Lean/Meta/Tactic/Simp.lean +++ b/src/Lean/Meta/Tactic/Simp.lean @@ -30,6 +30,7 @@ builtin_initialize registerTraceClass `Meta.Tactic.simp.rewrite (inherited := tr builtin_initialize registerTraceClass `Meta.Tactic.simp.backwardDefEq (inherited := true) builtin_initialize registerTraceClass `Meta.Tactic.simp.unify (inherited := true) builtin_initialize registerTraceClass `Meta.Tactic.simp.ground (inherited := true) +builtin_initialize registerTraceClass `Meta.Tactic.simp.resynthInstances (inherited := true) builtin_initialize registerTraceClass `Meta.Tactic.simp.loopProtection (inherited := true) builtin_initialize registerTraceClass `Meta.Tactic.simp.numSteps builtin_initialize registerTraceClass `Meta.Tactic.simp.heads diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index b648566cb9eb..4c64ef1046f8 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Simp.Diagnostics public import Lean.Meta.Match.Value public import Lean.Meta.MonadSimp public import Lean.Util.CollectLooseBVars +import Lean.Linter.Init import Lean.Meta.HaveTelescope import Lean.PrettyPrinter import Lean.ExtraModUses @@ -527,6 +528,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do (skipInstances := !cfg.instances) (pre := pre) (post := post) + (postApp := fixResynthInstancesD) def visitFn (e : Expr) : SimpM Result := do let f := e.getAppFn @@ -647,12 +649,46 @@ def congr (e : Expr) : SimpM Result := do else congrDefault e +/-- +Report the first instance argument in `eNew` whose type stopped matching at `.instances` +transparency, blaming the theorem that was applied most recently. + +`simp` reaches such a term when it rewrites a value an instance argument's type depends on without +being able to rewrite the instance along with it, which leaves every later lemma about that +instance inapplicable. The state is often transient — a later rewrite in the same `simp` call may +remove it again — so the tactic goals the `tacticCheckInstances` linter inspects need not show any +trace of it. +-/ +private def reportInstanceArgMismatch (eNew : Expr) : SimpM Unit := do + let some msg ← (try findInstanceArgMismatch? eNew catch _ => pure none) | return + -- At most one report per command, and stop checking once we have one: the check is a full + -- traversal of every intermediate result. + modify fun s => { s with checkInstanceArgs := false } + let alreadyReported := (← Core.getMessageLog).reportedPlusUnreported.any + (·.data.hasTag (· == Linter.linter.tacticCheckInstances.name)) + if alreadyReported then return + let rewrote ← match (← get).lastThm? with + | some thm => do pure m!"`simp` rewrote a term with {← ppOrigin thm}." + | none => pure m!"`simp` rewrote a term." + Linter.logLint Linter.linter.tacticCheckInstances (← getRef) + m!"{rewrote} The new term has an instance argument whose type does not match at \ + `.instances` transparency:{indentD msg}\n\ + For the rest of this `simp` call, lemmas that mention this instance do not apply." + def simpApp (e : Expr) : SimpM Result := do if isOfNatNatLit e || isOfScientificLit e || isCharLit e then -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n` return { expr := e } else - congr e + let r ← congr e + -- All argument-wise rebuilds (`simpAppUsingCongr`, `congrArgs`, `tryAutoCongrTheorem?`) + -- flow through here, so one fix-up covers them. + let r ← fixResynthInstances e r + -- Check here rather than once per simplified subterm: congruence is what leaves an instance + -- argument behind, and a `post` rewrite may well repair the result before it is cached. + if (← get).checkInstanceArgs && r.expr != e then + reportInstanceArgMismatch r.expr + return r def simpStep (e : Expr) : SimpM Result := do match e with diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 478b7f82f24f..e05e8f46e89a 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -21,6 +21,22 @@ register_builtin_option backward.dsimp.instances : Bool := { descr := "Let `dsimp` and `simp` simplify instance terms" } +/-- +After a definitional rewrite of an argument, check the instance arguments whose types depend on +it at `.instances` transparency; adopt a resynthesized instance when one exists and is defeq at +`.implicit`, and refuse the rewrite otherwise. See `Simp.resynthInstanceArgs`. +-/ +register_builtin_option dsimp.resynthInstances : Bool := { + defValue := false + descr := "check instance arguments after definitional rewrites of the arguments they \ + depend on; adopt a resynthesized instance when possible, refuse the rewrite otherwise" + } + +register_builtin_option dsimp.resynthInstances.warning : Bool := { + defValue := true + descr := "warn when `dsimp.resynthInstances` refuses a rewrite" + } + /-- The result of simplifying some expression `e`. -/ structure Result where /-- The simplified version of `e` -/ @@ -76,6 +92,8 @@ structure Context where maxDischargeDepth : UInt32 := UInt32.ofNatClamp config.maxDischargeDepth simpTheorems : SimpTheoremsArray := {} congrTheorems : SimpCongrTheorems := {} + /-- See `dsimp.resynthInstances`. Set by `mkContext`. -/ + resynthInstances : Bool := false /-- Stores the "parent" term for the term being simplified. If a simplification procedure result depends on this value, @@ -180,6 +198,7 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) ( config, userConfig, simpTheorems, congrTheorems metaConfig := (← mkMetaConfig config) indexConfig := (← mkIndexConfig config) + resynthInstances := dsimp.resynthInstances.get (← getOptions) } def Context.setConfig (context : Context) (config : Config) : MetaM Context := do @@ -252,6 +271,19 @@ structure State where usedTheorems : UsedSimps := {} numSteps : Nat := 0 diag : Diagnostics := {} + /-- + Whether to check intermediate results for instance arguments that stopped matching at + `.instances` transparency. Set from `linter.tacticCheckInstances` by `SimpM.run`, and cleared + again once a mismatch has been reported: the linter reports at most one per command. + -/ + checkInstanceArgs : Bool := false + /-- + Theorem applied by the most recent rewrite; only tracked while `checkInstanceArgs` or + `Context.resynthInstances` is set. + -/ + lastThm? : Option Origin := none + /-- Whether `resynthInstanceArgs` already warned about a refused rewrite in this run. -/ + resynthWarned : Bool := false structure Stats where usedTheorems : UsedSimps := {} @@ -308,7 +340,10 @@ opaque dsimp (e : Expr) : SimpM Expr @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit := do if (← isDiagnosticsEnabled) then - modify fun { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag } => { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag := f diag } + modify fun { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag, checkInstanceArgs, + lastThm?, resynthWarned } => + { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag := f diag, checkInstanceArgs, + lastThm?, resynthWarned } /-- Result type for a simplification procedure. We have `pre` and `post` simplification procedures. @@ -524,6 +559,8 @@ def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do { s with triedThmCounter := s.triedThmCounter.insert thmId cNew } def recordSimpTheorem (thmId : Origin) : SimpM Unit := do + if (← get).checkInstanceArgs || (← readThe Simp.Context).resynthInstances then + modify fun s => { s with lastThm? := some thmId } modifyDiag fun s => let cNew := if let some c := s.usedThmCounter.find? thmId then c + 1 else 1 { s with usedThmCounter := s.usedThmCounter.insert thmId cNew } @@ -642,6 +679,140 @@ where else e +/-- The binder domain of the `j`-th argument of `fType`, instantiated with `args[0..j-1]`. -/ +private def instantiatedBinderDomain? (fType : Expr) (args : Array Expr) (j : Nat) : + SimpM (Option Expr) := do + let mut t := fType + for i in [0:j] do + t ← whnfD t + let .forallE _ _ b _ := t | return none + t := b.instantiate1 args[i]! + t ← whnfD t + let .forallE _ d _ _ := t | return none + return some d + +/-- +Check the instance arguments of `f` after its arguments changed from `origArgs` to `args0`. +An instance argument whose type depends on a changed argument is checked against its new binder +domain at `.instances` transparency; classes exempted by `isLaxInstanceDefeqClass` (marked +`@[lax_instance_defeq]`, or propositional) are skipped. On a mismatch, synthesize an instance of the new domain and +adopt it if it is defeq to the old instance at `.implicit` transparency; otherwise revert the +changed arguments the instance depends on, i.e. refuse those rewrites. + +The arguments an instance depends on are only ever changed definitionally (they have forward +dependencies, so `simp` cannot rewrite them with a proof), which makes both adoption and +reversion transparent to an already-built `Result.proof?`. `e` is the original application, used +for messages. See `dsimp.resynthInstances`. +-/ +def resynthInstanceArgs (e f : Expr) (origArgs args0 : Array Expr) : SimpM (Array Expr) := do + let infos := (← getFunInfoNArgs f args0.size).paramInfo + let n := min (min infos.size args0.size) origArgs.size + let mut relevant := false + for j in [0:n] do + if infos[j]!.isInstance && infos[j]!.backDeps.any (fun i => i < n && args0[i]! != origArgs[i]!) then + relevant := true + break + unless relevant do return args0 + let fType ← inferType f + let mut args := args0 + let mut rounds := 0 + repeat + rounds := rounds + 1 + if rounds > n + 1 then break + let mut dirty := false + for j in [0:n] do + let info := infos[j]! + unless info.isInstance do continue + unless info.backDeps.any (fun i => i < n && args[i]! != origArgs[i]!) do continue + let some expected ← instantiatedBinderDomain? fType args j | continue + if let some className ← isClass? expected then + if isLaxInstanceDefeqClass (← getEnv) className then continue + let instOld := args[j]! + let actual ← inferType instOld + if ← withNewMCtxDepth <| withReducibleAndInstances <| isDefEqGuarded actual expected then + continue + let adopt? : Option Expr ← withNewMCtxDepth do + let inst'? ← try + match ← trySynthInstance expected with + | .some v => pure (some v) + | _ => pure none + catch _ => pure none + match inst'? with + | some inst' => + if ← withTransparency .implicit <| isDefEqGuarded instOld inst' then + pure (some inst') + else + pure none + | none => pure none + match adopt? with + | some inst' => + if inst' != instOld then + trace[Meta.Tactic.simp.resynthInstances] "adopted resynthesized instance \ + in{indentExpr e}\nold instance{indentExpr instOld}\nnew instance{indentExpr inst'}" + args := args.set! j inst' + dirty := true + | none => + -- Refuse: revert the changed arguments this instance depends on, and reset instance + -- arguments that depend on the reverted positions. + let mut reverted : Array Nat := #[] + for i in info.backDeps do + if i < n && args[i]! != origArgs[i]! then + -- Guard: reverting is only sound for definitional changes. + if ← withNewMCtxDepth <| withDefault <| isDefEqGuarded args[i]! origArgs[i]! then + args := args.set! i origArgs[i]! + reverted := reverted.push i + unless reverted.isEmpty do + for k in [0:n] do + if infos[k]!.isInstance && infos[k]!.backDeps.any reverted.contains + && args[k]! != origArgs[k]! then + if ← withNewMCtxDepth <| withDefault <| isDefEqGuarded args[k]! origArgs[k]! then + args := args.set! k origArgs[k]! + dirty := true + trace[Meta.Tactic.simp.resynthInstances] "refused rewrite in{indentExpr e}\n\ + instance argument{indentExpr instOld}\nhas type{indentExpr actual}\n\ + but is expected to have type{indentExpr expected}" + unless (← get).resynthWarned do + modify fun s => { s with resynthWarned := true } + if dsimp.resynthInstances.warning.get (← getOptions) then + let cause ← match (← get).lastThm? with + | some thm => do pure m!"A rewrite with {← ppOrigin thm}" + | none => pure m!"A rewrite" + logWarning <| m!"{cause} changed an argument of{indentExpr e}\n\ + The instance argument{indentExpr instOld}\nthen does not have the expected \ + type at `.instances` transparency, and no usable replacement instance was \ + found. The rewrite was not applied here." ++ + .note m!"Disable this warning with `set_option \ + dsimp.resynthInstances.warning false`, or the whole check with `set_option \ + dsimp.resynthInstances false`." + unless dirty do break + return args + +/-- +Apply `resynthInstanceArgs` to the result of simplifying the application `e`. The reverted or +adopted arguments are defeq to the ones they replace, so `r.proof?` remains valid. +-/ +def fixResynthInstances (e : Expr) (r : Result) : SimpM Result := do + unless (← readThe Simp.Context).resynthInstances do return r + let eNew := r.expr + unless e.isApp && eNew.isApp && eNew.getAppNumArgs == e.getAppNumArgs do return r + let origArgs := e.getAppArgs + let newArgs := eNew.getAppArgs + if origArgs == newArgs then return r + let fixed ← resynthInstanceArgs e eNew.getAppFn origArgs newArgs + if fixed == newArgs then return r + return { r with expr := mkAppN eNew.getAppFn fixed } + +/-- `fixResynthInstances` for `dsimp`'s application rebuild. -/ +def fixResynthInstancesD (orig new : Expr) : SimpM Expr := do + unless (← readThe Simp.Context).resynthInstances do return new + unless orig.isApp && new.isApp && new.getAppNumArgs == orig.getAppNumArgs do return new + let origArgs := orig.getAppArgs + let newArgs := new.getAppArgs + if origArgs == newArgs then return new + let fixed ← resynthInstanceArgs orig new.getAppFn origArgs newArgs + if fixed == newArgs then return new + return mkAppN new.getAppFn fixed + /-- Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`. The resulting proof is built using `congr` and `congrFun` theorems. @@ -990,6 +1161,7 @@ private def updateUsedSimpsWithZetaDelta (ctx : Context) (stats : Stats) : MetaM def SimpM.run (ctx : Context) (s : State := {}) (methods : Methods := {}) (k : SimpM α) : MetaM (α × State) := do let ctx ← ctx.setLctxInitIndices + let s := { s with checkInstanceArgs := Linter.linter.tacticCheckInstances.get (← getOptions) } withSimpContext ctx do let (r, s) ← k methods.toMethodsRef ctx |>.run s trace[Meta.Tactic.simp.numSteps] "{s.numSteps}" diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index e526c71d7539..28e17f9c8244 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -87,6 +87,8 @@ Parameters: over variables that are actually used in the body. - `skipConstInApp`: when true, constant heads in applications are not visited separately. - `skipInstances`: when true, instance arguments (determined via `getFunInfo`) are not visited. +- `postApp`: called on each rebuilt application with the original and the rebuilt application; + its result is passed to `post`. Used by `dsimp` to fix up instance arguments. The `skipInstances` flag is used by `dsimp` to avoid rewriting instances. @@ -103,6 +105,7 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT (usedLetOnly := false) (skipConstInApp := false) (skipInstances := false) + (postApp : Expr → Expr → m Expr := fun _ e => pure e) : m (Expr × Std.HashMap ExprStructEq Expr) := let _ : STWorld IO.RealWorld m := ⟨⟩ let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) } @@ -147,9 +150,9 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT args := args.set i (← visit arg) else args := args.set i (← visit arg) - visitPost (mkAppN f args.toArray) + visitPost (← postApp e (mkAppN f args.toArray)) else - visitPost (mkAppN f (← args.mapM visit)) + visitPost (← postApp e (mkAppN f (← args.mapM visit))) match (← pre e) with | .done e => pure e | .visit e => visit e diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 4a11d8b1b83d..e47937fb35d0 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -1235,6 +1235,8 @@ mutual mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs, ngen := s.ngen.next } + if (← mvarId.isInstanceTyped) then + newMVarId.markInstanceTyped if !mvarDecl.kind.isSyntheticOpaque then mvarId.assign result else diff --git a/src/Lean/Server/CodeActions/Provider.lean b/src/Lean/Server/CodeActions/Provider.lean index 91f4f795bbbc..8b7dd7e38e39 100644 --- a/src/Lean/Server/CodeActions/Provider.lean +++ b/src/Lean/Server/CodeActions/Provider.lean @@ -120,7 +120,7 @@ where if let some pos' := stx[2*i].getPos? then if range.stop < pos' then return i - (stx.getNumArgs + 1) / 2 + pure <| (stx.getNumArgs + 1) / 2 .tacticSeq (bracket || preferred pos) i ((stx, 0) :: stack) let mut childRes := none for i in (*...stx.getNumArgs).iter.stepSize 2 do diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index 38b719eb9cd2..303b3684b4bc 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -412,11 +412,13 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f rw [List.mem_iff_getElem] at c'_in_f rcases c'_in_f with ⟨i, hi, c'_in_f⟩ + -- The following `simp only` leaves behind a term containing a `decide` where the embedded + -- `Decidable` instances does not typecheck at `instances` transparency. simp only [ratHintsExhaustive, getRatClauseIndices] at ratHintsExhaustive_eq_true have i_in_bounds : i < Array.size (Array.range (Array.size f.clauses)) := by grind have i_lt_f_clauses_size : i < f.clauses.size := by grind have h : i ∈ (ratHints.map (fun x => x.1)).toList := by - rw [← of_decide_eq_true ratHintsExhaustive_eq_true] + simp only [← of_decide_eq_true ratHintsExhaustive_eq_true] have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by grind rw [i_eq_range_i] rw [Array.mem_toList_iff] diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index 10bdf6dfd934..3988d5bccdc0 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -731,6 +731,7 @@ private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon return Offset.ofSeconds ⟨hours.val * sign⟩ +set_option backward.isDefEq.respectTransparency false in private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (TypeFormat mod) | .G format => match format with @@ -740,13 +741,13 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ | .y format => match format with | .any => Int.ofNat <$> parseAtLeastNum 1 - | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2 + | .twoDigit => (fun x => (2000 + x : Int)) <$> Int.ofNat <$> parseNum 2 | .fourDigit => Int.ofNat <$> parseNum 4 | .extended n => Int.ofNat <$> parseNum n | .u format => match format with | .any => parseSigned <| parseAtLeastNum 1 - | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2 + | .twoDigit => (fun x => (2000 + x : Int)) <$> Int.ofNat <$> parseNum 2 | .fourDigit => parseSigned <| parseNum 4 | .extended n => parseSigned <| parseNum n | .Y format => diff --git a/src/Std/Time/Zoned/Database/PosixTz.lean b/src/Std/Time/Zoned/Database/PosixTz.lean index 1fe9328ca6cd..b568a35bec46 100644 --- a/src/Std/Time/Zoned/Database/PosixTz.lean +++ b/src/Std/Time/Zoned/Database/PosixTz.lean @@ -36,6 +36,7 @@ private def posixParseSign : Parser Int := <|> attempt (pchar '+' *> pure 1) <|> pure 1 +set_option backward.isDefEq.respectTransparency false in --