diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean index 215a56c32f..382e5f288c 100644 --- a/src/Init/Data/Fin/Fold.lean +++ b/src/Init/Data/Fin/Fold.lean @@ -183,10 +183,7 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x | zero => rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind] conv => rhs; rw [←bind_pure (f 0 x)] - congr - try -- TODO: block can be deleted after bootstrapping - funext - simp [foldrM_loop_zero] + rfl | succ i ih => rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc] congr; funext; exact ih .. diff --git a/src/Lean.lean b/src/Lean.lean index 50aef24aff..7e20b152d0 100644 --- a/src/Lean.lean +++ b/src/Lean.lean @@ -41,3 +41,4 @@ import Lean.PrivateName import Lean.PremiseSelection import Lean.Namespace import Lean.EnvExtension +import Lean.DefEqAttrib diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 1ab0b85502..0c2bd1620f 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -64,13 +64,6 @@ Checks whether the declaration was originally declared as a theorem; see also def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool := getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false --- HACK: remove together with MutualDef HACK when `[dsimp]` is introduced -private def isSimpleRflProof (proof : Expr) : Bool := - if let .lam _ _ proof _ := proof then - isSimpleRflProof proof - else - proof.isAppOfArity ``rfl 2 - private def looksLikeRelevantTheoremProofType (type : Expr) : Bool := if let .forallE _ _ type _ := type then looksLikeRelevantTheoremProofType type @@ -90,9 +83,6 @@ def addDecl (decl : Declaration) : CoreM Unit := do let (name, info, kind) ← match decl with | .thmDecl thm => let exportProof := !(← getEnv).header.isModule || - -- We should preserve rfl theorems but also we should not override a decision to hide by the - -- MutualDef elaborator via `withoutExporting` - (← getEnv).isExporting && isSimpleRflProof thm.value || -- TODO: this is horrible... looksLikeRelevantTheoremProofType thm.type if !exportProof then diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index c8dcc06fd8..f4c412c8d2 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -135,7 +135,9 @@ structure TagAttribute where deriving Inhabited def registerTagAttribute (name : Name) (descr : String) - (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO TagAttribute := do + (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) + (applicationTime := AttributeApplicationTime.afterTypeChecking) + (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO TagAttribute := do let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension { name := ref mkInitial := pure {} @@ -145,6 +147,12 @@ def registerTagAttribute (name : Name) (descr : String) let r : Array Name := es.fold (fun a e => a.push e) #[] r.qsort Name.quickLt statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size + asyncMode := asyncMode + replay? := some fun _ newState newConsts s => + newConsts.foldl (init := s) fun s c => + if newState.contains c then + s.insert c + else s } let attrImpl : AttributeImpl := { ref, name, descr, applicationTime @@ -153,7 +161,9 @@ def registerTagAttribute (name : Name) (descr : String) unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global" let env ← getEnv unless (env.getModuleIdxFor? decl).isNone do - throwError "invalid attribute '{name}', declaration is in an imported module" + throwError "invalid attribute '{name}', declaration {.ofConstName decl} is in an imported module" + unless env.asyncMayContain decl do + throwError "invalid attribute '{name}', declaration {.ofConstName decl} is not from the present async context {env.asyncPrefix?}" validate decl modifyEnv fun env => ext.addEntry env decl } @@ -162,10 +172,27 @@ def registerTagAttribute (name : Name) (descr : String) namespace TagAttribute +/-- Sets the attribute (without running `validate`) -/ +def setTag [Monad m] [MonadError m] [MonadEnv m] (attr : TagAttribute) (decl : Name) : m Unit := do + let env ← getEnv + unless (env.getModuleIdxFor? decl).isNone do + throwError "invalid attribute '{attr.attr.name}', declaration {.ofConstName decl} is in an imported module" + unless env.asyncMayContain decl do + throwError "invalid attribute '{attr.attr.name}', declaration {.ofConstName decl} is not from the present async context {env.asyncPrefix?}" + modifyEnv fun env => attr.ext.addEntry env decl + def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool := match env.getModuleIdxFor? decl with | some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt - | none => (attr.ext.getState env).contains decl + | none => + if attr.ext.toEnvExtension.asyncMode matches .async then + -- It seems that the env extension API doesn't quite allow querying attributes in a way + -- that works for realizable constants, but without waiting on proofs to finish. + -- Until then, we use the following overapproximation, to be refined later: + (attr.ext.findStateAsync env decl).contains decl || + (attr.ext.getState env (asyncMode := .local)).contains decl + else + (attr.ext.getState env).contains decl end TagAttribute diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index c695a47bee..b919d983a1 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -482,7 +482,7 @@ def value! (info : ConstantInfo) (allowOpaque := false) : Expr := | .defnInfo {value, ..} => value | .thmInfo {value, ..} => value | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected" - | _ => panic! "declaration with value expected" + | _ => panic! s!"declaration with value expected, but {info.name} has none" def hints : ConstantInfo → ReducibilityHints | .defnInfo {hints, ..} => hints diff --git a/src/Lean/DefEqAttrib.lean b/src/Lean/DefEqAttrib.lean new file mode 100644 index 0000000000..16be6de462 --- /dev/null +++ b/src/Lean/DefEqAttrib.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ +prelude + +import Lean.PrettyPrinter + +namespace Lean +open Meta + +/-- +There are defeq theorems that only hold at transparency `.all`, but also others that hold +(from the kernel's point of view) but where the defeq checker here will run out of cycles. + +So we try the more careful first. +-/ +private def isDefEqCareful (e1 e2 : Expr) : MetaM Bool := do + withOptions (smartUnfolding.set · false) <| do + withDefault (isDefEq e1 e2) <||> withTransparency .all (isDefEq e1 e2) + +def validateDefEqAttr (declName : Name) : AttrM Unit := do + let info ← getConstVal declName + MetaM.run' do + withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq` + forallTelescopeReducing info.type fun _ type => do + let type ← whnf type + -- NB: The warning wording should work both for explicit uses of `@[defeq]` as well as the implicit `:= rfl`. + let some (_, lhs, rhs) := type.eq? | + throwError m!"Not a definitional equality: the conclusion should be an equality, but is{inlineExpr type}" + let ok ← isDefEqCareful lhs rhs + unless ok do + let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do + let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs + let mut msg := m!"Not a definitional equality: the left-hand side{indentExpr lhs}\nis \ + not definitionally equal to the right-hand side{indentExpr rhs}" + if (← getEnv).isExporting then + let okPrivately ← withoutExporting <| isDefEqCareful lhs rhs + if okPrivately then + msg := msg ++ .note m!"This theorem is exported from the current module. \ + This requires that all definitions that need to be unfolded to prove this \ + theorem must be exposed." + pure msg + throwError explanation + +/-- +Marks the theorem as a definitional equality. + +The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem +when rewriting. + +A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`. +To avoid this behavior, write `:= (rfl)` instead. + +The attribute should be given before a `@[simp]` attribute to have effect. + +When using the module system, an exported theorem can only be `@[defeq]` if all definitions that +need to be unfolded to prove the theorem are exported and exposed. +-/ +@[builtin_doc] +builtin_initialize defeqAttr : TagAttribute ← + registerTagAttribute `defeq "mark theorem as a definitional equality, to be used by `dsimp`" + (validate := validateDefEqAttr) (applicationTime := .afterTypeChecking) + (asyncMode := .async) + +private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do + match type with + | .forallE _ _ type _ => + if let .lam _ _ proof _ := proof then + isRflProofCore type proof + else + return false + | _ => + if type.isAppOfArity ``Eq 3 then + if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then + return true + else if proof.isAppOfArity ``Eq.symm 4 then + -- `Eq.symm` of rfl proof is a rfl proof + isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type + else if proof.getAppFn.isConst then + -- The application of a `defeq` theorem is a `rfl` proof + return defeqAttr.hasTag (← getEnv) proof.getAppFn.constName! + else + return false + else + return false + +/-- +For automatically generated theorems (equational theorems etc.), we want to set the `defeq` attribute +if the proof is `rfl`, essentially reproducing the behavior before the introduction of the `defeq` +attribute. This function infers the `defeq` attribute based on the declaration value. +-/ +def inferDefEqAttr (declName : Name) : MetaM Unit := do + withoutExporting do + let info ← getConstInfo declName + let isRfl ← + if let some value := info.value? then + isRflProofCore info.type value + else + pure false + if isRfl then + try + withExporting (isExporting := !isPrivateName declName) do + validateDefEqAttr declName -- sanity-check: would we have accepted `@[defeq]` on this? + catch e => + logError m!"Theorem {declName} has a `rfl`-proof and was thus inferred to be `@[defeq]`, \ + but validating that attribute failed:{indentD e.toMessageData}" + defeqAttr.setTag declName diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 8683129315..0ac147f053 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -84,10 +84,14 @@ def Modifiers.isNonrec : Modifiers → Bool | { recKind := .nonrec, .. } => true | _ => false -/-- Adds attribute `attr` in `modifiers` -/ +/-- Adds attribute `attr` in `modifiers`, at the end -/ def Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers := { modifiers with attrs := modifiers.attrs.push attr } +/-- Adds attribute `attr` in `modifiers`, at the beginning -/ +def Modifiers.addFirstAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers := + { modifiers with attrs := #[attr] ++ modifiers.attrs } + /-- Filters attributes using `p` -/ def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers := { modifiers with attrs := modifiers.attrs.filter p } diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 1ad9d32e13..7a74c02d1a 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -127,6 +127,11 @@ structure DefView where def DefView.isInstance (view : DefView) : Bool := view.modifiers.attrs.any fun attr => attr.name == `instance +/-- Prepends the `defeq` attribute, removing existing ones if there are any -/ +def DefView.markDefEq (view : DefView) : DefView := + { view with modifiers := + view.modifiers.filterAttrs (·.name != `defeq) |>.addFirstAttr { name := `defeq } } + namespace Command open Meta diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 5d0ea17f34..19b5ba1c9e 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1072,34 +1072,20 @@ where withExporting (isExporting := !expandedDeclIds.all (isPrivateName ·.declName)) do let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises let headers ← levelMVarToParamHeaders views headers - -- If the decl looks like a `rfl` theorem, we elaborate is synchronously as we need to wait for - -- the type before we can decide whether the theorem body should be exported and then waiting - -- for the body as well should not add any significant overhead. - let isRflLike := headers.all (·.value matches `(declVal| := rfl)) - -- elaborate body in parallel when all stars align if let (#[view], #[declId]) := (views, expandedDeclIds) then - if Elab.async.get (← getOptions) && view.kind.isTheorem && !isRflLike && + if Elab.async.get (← getOptions) && view.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) && -- holes in theorem types is not a fatal error, but it does make parallelism impossible !headers[0]!.type.hasMVar then elabAsync headers[0]! view declId - else elabSync headers isRflLike - else elabSync headers isRflLike + else elabSync headers + else elabSync headers for view in views, declId in expandedDeclIds do -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting -- that depends only on a part of the ref addDeclarationRangesForBuiltin declId.declName view.modifiers.stx view.ref - elabSync headers isRflLike := do - -- If the reflexivity holds publicly as well (we're still inside `withExporting` here), export - -- the body even if it is a theorem so that it is recognized as a rfl theorem even without - -- `import all`. - let rflPublic ← pure isRflLike <&&> pure (← getEnv).header.isModule <&&> - forallTelescopeReducing headers[0]!.type fun _ type => do - let some (_, lhs, rhs) := type.eq? | pure false - try - isDefEq lhs rhs - catch _ => pure false - finishElab (isExporting := rflPublic) headers + elabSync headers := do + finishElab headers processDeriving headers elabAsync header view declId := do let env ← getEnv @@ -1147,7 +1133,7 @@ where (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do setEnv async.asyncEnv try - finishElab (isExporting := false) #[header] + finishElab #[header] finally reportDiag -- must introduce node to fill `infoHole` with multiple info trees @@ -1279,6 +1265,8 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do if ds.size > 1 && modifiers.isNonrec then throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block" let mut view ← mkDefView modifiers d[1] + if view.kind != .example && view.value matches `(declVal| := rfl) then + view := view.markDefEq let fullHeaderRef := mkNullNode #[d[0], view.headerRef] if let some snap := snap? then view := { view with headerSnap? := some { diff --git a/src/Lean/Elab/PreDefinition/EqUnfold.lean b/src/Lean/Elab/PreDefinition/EqUnfold.lean index a8ce1f5084..e801a0b350 100644 --- a/src/Lean/Elab/PreDefinition/EqUnfold.lean +++ b/src/Lean/Elab/PreDefinition/EqUnfold.lean @@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Util import Lean.Meta.Tactic.Rfl import Lean.Meta.Tactic.Intro import Lean.Meta.Tactic.Apply +import Lean.DefEqAttrib namespace Lean.Meta @@ -53,6 +54,7 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do name, type, value levelParams := info.levelParams } + inferDefEqAttr name return some name diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 91ba9e1a35..b501ce966e 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Split import Lean.Meta.Tactic.Apply import Lean.Meta.Tactic.Refl import Lean.Meta.Match.MatchEqs +import Lean.DefEqAttrib namespace Lean.Elab.Eqns open Meta @@ -429,6 +430,7 @@ where name, type, value levelParams := info.levelParams } + inferDefEqAttr name /-- Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`. diff --git a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean index 850c4abe08..a4fcd1bdc4 100644 --- a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean @@ -36,6 +36,7 @@ where name, type, value levelParams := info.levelParams } + inferDefEqAttr name def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do if (← isRecursiveDefinition declName) then diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index 8327bac76e..890cc07902 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -26,40 +26,51 @@ structure EqnInfo extends EqnInfoCore where deriving Inhabited private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do - trace[Elab.definition.structural.eqns] "proving: {type}" - withNewMCtxDepth do - let main ← mkFreshExprSyntheticOpaqueMVar type - let (_, mvarId) ← main.mvarId!.intros - unless (← tryURefl mvarId) do -- catch easy cases - go (← deltaLHS mvarId) - instantiateMVars main + withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do + withNewMCtxDepth do + let main ← mkFreshExprSyntheticOpaqueMVar type + let (_, mvarId) ← main.mvarId!.intros + unless (← tryURefl mvarId) do -- catch easy cases + go (← deltaLHS mvarId) + instantiateMVars main where go (mvarId : MVarId) : MetaM Unit := do - trace[Elab.definition.structural.eqns] "step\n{MessageData.ofGoal mvarId}" - if (← tryURefl mvarId) then - return () - else if (← tryContradiction mvarId) then - return () - else if let some mvarId ← whnfReducibleLHS? mvarId then - go mvarId - else if let some mvarId ← simpMatch? mvarId then - go mvarId - else if let some mvarId ← simpIf? mvarId then - go mvarId - else - let ctx ← Simp.mkContext - match (← simpTargetStar mvarId ctx (simprocs := {})).1 with - | TacticResultCNM.closed => return () - | TacticResultCNM.modified mvarId => go mvarId - | TacticResultCNM.noChange => - if let some mvarId ← deltaRHS? mvarId declName then + withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do + if (← tryURefl mvarId) then + trace[Elab.definition.structural.eqns] "tryURefl succeeded" + return () + else if (← tryContradiction mvarId) then + trace[Elab.definition.structural.eqns] "tryContadiction succeeded" + return () + else if let some mvarId ← whnfReducibleLHS? mvarId then + trace[Elab.definition.structural.eqns] "whnfReducibleLHS succeeded" + go mvarId + else if let some mvarId ← simpMatch? mvarId then + trace[Elab.definition.structural.eqns] "simpMatch? succeeded" + go mvarId + else if let some mvarId ← simpIf? mvarId then + trace[Elab.definition.structural.eqns] "simpIf? succeeded" + go mvarId + else + let ctx ← Simp.mkContext + match (← simpTargetStar mvarId ctx (simprocs := {})).1 with + | TacticResultCNM.closed => + trace[Elab.definition.structural.eqns] "simpTargetStar closed the goal" + | TacticResultCNM.modified mvarId => + trace[Elab.definition.structural.eqns] "simpTargetStar modified the goal" go mvarId - else if let some mvarIds ← casesOnStuckLHS? mvarId then - mvarIds.forM go - else if let some mvarIds ← splitTarget? mvarId then - mvarIds.forM go - else - throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}" + | TacticResultCNM.noChange => + if let some mvarId ← deltaRHS? mvarId declName then + trace[Elab.definition.structural.eqns] "deltaRHS? succeeded" + go mvarId + else if let some mvarIds ← casesOnStuckLHS? mvarId then + trace[Elab.definition.structural.eqns] "casesOnStuckLHS? succeeded" + mvarIds.forM go + else if let some mvarIds ← splitTarget? mvarId then + trace[Elab.definition.structural.eqns] "splitTarget? succeeded" + mvarIds.forM go + else + throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}" def mkEqns (info : EqnInfo) : MetaM (Array Name) := withOptions (tactic.hygienic.set · false) do @@ -71,7 +82,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) := let mut thmNames := #[] for h : i in [: eqnTypes.size] do let type := eqnTypes[i] - trace[Elab.definition.structural.eqns] "eqnType {i}: {type}" + trace[Elab.definition.structural.eqns] "eqnType {i+1}: {type}" let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}" thmNames := thmNames.push name -- determinism: `type` should be independent of the environment changes since `baseName` was @@ -86,6 +97,7 @@ where name, type, value levelParams := info.levelParams } + inferDefEqAttr name builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension @@ -119,6 +131,7 @@ where name, type, value levelParams := info.levelParams } + inferDefEqAttr name def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do if let some info := eqnInfoExt.find? (← getEnv) declName then diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean index 67a30a9c67..01373ec649 100644 --- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean +++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean @@ -96,6 +96,7 @@ def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessPr name, type, value levelParams := preDef.levelParams } + inferDefEqAttr name trace[Elab.definition.wf] "mkUnfoldEq defined {.ofConstName name}" /-- @@ -127,6 +128,7 @@ def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM U name, type, value levelParams := preDef.levelParams } + inferDefEqAttr name trace[Elab.definition.wf] "mkBinaryUnfoldEq defined {.ofConstName name}" builtin_initialize diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 5853ec1a25..db5e66cbb0 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -29,6 +29,9 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type | ReducibilityStatus.reducible => attrs := attrs.push m!"reducible" | ReducibilityStatus.semireducible => pure () + if defeqAttr.hasTag (← getEnv) id then + attrs := attrs.push m!"defeq" + let mut m : MessageData := m!"" unless attrs.isEmpty do m := m ++ "@[" ++ MessageData.joinSep attrs.toList ", " ++ "] " diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index 3f80cc715a..acce8162dd 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -9,6 +9,7 @@ import Lean.AddDecl import Lean.Meta.Basic import Lean.Meta.AppBuilder import Lean.Meta.Match.MatcherInfo +import Lean.DefEqAttrib namespace Lean.Meta @@ -182,6 +183,7 @@ where doRealize name info := do name, type, value levelParams := info.levelParams } + inferDefEqAttr name -- should always succeed /-- Returns `some declName` if `thmName` is an equational theorem for `declName`. diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 06ab8e94a5..35b5564674 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -8,6 +8,7 @@ import Init.Data.List.BasicAux import Lean.AddDecl import Lean.Meta.AppBuilder import Lean.Meta.Instances +import Lean.DefEqAttrib namespace Lean.Meta @@ -148,14 +149,16 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do trace[Meta.sizeOf] "declName: {declName}" trace[Meta.sizeOf] "type: {sizeOfType}" trace[Meta.sizeOf] "val: {sizeOfValue}" - addDecl <| Declaration.defnDecl { - name := declName - levelParams := levelParams - type := sizeOfType - value := sizeOfValue - safety := DefinitionSafety.safe - hints := ReducibilityHints.abbrev - } + -- We expose the `sizeOf` functions so that the `spec` theorems can be publicly `defeq` + withExporting do + addDecl <| Declaration.defnDecl { + name := declName + levelParams := levelParams + type := sizeOfType + value := sizeOfValue + safety := DefinitionSafety.safe + hints := ReducibilityHints.abbrev + } /-- Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName` @@ -457,6 +460,7 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name type := thmType value := thmValue } + inferDefEqAttr thmName simpAttr.add thmName default AttributeKind.global private def mkSizeOfSpecTheorems (indTypeNames : Array Name) (sizeOfFns : Array Name) (recMap : NameMap Name) : MetaM Unit := do @@ -500,14 +504,16 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}" - addDecl <| Declaration.defnDecl { - name := instDeclName - levelParams := indInfo.levelParams - type := instDeclType - value := instDeclValue - safety := .safe - hints := .abbrev - } + -- We expose the `sizeOf` instance so that the `spec` theorems can be publicly `defeq` + withExporting do + addDecl <| Declaration.defnDecl { + name := instDeclName + levelParams := indInfo.levelParams + type := instDeclType + value := instDeclValue + safety := .safe + hints := .abbrev + } addInstance instDeclName AttributeKind.global (eval_prio default) if genSizeOfSpec.get (← getOptions) then mkSizeOfSpecTheorems indInfo.all.toArray fns recMap diff --git a/src/Lean/Meta/Tactic/AuxLemma.lean b/src/Lean/Meta/Tactic/AuxLemma.lean index 128507360c..c45493204f 100644 --- a/src/Lean/Meta/Tactic/AuxLemma.lean +++ b/src/Lean/Meta/Tactic/AuxLemma.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.AddDecl import Lean.Meta.Basic +import Lean.DefEqAttrib namespace Lean.Meta @@ -27,7 +28,8 @@ builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ← This method is useful for tactics (e.g., `simp`) that may perform preprocessing steps to lemmas provided by users. For example, `simp` preprocessor may convert a lemma into multiple ones. -/ -def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : Option Name := none) (cache := true) : MetaM Name := do +def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : Option Name := none) + (cache := true) (inferRfl := false) : MetaM Name := do let env ← getEnv let s := auxLemmasExt.getState env let mkNewAuxLemma := do @@ -47,6 +49,8 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O levelParams, type, value } addDecl decl + if inferRfl then + inferDefEqAttr auxName modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert type (auxName, levelParams)⟩ return auxName if cache then diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index d053611563..c215d31322 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -110,7 +110,7 @@ where return false private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do - if thm.isRfl (← getEnv) then + if thm.rfl then return (← getConfig).implicitDefEqProofs else return false @@ -218,10 +218,19 @@ where else let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority for (thm, numExtraArgs) in candidates do - unless inErasedSet thm || (rflOnly && !thm.isRfl (← getEnv)) do - if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then - trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}" - return some result + if inErasedSet thm then continue + if rflOnly then + unless thm.rfl do + if debug.tactic.simp.checkDefEqAttr.get (← getOptions) && + backward.dsimp.useDefEqAttr.get (← getOptions) then + let isRflOld ← withOptions (backward.dsimp.useDefEqAttr.set · false) do + isRflProof thm.proof + if isRflOld then + logWarning m!"theorem {thm.proof} is no longer rfl" + continue + if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then + trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}" + return some result return none /-- @@ -236,7 +245,7 @@ where else let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority for thm in candidates do - unless inErasedSet thm || (rflOnly && !thm.isRfl (← getEnv)) do + unless inErasedSet thm || (rflOnly && !thm.rfl) do let result? ← withNewMCtxDepth do let val ← thm.getValue let type ← inferType val diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index dbad7222aa..cdcd409642 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -10,10 +10,23 @@ import Lean.Meta.DiscrTree import Lean.Meta.AppBuilder import Lean.Meta.Eqns import Lean.Meta.Tactic.AuxLemma +import Lean.DefEqAttrib import Lean.DocString -import Lean.PrettyPrinter namespace Lean.Meta +register_builtin_option backward.dsimp.useDefEqAttr : Bool := { + defValue := true + descr := "Use `defeq` attribute rather than checking theorem body to decide whether a theroem \ + can be used in `dsimp` or with `implicitDefEqProofs`." +} + +register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := { + defValue := false + descr := "If true, whenever `dsimp` fails to apply a rewrite rule because it is not marked as \ + `defeq`, check whether it would have been considered as a rfl theorem before the introduction \ + of the `defeq` attribute, and warn if it was. Note that this is a costly check." +} + /-- An `Origin` is an identifier for simp theorems which indicates roughly what action the user took which lead to this theorem existing in the simp set. @@ -123,23 +136,11 @@ structure SimpTheorem where -/ origin : Origin /-- - `rfl` is true if `proof` is by `Eq.refl` or `rfl`. - - NOTE: As the visibility of `proof` may have changed between the point of declaration and use - of a `@[simp]` theorem, `isRfl` must be used to check for this flag. + `rfl` is true if `proof` is by `Eq.refl`, `rfl` or a `@[defeq]` theorem. -/ rfl : Bool deriving Inhabited -/-- Checks whether the theorem holds by reflexivity in the scope given by the environment. -/ -def SimpTheorem.isRfl (s : SimpTheorem) (env : Environment) : Bool := Id.run do - if !s.rfl then - return false - let .decl declName _ _ := s.origin | - return true -- not a global simp theorem, proof visibility must be unchanged - -- If we can see the proof, it must hold in the current scope. - env.findAsync? declName matches some ({ kind := .thm, .. }) - mutual private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do match type with @@ -165,9 +166,12 @@ mutual return false private partial def isRflTheoremCore (declName : Name) : CoreM Bool := do - let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false - let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false - isRflProofCore info.type info.value + if backward.dsimp.useDefEqAttr.get (← getOptions) then + return defeqAttr.hasTag (← getEnv) declName + else + let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false + let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false + isRflProofCore info.type info.value end def isRflTheorem (declName : Name) : CoreM Bool := @@ -439,7 +443,7 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool) if inv || (← shouldPreprocess type) then let mut r := #[] for (val, type) in (← preprocess val type inv (isGlobal := true)) do - let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val + let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val (inferRfl := true) r := r.push <| (← withoutExporting do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false)) return r else diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..f4d5f7ddae 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// please update stage0 + namespace lean { options get_default_options() { options opts; diff --git a/tests/lean/1081.lean b/tests/lean/1081.lean index 184e70b9ba..08335d60f5 100644 --- a/tests/lean/1081.lean +++ b/tests/lean/1081.lean @@ -20,7 +20,7 @@ namespace Vector' | ⟨i+1, h⟩, cons x xs => cons x $ xs.insert a ⟨i, Nat.lt_of_succ_lt_succ h⟩ theorem insert_at_0_eq_cons1 (a: α) (v: Vector' α n): v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := - rfl -- Error, it does not hold by reflexivity because the recursion is on v + (rfl) -- Error, it does not hold by reflexivity because the recursion is on v example (a : α) : nil.insert a ⟨0, by simp +arith⟩ = cons a nil := rfl diff --git a/tests/lean/1081.lean.expected.out b/tests/lean/1081.lean.expected.out index f91fb5ca47..4afda1a68a 100644 --- a/tests/lean/1081.lean.expected.out +++ b/tests/lean/1081.lean.expected.out @@ -4,7 +4,7 @@ has type ?m = ?m : Prop but is expected to have type f 0 y = y : Prop -1081.lean:23:4-23:7: error: type mismatch +1081.lean:23:4-23:9: error: type mismatch rfl has type ?m = ?m : Prop diff --git a/tests/lean/1113.lean b/tests/lean/1113.lean index 0c4035e85a..44c6b8648c 100644 --- a/tests/lean/1113.lean +++ b/tests/lean/1113.lean @@ -2,15 +2,19 @@ def foo: {n: Nat} → Fin n → Nat | 0, _ => 0 | n+1, _ => 0 +-- Local copy to make test more robust against staging issues +@[simp] theorem Nat.succ_eq_add_one' (n : Nat) : succ n = n + 1 := + rfl + theorem t3 {f: Fin (n+1)}: foo f = 0 := by - dsimp only [←Nat.succ_eq_add_one n] at f -- use `dsimp` to ensure we don't copy `f` + dsimp only [←Nat.succ_eq_add_one' n] at f -- use `dsimp` to ensure we don't copy `f` trace_state - simp only [←Nat.succ_eq_add_one n, foo] + simp only [←Nat.succ_eq_add_one' n, foo] example {n: Nat} {f: Fin (n+1)}: foo f = 0 := by revert f - rw[←Nat.succ_eq_add_one n] + rw[←Nat.succ_eq_add_one' n] intro f simp only [foo] diff --git a/tests/lean/1433.lean b/tests/lean/1433.lean index 3dec7cc651..76ef5d654c 100644 --- a/tests/lean/1433.lean +++ b/tests/lean/1433.lean @@ -8,7 +8,7 @@ def wrongRem := 1 theorem correct₁ : dividend / divisor = correctQuot := rfl theorem correct₂ : dividend = divisor * correctQuot + correctRem := rfl -theorem wrong : dividend % divisor = wrongRem := rfl +theorem wrong : dividend % divisor = wrongRem := (rfl) theorem unsound : False := by have : wrongRem = correctRem := by diff --git a/tests/lean/1433.lean.expected.out b/tests/lean/1433.lean.expected.out index 27fd5f033d..cfe2d65032 100644 --- a/tests/lean/1433.lean.expected.out +++ b/tests/lean/1433.lean.expected.out @@ -1,4 +1,4 @@ -1433.lean:11:49-11:52: error: type mismatch +1433.lean:11:49-11:54: error: type mismatch rfl has type ?m = ?m : Prop diff --git a/tests/lean/dsimpViaConst.lean b/tests/lean/dsimpViaConst.lean index a61704999f..199d1a430c 100644 --- a/tests/lean/dsimpViaConst.lean +++ b/tests/lean/dsimpViaConst.lean @@ -36,7 +36,7 @@ def w : Bool → Bool | b => b example : w true = true := by dsimp theorem foo_internal_with_arg (_ : Nat) : w true = true := rfl -@[simp] theorem foo_using_arg : w true = true := foo_internal_with_arg 0 +@[simp, defeq] theorem foo_using_arg : w true = true := foo_internal_with_arg 0 example : w true = true := by dsimp @@ -47,6 +47,6 @@ example : w true = true := by dsimp example : w false = false := by dsimp theorem foo_internal_without_arg : w false = false := rfl -@[simp] theorem foo_without_arg : w false = false := foo_internal_without_arg +@[simp, defeq] theorem foo_without_arg : w false = false := foo_internal_without_arg example : w false = false := by dsimp diff --git a/tests/lean/etaStructIssue.lean b/tests/lean/etaStructIssue.lean index b66f2dc7a4..e7b0227db0 100644 --- a/tests/lean/etaStructIssue.lean +++ b/tests/lean/etaStructIssue.lean @@ -17,4 +17,4 @@ def mkNat (e : E) (x : F e) : Nat := theorem fail (e : E) (x₁ : F e) (x₂ : F (E.mk e)) : mkNat e x₁ = mkNat (E.mk e) x₂ := /- The following rfl was succeeding in the elaborator but failing in the kernel because of a discrepancy in the implementation for Eta-for-structures. -/ - rfl -- should fail + (rfl) -- should fail diff --git a/tests/lean/etaStructIssue.lean.expected.out b/tests/lean/etaStructIssue.lean.expected.out index b812890c04..450aa6e48d 100644 --- a/tests/lean/etaStructIssue.lean.expected.out +++ b/tests/lean/etaStructIssue.lean.expected.out @@ -1,4 +1,4 @@ -etaStructIssue.lean:20:2-20:5: error: type mismatch +etaStructIssue.lean:20:2-20:7: error: type mismatch rfl has type ?m = ?m : Prop diff --git a/tests/lean/interactive/isRflParallel.lean b/tests/lean/interactive/isRflParallel.lean new file mode 100644 index 0000000000..6ea9f91b57 --- /dev/null +++ b/tests/lean/interactive/isRflParallel.lean @@ -0,0 +1,42 @@ +import Lean.Server.Test.Cancel + +open Lean Meta + +/-! +The following should not deadlock: The `simp` tactic should be able to use `a_eq_b` even before +that theorem body is evaluated. + +TODO: Does't work any more with the rfl extension being .async, as that waits for the body to be +evaluated. +-/ + +-- set_option trace.Elab.block true +set_option debug.skipKernelTC true +set_option backward.dsimp.useDefEqAttr false +set_option debug.tactic.simp.checkDefEqAttr false + +axiom testSorry : α + +opaque a : Nat +opaque b : Nat + +theorem a_eq_b : a = b := by + -- Three possible ways to pretend this theorem takes a long time: + + -- wait_for_unblock_async + + -- run_tac + -- while true do + -- if (← Server.Test.Cancel.unblockedCancelTk.isSet) then + -- break + -- IO.sleep 30 + + -- sleep 100000 + exact testSorry + +theorem bar : 2 * a = 2 * b := by + congr 1 + -- apply a_eq_b + simp only [a_eq_b] + run_tac + Server.Test.Cancel.unblockedCancelTk.set diff --git a/tests/lean/interactive/isRflParallel.lean.expected.out b/tests/lean/interactive/isRflParallel.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/lean/isDefEqOffsetBug.lean b/tests/lean/isDefEqOffsetBug.lean index 5880c3a3a4..39eedca42d 100644 --- a/tests/lean/isDefEqOffsetBug.lean +++ b/tests/lean/isDefEqOffsetBug.lean @@ -16,4 +16,4 @@ theorem subZero [AddGroup α] {a : α} : a + -(0 : α) = a := by rw [addZero] theorem shouldFail [AddGroup α] : ((0 : α) + 0) = 0 := - rfl -- Error + (rfl) -- Error diff --git a/tests/lean/isDefEqOffsetBug.lean.expected.out b/tests/lean/isDefEqOffsetBug.lean.expected.out index 4d89f3ab96..66016501e9 100644 --- a/tests/lean/isDefEqOffsetBug.lean.expected.out +++ b/tests/lean/isDefEqOffsetBug.lean.expected.out @@ -1,4 +1,4 @@ -isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch +isDefEqOffsetBug.lean:19:2-19:7: error: type mismatch rfl has type ?m = ?m : Prop diff --git a/tests/lean/run/2961.lean b/tests/lean/run/2961.lean index e55dbb80af..7a82a734a7 100644 --- a/tests/lean/run/2961.lean +++ b/tests/lean/run/2961.lean @@ -8,12 +8,12 @@ def replace (f : Nat → Option Nat) (t : Nat) : Nat := /-- info: equations: -theorem replace.eq_1 : ∀ (f : Nat → Option Nat), +@[defeq] theorem replace.eq_1 : ∀ (f : Nat → Option Nat), replace f Nat.zero = match f Nat.zero with | some u => u | none => Nat.zero -theorem replace.eq_2 : ∀ (f : Nat → Option Nat) (t' : Nat), +@[defeq] theorem replace.eq_2 : ∀ (f : Nat → Option Nat) (t' : Nat), replace f t'.succ = match f t'.succ with | some u => u @@ -58,12 +58,12 @@ def replace2 (f : Nat → Option Nat) (t1 t2 : Nat) : Nat := /-- info: equations: -theorem replace2.eq_1 : ∀ (f : Nat → Option Nat) (t1 : Nat), +@[defeq] theorem replace2.eq_1 : ∀ (f : Nat → Option Nat) (t1 : Nat), replace2 f t1 Nat.zero = match f t1 with | some u => u | none => Nat.zero -theorem replace2.eq_2 : ∀ (f : Nat → Option Nat) (t1 t' : Nat), +@[defeq] theorem replace2.eq_2 : ∀ (f : Nat → Option Nat) (t1 t' : Nat), replace2 f t1 t'.succ = match f t1 with | some u => u diff --git a/tests/lean/run/5667.lean b/tests/lean/run/5667.lean index c64a6d9926..e70afad7a5 100644 --- a/tests/lean/run/5667.lean +++ b/tests/lean/run/5667.lean @@ -92,8 +92,8 @@ def optimize2 : Expr → Expr /-- info: equations: -theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i -theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr), +@[defeq] theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i +@[defeq] theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr), optimize2 (Expr.op bop e1) = match optimize2 e1 with | Expr.const i => Expr.op bop (Expr.const 0) @@ -113,8 +113,8 @@ def optimize3 : Expr → Expr /-- info: equations: -theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i -theorem optimize3.eq_2 : ∀ (bop : Unit) (i : BitVec 32), +@[defeq] theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i +@[defeq] theorem optimize3.eq_2 : ∀ (bop : Unit) (i : BitVec 32), optimize3 (Expr.op bop (Expr.const i)) = Expr.op bop (optimize3 (Expr.const i)) theorem optimize3.eq_3 : ∀ (bop : Unit) (e1 : Expr), (∀ (i : BitVec 32), e1 = Expr.const i → False) → optimize3 (Expr.op bop e1) = Expr.const 0 diff --git a/tests/lean/run/6789.lean b/tests/lean/run/6789.lean index 48b0f33245..a0ecc1172e 100644 --- a/tests/lean/run/6789.lean +++ b/tests/lean/run/6789.lean @@ -36,7 +36,7 @@ theorem Extension.recOn'.eq_1.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ (zero : {Γ : Con} → motive Γ Γ Extension.zero) (succ : {Γ Δ : Con} → (xt : Extension Γ Δ) → (A : Nat) → motive Γ Δ xt → motive Γ (Δ.ext A) (xt.succ A)) (x : Con), Extension.recOn' zero succ Extension.zero = zero -theorem Extension.recOn'.eq_2.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ Δ → Sort v} +@[defeq] theorem Extension.recOn'.eq_2.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ Δ → Sort v} (zero : {Γ : Con} → motive Γ Γ Extension.zero) (succ : {Γ Δ : Con} → (xt : Extension Γ Δ) → (A : Nat) → motive Γ Δ xt → motive Γ (Δ.ext A) (xt.succ A)) (x Δ : Con) (A : Nat) (xt : Extension x Δ), @@ -53,9 +53,9 @@ def Extension.pullback_con /-- info: equations: -theorem Extension.pullback_con.eq_1.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B), +@[defeq] theorem Extension.pullback_con.eq_1.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B), Extension.zero.pullback_con x = B' -theorem Extension.pullback_con.eq_2.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B) (Δ_2 : Con) +@[defeq] theorem Extension.pullback_con.eq_2.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B) (Δ_2 : Con) (xt : Extension B Δ_2) (A : Nat), (xt.succ A).pullback_con x = (xt.pullback_con x).ext A -/ #guard_msgs in diff --git a/tests/lean/run/def20.lean b/tests/lean/run/def20.lean index 9e1bf81d4b..7b5ac4e092 100644 --- a/tests/lean/run/def20.lean +++ b/tests/lean/run/def20.lean @@ -6,8 +6,7 @@ def f : Char → Nat | 'e' => 4 | _ => 5 -theorem ex1 : (f 'a', f 'b', f 'c', f 'd', f 'e', f 'f') = (0, 1, 2, 3, 4, 5) := -rfl +theorem ex1 : (f 'a', f 'b', f 'c', f 'd', f 'e', f 'f') = (0, 1, 2, 3, 4, 5) := rfl def g : Nat → Nat | 100000 => 0 @@ -16,8 +15,10 @@ def g : Nat → Nat | 400000 => 3 | _ => 5 -theorem ex2 : (g 100000, g 200000, g 300000, g 400000, g 0) = (0, 1, 2, 3, 5) := -rfl +-- This uses `(rfl)` and no `rfl` to avoid the `rfl` attribute kicking in +-- and trying to prove the theorem with full transparency and without smart unfolding, +-- which goes wrong +theorem ex2 : (g 100000, g 200000, g 300000, g 400000, g 0) = (0, 1, 2, 3, 5) := (rfl) def h : String → Nat | "hello" => 0 diff --git a/tests/lean/run/defeqAttrib.lean b/tests/lean/run/defeqAttrib.lean new file mode 100644 index 0000000000..3e4f6214a9 --- /dev/null +++ b/tests/lean/run/defeqAttrib.lean @@ -0,0 +1,93 @@ +axiom testSorry : α + +opaque a : Nat +opaque b : Nat +def c := a +@[irreducible] def d := a +opaque P : Nat → Prop + +@[irreducible] def ac := a = c + +/-- +error: Not a definitional equality: the left-hand side + a +is not definitionally equal to the right-hand side + b +-/ +#guard_msgs in +@[defeq] theorem a_eq_b : a = b := testSorry +theorem a_eq_c : a = c := rfl +@[defeq] theorem a_eq_c' : a = c := Eq.refl _ +theorem a_eq_c'' : a = c := Eq.refl _ +@[defeq] theorem a_eq_c''' : ac := by with_unfolding_all rfl +@[defeq] theorem a_eq_d : a = d := by simp [d] + +/-- error: Not a definitional equality: the conclusion should be an equality, but is True -/ +#guard_msgs in +@[defeq] def not_an_eq : True := trivial + + +def Tricky.rfl := a_eq_b +/-- +error: Not a definitional equality: the left-hand side + a +is not definitionally equal to the right-hand side + b +-/ +#guard_msgs in +theorem Tricky.a_eq_b : a = b := rfl -- to confuse the heuristics + +/-! Does `#print` show the attribute? -/ + +/-- info: @[defeq] theorem a_eq_c : a = c -/ +#guard_msgs in +#print sig a_eq_c + +/-! Does dsimp use it? -/ + +/-- error: dsimp made no progress -/ +#guard_msgs in example (h : P b) : P a := by dsimp [a_eq_b]; exact h + +/-- error: dsimp made no progress -/ +#guard_msgs in example (h : P b) : P a := by dsimp [Tricky.a_eq_b]; exact h + +#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c]; exact h + +#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c']; exact h + +/-- error: dsimp made no progress -/ +#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c'']; exact h + +-- a_eq_c''' is correctly tagged, but not used by `a_eq_c` because simp does not look through `ac`. +/-- error: dsimp made no progress -/ +#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c''']; exact h + +#guard_msgs in example (h : P d) : P a := by dsimp [a_eq_d]; exact h + +-- Order of simp and rfl attribute +def e1 := a +@[simp] theorem e1_eq_a : e1 = a := rfl +#guard_msgs in example (h : P a) : P e1 := by dsimp; exact h + +def e2 := a +@[defeq,simp] theorem e2_eq_a : e2 = a := (rfl) +#guard_msgs in example (h : P a) : P e2 := by dsimp; exact h + +def e3 := a +@[simp,defeq] theorem e3_eq_a : e2 = a := (rfl) -- defeq has to come before simp +/-- error: dsimp made no progress -/ +#guard_msgs in example (h : P a) : P e3 := by dsimp; exact h + +-- Tests the `defeq` attibute on a realized constant: That they are set, and that they +-- are transported out +def f := a +#guard_msgs in example (h : P a) : P f := by dsimp [f]; exact h +#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_1]; exact h +#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_def]; exact h +#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_unfold]; exact h + + +def Q := 1 = 1 +@[defeq, simp] theorem Q_true : Q := rfl +/-- error: dsimp made no progress -/ +#guard_msgs in example : Q := by dsimp [Q_true] diff --git a/tests/lean/run/dsimp1.lean b/tests/lean/run/dsimp1.lean index 1629e65b09..99527bb280 100644 --- a/tests/lean/run/dsimp1.lean +++ b/tests/lean/run/dsimp1.lean @@ -22,8 +22,14 @@ example (x : Nat) : P (id x.succ.succ).isZero := by dsimp [Nat.isZero] apply P_false +/-- +trace: x : Nat +⊢ P false +-/ +#guard_msgs in example (x : Nat) : P (id x.succ.succ).isZero := by dsimp [Nat.isZero.eq_2] + trace_state apply P_false example (x : Nat) : P (id x.succ.succ).isZero := by diff --git a/tests/lean/run/eqnOptions.lean b/tests/lean/run/eqnOptions.lean index 7d5c7cd501..73b0ef5109 100644 --- a/tests/lean/run/eqnOptions.lean +++ b/tests/lean/run/eqnOptions.lean @@ -7,8 +7,8 @@ def nonrecfun : Bool → Nat /-- info: equations: -theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0 -theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0 +@[defeq] theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0 +@[defeq] theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0 -/ #guard_msgs in #print equations nonrecfun @@ -24,7 +24,7 @@ def nonrecfun : Bool → Nat /-- info: equations: -theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool), +@[defeq] theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool), nonrecfun x = match x with | false => 0 @@ -46,8 +46,8 @@ set_option backward.eqns.nonrecursive false /-- info: equations: -theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0 -theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0 +@[defeq] theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0 +@[defeq] theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0 -/ #guard_msgs in #print equations nonrecfun diff --git a/tests/lean/run/issue5661.lean b/tests/lean/run/issue5661.lean index c3d747d5a1..dc2978ca48 100644 --- a/tests/lean/run/issue5661.lean +++ b/tests/lean/run/issue5661.lean @@ -8,7 +8,7 @@ inductive Nested where | other /-- -info: theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a := +info: @[defeq] theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a := fun a => Eq.refl (1 + sizeOf a) -/ #guard_msgs in diff --git a/tests/lean/run/partial_fixpoint.lean b/tests/lean/run/partial_fixpoint.lean index 16d1688aef..43e0740305 100644 --- a/tests/lean/run/partial_fixpoint.lean +++ b/tests/lean/run/partial_fixpoint.lean @@ -13,7 +13,7 @@ partial_fixpoint /-- info: equations: -theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1) +@[defeq] theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1) -/ #guard_msgs in #print equations loop diff --git a/tests/lean/run/printEqns.lean b/tests/lean/run/printEqns.lean index 42f24d1f19..263695a359 100644 --- a/tests/lean/run/printEqns.lean +++ b/tests/lean/run/printEqns.lean @@ -1,3 +1,8 @@ +/-! + +Re-instantiate these after a stage0 update + + /-- info: equations: theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), [].append x = x @@ -14,6 +19,8 @@ theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : Lis #guard_msgs in #print equations List.append +-/ + @[simp] def ack : Nat → Nat → Nat | 0, y => y+1 | x+1, 0 => ack x 1 diff --git a/tests/lean/run/proofAsSorry.lean b/tests/lean/run/proofAsSorry.lean index 977fce5fe3..d93b7473aa 100644 --- a/tests/lean/run/proofAsSorry.lean +++ b/tests/lean/run/proofAsSorry.lean @@ -14,7 +14,7 @@ example : 2 + 2 = 5 := rfl -- This is not a theorem /-- warning: declaration uses 'sorry' -/ #guard_msgs in -theorem ex : 2 + 2 = 5 := rfl +theorem ex : 2 + 2 = 5 := id rfl -- id rfl to avoid the rfl attribute kicking in #guard_msgs in def data (w : Nat) : String := toString w diff --git a/tests/lean/run/structuralOverNested.lean b/tests/lean/run/structuralOverNested.lean index 8f68a277f2..6f269537b4 100644 --- a/tests/lean/run/structuralOverNested.lean +++ b/tests/lean/run/structuralOverNested.lean @@ -31,7 +31,7 @@ def RTree.simple_size : RTree α → Nat | .node _x t _ts => 1 + (t true).simple_size + (t false).simple_size /-- -info: theorem RTree.simple_size.eq_1.{u_1} : ∀ {α : Type u_1} (_x : α) (t : Bool → RTree α) (_ts : List (RTree α)), +info: @[defeq] theorem RTree.simple_size.eq_1.{u_1} : ∀ {α : Type u_1} (_x : α) (t : Bool → RTree α) (_ts : List (RTree α)), (RTree.node _x t _ts).simple_size = 1 + (t true).simple_size + (t false).simple_size := fun {α} _x t _ts => Eq.refl (RTree.node _x t _ts).simple_size -/ @@ -51,7 +51,7 @@ def RTree.aux_size : List (RTree α) → Nat end /-- -info: theorem RTree.aux_size.eq_2.{u_1} : ∀ {α : Type u_1} (t : RTree α) (ts : List (RTree α)), +info: @[defeq] theorem RTree.aux_size.eq_2.{u_1} : ∀ {α : Type u_1} (t : RTree α) (ts : List (RTree α)), RTree.aux_size (t :: ts) = t.size + RTree.aux_size ts := fun {α} t ts => Eq.refl (RTree.aux_size (t :: ts)) -/ @@ -67,8 +67,8 @@ def RTree.map_aux (f : α → β) : List (RTree α) → List (RTree β) end /-- -info: theorem RTree.map_aux.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : RTree α) (ts : List (RTree α)), - RTree.map_aux f (t :: ts) = RTree.map f t :: RTree.map_aux f ts := +info: @[defeq] theorem RTree.map_aux.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : RTree α) + (ts : List (RTree α)), RTree.map_aux f (t :: ts) = RTree.map f t :: RTree.map_aux f ts := fun {α} {β} f t ts => Eq.refl (RTree.map_aux f (t :: ts)) -/ #guard_msgs in @@ -95,7 +95,7 @@ def VTree.vec_size : Vec (VTree α true 5) n b → Nat end /-- -info: theorem VTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (b_2 : Bool) (n_2 : Nat) (a : α) +info: @[defeq] theorem VTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (b_2 : Bool) (n_2 : Nat) (a : α) (f : List Bool → List Nat → Vec (VTree α true 5) n_2 b_2), (VTree.node b_2 n_2 a f).size = 1 + VTree.vec_size (f [] []) := fun {α} b_2 n_2 a f => Eq.refl (VTree.node b_2 n_2 a f).size diff --git a/tests/lean/run/unfoldLemma.lean b/tests/lean/run/unfoldLemma.lean index ab6f2bd138..1a89adc870 100644 --- a/tests/lean/run/unfoldLemma.lean +++ b/tests/lean/run/unfoldLemma.lean @@ -4,8 +4,8 @@ def Option_map (f : α → β) : Option α → Option β /-- info: equations: -theorem Option_map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option_map f none = none -theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x_1 : α), +@[defeq] theorem Option_map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option_map f none = none +@[defeq] theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x_1 : α), Option_map f (some x_1) = some (f x_1) -/ #guard_msgs in diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean index 027682ab51..9ae8f71151 100644 --- a/tests/lean/run/wfEqns5.lean +++ b/tests/lean/run/wfEqns5.lean @@ -87,9 +87,9 @@ termination_by structural n => n /-- info: equations: -theorem Structural.foo.eq_1 : foo 0 0 = 0 +@[defeq] theorem Structural.foo.eq_1 : foo 0 0 = 0 theorem Structural.foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x -theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x +@[defeq] theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x -/ #guard_msgs in #print equations foo diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 5106225474..277f308d65 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -1,17 +1,100 @@ module +axiom testSorry : α + /-! Module docstring -/ -/-- A definition. -/ +/-- A definition (not exposed). -/ def f := 1 +/-- An definition (exposed) -/ +@[expose] def fexp := 1 #guard_msgs(drop warning) in /-- A theorem. -/ -theorem t : f = 1 := sorry +theorem t : f = 1 := testSorry +-- Check that the theorem types are checked in exported context, where `f` is not defeq to `1` +-- (but `fexp` is) + +/-- +error: type mismatch + y +has type + Vector Unit 1 : Type +but is expected to have type + Vector Unit f : Type +-/ +#guard_msgs in +theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry + +private theorem v' (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry + +private theorem v'' (x : Vector Unit fexp) (y : Vector Unit 1) : x = y := testSorry + +-- Check that rfl theorems are complained about if they aren't rfl in the context of their type + +/-- +error: Not a definitional equality: the left-hand side + f +is not definitionally equal to the right-hand side + 1 + +Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed. +-/ +#guard_msgs in theorem trfl : f = 1 := rfl +/-- +error: Not a definitional equality: the left-hand side + f +is not definitionally equal to the right-hand side + 1 -@[expose] def fexp := 1 +Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed. +-/ +#guard_msgs in +@[defeq] theorem trfl' : f = 1 := (rfl) + +private theorem trflprivate : f = 1 := rfl +private def trflprivate' : f = 1 := rfl +@[defeq] private def trflprivate''' : f = 1 := rfl +private theorem trflprivate'''' : f = 1 := (rfl) + +theorem fexp_trfl : fexp = 1 := rfl +@[defeq] theorem fexp_trfl' : fexp = 1 := rfl + +opaque P : Nat → Prop +axiom hP1 : P 1 + +/-- error: dsimp made no progress -/ +#guard_msgs in +example : P f := by dsimp only [t]; exact hP1 +example : P f := by simp only [t]; exact hP1 + +/-- error: dsimp made no progress -/ +#guard_msgs in +example : P f := by dsimp only [trfl]; exact hP1 +/-- error: dsimp made no progress -/ +#guard_msgs in +example : P f := by dsimp only [trfl']; exact hP1 +example : P f := by dsimp only [trflprivate]; exact hP1 +example : P f := by dsimp only [trflprivate']; exact hP1 + + +example : P fexp := by dsimp only [fexp_trfl]; exact hP1 +example : P fexp := by dsimp only [fexp_trfl]; exact hP1 + + +-- Check that the error message does not mention the export issue if +-- it wouldn’t be a rfl otherwise either + +/-- +error: Not a definitional equality: the left-hand side + f +is not definitionally equal to the right-hand side + 2 +-/ +#guard_msgs in +@[defeq] theorem not_rfl : f = 2 := testSorry private def priv := 2 @@ -52,90 +135,74 @@ def f.eq_def := 1 #guard_msgs in def fexp.eq_def := 1 -/-- info: f.eq_def : f = 1 -/ -#guard_msgs in -#check f.eq_def +/-- info: @[defeq] private theorem f.eq_def : f = 1 -/ +#guard_msgs in #print sig f.eq_def -/-- info: f.eq_unfold : f = 1 -/ -#guard_msgs in -#check f.eq_unfold +/-- info: @[defeq] private theorem f.eq_unfold : f = 1 -/ +#guard_msgs in #print sig f.eq_unfold -/-- info: fexp.eq_def : fexp = 1 -/ -#guard_msgs in -#check fexp.eq_def +/-- info: @[defeq] theorem fexp.eq_def : fexp = 1 -/ +#guard_msgs in #print sig fexp.eq_def -/-- info: fexp.eq_unfold : fexp = 1 -/ -#guard_msgs in -#check fexp.eq_unfold +/-- info: @[defeq] theorem fexp.eq_unfold : fexp = 1 -/ +#guard_msgs in #print sig fexp.eq_unfold -/-- info: f_struct.eq_1 : f_struct 0 = 0 -/ -#guard_msgs in -#check f_struct.eq_1 +/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/ +#guard_msgs in #print sig f_struct.eq_1 /-- -info: f_struct.eq_def (x✝ : Nat) : - f_struct x✝ = - match x✝ with - | 0 => 0 - | n.succ => f_struct n --/ -#guard_msgs in -#check f_struct.eq_def - -/-- -info: f_struct.eq_unfold : - f_struct = fun x => +info: private theorem f_struct.eq_def : ∀ (x : Nat), + f_struct x = match x with | 0 => 0 | n.succ => f_struct n -/ -#guard_msgs(pass trace, all) in -#check f_struct.eq_unfold - -/-- info: f_wfrec.eq_1 (x✝ : Nat) : f_wfrec 0 x✝ = x✝ -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.eq_1 +#guard_msgs in #print sig f_struct.eq_def /-- -info: f_wfrec.eq_def (x✝ x✝¹ : Nat) : - f_wfrec x✝ x✝¹ = - match x✝, x✝¹ with - | 0, acc => acc - | n.succ, acc => f_wfrec n (acc + 1) +info: private theorem f_struct.eq_unfold : f_struct = fun x => + match x with + | 0 => 0 + | n.succ => f_struct n -/ -#guard_msgs in -#check f_wfrec.eq_def +#guard_msgs(pass trace, all) in #print sig f_struct.eq_unfold + +/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/ +#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1 /-- -info: f_wfrec.eq_unfold : - f_wfrec = fun x x_1 => +info: private theorem f_wfrec.eq_def : ∀ (x x_1 : Nat), + f_wfrec x x_1 = match x, x_1 with | 0, acc => acc | n.succ, acc => f_wfrec n (acc + 1) -/ -#guard_msgs in -#check f_wfrec.eq_unfold - -/-- info: f_exp_wfrec.eq_1 (x✝ : Nat) : f_exp_wfrec 0 x✝ = x✝ -/ -#guard_msgs in -#check f_exp_wfrec.eq_1 +#guard_msgs in #print sig f_wfrec.eq_def /-- -info: f_exp_wfrec.eq_def (x✝ x✝¹ : Nat) : - f_exp_wfrec x✝ x✝¹ = - match x✝, x✝¹ with - | 0, acc => acc - | n.succ, acc => f_exp_wfrec n (acc + 1) +info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 => + match x, x_1 with + | 0, acc => acc + | n.succ, acc => f_wfrec n (acc + 1) -/ -#guard_msgs in -#check f_exp_wfrec.eq_def +#guard_msgs in #print sig f_wfrec.eq_unfold + +/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ +#guard_msgs in #print sig f_exp_wfrec.eq_1 /-- -info: f_exp_wfrec.eq_unfold : - f_exp_wfrec = fun x x_1 => +info: theorem f_exp_wfrec.eq_def : ∀ (x x_1 : Nat), + f_exp_wfrec x x_1 = match x, x_1 with | 0, acc => acc | n.succ, acc => f_exp_wfrec n (acc + 1) -/ -#guard_msgs in -#check f_exp_wfrec.eq_unfold +#guard_msgs in #print sig f_exp_wfrec.eq_def + +/-- +info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 => + match x, x_1 with + | 0, acc => acc + | n.succ, acc => f_exp_wfrec n (acc + 1) +-/ +#guard_msgs in #print sig f_exp_wfrec.eq_unfold diff --git a/tests/pkg/module/Module/Imported.lean b/tests/pkg/module/Module/Imported.lean index 642e5a065c..9bbeccd8dd 100644 --- a/tests/pkg/module/Module/Imported.lean +++ b/tests/pkg/module/Module/Imported.lean @@ -3,6 +3,15 @@ module prelude import Module.Basic +/-! Definitions should be exported without their bodies by default -/ + +/-- +info: def f : Nat := + +-/ +#guard_msgs in +#print f + /-! Theorems should be exported without their bodies -/ /-- @@ -12,10 +21,27 @@ info: theorem t : f = 1 := #guard_msgs in #print t +/-- +info: theorem trfl : f = 1 := + +-/ +#guard_msgs in +#print trfl + /-- error: dsimp made no progress -/ #guard_msgs in -example : f = 1 := by dsimp only [t] +example : P f := by dsimp only [t]; exact hP1 +example : P f := by simp only [t]; exact hP1 +/-- error: dsimp made no progress -/ +#guard_msgs in +example : P f := by dsimp only [trfl]; exact hP1 +/-- error: dsimp made no progress -/ +#guard_msgs in +example : P f := by dsimp only [trfl']; exact hP1 + +example : P fexp := by dsimp only [fexp_trfl]; exact hP1 +example : P fexp := by dsimp only [fexp_trfl']; exact hP1 example : t = t := by dsimp only [trfl] /-- diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index f36614680a..69d335ed58 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/tests/pkg/module/Module/ImportedAll.lean @@ -7,7 +7,7 @@ import all Module.Basic /-- info: theorem t : f = 1 := -sorry +testSorry -/ #guard_msgs in #print t @@ -23,100 +23,116 @@ but is expected to have type #guard_msgs in theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := sorry - - -/-- info: f.eq_def : f = 1 -/ +/-- error: dsimp made no progress -/ #guard_msgs in -#check f.eq_def +example : P f := by dsimp only [t]; exact hP1 +example : P f := by simp only [t]; exact hP1 -/-- info: f.eq_unfold : f = 1 -/ +/-- error: dsimp made no progress -/ #guard_msgs in -#check f.eq_unfold - -/-- info: f_struct.eq_1 : f_struct 0 = 0 -/ +example : P f := by dsimp only [trfl]; exact hP1 +/-- error: dsimp made no progress -/ #guard_msgs in -#check f_struct.eq_1 +example : P f := by dsimp only [trfl']; exact hP1 /-- -info: f_struct.eq_def (x✝ : Nat) : - f_struct x✝ = - match x✝ with - | 0 => 0 - | n.succ => f_struct n +error: unknown identifier 'trflprivate' +--- +error: dsimp made no progress -/ #guard_msgs in -#check f_struct.eq_def +example : P f := by dsimp only [trflprivate]; exact hP1 +/-- +error: unknown identifier 'trflprivate'' +--- +error: dsimp made no progress +-/ +#guard_msgs in +example : P f := by dsimp only [trflprivate']; exact hP1 + + +example : P fexp := by dsimp only [fexp_trfl]; exact hP1 +example : P fexp := by dsimp only [fexp_trfl']; exact hP1 + + +/-- info: @[defeq] private theorem f.eq_def : f = 1 -/ +#guard_msgs in #print sig f.eq_def + +/-- info: @[defeq] private theorem f.eq_unfold : f = 1 -/ +#guard_msgs in #print sig f.eq_unfold + +/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/ +#guard_msgs in #print sig f_struct.eq_1 /-- -info: f_struct.eq_unfold : - f_struct = fun x => +info: private theorem f_struct.eq_def : ∀ (x : Nat), + f_struct x = match x with | 0 => 0 | n.succ => f_struct n -/ -#guard_msgs in -#check f_struct.eq_unfold - -/-- info: f_wfrec.eq_1 (x✝ : Nat) : f_wfrec 0 x✝ = x✝ -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.eq_1 +#guard_msgs in #print sig f_struct.eq_def /-- -info: f_wfrec.eq_def (x✝ x✝¹ : Nat) : - f_wfrec x✝ x✝¹ = - match x✝, x✝¹ with - | 0, acc => acc - | n.succ, acc => f_wfrec n (acc + 1) +info: private theorem f_struct.eq_unfold : f_struct = fun x => + match x with + | 0 => 0 + | n.succ => f_struct n -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.eq_def +#guard_msgs in #print sig f_struct.eq_unfold + +/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/ +#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1 /-- -info: f_wfrec.eq_unfold : - f_wfrec = fun x x_1 => +info: private theorem f_wfrec.eq_def : ∀ (x x_1 : Nat), + f_wfrec x x_1 = match x, x_1 with | 0, acc => acc | n.succ, acc => f_wfrec n (acc + 1) -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.eq_unfold +#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_def /-- -info: f_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc) - (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1))) - (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_wfrec a✝ a✝¹) +info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 => + match x, x_1 with + | 0, acc => acc + | n.succ, acc => f_wfrec n (acc + 1) -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.induct_unfolding - -/-- info: f_exp_wfrec.eq_1 (x✝ : Nat) : f_exp_wfrec 0 x✝ = x✝ -/ -#guard_msgs in -#check f_exp_wfrec.eq_1 +#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_unfold /-- -info: f_exp_wfrec.eq_def (x✝ x✝¹ : Nat) : - f_exp_wfrec x✝ x✝¹ = - match x✝, x✝¹ with - | 0, acc => acc - | n.succ, acc => f_exp_wfrec n (acc + 1) +info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop), + (∀ (acc : Nat), motive 0 acc acc) → + (∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1))) → + ∀ (a a_1 : Nat), motive a a_1 (f_wfrec a a_1) -/ -#guard_msgs in -#check f_exp_wfrec.eq_def +#guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding + +/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ +#guard_msgs in #print sig f_exp_wfrec.eq_1 /-- -info: f_exp_wfrec.eq_unfold : - f_exp_wfrec = fun x x_1 => +info: theorem f_exp_wfrec.eq_def : ∀ (x x_1 : Nat), + f_exp_wfrec x x_1 = match x, x_1 with | 0, acc => acc | n.succ, acc => f_exp_wfrec n (acc + 1) -/ -#guard_msgs in -#check f_exp_wfrec.eq_unfold +#guard_msgs in #print sig f_exp_wfrec.eq_def /-- -info: f_exp_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc) - (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1))) - (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_exp_wfrec a✝ a✝¹) +info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 => + match x, x_1 with + | 0, acc => acc + | n.succ, acc => f_exp_wfrec n (acc + 1) -/ -#guard_msgs(pass trace, all) in -#check f_exp_wfrec.induct_unfolding +#guard_msgs in #print sig f_exp_wfrec.eq_unfold + +/-- +info: theorem f_exp_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop), + (∀ (acc : Nat), motive 0 acc acc) → + (∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1))) → + ∀ (a a_1 : Nat), motive a a_1 (f_exp_wfrec a a_1) +-/ +#guard_msgs(pass trace, all) in #print sig f_exp_wfrec.induct_unfolding diff --git a/tests/pkg/module/Module/NonModule.lean b/tests/pkg/module/Module/NonModule.lean index b339a9a0f0..48bfa62e2b 100644 --- a/tests/pkg/module/Module/NonModule.lean +++ b/tests/pkg/module/Module/NonModule.lean @@ -1,98 +1,84 @@ import Module.Basic import Lean -/-- info: f.eq_def : f = 1 -/ -#guard_msgs in -#check f.eq_def +/-- info: @[defeq] theorem f.eq_def : f = 1 -/ +#guard_msgs in #print sig f.eq_def -/-- info: f.eq_unfold : f = 1 -/ -#guard_msgs in -#check f.eq_unfold - -/-- info: f_struct.eq_1 : f_struct 0 = 0 -/ -#guard_msgs in -#check f_struct.eq_1 +/-- info: @[defeq] theorem f.eq_unfold : f = 1 -/ +#guard_msgs in #print sig f.eq_unfold +/-- info: @[defeq] theorem f_struct.eq_1 : f_struct 0 = 0 -/ +#guard_msgs in #print sig f_struct.eq_1 /-- -info: f_struct.eq_def (x✝ : Nat) : - f_struct x✝ = - match x✝ with - | 0 => 0 - | n.succ => f_struct n --/ -#guard_msgs in -#check f_struct.eq_def - -/-- -info: f_struct.eq_unfold : - f_struct = fun x => +info: theorem f_struct.eq_def : ∀ (x : Nat), + f_struct x = match x with | 0 => 0 | n.succ => f_struct n -/ -#guard_msgs in -#check f_struct.eq_unfold - -/-- info: f_wfrec.eq_1 (x✝ : Nat) : f_wfrec 0 x✝ = x✝ -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.eq_1 +#guard_msgs in #print sig f_struct.eq_def /-- -info: f_wfrec.eq_def (x✝ x✝¹ : Nat) : - f_wfrec x✝ x✝¹ = - match x✝, x✝¹ with - | 0, acc => acc - | n.succ, acc => f_wfrec n (acc + 1) +info: theorem f_struct.eq_unfold : f_struct = fun x => + match x with + | 0 => 0 + | n.succ => f_struct n -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.eq_def +#guard_msgs in #print sig f_struct.eq_unfold + +/-- info: theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/ +#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1 /-- -info: f_wfrec.eq_unfold : - f_wfrec = fun x x_1 => +info: theorem f_wfrec.eq_def : ∀ (x x_1 : Nat), + f_wfrec x x_1 = match x, x_1 with | 0, acc => acc | n.succ, acc => f_wfrec n (acc + 1) -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.eq_unfold +#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_def /-- -info: f_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc) - (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1))) - (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_wfrec a✝ a✝¹) +info: theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 => + match x, x_1 with + | 0, acc => acc + | n.succ, acc => f_wfrec n (acc + 1) -/ -#guard_msgs(pass trace, all) in -#check f_wfrec.induct_unfolding - -/-- info: f_exp_wfrec.eq_1 (x✝ : Nat) : f_exp_wfrec 0 x✝ = x✝ -/ -#guard_msgs(pass trace, all) in -#check f_exp_wfrec.eq_1 +#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_unfold /-- -info: f_exp_wfrec.eq_def (x✝ x✝¹ : Nat) : - f_exp_wfrec x✝ x✝¹ = - match x✝, x✝¹ with - | 0, acc => acc - | n.succ, acc => f_exp_wfrec n (acc + 1) +info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop), + (∀ (acc : Nat), motive 0 acc acc) → + (∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1))) → + ∀ (a a_1 : Nat), motive a a_1 (f_wfrec a a_1) -/ -#guard_msgs in -#check f_exp_wfrec.eq_def +#guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding + +/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ +#guard_msgs(pass trace, all) in +#print sig f_exp_wfrec.eq_1 /-- -info: f_exp_wfrec.eq_unfold : - f_exp_wfrec = fun x x_1 => +info: theorem f_exp_wfrec.eq_def : ∀ (x x_1 : Nat), + f_exp_wfrec x x_1 = match x, x_1 with | 0, acc => acc | n.succ, acc => f_exp_wfrec n (acc + 1) -/ -#guard_msgs(pass trace, all) in -#check f_exp_wfrec.eq_unfold +#guard_msgs in #print sig f_exp_wfrec.eq_def /-- -info: f_exp_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc) - (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1))) - (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_exp_wfrec a✝ a✝¹) +info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 => + match x, x_1 with + | 0, acc => acc + | n.succ, acc => f_exp_wfrec n (acc + 1) -/ -#guard_msgs(pass trace, all) in -#check f_exp_wfrec.induct_unfolding +#guard_msgs(pass trace, all) in #print sig f_exp_wfrec.eq_unfold + +/-- +info: theorem f_exp_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop), + (∀ (acc : Nat), motive 0 acc acc) → + (∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1))) → + ∀ (a a_1 : Nat), motive a a_1 (f_exp_wfrec a a_1) +-/ +#guard_msgs(pass trace, all) in #print sig f_exp_wfrec.induct_unfolding