feat: add @[backward_defeq] attribute and local useBackward simp option (#13492)
This PR introduces stricter inference for the `@[defeq]` attribute and a companion `@[backward_defeq]` attribute that preserves the pre-PR behavior as an opt-in. ### What changed * `@[defeq]` is now inferred only when the equation holds at `.instances` transparency (the transparency `dsimp` operates at). * `@[backward_defeq]` is the old set: every theorem whose `rfl` proof the legacy inference would have accepted is tagged `@[backward_defeq]`, so `defeq ⊆ backward_defeq` holds by construction. * The option `backward.defeqAttrib.useBackward` (default `false`) makes `dsimp` also use `@[backward_defeq]` theorems, restoring the pre-PR behavior for a specific proof or file. * The option is eqn-affecting: its value at the point of a function's definition is recorded so that the equation lemmas later generated for that function use the same value, regardless of the ambient option at the use site. ### Mathlib adaption A companion adaption branch (`lean-pr-testing-backward-defeq-attrib` on mathlib4) builds cleanly against this PR and passes `lake test` without warnings. Most adaption changes are scoped `set_option backward.defeqAttrib.useBackward true in` additions on the failing declarations; a small number of files needed proof-level edits where the stored form of a `dsimp%`/`@[reassoc]`/`@[elementwise]` /`@[simps]`/`@[to_app]`-generated lemma had drifted under the stricter regime. --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Joachim Breitner
GitHub
parent
b0d6a3c283
commit
ac9a1cb415
29 changed files with 306 additions and 123 deletions
|
|
@ -42,5 +42,5 @@ This gadget is supported by
|
|||
It is ineffective in other positions (hypotheses of rewrite rules) or when used by other tactics
|
||||
(e.g. `apply`).
|
||||
-/
|
||||
@[simp ↓, expose]
|
||||
@[simp ↓, expose, implicit_reducible]
|
||||
def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e
|
||||
|
|
|
|||
|
|
@ -16,6 +16,14 @@ public section
|
|||
namespace Lean
|
||||
open Meta
|
||||
|
||||
register_builtin_option backward.defeqAttrib.useBackward : Bool := {
|
||||
defValue := false
|
||||
descr := "When true, `dsimp` also uses theorems tagged `@[backward_defeq]`, i.e. \
|
||||
theorems inferred to be rfl only at default (not instance) transparency. Set this \
|
||||
locally (e.g. `set_option backward.defeqAttrib.useBackward true in ...`) to restore the \
|
||||
pre-stricter-inference behavior for a specific proof."
|
||||
}
|
||||
|
||||
/--
|
||||
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.
|
||||
|
|
@ -26,48 +34,88 @@ 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
|
||||
private def withEqLhsRhs (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
|
||||
withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq`
|
||||
forallTelescopeReducing 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}"
|
||||
k lhs rhs
|
||||
|
||||
/--
|
||||
Marks the theorem as a definitional equality.
|
||||
Validates that `declName` is a definitional equality at `.default`/`.all` transparency
|
||||
(the legacy permissive check). Throws a diagnostic error if not. This is used both as
|
||||
the validator for the `@[defeq]` and `@[backward_defeq]` attributes and as a building
|
||||
block for `inferDefEqAttr`.
|
||||
-/
|
||||
def validateDefEqAttr (declName : Name) : AttrM Unit := do
|
||||
let info ← getConstVal declName
|
||||
MetaM.run' do withEqLhsRhs info.type fun lhs rhs => do
|
||||
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
|
||||
|
||||
The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem
|
||||
when rewriting.
|
||||
/--
|
||||
Marks a theorem as a definitional equality under the permissive transparency rules that
|
||||
predated the stricter `@[defeq]` inference (i.e. an equality that holds at `.default` or
|
||||
`.all` transparency, but possibly not at `.instances` transparency as required by `dsimp`).
|
||||
|
||||
A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
|
||||
To avoid this behavior, write `:= (rfl)` instead.
|
||||
Such theorems are inferred automatically by `inferDefEqAttr`: any theorem that the old
|
||||
`:= rfl` inference would have accepted is tagged `@[backward_defeq]`, and additionally
|
||||
tagged `@[defeq]` when it also passes the stricter check at instance transparency.
|
||||
|
||||
`dsimp` ignores `@[backward_defeq]` theorems by default. Setting
|
||||
`set_option backward.defeqAttrib.useBackward true` (typically scoped to a single proof
|
||||
with `set_option ... in`) makes `dsimp` treat them like `@[defeq]` theorems, which
|
||||
provides a local backwards-compatibility escape hatch for proofs broken by the stricter
|
||||
inference.
|
||||
-/
|
||||
@[builtin_doc]
|
||||
builtin_initialize backwardDefeqAttr : TagAttribute ←
|
||||
registerTagAttribute `backward_defeq
|
||||
"mark theorem as a definitional equality under the permissive pre-stricter-inference \
|
||||
rules, used by `dsimp` when `set_option backward.defeqAttrib.useBackward true`"
|
||||
(validate := validateDefEqAttr) (applicationTime := .afterTypeChecking)
|
||||
(asyncMode := .async .mainEnv)
|
||||
|
||||
/--
|
||||
Marks the theorem as a definitional equality that can be used by `dsimp`.
|
||||
|
||||
The theorem must be an equality that holds at `.instances` transparency. A theorem
|
||||
with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`
|
||||
(and also `@[backward_defeq]`, since the latter is a superset); write `:= (rfl)`
|
||||
instead to suppress this.
|
||||
|
||||
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.
|
||||
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.
|
||||
|
||||
Tagging a theorem with `@[defeq]` automatically also tags it with `@[backward_defeq]`,
|
||||
maintaining the invariant that `@[defeq]` theorems form a subset of `@[backward_defeq]`
|
||||
theorems.
|
||||
-/
|
||||
@[builtin_doc]
|
||||
builtin_initialize defeqAttr : TagAttribute ←
|
||||
registerTagAttribute `defeq "mark theorem as a definitional equality, to be used by `dsimp`"
|
||||
(validate := validateDefEqAttr) (applicationTime := .afterTypeChecking)
|
||||
(validate := fun declName => do
|
||||
-- Validate via the same check as `@[backward_defeq]`, then maintain the invariant
|
||||
-- `defeq ⊆ backward_defeq` by also tagging `backward_defeq`.
|
||||
validateDefEqAttr declName
|
||||
backwardDefeqAttr.setTag declName)
|
||||
(applicationTime := .afterTypeChecking)
|
||||
(asyncMode := .async .mainEnv)
|
||||
|
||||
private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
|
||||
|
|
@ -85,17 +133,28 @@ private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool :=
|
|||
-- `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!
|
||||
-- The application of a `defeq` or `backward_defeq` theorem is a `rfl` proof
|
||||
let env ← getEnv
|
||||
let c := proof.getAppFn.constName!
|
||||
return defeqAttr.hasTag env c || backwardDefeqAttr.hasTag env c
|
||||
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.
|
||||
For automatically generated theorems (equational theorems etc.), we tag the theorem with
|
||||
the `defeq`/`backward_defeq` attributes based on its `rfl` proof:
|
||||
|
||||
* If the equation holds at `.instances` transparency (matching the transparency at which
|
||||
`dsimp` operates), we tag it with `@[defeq]`.
|
||||
* Independently, if the equation holds under the more permissive legacy check (equivalent
|
||||
to `validateDefEqAttr`, i.e. at `.default` or `.all` transparency), we tag it with
|
||||
`@[backward_defeq]`.
|
||||
|
||||
In particular, every theorem that would have been tagged `@[defeq]` before the stricter
|
||||
inference rules were introduced is now tagged `@[backward_defeq]`. Local backwards
|
||||
compatibility can be restored with `set_option backward.defeqAttrib.useBackward true`.
|
||||
-/
|
||||
def inferDefEqAttr (declName : Name) : MetaM Unit := do
|
||||
withoutExporting do
|
||||
|
|
@ -105,11 +164,25 @@ def inferDefEqAttr (declName : Name) : MetaM Unit := do
|
|||
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}"
|
||||
unless isRfl do return
|
||||
-- Strict check: defeq at instance transparency (as used by `dsimp`).
|
||||
let strict ← withEqLhsRhs info.type fun lhs rhs =>
|
||||
withReducibleAndInstances (isDefEq lhs rhs)
|
||||
-- Sanity-check: is the theorem also defeq at the permissive (`.default`/`.all`)
|
||||
-- transparency we use for `@[backward_defeq]`? If not, log the error that the
|
||||
-- legacy inference would have emitted — but still proceed to tag
|
||||
-- `@[backward_defeq]` unconditionally. The legacy (pre-PR) behavior tagged
|
||||
-- `@[defeq]` unconditionally whenever `isRflProofCore` returned true,
|
||||
-- regardless of whether the validation check passed, and we want to preserve
|
||||
-- exactly that set under `backward_defeq` so that `useBackward=true` reliably
|
||||
-- restores the old behavior.
|
||||
try
|
||||
withExporting (isExporting := !isPrivateName declName) do
|
||||
validateDefEqAttr declName
|
||||
catch e =>
|
||||
unless strict do
|
||||
logError m!"Theorem {declName} has a `rfl`-proof but could not be validated \
|
||||
as a definitional equality:{indentD e.toMessageData}"
|
||||
if strict then
|
||||
defeqAttr.setTag declName
|
||||
backwardDefeqAttr.setTag declName
|
||||
|
|
|
|||
|
|
@ -129,7 +129,9 @@ 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 -/
|
||||
/-- Prepends the `defeq` attribute, removing existing ones if there are any.
|
||||
The `defeq` attribute's validator also tags `backward_defeq` on success, so the
|
||||
superset invariant `defeq ⊆ backward_defeq` is preserved. -/
|
||||
def DefView.markDefEq (view : DefView) : DefView :=
|
||||
{ view with modifiers :=
|
||||
view.modifiers.filterAttrs (·.name != `defeq) |>.addFirstAttr { name := `defeq } }
|
||||
|
|
|
|||
|
|
@ -37,6 +37,8 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
|
|||
|
||||
if defeqAttr.hasTag (← getEnv) id then
|
||||
attrs := attrs.push m!"defeq"
|
||||
else if backwardDefeqAttr.hasTag (← getEnv) id then
|
||||
attrs := attrs.push m!"backward_defeq"
|
||||
|
||||
let mut m : MessageData := m!""
|
||||
unless attrs.isEmpty do
|
||||
|
|
|
|||
|
|
@ -40,7 +40,8 @@ value at definition time, not realization time, should matter.
|
|||
This is implemented by storing their values at definition time (when non-default) in an environment
|
||||
extension, and restoring them when the equations are lazily realized.
|
||||
-/
|
||||
def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
|
||||
def eqnAffectingOptions : Array (Lean.Option Bool) :=
|
||||
#[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit, backward.defeqAttrib.useBackward]
|
||||
|
||||
/-- Environment extension that stores the values of `eqnAffectingOptions` at definition time,
|
||||
keyed by declaration name. Only populated when at least one option has a non-default value.
|
||||
|
|
|
|||
|
|
@ -18,6 +18,8 @@ structure AuxLemmaKey where
|
|||
-- When an aux lemma is created in a private context and thus has a private name, we must not
|
||||
-- reuse it in an exported context.
|
||||
isPrivate : Bool
|
||||
-- Whether the theorem should be tagged with `[defeq]` (needs to happen before caching)
|
||||
defeq : Bool
|
||||
deriving BEq, Hashable
|
||||
|
||||
structure AuxLemmas where
|
||||
|
|
@ -39,10 +41,10 @@ builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ←
|
|||
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) (inferRfl := false) (forceExpose := false) : MetaM Name := do
|
||||
(cache := true) (inferRfl := false) (forceExpose := false) (defeq := false) : MetaM Name := do
|
||||
let env ← getEnv
|
||||
let s := auxLemmasExt.getState env
|
||||
let key := { type, isPrivate := !env.isExporting }
|
||||
let key := { type, isPrivate := !env.isExporting, defeq }
|
||||
let mkNewAuxLemma := do
|
||||
let auxName ← mkAuxDeclName (kind := kind?.getD `_proof)
|
||||
let decl :=
|
||||
|
|
@ -60,6 +62,7 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
|
|||
levelParams, type, value
|
||||
}
|
||||
addDecl (forceExpose := forceExpose) decl
|
||||
if defeq then defeqAttr.setTag auxName
|
||||
if inferRfl then
|
||||
inferDefEqAttr auxName
|
||||
modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert key (auxName, levelParams)⟩
|
||||
|
|
|
|||
|
|
@ -107,7 +107,7 @@ where
|
|||
return false
|
||||
|
||||
private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
|
||||
if thm.rfl then
|
||||
if thm.rfl || (thm.backwardRfl && backward.defeqAttrib.useBackward.get (← getOptions)) then
|
||||
return (← getConfig).implicitDefEqProofs
|
||||
else
|
||||
return false
|
||||
|
|
@ -218,11 +218,12 @@ where
|
|||
return none
|
||||
else
|
||||
let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
|
||||
let useBackward := backward.defeqAttrib.useBackward.get (← getOptions)
|
||||
for (thm, numExtraArgs) in candidates do
|
||||
checkSystem "simp"
|
||||
if inErasedSet thm then continue
|
||||
if rflOnly then
|
||||
unless thm.rfl do
|
||||
unless thm.rfl || (useBackward && thm.backwardRfl) do
|
||||
if debug.tactic.simp.checkDefEqAttr.get (← getOptions) &&
|
||||
backward.dsimp.useDefEqAttr.get (← getOptions) then
|
||||
let isRflOld ← withOptions (backward.dsimp.useDefEqAttr.set · false) do
|
||||
|
|
@ -246,9 +247,10 @@ where
|
|||
return none
|
||||
else
|
||||
let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
|
||||
let useBackward := backward.defeqAttrib.useBackward.get (← getOptions)
|
||||
for thm in candidates do
|
||||
checkSystem "simp"
|
||||
unless inErasedSet thm || (rflOnly && !thm.rfl) do
|
||||
unless inErasedSet thm || (rflOnly && !(thm.rfl || (useBackward && thm.backwardRfl))) do
|
||||
let result? ← withNewMCtxDepth do
|
||||
let val ← thm.getValue
|
||||
let type ← inferType val
|
||||
|
|
@ -360,7 +362,7 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
|
|||
def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
|
||||
for matchEq in (← Match.getEquationsFor matcherName).eqnNames do
|
||||
-- Try lemma
|
||||
match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) }) with
|
||||
match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq), backwardRfl := (← isBackwardRflTheorem matchEq) }) with
|
||||
| none => pure ()
|
||||
| some r => return .visit r
|
||||
return .continue
|
||||
|
|
@ -441,7 +443,7 @@ def sevalGround : Simproc := fun e => do
|
|||
-- `declName` has equation theorems associated with it.
|
||||
for eqn in eqns do
|
||||
-- TODO: cache SimpTheorem to avoid calls to `isRflTheorem`
|
||||
if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn) } then
|
||||
if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn), backwardRfl := (← isBackwardRflTheorem eqn) } then
|
||||
trace[Meta.Tactic.simp.ground] "unfolded, {e} => {result.expr}"
|
||||
return .visit result
|
||||
return .continue
|
||||
|
|
|
|||
|
|
@ -174,14 +174,20 @@ structure SimpTheorem where
|
|||
`rfl` is true if `proof` is by `Eq.refl`, `rfl` or a `@[defeq]` theorem.
|
||||
-/
|
||||
rfl : Bool
|
||||
/--
|
||||
`backwardRfl` is true if `proof` is by a `@[backward_defeq]` theorem (i.e. rfl at default,
|
||||
but not instance, transparency). Honored by `dsimp` only when
|
||||
`backward.defeqAttrib.useBackward` is set.
|
||||
-/
|
||||
backwardRfl : Bool := false
|
||||
deriving Inhabited
|
||||
|
||||
mutual
|
||||
private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
|
||||
private partial def isRflProofCore (includeBackward : Bool) (type : Expr) (proof : Expr) : CoreM Bool := do
|
||||
match type with
|
||||
| .forallE _ _ type _ =>
|
||||
if let .lam _ _ proof _ := proof then
|
||||
isRflProofCore type proof
|
||||
isRflProofCore includeBackward type proof
|
||||
else
|
||||
return false
|
||||
| _ =>
|
||||
|
|
@ -190,23 +196,25 @@ mutual
|
|||
return true
|
||||
else if proof.isAppOfArity ``Eq.symm 4 then
|
||||
-- `Eq.symm` of rfl theorem is a rfl theorem
|
||||
isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
|
||||
isRflProofCore includeBackward type proof.appArg! -- small hack: we don't need to set the exact type
|
||||
else if proof.getAppFn.isConst then
|
||||
-- The application of a `rfl` theorem is a `rfl` theorem
|
||||
-- A constant which is a `rfl` theorem is a `rfl` theorem
|
||||
isRflTheoremCore proof.getAppFn.constName!
|
||||
isRflTheoremCore includeBackward proof.getAppFn.constName!
|
||||
else
|
||||
return false
|
||||
else
|
||||
return false
|
||||
|
||||
private partial def isRflTheoremCore (declName : Name) : CoreM Bool := do
|
||||
private partial def isRflTheoremCore (includeBackward : Bool) (declName : Name) : CoreM Bool := do
|
||||
if backward.dsimp.useDefEqAttr.get (← getOptions) then
|
||||
return defeqAttr.hasTag (← getEnv) declName
|
||||
let env ← getEnv
|
||||
return defeqAttr.hasTag env declName ||
|
||||
(includeBackward && backwardDefeqAttr.hasTag env 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
|
||||
isRflProofCore includeBackward info.type info.value
|
||||
end
|
||||
|
||||
def isRflTheorem (declName : Name) : CoreM Bool :=
|
||||
|
|
@ -214,7 +222,12 @@ def isRflTheorem (declName : Name) : CoreM Bool :=
|
|||
-- for the ultimate application of a rfl theorem, only that the theorem type's LHS and RHS are
|
||||
-- defeq.
|
||||
withoutExporting do
|
||||
isRflTheoremCore declName
|
||||
isRflTheoremCore (includeBackward := false) declName
|
||||
|
||||
/-- Like `isRflTheorem`, but also returns `true` for `@[backward_defeq]` theorems. -/
|
||||
def isBackwardRflTheorem (declName : Name) : CoreM Bool :=
|
||||
withoutExporting do
|
||||
isRflTheoremCore (includeBackward := true) declName
|
||||
|
||||
def isRflProof (proof : Expr) : MetaM Bool := do
|
||||
-- Make theorem body available if `declName` is from the current module; the body does not matter
|
||||
|
|
@ -222,9 +235,18 @@ def isRflProof (proof : Expr) : MetaM Bool := do
|
|||
-- defeq.
|
||||
withoutExporting do
|
||||
if let .const declName .. := proof then
|
||||
isRflTheoremCore declName
|
||||
isRflTheoremCore (includeBackward := false) declName
|
||||
else
|
||||
isRflProofCore (← inferType proof) proof
|
||||
isRflProofCore (includeBackward := false) (← inferType proof) proof
|
||||
|
||||
/-- Like `isRflProof`, but also returns `true` for proofs that are rfl only at default
|
||||
transparency (via `@[backward_defeq]`). -/
|
||||
def isBackwardRflProof (proof : Expr) : MetaM Bool := do
|
||||
withoutExporting do
|
||||
if let .const declName .. := proof then
|
||||
isRflTheoremCore (includeBackward := true) declName
|
||||
else
|
||||
isRflProofCore (includeBackward := true) (← inferType proof) proof
|
||||
|
||||
instance : ToFormat SimpTheorem where
|
||||
format s :=
|
||||
|
|
@ -405,6 +427,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
|
|||
let type ← instantiateMVars (← inferType e)
|
||||
let (keys, perm) ← mkSimpTheoremKeys type noIndexAtArgs checkLhs
|
||||
let rfl ← isRflProof proof
|
||||
let backwardRfl ← if rfl then pure true else isBackwardRflProof proof
|
||||
if rfl && simp.rfl.checkTransparency.get (← getOptions) then
|
||||
forallTelescopeReducing type fun _ type => do
|
||||
let checkDefEq (lhs rhs : Expr) := do
|
||||
|
|
@ -419,7 +442,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
|
|||
| Iff lhs rhs => checkDefEq lhs rhs
|
||||
| _ =>
|
||||
logWarning m!"'{origin.key}' is a 'rfl' simp theorem, unexpected resulting type{indentExpr type}"
|
||||
return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl }
|
||||
return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl, backwardRfl }
|
||||
|
||||
/--
|
||||
Creates a `SimpTheorem` from a global theorem.
|
||||
|
|
@ -440,6 +463,8 @@ def mkSimpTheoremFromConst (declName : Name) (post := true) (inv := false)
|
|||
let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val (inferRfl := true)
|
||||
(forceExpose := true) -- These kinds of theorems are small and `to_additive` may need to
|
||||
-- unfold them.
|
||||
-- The `[defeq]` attribute transfers (should only matter for `[← thm]`)
|
||||
(defeq := inv && defeqAttr.hasTag (← getEnv) declName)
|
||||
r := r.push <| (← do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false) (checkLhs := checkLhs))
|
||||
return r
|
||||
else
|
||||
|
|
|
|||
|
|
@ -57,6 +57,7 @@ where
|
|||
origin := .decl matchEqDeclName
|
||||
proof := mkConst matchEqDeclName
|
||||
rfl := (← isRflTheorem matchEqDeclName)
|
||||
backwardRfl := (← isBackwardRflTheorem matchEqDeclName)
|
||||
}
|
||||
match (← withReducible <| Simp.tryTheorem? e simpTheorem) with
|
||||
| none => return .continue
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
|
|||
return { expr := (← deltaExpand e (· == declName)) }
|
||||
where
|
||||
pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
|
||||
match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) }) with
|
||||
match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm), backwardRfl := (← isBackwardRflTheorem unfoldThm) }) with
|
||||
| none => pure ()
|
||||
| some r => match (← reduceMatcher? r.expr) with
|
||||
| .reduced e' => return .done { r with expr := e' }
|
||||
|
|
|
|||
|
|
@ -538,10 +538,10 @@ theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (
|
|||
|
||||
theorem alter_eq_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
|
||||
(f : Option (β a) → Option (β a)) : m.alter a f = m.alterₘ a f := by
|
||||
dsimp only [alter, alterₘ, containsₘ, ← bucket_eq]
|
||||
simp only [alter, alterₘ, containsₘ, ← bucket_eq]
|
||||
split
|
||||
· congr 2
|
||||
· simp only [withComputedSize, bucket_updateBucket]
|
||||
· simp only [withComputedSize, bucket_updateBucket, AssocList.contains_eq]
|
||||
· simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]
|
||||
· congr
|
||||
|
||||
|
|
@ -568,10 +568,10 @@ variable {β : Type v}
|
|||
|
||||
theorem alter_eq_alterₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α)
|
||||
(f : Option β → Option β) : Const.alter m a f = Const.alterₘ m a f := by
|
||||
dsimp only [alter, alterₘ, containsₘ, ← bucket_eq]
|
||||
simp only [alter, alterₘ, containsₘ, ← bucket_eq]
|
||||
split
|
||||
· congr 2
|
||||
· simp only [withComputedSize, bucket_updateBucket]
|
||||
· simp only [withComputedSize, bucket_updateBucket, AssocList.contains_eq]
|
||||
· simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]
|
||||
· congr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
// please update stage0
|
||||
#include "util/options.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ info: optimize.eq_def (x✝ : Expr) :
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i
|
||||
@[backward_defeq] theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i
|
||||
theorem optimize.eq_2 : ∀ (e1 : Expr) (bop : Unit) (i : BitVec 32),
|
||||
optimize e1 = Expr.const i → optimize (Expr.op bop e1) = Expr.op bop (Expr.const 0)
|
||||
theorem optimize.eq_3 : ∀ (e1 : Expr) (bop : Unit),
|
||||
|
|
@ -44,8 +44,8 @@ def optimize2 : Expr → Expr
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i
|
||||
@[defeq] theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr),
|
||||
@[backward_defeq] theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i
|
||||
@[backward_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)
|
||||
|
|
@ -65,8 +65,8 @@ def optimize3 : Expr → Expr
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[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),
|
||||
@[backward_defeq] theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i
|
||||
@[backward_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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
@[defeq] theorem Extension.recOn'.eq_2.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ Δ → Sort v}
|
||||
@[backward_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,10 +53,10 @@ def Extension.pullback_con
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem Extension.pullback_con.eq_1.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B),
|
||||
@[backward_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'
|
||||
@[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
|
||||
@[backward_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
|
||||
#print equations Extension.pullback_con
|
||||
|
|
|
|||
|
|
@ -82,8 +82,13 @@ def e3 := a
|
|||
-- are transported out
|
||||
def f := a
|
||||
#guard_msgs in example (h : P a) : P f := by dsimp [f]; exact h
|
||||
-- `f.eq_1` etc. are only `[backward_defeq]` (not `[defeq]`) since `f` is semireducible;
|
||||
-- so we need to opt into the backward behavior for `dsimp` to use them.
|
||||
set_option backward.defeqAttrib.useBackward true in
|
||||
#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_1]; exact h
|
||||
set_option backward.defeqAttrib.useBackward true in
|
||||
#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_def]; exact h
|
||||
set_option backward.defeqAttrib.useBackward true in
|
||||
#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_unfold]; exact h
|
||||
|
||||
|
||||
|
|
|
|||
65
tests/elab/defeqAttribStrictOnly.lean
Normal file
65
tests/elab/defeqAttribStrictOnly.lean
Normal file
|
|
@ -0,0 +1,65 @@
|
|||
module
|
||||
|
||||
prelude
|
||||
|
||||
public import Lean.DefEqAttrib
|
||||
import Init.Data.Nat.Basic
|
||||
|
||||
/-!
|
||||
# Can `@[defeq]` inference have `strict=true` while `validateDefEqAttr` throws?
|
||||
|
||||
The algorithm in `inferDefEqAttr` swallows `validateDefEqAttr` errors when
|
||||
`strict` passed:
|
||||
|
||||
```
|
||||
try withExporting ... validateDefEqAttr declName
|
||||
catch e =>
|
||||
unless strict do logError m!"..."
|
||||
```
|
||||
|
||||
This guards a theoretical case where the strict check (`.instances` transparency,
|
||||
smart-unfolding ON, under `withoutExporting`) passes but the permissive check
|
||||
(`.default`/`.all`, smart-unfolding OFF, under `withExporting` for public decls)
|
||||
fails. The two differ along three axes: transparency, export-view, smart-unfolding.
|
||||
|
||||
Trying to construct a case:
|
||||
|
||||
1. Public `@[reducible] def hidden := 42` + public `theorem h = 42 := rfl`:
|
||||
Both strict and permissive fail. The `@[reducible]` marker apparently attaches
|
||||
to the exported view and does not make `hidden` instance-reducible under
|
||||
`withoutExporting`. Not a counterexample.
|
||||
|
||||
2. The same pair as private: strict=true, permissive=true. Both pass.
|
||||
|
||||
3. Recursive `@[reducible]` def relying on smart unfolding: same pattern — public
|
||||
fails both, private passes both.
|
||||
|
||||
Under the module system, it seems the `withoutExporting` in `inferDefEqAttr` does
|
||||
not give the strict check a strictly-bigger view than the permissive check has.
|
||||
Every case where strict succeeds, permissive succeeds too. The `unless strict do
|
||||
logError` branch is therefore a defensive guard that (as far as this demonstrates)
|
||||
is unreachable in practice.
|
||||
-/
|
||||
|
||||
@[reducible] public def hidden : Nat := 42
|
||||
|
||||
-- Public version: error message from `validateDefEqAttr` surfaces via
|
||||
-- `unless strict do logError` because strict=false (reducibility of the exported
|
||||
-- view is gone under `withoutExporting`).
|
||||
/--
|
||||
error: Not a definitional equality: the left-hand side
|
||||
hidden
|
||||
is not definitionally equal to the right-hand side
|
||||
42
|
||||
|
||||
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
|
||||
public theorem test_public : hidden = 42 := rfl
|
||||
|
||||
-- Private version: both strict and permissive checks pass, tagged `@[defeq]`.
|
||||
theorem test_private : hidden = 42 := rfl
|
||||
|
||||
/-- info: @[defeq] private theorem test_private : hidden = 42 -/
|
||||
#guard_msgs in
|
||||
#print sig test_private
|
||||
|
|
@ -27,6 +27,7 @@ trace: x : Nat
|
|||
⊢ P false
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option backward.defeqAttrib.useBackward true in
|
||||
example (x : Nat) : P (id x.succ.succ).isZero := by
|
||||
dsimp [Nat.isZero.eq_2]
|
||||
trace_state
|
||||
|
|
|
|||
|
|
@ -8,8 +8,8 @@ def nonrecfun : Bool → Nat
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
|
||||
@[defeq] theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
|
||||
@[backward_defeq] theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
|
||||
@[backward_defeq] theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
|
||||
-/
|
||||
#guard_msgs in
|
||||
#print equations nonrecfun
|
||||
|
|
@ -25,7 +25,7 @@ def nonrecfun : Bool → Nat
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool),
|
||||
@[backward_defeq] theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool),
|
||||
nonrecfun x =
|
||||
match x with
|
||||
| false => 0
|
||||
|
|
@ -47,8 +47,8 @@ set_option backward.eqns.nonrecursive false
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
|
||||
@[defeq] theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
|
||||
@[backward_defeq] theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
|
||||
@[backward_defeq] theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
|
||||
-/
|
||||
#guard_msgs in
|
||||
#print equations nonrecfun
|
||||
|
|
|
|||
|
|
@ -10,9 +10,9 @@ termination_by x
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem f.eq_1 : f 0 = 1
|
||||
@[defeq] theorem f.eq_2 : f 100 = 2
|
||||
@[defeq] theorem f.eq_3 : f 1000 = 3
|
||||
@[backward_defeq] theorem f.eq_1 : f 0 = 1
|
||||
@[backward_defeq] theorem f.eq_2 : f 100 = 2
|
||||
@[backward_defeq] theorem f.eq_3 : f 1000 = 3
|
||||
theorem f.eq_4 : ∀ (x_2 : Nat), (x_2 = 99 → False) → (x_2 = 999 → False) → f x_2.succ = f x_2
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
|
|
@ -27,9 +27,9 @@ def g (x : Nat) : Nat :=
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem g.eq_1 : g 0 = 1
|
||||
@[defeq] theorem g.eq_2 : g 100 = 2
|
||||
@[defeq] theorem g.eq_3 : g 1000 = 3
|
||||
@[backward_defeq] theorem g.eq_1 : g 0 = 1
|
||||
@[backward_defeq] theorem g.eq_2 : g 100 = 2
|
||||
@[backward_defeq] theorem g.eq_3 : g 1000 = 3
|
||||
theorem g.eq_4 : ∀ (x_2 : Nat), (x_2 = 99 → False) → (x_2 = 999 → False) → g x_2.succ = x_2
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
|
|
|
|||
|
|
@ -12,12 +12,12 @@ def replace (f : N → Option N) (t : N) : N :=
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem replace.eq_1 : ∀ (f : N → Option N),
|
||||
@[backward_defeq] theorem replace.eq_1 : ∀ (f : N → Option N),
|
||||
replace f N.zero =
|
||||
match f N.zero with
|
||||
| some u => u
|
||||
| none => N.zero
|
||||
@[defeq] theorem replace.eq_2 : ∀ (f : N → Option N) (t' : N),
|
||||
@[backward_defeq] theorem replace.eq_2 : ∀ (f : N → Option N) (t' : N),
|
||||
replace f t'.succ =
|
||||
match f t'.succ with
|
||||
| some u => u
|
||||
|
|
@ -36,12 +36,12 @@ def replace2 (f : N → Option N) (t1 t2 : N) : N :=
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem replace2.eq_1 : ∀ (f : N → Option N) (t1 : N),
|
||||
@[backward_defeq] theorem replace2.eq_1 : ∀ (f : N → Option N) (t1 : N),
|
||||
replace2 f t1 N.zero =
|
||||
match f t1 with
|
||||
| some u => u
|
||||
| none => N.zero
|
||||
@[defeq] theorem replace2.eq_2 : ∀ (f : N → Option N) (t1 t' : N),
|
||||
@[backward_defeq] theorem replace2.eq_2 : ∀ (f : N → Option N) (t1 t' : N),
|
||||
replace2 f t1 t'.succ =
|
||||
match f t1 with
|
||||
| some u => u
|
||||
|
|
|
|||
|
|
@ -99,9 +99,9 @@ def del [Ord α] (d : α) : Raw α → Raw α
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem Raw.del.eq_1.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α), del d nil = nil
|
||||
@[defeq] theorem Raw.del.eq_2.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color) (left_1 : Raw α)
|
||||
(data : α) (right left_3 : Raw α) (data_1 : α) (right_1 : Raw α),
|
||||
@[backward_defeq] theorem Raw.del.eq_1.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α), del d nil = nil
|
||||
@[backward_defeq] theorem Raw.del.eq_2.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color)
|
||||
(left_1 : Raw α) (data : α) (right left_3 : Raw α) (data_1 : α) (right_1 : Raw α),
|
||||
del d ((left_1.node data Color.black right).node d_1 color (left_3.node data_1 Color.black right_1)) =
|
||||
match compare d d_1 with
|
||||
| Ordering.lt => baldL d_1 (del d (left_1.node data Color.black right)) (left_3.node data_1 Color.black right_1)
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
|
||||
@[defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
|
||||
@[backward_defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
|
||||
@[backward_defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
|
||||
(a :: as).append x = a :: as.append x
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
@ -9,8 +9,8 @@ info: equations:
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
|
||||
@[defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
|
||||
@[backward_defeq] theorem List.append.eq_1.{u_1} : ∀ {α : Type u_1} (x : List α), [].append x = x
|
||||
@[backward_defeq] theorem List.append.eq_2.{u_1} : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α),
|
||||
(a :: as).append x = a :: as.append x
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ where
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
|
||||
@[backward_defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
|
||||
(hk_2 : i.natAbs ≤ k_2 + 1),
|
||||
trailingZeros.aux k_2.succ i hi hk_2 acc = if h : i % 2 = 0 then trailingZeros.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
|
||||
-/
|
||||
|
|
@ -55,10 +55,11 @@ where
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem trailingZeros2.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
|
||||
@[backward_defeq] theorem trailingZeros2.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat)
|
||||
(hk_2 : i.natAbs ≤ k_2 + 1),
|
||||
trailingZeros2.aux k_2.succ i hi hk_2 acc =
|
||||
if h : i % 2 = 0 then trailingZeros2.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
|
||||
@[defeq] theorem trailingZeros2.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
|
||||
@[backward_defeq] theorem trailingZeros2.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
|
||||
trailingZeros2.aux 0 i hi hk_2 acc = acc
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@ def RTree.simple_size : RTree α → Nat
|
|||
| .node _x t _ts => 1 + (t true).simple_size + (t false).simple_size
|
||||
|
||||
/--
|
||||
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 :=
|
||||
info: @[backward_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
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
@ -51,7 +51,7 @@ def RTree.aux_size : List (RTree α) → Nat
|
|||
end
|
||||
|
||||
/--
|
||||
info: @[defeq] theorem RTree.aux_size.eq_2.{u_1} : ∀ {α : Type u_1} (t : RTree α) (ts : List (RTree α)),
|
||||
info: @[backward_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,7 +67,7 @@ def RTree.map_aux (f : α → β) : List (RTree α) → List (RTree β)
|
|||
end
|
||||
|
||||
/--
|
||||
info: @[defeq] theorem RTree.map_aux.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : RTree α)
|
||||
info: @[backward_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))
|
||||
-/
|
||||
|
|
@ -95,7 +95,7 @@ def VTree.vec_size : Vec (VTree α true 5) n b → Nat
|
|||
end
|
||||
|
||||
/--
|
||||
info: @[defeq] theorem VTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (b_2 : Bool) (n_2 : Nat) (a : α)
|
||||
info: @[backward_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
|
||||
|
|
|
|||
|
|
@ -4,8 +4,9 @@ def Option_map (f : α → β) : Option α → Option β
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[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 : α),
|
||||
@[backward_defeq] theorem Option_map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
|
||||
Option_map f none = none
|
||||
@[backward_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
|
||||
|
|
|
|||
|
|
@ -88,9 +88,9 @@ termination_by structural n => n
|
|||
|
||||
/--
|
||||
info: equations:
|
||||
@[defeq] theorem Structural.foo.eq_1 : foo 0 0 = 0
|
||||
@[backward_defeq] theorem Structural.foo.eq_1 : foo 0 0 = 0
|
||||
theorem Structural.foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x
|
||||
@[defeq] theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
|
||||
@[backward_defeq] theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
|
||||
-/
|
||||
#guard_msgs in
|
||||
#print equations foo
|
||||
|
|
|
|||
|
|
@ -227,19 +227,19 @@ public def f.eq_def := 1
|
|||
#guard_msgs in
|
||||
public def fexp.eq_def := 1
|
||||
|
||||
/-- info: @[defeq] private theorem f.eq_def : f = 1 -/
|
||||
/-- info: @[backward_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 -/
|
||||
/-- info: @[backward_defeq] private theorem f.eq_unfold : f = 1 -/
|
||||
#guard_msgs in #print sig f.eq_unfold
|
||||
|
||||
/-- info: @[defeq] theorem fexp.eq_def : fexp = 1 -/
|
||||
/-- info: @[backward_defeq] theorem fexp.eq_def : fexp = 1 -/
|
||||
#guard_msgs in #print sig fexp.eq_def
|
||||
|
||||
/-- info: @[defeq] theorem fexp.eq_unfold : fexp = 1 -/
|
||||
/-- info: @[backward_defeq] theorem fexp.eq_unfold : fexp = 1 -/
|
||||
#guard_msgs in #print sig fexp.eq_unfold
|
||||
|
||||
/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
|
||||
/-- info: @[backward_defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
|
||||
#guard_msgs in #print sig f_struct.eq_1
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -51,13 +51,13 @@ 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 -/
|
||||
/-- info: @[backward_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 -/
|
||||
/-- info: @[backward_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 -/
|
||||
/-- info: @[backward_defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
|
||||
#guard_msgs in #print sig f_struct.eq_1
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
import Module.Basic
|
||||
import Lean
|
||||
|
||||
/-- info: @[defeq] theorem f.eq_def : f = 1 -/
|
||||
/-- info: @[backward_defeq] theorem f.eq_def : f = 1 -/
|
||||
#guard_msgs in #print sig f.eq_def
|
||||
|
||||
/-- info: @[defeq] theorem f.eq_unfold : f = 1 -/
|
||||
/-- info: @[backward_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 -/
|
||||
/-- info: @[backward_defeq] theorem f_struct.eq_1 : f_struct 0 = 0 -/
|
||||
#guard_msgs in #print sig f_struct.eq_1
|
||||
/--
|
||||
info: theorem f_struct.eq_def : ∀ (x : Nat),
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue