Verification

This module concerns itself with elaborating a weakened term (usually the proof term of a theorem) and type-checking the result against some expected type (usually the conclusion of a theorem). This is used to verify a weakening candidate before it is ever suggested. The goal is to never emit a single false positive, i.e., an erroneous suggestion.

def GeneralizationLinter.suppressingDiagnostics {m : Type → Type} {α : Type} [Monad m] [MonadFinally m] [Lean.MonadWithOptions m] [MonadLiftT Lean.CoreM m] (act : m α) : m α

Run act quietly. When we run a verification gate, candidates that are rejected would emit errors that we don't want to bother the user with.

---

Implementation notes

We turn off Elab.async because asynchronicity would make it impossible for us to ensure we capture the emitted messages.

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.weakenedImpliesOriginal (W origType : Lean.Expr) : Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.stillAdmissibleInstance (declName : Lean.Name) (W : Lean.Expr) (levelParams : List Lean.Name) : Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.weakeningHolds (declInfo : Lean.ConstantInfo) (c : Candidate) : Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.guardedCandidates (config : LinterConfig) (G : ClassGraph) (declInfo : Lean.ConstantInfo) : Lean.MetaM (Array Candidate)

Returns weakening suggestion candidates for a given declaration. These are unverified, except that, when config.redundancyGuard and config.verify are both set, candidates reshaped into drops by reshapeRedundantToDrops have been verified (and removed if they failed).

Equations

• One or more equations did not get rendered due to their size.

Recompile

structure GeneralizationLinter.SourceIntact : Type

• binders : Bool

  true if no other binder mentions the weakened binder by name, false if one does. Note that this is a syntactic scan (bindersMention), not a re-elaboration: it does not see a binder whose type the elaborator filled in from the weakened one.

• concl : Bool

  true if the declaration's conclusion would not have to be modified after applying the weakening, false if it might. A false records only a failure to confirm: re-elaboration failed, or the conclusion's source syntax was unavailable.

• body : Bool

  true if the declaration's body (i.e., value) wouldn't have to be modified after applying the weakening, false if it might. As for concl, a false is only a failure to confirm.

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedSourceIntact : Inhabited SourceIntact

Equations

• GeneralizationLinter.instInhabitedSourceIntact = { default := GeneralizationLinter.instInhabitedSourceIntact.default }

def GeneralizationLinter.instBEqSourceIntact.beq : SourceIntact → SourceIntact → Bool

Equations

• GeneralizationLinter.instBEqSourceIntact.beq { binders := a, concl := a_1, body := a_2 } { binders := b, concl := b_1, body := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• GeneralizationLinter.instBEqSourceIntact.beq x✝¹ x✝ = false

@[implicit_reducible]

instance GeneralizationLinter.instBEqSourceIntact : BEq SourceIntact

Equations

• GeneralizationLinter.instBEqSourceIntact = { beq := GeneralizationLinter.instBEqSourceIntact.beq }

inductive GeneralizationLinter.WeakeningGrade : Type

Some weakenings may be genuine weakenings, but require modifications in the binders', conclusion's, or value's (i.e., proof term's) source code. We specify which parts don't need modifications and which parts do (or might) in the parts argument passed to the .holds "grade".

If verification is turned off, the .unverified "grade" is assigned instead.

• holds (parts : SourceIntact) : WeakeningGrade

  Example: .holds { binders := true, concl := true, body := true } indicates that applying the weakening would require no additional modifications.

• unverified : WeakeningGrade

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedWeakeningGrade : Inhabited WeakeningGrade

Equations

• GeneralizationLinter.instInhabitedWeakeningGrade = { default := GeneralizationLinter.instInhabitedWeakeningGrade.default }

@[implicit_reducible]

instance GeneralizationLinter.instBEqWeakeningGrade : BEq WeakeningGrade

Equations

• GeneralizationLinter.instBEqWeakeningGrade = { beq := GeneralizationLinter.instBEqWeakeningGrade.beq }

def GeneralizationLinter.instBEqWeakeningGrade.beq : WeakeningGrade → WeakeningGrade → Bool

Equations

