diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index f8c04d6d1e23..df28711a9300 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -14,6 +14,7 @@ public import Lean.Elab.Tactic.Do.ConjunctivePre import Init.While import Init.Syntax import Lean.Meta.Sym.Simp.DiscrTree +import Lean.Meta.DiscrTree.Util public section @@ -515,6 +516,12 @@ private def etaExpandEqPattern (pattern : Sym.Pattern) (eqTy : Expr) : Sym.Patte checkTypeMask? := none } (newPattern, k) +/-- Whether some hypothesis of the equation type is an overlap hypothesis +(see `Simp.isEqnThmHypothesis`), as in the wildcard-row equation of an overlapping `match`. -/ +private def hasOverlapHypothesis : Expr → Bool + | .forallE _ d b _ => Simp.isEqnThmHypothesis d || hasOverlapHypothesis b + | _ => false + /-- Create a `SpecTheorem` from a simp/equational declaration `declName : ∀ xs, lhs = rhs`, keyed on the LHS. Function-level equations (e.g. class projection unfold lemmas) are eta-expanded so the @@ -531,29 +538,72 @@ def mkSpecTheoremFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option Sp let (pattern, etaArgs) := etaExpandEqPattern pattern eqTy return some { pattern, proof := .global declName, kind := .simp etaArgs, priority := prio } +/-- +The unfold theorem `declName.eq_def` through which a definition in a simp set's `toUnfold` +rewrites, the spec-database counterpart of `simp`'s delta unfolding. `none` for a recursive +definition, whose unconditional unfolding would not terminate. +-/ +def unfoldSpecEqn? (declName : Name) : MetaM (Option Name) := do + if (← isRecursiveDefinition declName) then return none + getUnfoldEqnFor? declName (nonRec := true) + +/-- +The spec theorems the simp entries `entries` contribute, the single place a `vcgen [...]` argument or +an `attribute [spec] f` definition (through `mkSimpEntryOfDeclToUnfold`) turns into specs: +- each `.thm` entry, keyed on its left-hand side (`mkSpecTheoremFromSimpDecl?`) at `prio`, skipping + wildcard-row equations guarded by an overlap hypothesis (as a spec such an equation matches any + call and strands the hypothesis as a verification condition), +- each `.toUnfold` definition through its unfold theorem `f.eq_def` (`unfoldSpecEqn?`) at priority + `0`, below every equation, so a call with an opaque discriminant still rewrites to the underlying + `match` expression, which `vcgen` then splits. +A single malformed entry is traced and skipped rather than aborting the set. +-/ +def simpSpecTheorems (entries : Array SimpEntry) (prio : Nat) : MetaM (Array SpecTheorem) := do + let mut result := #[] + for entry in entries do + match entry with + | .thm thm => + if let .decl declName .. := thm.origin then + try + if hasOverlapHypothesis (← getConstInfo declName).type then + trace[Elab.Tactic.Do.specAttr] "Skipping overlap-hypothesis equation {declName}" + else if let some spec ← mkSpecTheoremFromSimpDecl? declName prio then + result := result.push spec + catch e => + trace[Elab.Tactic.Do.specAttr] "Failed to add simp spec {declName}: {e.toMessageData}" + | .toUnfold declName => + try + if let some eqDef ← unfoldSpecEqn? declName then + if let some spec ← mkSpecTheoremFromSimpDecl? eqDef 0 then + result := result.push spec + catch e => + trace[Elab.Tactic.Do.specAttr] "Failed to add unfold spec {declName}: {e.toMessageData}" + | .toUnfoldThms .. => pure () + return result + /-- Register the equational lemmas of a `@[spec]`-annotated declaration as `.simp` entries with the -given priority. An equational proposition is registered directly; a definition is registered via its -equation lemmas (`getEqnsFor?`). Anything else throws, since it cannot serve as a `vcgen` spec. +given priority. An equational proposition is registered directly; a definition is registered via the +specs its simp entries contribute (`simpSpecTheorems`). Anything else throws, since it cannot serve as +a `vcgen` spec. -/ def SpecExtension.addSimpSpecTheoremsFromConst (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit := do - let add (declName : Name) : MetaM Unit := do - if let some thm ← mkSpecTheoremFromSimpDecl? declName prio then - ext.add thm attrKind let info ← getConstInfo declName if (← isProp info.type) then - add declName - else if let some eqns ← getEqnsFor? declName then - eqns.forM add + if let some thm ← mkSpecTheoremFromSimpDecl? declName prio then + ext.add thm attrKind + else if info.isDefinition then + for thm in ← simpSpecTheorems (← mkSimpEntryOfDeclToUnfold declName) prio do + ext.add thm attrKind else throwError "'{declName}' is neither an equational theorem nor a definition with unfold equations" /-- The spec proofs a `@[spec]` constant contributes to the database: the constant itself for a -`Triple`/`⊑ wp` spec, the equation itself for an equational spec, or its equation lemmas for a -definition registered to unfold. Mirrors `addSimpSpecTheoremsFromConst` so `[-foo]` erases exactly -the entries that annotating `foo` inserted. +`Triple`/`⊑ wp` spec, the equation itself for an equational spec, or the specs its simp set +contributes for a definition registered to unfold. Mirrors `addSimpSpecTheoremsFromConst` so `[-foo]` +erases exactly the entries that annotating `foo` inserted. -/ def specEraseProofs (declName : Name) : MetaM (Array SpecProof) := do if (← mkSpecTheoremFromConst declName).isSome then @@ -561,8 +611,8 @@ def specEraseProofs (declName : Name) : MetaM (Array SpecProof) := do let info ← getConstInfo declName if (← isProp info.type) then return #[.global declName] - else if let some eqns ← getEqnsFor? declName then - return eqns.map (.global ·) + else if info.isDefinition then + return (← simpSpecTheorems (← mkSimpEntryOfDeclToUnfold declName) (eval_prio default)).map (·.proof) else return #[] diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean index 00ec58cd486f..e6fd0a1f7f4d 100644 --- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean +++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean @@ -116,7 +116,7 @@ public def mkContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg := false) specThms := specThms.insert thm catch _ => continue let backwardRules ← VCGen.mkBackwardRules - let allSpecThms ← extendWithSimpSpecs specThms simpThms + let allSpecThms ← addSimpSpecs specThms simpThms let ctx : VCGen.Context := { backwardRules } return (ctx, { specs := allSpecThms }) diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean index b774ffb8b602..3268d12f7932 100644 --- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean +++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean @@ -18,8 +18,8 @@ open Lean Meta Elab Tactic Sym Spec-theorem database used by `vcgen`. The `@[spec]` attribute already stores `Std.Internal.Do` specs as pattern-keyed `SpecTheorem`s (see `Lean.Elab.Tactic.Do.Attr`); this module adds the operations the VC generator needs on top: instantiating a spec to -`pre ⊑ wp …` form, migrating the equational lemmas registered through the `mvcgen_simp` -side of `@[spec]` into the same database, and looking up the specs matching a program. +`pre ⊑ wp …` form, folding a `vcgen [...]` call's simp-style arguments into the same +database, and looking up the specs matching a program. -/ namespace Lean.Elab.Tactic.Do.Internal @@ -79,16 +79,13 @@ public def SpecAttr.SpecTheorem.global? (specThm : SpecTheorem) : Option Name := namespace VCGen /-- -Extend the `@[spec]` database with the equational lemmas registered through the `mvcgen_simp` -side of `@[spec]`: -- simp theorem declarations registered directly as `@[spec]`, -- unfold entries registered with `attribute [spec] foo`, using stored equation lemmas when - available and falling back to `Meta.getEqnsFor?`. +Extend the spec `database` with the specs a `vcgen [...]` call's simp-style arguments contribute +(`simpSpecTheorems` over the `simpThms` that `mkSimpContext` collected). Hoare triple and `⊑ wp` specs are already in `database`: the attribute stores them pattern-keyed at annotation time. -/ -public def extendWithSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorems) : +public def addSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorems) : MetaM SpecTheorems := do let mut specs := database.specs -- Erased entries are still inserted into `specs` below; `findSpecs` filters them out @@ -97,28 +94,16 @@ public def extendWithSimpSpecs (database : SpecTheorems) (simpThms : SimpTheorem match SpecProof.ofOrigin o with | some p => acc.insert p | none => acc - -- Add simp spec theorems (equational lemmas registered via `@[spec]`) - for simpThm in simpThms.post.values do - if let .decl declName .. := simpThm.origin then - try - if let some newSpec ← mkSpecTheoremFromSimpDecl? declName simpThm.priority then - specs := Sym.insertPattern specs newSpec.pattern newSpec - catch e => - trace[Elab.Tactic.Do.vcgen] "Failed to add simp spec {declName}: {e.toMessageData}" - -- Add definitions to unfold (registered via `attribute [spec] foo`) - for declName in simpThms.toUnfold.toList do - let eqThms ← match simpThms.toUnfoldThms.find? declName with - | some eqThms => pure eqThms - | none => - -- No explicit equational theorems stored; generate them via `getEqnsFor?` - let some eqThms ← Meta.getEqnsFor? declName | continue - pure eqThms - for eqThm in eqThms do - try - if let some newSpec ← mkSpecTheoremFromSimpDecl? eqThm (prio := eval_prio default) then - specs := Sym.insertPattern specs newSpec.pattern newSpec - catch e => - trace[Elab.Tactic.Do.vcgen] "Failed to add unfold spec {declName}/{eqThm}: {e.toMessageData}" + -- Only post-rewrite simp lemmas become specs, so a `↓`-marked (pre-rewrite) argument is dropped. + for simpThm in simpThms.pre.values do + logWarning m!"`vcgen` uses only post-rewrite simp lemmas as specs; ignoring the pre-rewrite \ + lemma `{simpThm.origin.key}`." + -- `mkSimpContext` splits a bracketed definition into its equations (in `post`) and a `toUnfold` + -- entry; feed both back to `simpSpecTheorems` as the `SimpEntry`s the definition would produce. + let entries := simpThms.post.values.map (SimpEntry.thm ·) + ++ simpThms.toUnfold.toList.toArray.map (SimpEntry.toUnfold ·) + for newSpec in ← simpSpecTheorems entries (eval_prio default) do + specs := Sym.insertPattern specs newSpec.pattern newSpec return { specs, erased } end VCGen diff --git a/tests/elab/vcgenUnfoldMatchDef.lean b/tests/elab/vcgenUnfoldMatchDef.lean new file mode 100644 index 000000000000..0db098816ac9 --- /dev/null +++ b/tests/elab/vcgenUnfoldMatchDef.lean @@ -0,0 +1,78 @@ +import Std.Tactic.Do +import Std.Internal.Do + +/-! +Test for `vcgen [f]` where `f` is defined by a root `match` on its arguments. With an opaque +discriminant the constructor equations cannot rewrite the call, so the unfold theorem `f.eq_def` +rewrites it to the `match` expression and `vcgen` splits it, mirroring `simp`'s unfolding of +non-recursive definitions. The wildcard-row equation of an overlapping `match` must not be used +as a spec: it matches any call and would strand its overlap hypothesis as an unprovable +verification condition. +-/ + +set_option mvcgen.warning false + +def dep (n : Option Nat) : Id Nat := + match n with | some y => pure (y + 1) | none => pure 2 + +/-- Overlapping wildcard row: its equation is guarded by an overlap hypothesis. -/ +def wild (n m : Option Nat) : Id Nat := + match n, m with + | some y, some z => pure (y + z + 1) + | _, _ => pure 1 + +/-- Reducible: `mkSimpEntryOfDeclToUnfold` yields no equations for it, so it contributes only its +unfold theorem, matching `simp`'s delta unfolding of reducible definitions. -/ +@[reducible] def red (n : Option Nat) : Id Nat := + match n with | some y => pure (y + 1) | none => pure 2 + +/-- Recursive: no `eq_def` fallback, so an opaque discriminant still reports a missing spec +instead of unfolding indefinitely. -/ +def recf (n : Nat) : Id Nat := + match n with | 0 => pure 1 | n + 1 => recf n + +section +open Lean.Order Std.Internal.Do + +example (n : Option Nat) : ⦃ True ⦄ dep n ⦃ fun r => r > 0 ⦄ := by + vcgen [dep] with finish + +-- A concrete discriminant is rewritten by the constructor equation directly. +example : ⦃ True ⦄ dep (some 5) ⦃ fun r => r = 6 ⦄ := by + vcgen [dep] with finish + +example (n m : Option Nat) : ⦃ True ⦄ wild n m ⦃ fun r => r > 0 ⦄ := by + vcgen [wild] with finish + +example (n : Option Nat) : ⦃ True ⦄ red n ⦃ fun r => r > 0 ⦄ := by + vcgen [red] with finish + +-- The global attribute goes through the same registration. +attribute [local spec] wild in +example (n m : Option Nat) : ⦃ True ⦄ wild n m ⦃ fun r => r > 0 ⦄ := by + vcgen with finish + +/-- +error: Failed to apply rule SpecProof.global recf.eq_2 for + recf n +target: + ⊤ ⊑ wp (recf n) (LT.lt 0) ⊥ +Pred: + Prop +excessArgs: [] +rule type: + ∀ (Pre : Prop) (n_2 : Nat) (Q : Nat → Prop) (E : EPost⟨⟩), Pre ⊑ wp (recf n_2) Q E → Pre ⊑ wp (recf n_2.succ) Q E +-/ +#guard_msgs (whitespace := lax) in +example (n : Nat) : ⦃ True ⦄ recf n ⦃ fun r => r > 0 ⦄ := by + vcgen [recf] with finish + +-- Only post-rewrite simp lemmas become specs; a `↓` (pre-rewrite) argument is ignored with a warning. +@[simp] theorem two_eq : (1 + 1 : Nat) = 2 := rfl + +/-- warning: `vcgen` uses only post-rewrite simp lemmas as specs; ignoring the pre-rewrite lemma `two_eq`. -/ +#guard_msgs in +example (n : Option Nat) : ⦃ True ⦄ dep n ⦃ fun r => r > 0 ⦄ := by + vcgen [dep, ↓ two_eq] with finish + +end