From 24cb133eb2884ca388c8fce69752911bcd98a2e0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 6 Jun 2025 20:40:06 +0200 Subject: [PATCH] feat: explicit `defeq` attribute (#8419) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR introduces an explicit `defeq` attribute to mark theorems that can be used by `dsimp`. The benefit of an explicit attribute over the prior logic of looking at the proof body is that we can reliably omit theorem bodies across module boundaries. It also helps with intra-file parallelism. If a theorem is syntactically defined by `:= rfl`, then the attribute is assumed and need not given explicitly. This is a purely syntactic check and can be fooled, e.g. if in the current namespace, `rfl` is not actually “the” `rfl` of `Eq`. In that case, some other syntax has be used, such as `:= (rfl)`. This is also the way to go if a theorem can be proved by `defeq`, but one does not actually want `dsimp` to use this fact. The `defeq` attribute will look at the *type* of the declaration, not the body, to check if it really holds definitionally. Because of different reduction settings, this can sometimes go wrong. Then one should also write `:= (rfl)`, if one does not want this to be a defeq theorem. (If one does then this is currently not possible, but it’s probably a bad idea anyways). The `set_option debug.tactic.simp.checkDefEqAttr true`, `dsimp` will warn if could not apply a lemma due to a missing `defeq` attribute. With `set_option backward.dsimp.useDefEqAttr.get false` one can revert to the old behavior of inferring rfl-ness based on the theorem body. Both options will go away eventually (too bad we can’t mark them as deprecated right away, see #7969) Meta programs that generate theorems (e.g. equational theorems) can use `inferDefEqAttr` to set the attribute based on the theorem body of the just created declaration. This builds on #8501 to update Init to `@[expose]` a fair amount of definitions that, if not exposed, would prevent some existing `:= rfl` theorems from being `defeq` theorems. In the interest of starting backwards compatible, I exposed these function. Hopefully many can be un-exposed later again. A mathlib adaption branch exists that includes both the meta programming fixes and changes to the theorems (e.g. changing `:= by rfl` to `:= rfl`). With the module system there is now no special handling for `defeq` theorem bodies, because we don’t look at the body anymore. The previous hack is removed. The `defeq`-ness of the theorem needs to be checked in the context of the theorem’s *type*; the error message contains a hint if the defeq check fails because of the exported context. --- src/Init/Data/Fin/Fold.lean | 5 +- src/Lean.lean | 1 + src/Lean/AddDecl.lean | 10 - src/Lean/Attributes.lean | 33 ++- src/Lean/Declaration.lean | 2 +- src/Lean/DefEqAttrib.lean | 109 ++++++++++ src/Lean/Elab/DeclModifiers.lean | 6 +- src/Lean/Elab/DefView.lean | 5 + src/Lean/Elab/MutualDef.lean | 28 +-- src/Lean/Elab/PreDefinition/EqUnfold.lean | 2 + src/Lean/Elab/PreDefinition/Eqns.lean | 2 + src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean | 1 + .../Elab/PreDefinition/Structural/Eqns.lean | 77 ++++--- src/Lean/Elab/PreDefinition/WF/Unfold.lean | 2 + src/Lean/Elab/Print.lean | 3 + src/Lean/Meta/Eqns.lean | 2 + src/Lean/Meta/SizeOf.lean | 38 ++-- src/Lean/Meta/Tactic/AuxLemma.lean | 6 +- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 21 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 40 ++-- stage0/src/stdlib_flags.h | 2 + tests/lean/1081.lean | 2 +- tests/lean/1081.lean.expected.out | 2 +- tests/lean/1113.lean | 10 +- tests/lean/1433.lean | 2 +- tests/lean/1433.lean.expected.out | 2 +- tests/lean/dsimpViaConst.lean | 4 +- tests/lean/etaStructIssue.lean | 2 +- tests/lean/etaStructIssue.lean.expected.out | 2 +- tests/lean/interactive/isRflParallel.lean | 42 ++++ .../isRflParallel.lean.expected.out | 0 tests/lean/isDefEqOffsetBug.lean | 2 +- tests/lean/isDefEqOffsetBug.lean.expected.out | 2 +- tests/lean/run/2961.lean | 8 +- tests/lean/run/5667.lean | 8 +- tests/lean/run/6789.lean | 6 +- tests/lean/run/def20.lean | 9 +- tests/lean/run/defeqAttrib.lean | 93 +++++++++ tests/lean/run/dsimp1.lean | 6 + tests/lean/run/eqnOptions.lean | 10 +- tests/lean/run/issue5661.lean | 2 +- tests/lean/run/partial_fixpoint.lean | 2 +- tests/lean/run/printEqns.lean | 7 + tests/lean/run/proofAsSorry.lean | 2 +- tests/lean/run/structuralOverNested.lean | 10 +- tests/lean/run/unfoldLemma.lean | 4 +- tests/lean/run/wfEqns5.lean | 4 +- tests/pkg/module/Module/Basic.lean | 191 ++++++++++++------ tests/pkg/module/Module/Imported.lean | 28 ++- tests/pkg/module/Module/ImportedAll.lean | 136 +++++++------ tests/pkg/module/Module/NonModule.lean | 114 +++++------ 51 files changed, 763 insertions(+), 344 deletions(-) create mode 100644 src/Lean/DefEqAttrib.lean create mode 100644 tests/lean/interactive/isRflParallel.lean create mode 100644 tests/lean/interactive/isRflParallel.lean.expected.out create mode 100644 tests/lean/run/defeqAttrib.lean 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