• GeneralizationLinter.instBEqWeakeningGrade.beq (GeneralizationLinter.WeakeningGrade.holds a) (GeneralizationLinter.WeakeningGrade.holds b) = (a == b)
• GeneralizationLinter.instBEqWeakeningGrade.beq GeneralizationLinter.WeakeningGrade.unverified GeneralizationLinter.WeakeningGrade.unverified = true
• GeneralizationLinter.instBEqWeakeningGrade.beq x✝¹ x✝ = false

structure GeneralizationLinter.DeclSource : Type

Source code (Syntax) of a declaration and its value.

• body : Lean.Syntax
• concl? : Option Lean.Syntax
• binders : Array Lean.Syntax

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedDeclSource : Inhabited DeclSource

Equations

• GeneralizationLinter.instInhabitedDeclSource = { default := GeneralizationLinter.instInhabitedDeclSource.default }

def GeneralizationLinter.recompiledAgainst? (W : Lean.Expr) (src : DeclSource) (levelNames : List Lean.Name := []) : Lean.Elab.TermElabM (Option Lean.Expr)

Given a weakened declaration W of the form ‹binders› : concl (where concl is the same as the original declaration's), re-elaborate the declaration's value's source code (src.body, usually corresponding to a proof term) into val and type-check that we have val : concl. Return some val if successful, or none otherwise.

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.conclSourceIntact (W : Lean.Expr) (conclStx : Lean.Syntax) (levelNames : List Lean.Name := []) : Lean.Elab.TermElabM Bool

Check that re-elaborated conclusion is definitionally equal to the old conclusion.

---

Implementation notes

forallTelescope W strips every ∀ from W, even ones that may actually belong to the conclusion of W, which we don't want. So we consult conclStx and check how many leading ∀s it has, and re-abstract precisely that number of the telescoped W's trailing binders.

For example, if the declaration's signature were [Group α] (a b : α) : ∀ (c : α), a = b → b = c → a = c and Group α got weakened to Monoid α, then W would be that signature with [Monoid α] in place of [Group α], so args would be #[α, inst, a, b, c, t₁, t₂], where inst : Monoid α, t₁ : a = b, and t₂ : b = c would in truth be dynamically-generated hygienic binder names, and shortConcl would be a = c. Meanwhile, conclStx = ‹∀ (c : α), a = b → b = c → a = c›, so it can tell us that the "real" conclusion actually has 3 leading ∀s (corresponding to c, t₁, and t₂).

Now, newConcl = ‹∀ (c : α), a = b → b = c → a = c› (note that the ‹› brackets are being used both for Syntax and Exprs). We now want to check that newConcl matches the old conclusion, but only have the shortConcl version of the old conclusion. Hence, we extract the last 3 arguments (we know it's 3 because that's how many leading ∀s conclStx has) from args (which were telescoped from W) and build a forall-expression, using them as the arguments and shortConcl as the conclusion, which yields ∀ (c : α) (t₁ : a = b) (t₂ : b = c), a = c. We then check whether this "full" old conclusion Expr is definitionally equal to newConcl, and receive a verdict that is informative to us, and not simply false because of a mismatch in ∀-arity of the expressions.

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.bindersMention (binders : Array Lean.Syntax) (name : Lean.Name) : Bool

Does any binder in binders, as source code (Syntax), mention the binder name?

---

Examples

Suppose we have

theorem foo {R M : Type*}
  [inst₁ : Ring R]
  [inst₂ : AddCommMonoid M]
  [inst₃ : @Module R M (@Ring.toSemiring R inst₁) inst₂] : … := …

The typical use case for bindersMention would be checking whether weakening [inst₁ : Ring R] to [inst₁ : Semiring R] would require the user to modify foo's other binders in any way. To check this, we would call bindersMention #[‹[inst₂ : AddCommMonoid M]›, ‹[inst₃ : @Module R M (@Ring.toSemiring R inst₁) inst₂]›] `inst₁ and get true.

Had we instead had the following

theorem foo {R M : Type*}
  [inst₁ : Ring R]
  [inst₂ : AddCommMonoid M]
  [inst₃ : Module R M] : … := …

then we'd have called bindersMention #[‹[inst₂ : AddCommMonoid M]›, ‹[inst₃ : Module R M]›] `inst₁ and gotten false.

bindersMention #[‹[inst₁ : Ring R]›] `R = true
bindersMention #[‹[inst₁ : Ring R]›] `inst₁ = false
bindersMention #[‹{R M : Type*}›] `R = false

---

Implementation notes

For reference:

[inst₃ : @Module R M (@Ring.toSemiring R inst₁) inst₂]    [Module R M]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^
`Lean.Parser.Term.instBinder`                             `Lean.Parser.Term.instBinder`
├─ [0] `atom "["`                                         ├─ [0] `atom "["`
├─ [1] `null`                                             ├─ [1] `null`
│  ├─ [0] `ident inst₃`                                   ├─ [2] `Lean.Parser.Term.app`
│  └─ [1] `atom ":"`                                      │  ├─ [0] `ident Module`
├─ [2] `Lean.Parser.Term.app`                             │  └─ [1] `null`
│  ├─ [0] `Lean.Parser.Term.explicit`                     │     ├─ [0] `ident R`
│  │  ├─ [0] `atom "@"`                                   │     └─ [1] `ident M`
│  │  └─ [1] `ident Module`                               └─ [3] `atom "]"`
│  └─ [1] `null`
│     ├─ [0] `ident R`
│     ├─ [1] `ident M`
│     ├─ [2] `Lean.Parser.Term.paren`
│     │  ├─ [0] `Lean.Parser.Term.hygienicLParen`
│     │  │  ├─ [0] `atom "("`
│     │  │  └─ [1] `hygieneInfo`
│     │  │     └─ [0] `ident [anonymous]`
│     │  ├─ [1] `Lean.Parser.Term.app`
│     │  │  ├─ [0] `Lean.Parser.Term.explicit`
│     │  │  │  ├─ [0] `atom "@"`
│     │  │  │  └─ [1] `ident Ring.toSemiring`
│     │  │  └─ [1] `null`
│     │  │     ├─ [0] `ident R`
│     │  │     └─ [1] `ident inst₁`
│     │  └─ [2] `atom ")"`
│     └─ [3] `ident inst₂`
└─ [3] `atom "]"`

Equations

• One or more equations did not get rendered due to their size.

opaque GeneralizationLinter.budgetExhaustedRef : IO.Ref Bool

Run x with maxHeartbeats set to the lesser of budget and the ambient maxHeartbeats, treating an ambient value of 0 ("unlimited") as larger than any budget. In either case x runs under withCurrHeartbeats, so it gets a fresh allowance of that many heartbeats rather than whatever is left of the ambient one.

If a runtime (or other non-interrupt) exception occurs while running x, it is caught and dflt ("default") is returned.

If budget is 0, runs x directly without any restrictions or exception handling.

---

Examples

-- ambient `maxHeartbeats 200_000`, i.e. `Core.Context.maxHeartbeats = 200_000_000`
withHeartbeatBudget 1_000 dflt x             -- `x` gets a fresh 1_000 heartbeats
withHeartbeatBudget 1_000_000_000_000 dflt x -- `x` gets a fresh 200_000_000 heartbeats
withHeartbeatBudget 0 dflt x                 -- `x` gets what is left of the ambient allowance
-- ambient `maxHeartbeats 0`
withHeartbeatBudget 1_000 dflt x             -- `x` gets a fresh 1_000 heartbeats

def GeneralizationLinter.withHeartbeatBudget {α : Type} (budget : Nat) (dflt : α) (x : Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

Equations

• One or more equations did not get rendered due to their size.

structure GeneralizationLinter.GradedWeakening : Type

• candidate : Candidate
• grade : WeakeningGrade

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedGradedWeakening : Inhabited GradedWeakening

Equations

• GeneralizationLinter.instInhabitedGradedWeakening = { default := GeneralizationLinter.instInhabitedGradedWeakening.default }

def GeneralizationLinter.gradedWeakenings (cfg : LinterConfig) (graph : ClassGraph) (const : Lean.ConstantInfo) (src : DeclSource) : Lean.Elab.TermElabM (Array GradedWeakening)

Given a declaration with constant info const and value source code src.body (as well as a linter config and class graph), return an array of verified, graded weakenings that could be applied to the declaration.

Equations

• One or more equations did not get rendered due to their size.