Documentation

GeneralizationLinter.Core.Recompile

Recompile #

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.

inductive GeneralizationLinter.WeakeningGrade :

Some weakenings may be genuine weakenings, but require modifications in the value's (i.e., proof term's) source code. We "grade" these weakenings as needsModification. We grade weakenings that don't require any such modification as proofIntact.

proofIntact : WeakeningGrade
needsModification : WeakeningGrade
unverified : WeakeningGrade

Instances For

@[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 x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

inductive GeneralizationLinter.WrapperClassification :

replayable : WrapperClassification
"Declaration wrappers" that we can and should "replay", because they may affect our linter's verdict. These are open … in and set_option … in commands.
ignorable : WrapperClassification
"Declaration wrappers" that we can ignore, because they don't affect our linter's verdict. These are include … in commands, and omit … in commands that don't contain any Term.hole or Term.syntheticHole within them. #TODO: More details on why.
refused : WrapperClassification
"Declaration wrappers" that we cannot replay, and which may affect our linter's verdict. When a declaration is wrapped with one or more of these kinds of wrappers, we skip it. Any wrappers that are not .replayable or .ignorable are treated as .refused.

Instances For

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedWrapperClassification :

Inhabited WrapperClassification

Equations

GeneralizationLinter.instInhabitedWrapperClassification = { default := GeneralizationLinter.instInhabitedWrapperClassification.default }

@[implicit_reducible]

instance GeneralizationLinter.instBEqWrapperClassification :

BEq WrapperClassification

Equations

GeneralizationLinter.instBEqWrapperClassification = { beq := GeneralizationLinter.instBEqWrapperClassification.beq }

def GeneralizationLinter.instBEqWrapperClassification.beq :

WrapperClassification → WrapperClassification → Bool

Equations

GeneralizationLinter.instBEqWrapperClassification.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def GeneralizationLinter.lemmaKind :

Lean.SyntaxNodeKind

lemma is a Mathlib macro that the elaborator expands to theorem. However, pre-elaboration, its SyntaxNodeKind is `lemma, while the pre-elaboration SyntaxNodeKind of all other declarations that the linter may analize is Parser.Command.declaration.

Equations

GeneralizationLinter.lemmaKind = `lemma

Instances For

def GeneralizationLinter.classifyWrapper (w : Lean.Syntax) :

WrapperClassification

Classify "wrappers"

Equations

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

Instances For

partial def GeneralizationLinter.peelWrappers? (stx : Lean.Syntax) (wrappers : Array Lean.Syntax := #[]) :

Option (Array Lean.Syntax × Lean.Syntax)

Peel any open … in, set_option … in, and "hole-less" omit … in … "wrappers" off of the main declaration. For example, if stx was

open Nat in
set_option pp.all true in
omit [Monoid M] in
@[instance] theorem something : … := …

then calling peelWrappers? stx would return some (#[‹open Nat›, ‹set_option pp.all›], ‹@[instance] lemma something : … := …›). (Note that the omit [Monoid M] in wrapper is not among those returned; this is because #TODO)

If the declaration includes any other wrappers (omit … in … with holes, attribute … in …, include … in …, etc.), return none. This is because peelWrappers?'s output is passed on to rewrapTerm to get rewrapped into a term instead of a command or declaration (which would be much harder to deal with further down the line), and only open and set_option are the only wrappers of this kind that are available in Parser.Command.Term.

There's <2000 declarations in Mathlib v4.32.0 that use wrappers that lead peelWrappers? to return none (which in turn prevents the linter from being able to emit any suggestions).

Example

Suppose we have the following declaration:

open Nat in
@[instance] theorem t : True := trivial

The corresponding Syntax tree is:

`Lean.Parser.Command.in`
├─ `Lean.Parser.Command.open`                             ─┐
│  ├─ `atom "open"`                                        │ `wrappers[0]`
│  └─ `Lean.Parser.Command.openSimple`                     │
│     └─ `null` (many1 ident)                              │
│        └─ `ident Nat`                                   ─┘
├─ `atom "in"`
└─ `Lean.Parser.Command.declaration`                      ─┐
   ├─ `Lean.Parser.Command.declModifiers`                  │ `decl`
   │  ├─ `null` (optional docComment)                      │
   │  ├─ `null` (optional attributes)                      │
   │  │  └─ `Lean.Parser.Term.attributes`                  │
   │  │     ├─ `atom "@["`                                 │
   │  │     ├─ `null` (sepBy1 attrInstance)                │
   │  │     │  └─ `Lean.Parser.Term.attrInstance`          │
   │  │     │     ├─ `Lean.Parser.Term.attrKind`           │
   │  │     │     │  └─ `null` (optional scoped / local)   │
   │  │     │     └─ `Lean.Parser.Attr.instance`           │
   │  │     │        ├─ `atom "instance"`                  │
   │  │     │        └─ `null` (optional priority)         │
   │  │     └─ `atom "]"`                                  │
   │  ├─ `null` (optional visibility)                      │
   │  ├─ `null` (optional protected)                       │
   │  ├─ `null` (optional meta / noncomputable)            │
   │  ├─ `null` (optional unsafe)                          │
   │  └─ `null` (optional partial / nonrec)                │
   └─ `Lean.Parser.Command.theorem`                        │
      ├─ `atom "theorem"`                                  │
      ├─ `Lean.Parser.Command.declId`                      │
      │  ├─ `ident t`                                      │
      │  └─ `null` (optional universe binders)             │
      ├─ `Lean.Parser.Command.declSig`                     │
      │  ├─ `null` (many binder)                           │
      │  └─ `Lean.Parser.Term.typeSpec`                    │
      │     ├─ `atom ":"`                                  │
      │     └─ `ident True`                                │
      └─ `Lean.Parser.Command.declValSimple`               │
         ├─ `atom ":="`                                    │
         ├─ `ident trivial`                                │
         ├─ `Lean.Parser.Termination.suffix`               │
         │  ├─ `null` (optional terminationBy / fixpoint)  │
         │  └─ `null` (optional decreasingBy)              │
         └─ `null` (optional whereDecls)                  ─┘

(See Lean/Parser/Command.lean, Lean/Parser/Term.lean, and Lean/Parser/Attr.lean for more information on the parentheticals in the tree above.)

So peelWrappers would return some (wrappers, decl), where wrappers and decl are as indicated above.

def GeneralizationLinter.bodyTermOfDeclVal? (dval : Lean.Syntax) (wrapped : Bool) :

Lean.Elab.TermElabM (Option Lean.Syntax)

Given the syntax tree declVal of a declaration, return the value as a term syntax tree. In the case of theorems, this value corresponds to the proof term.

Implementation notes

Argument positions of relevant SyntaxNodeKind can be seen in the following code block, adapted by us from code from Lean/Parser/Command.lean:

def declValSimple    := leading_parser
  " :=" >>                      -- dval[0]
  ppHardLineUnlessUngrouped >>  -- pretty-printer stuff
  declBody >>                   -- dval[1]
  Termination.suffix >>         -- dval[2]
  optional Term.whereDecls      -- dval[3]

def whereStructInst  := leading_parser
  ppIndent ppSpace >>       -- pretty-printer stuff
  "where" >>                -- dval[0]
  -- ↓ dval[1]
  Term.structInstFields (sepByIndent Term.structInstField "; " (allowTrailingSep := true)) >>
  optional Term.whereDecls  -- dval[2]

Example

For the example from peelWrappers?, bodyTermOfDeclVal? returns the following syntax tree:

`ident trivial`

Equations

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

Instances For

def GeneralizationLinter.rewrapTerm (wrappers : Array Lean.Syntax) (stx : Lean.Syntax) :

Example

Continuing the example from peelWrappers?, we have that rewrapTerm would combine the single wrapper in wrappers

`Lean.Parser.Command.open`
├─ `atom "open"`
└─ `Lean.Parser.Command.openSimple`
    └─ `null` (many1 ident)
      └─ `ident Nat`

with the bodyTermOfDeclVal? output stx

`ident trivial`

into the Syntax tree

`Lean.Parser.Term.open`
├─ `atom "open"`
├─ `Lean.Parser.Command.openSimple`
│  └─ `null` (many1 ident)
│     └─ `ident Nat`
├─ `atom "in"`
└─ `ident trivial`

Equations

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

Instances For

def GeneralizationLinter.foldSetOptionWrappers? {m : Type → Type} [Monad m] (wrappers : Array Lean.Syntax) (init : Lean.Options) (elabOne : Lean.Options → Lean.Syntax → m (Option Lean.Options)) :

m (Option Lean.Options)

Applies set_option wrappers to init using elabOne and returns the result.

Implementation notes

An Options value is essentially just a map: Options.map : NameMap DataValue from Name of options (e.g., `pp.raw in set_option pp.raw true) to DataValues (e.g., ofBool true in set_option pp.raw true). foldSetOptionWrappers? just "applies" the set_option commands among wrappers to init : Options using elabOne and returns the result, or none if elabOne returned none at any point.

Equations

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

Instances For

partial def GeneralizationLinter.collectNodes (kind : Lean.SyntaxNodeKind) :

Lean.Syntax → Array Lean.Syntax

Returns all child nodes of kind kind.

def GeneralizationLinter.declValNodes (stx : Lean.Syntax) :

Array Lean.Syntax

Returns the "value" nodes of stx, i.e., the := … node (Parser.Command.declValSimple) and optional where … node (Parser.Command.whereStructInst).

See implementation notes of bodyTermOfDeclVal? for more info.

Equations

GeneralizationLinter.declValNodes stx = GeneralizationLinter.collectNodes `Lean.Parser.Command.declValSimple stx ++ GeneralizationLinter.collectNodes `Lean.Parser.Command.whereStructInst stx

Instances For

def GeneralizationLinter.recompiledAgainst? (W : Lean.Expr) (bodyStx : Lean.Syntax) :

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 (bodyStx, 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.

Instances For

def GeneralizationLinter.recompiledVal? (const : Lean.ConstantInfo) (bodyStx : Lean.Syntax) (ws : Array (Nat × Array Vertex)) :

Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr))

#TODO

Equations

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

Instances For

def GeneralizationLinter.recompileHolds (const : Lean.ConstantInfo) (bodyStx : Lean.Syntax) (ws : Array (Nat × Array Vertex)) :

Lean.Elab.TermElabM Bool

Wrapper around recompiledVal?; returns true iff #TODO

Equations

GeneralizationLinter.recompileHolds const bodyStx ws = do let __do_lift ← GeneralizationLinter.recompiledVal? const bodyStx ws pure __do_lift.isSome

Instances For

structure GeneralizationLinter.GradedWeakening :

candidate : Candidate
grade : WeakeningGrade

Instances For

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedGradedWeakening :

Inhabited GradedWeakening

Equations

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

def GeneralizationLinter.gradedWeakenings (cfg : LinterConfig) (graph : ClassGraph) (const : Lean.ConstantInfo) (bodyStx : Lean.Syntax) :

Lean.Elab.TermElabM (Array GradedWeakening)

Given a declaration with constant into const and value source code bodyStx (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.

Instances For