structure Canonical.Var : Type

A variable with a name, and whether it is proof irrelevant (unused).

• name : String
• irrelevant : Bool

instance Canonical.instInhabitedVar : Inhabited Var

Equations

• Canonical.instInhabitedVar = { default := { name := default, irrelevant := default } }

inductive Canonical.Value : Type

The value of a let declaration, which can be a term, custom reduction behavior (like recursor), or opaque.

• definition (term : Tm) : Value
• constructor (type : String) (index argsStart : USize) : Value
• recursor (type : String) (rules : Array Tm) (shared major : USize) : Value
• projection (type : String) (index major : USize) : Value
• opaque : Value

instance Canonical.instInhabitedTm : Inhabited Tm

Equations

• Canonical.instInhabitedTm = { default := { params := default, lets := default, head := default, args := default } }

instance Canonical.instInhabitedLet : Inhabited Let

Equations

• Canonical.instInhabitedLet = { default := { name := default, irrelevant := default, value := default } }

instance Canonical.instInhabitedValue : Inhabited Value

Equations

• Canonical.instInhabitedValue = { default := Canonical.Value.constructor default default default }

structure Canonical.Let : Type

A let declaration, with a name and value.

• name : String
• irrelevant : Bool
• value : Value

structure Canonical.Tm : Type

A term is an n-ary, β-normal, η-long λ expression: λ params lets . head args

• params : Array Var
• lets : Array Let
• head : String
• args : Array Tm

structure Canonical.Typ : Type

A type is an n-ary Π-type: Π params lets . codomain

• params : Array (Option Typ)
• lets : Array (Option Typ)
• codomain : Tm

instance Canonical.instInhabitedTyp : Inhabited Typ

Equations

• Canonical.instInhabitedTyp = { default := { params := default, lets := default, codomain := default } }

structure Canonical.CanonicalResult : Type

The return type of Canonical, with the generated terms.

• terms : Array Tm
• attempted_resolutions : UInt32
• successful_resolutions : UInt32
• steps : UInt32
• last_level_steps : UInt32
• branching : Float32

instance Canonical.instInhabitedCanonicalResult : Inhabited CanonicalResult

Equations

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

@[extern term_to_string]

opaque Canonical.termToString : Tm → String

instance Canonical.instToStringTm : ToString Tm

Equations

• Canonical.instToStringTm = { toString := Canonical.termToString }

@[extern typ_to_string]

opaque Canonical.typToString : Typ → String

instance Canonical.instToStringTyp : ToString Typ

Equations

• Canonical.instToStringTyp = { toString := Canonical.typToString }

@[extern canonical]

opaque Canonical.canonical : Typ → UInt64 → USize → Bool → Bool → CanonicalResult

Generate terms of a given type, with given timeout, desired count, synth and debug flags

@[extern refine]

opaque Canonical.refine : Typ → Bool → Bool

Start a server with the refinement UI on the given type.

structure Canonical.Pi (A : Type u) (B : A → Type v) : Type (max u v)

Some Lean Π-types cannot be converted into Canonical Π-types, and are instead converted into this structure.

• f (a : A) : B a

structure Canonical.HardCode : Type

define is a list of names that should be defined if this HardCode is triggered

• define : List Lean.Name

def Canonical.HARD_CODE : Std.HashMap (Lean.Name × Lean.Name) HardCode

Rather than recursively unfolding definitions, HARD_CODE overrides the definitions introduced by a given symbol.

Equations

• Canonical.HARD_CODE = Std.HashMap.ofList [((`Mathlib.Data.Real.Basic, `Real), { define := [] })]

def Canonical.getHardCode (name : Lean.Name) : Lean.CoreM (Option HardCode)

Equations

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

structure Canonical.Definition : Type

Structure for storing the type and value of let definitions.

• type : Option Typ
• irrelevant : Bool
• value : Value
• shouldReplace : Bool

@[reducible, inline]

abbrev Canonical.ToCanonicalM (α : Type) : Type

When translating to Canonical, we maintain a state of translated constant symbols.

Equations

• Canonical.ToCanonicalM = StateT (Lean.AssocList Lean.Name Canonical.Definition) Lean.MetaM

def Canonical.name : Lean.Expr → Lean.MetaM Lean.Name

For readability, we identify free variables by their userName, but with the suffix of the FVarId.name for completeness.

Equations

• Canonical.name (Lean.Expr.fvar fvarId) = do let __do_lift ← fvarId.getUserName pure (fvarId.name.updatePrefix __do_lift.getRoot)
• Canonical.name x✝ = panicWithPosWithDecl "Canonical" "Canonical.name" 108 7 "name of non-fvar"

def Canonical.nameString (e : Lean.Expr) : Lean.MetaM String

Equations

• Canonical.nameString e = do let __do_lift ← Canonical.name e pure __do_lift.toString

def Canonical.natToTerm (n : Nat) : Tm

A Tm representing a natural number.

Equations

• Canonical.natToTerm Nat.zero = { head := `Nat.zero.toString }
• Canonical.natToTerm n_2.succ = { head := `Nat.succ.toString, args := #[Canonical.natToTerm n_2] }

partial def Canonical.forallArity (e : Lean.Expr) : Lean.MetaM Nat

The default arity of a type e.

partial def Canonical.paramArities (e : Lean.Expr) : Lean.MetaM (List Nat)

The arities of the types of the parameters of type e.

def Canonical.isOpaque (info : Lean.ConstantInfo) : ToCanonicalM Bool

Equations

• One or more equations did not get rendered due to their size.
• Canonical.isOpaque (Lean.ConstantInfo.recInfo val) = do let __do_lift ← Lean.isIrreducible (Lean.ConstantInfo.recInfo val).name if __do_lift = true then pure false else pure true
• Canonical.isOpaque info = do let __do_lift ← Lean.isIrreducible info.name if __do_lift = true then pure false else pure false

def Canonical.includeLetType (expr : Lean.Expr) : ToCanonicalM Bool

Equations

• Canonical.includeLetType (fn.app arg) = (Canonical.includeLetType fn <||> Canonical.includeLetType arg)
• Canonical.includeLetType (Lean.Expr.lam binderName binderType body binderInfo) = Canonical.includeLetType body
• Canonical.includeLetType (Lean.Expr.forallE binderName binderType body binderInfo) = Canonical.includeLetType body
• Canonical.includeLetType (Lean.Expr.letE declName type value body nonDep) = Canonical.includeLetType body
• Canonical.includeLetType (Lean.Expr.mdata data body) = Canonical.includeLetType body
• Canonical.includeLetType (Lean.Expr.const declName us) = do let __do_lift ← Lean.getEnv let decl : Lean.ConstantInfo := (__do_lift.find? declName).get! Canonical.isOpaque decl
• Canonical.includeLetType expr = pure false

def Canonical.includeType (info : Lean.ConstantInfo) : ToCanonicalM Bool

Equations

• One or more equations did not get rendered due to their size.
• Canonical.includeType info = do let __do_lift ← Lean.isIrreducible info.name if __do_lift = true then pure true else pure true

partial def Canonical.defineLiteral (val : Lean.Literal) (insideLet : Nat) : ToCanonicalM String

At present, only small natural numbers are converted into a Tm. Other literals are opaque.

partial def Canonical.define (declName : Lean.Name) (insideLet : Nat) (force : Bool := false) : ToCanonicalM Lean.ConstantInfo

Insert declName into the ToCanonicalM definitions, with the correct type and value.

partial def Canonical.toTyp (e : Lean.Expr) (insideLet : Nat) (params : List Var := []) (paramTypes defTypes : List (Option Typ) := []) (defs : List Let := []) (args : List Lean.Expr := []) : ToCanonicalM Typ

Translate an Expr into a Typ, by collecting the forallE bindings and app arguments until a head symbol is reached.

partial def Canonical.toBody (ty : Lean.Expr) (params : List Var) (defs : List Let) (head : String) (args : List Lean.Expr) (insideLet : Nat) (arity : List Nat) (state : Array Tm := #[]) (typeArgs : List Lean.Expr := []) : ToCanonicalM Tm

When we reach the head symbol, we call toBody with its type and paramArities. This function is responsible for recursively tranlating the arguments and building the resultant Tm.

partial def Canonical.toTerm (term type : Lean.Expr) (insideLet arity : Nat) (params : List Var := []) (defs : List Let := []) (args typeArgs : List Lean.Expr := []) : ToCanonicalM Tm

Transalate an Expr to a Tm, by collecting the lam bindings and app arguments until a head symbol is reached.

def Canonical.toCanonical (e : Lean.Expr) (consts : List Lean.Syntax) (pi : Bool) : ToCanonicalM Typ

Converts an Expr e into a Canonical Typ, complete with Definitions in the lets.

Equations

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

@[reducible, inline]

abbrev Canonical.FromCanonicalM (α : Type) : Type

When translating from Canonical, we associate names in the Tm with corresponding Lean FVarIds

Equations

• Canonical.FromCanonicalM = StateT (Lean.AssocList String Lean.FVarId) Lean.MetaM

def Canonical.mvarLevels (n : Nat) : FromCanonicalM (List Lean.Level)

Create n fresh LevelMVars.

Equations

• Canonical.mvarLevels Nat.zero = pure []
• Canonical.mvarLevels n_2.succ = do let fresh ← Lean.mkFreshLMVarId let l ← Canonical.mvarLevels n_2 pure (Lean.mkLevelMVar fresh :: l)

partial def Canonical.toLam (type : Lean.Expr) (term : Tm) (typeArgs : List Lean.Expr) (paramIndex : Nat) : FromCanonicalM Lean.Expr

Builds a lambda expression of type type following the parameters of Tm term.

partial def Canonical.toApp (type spine : Lean.Expr) (args : List Tm) (argsIndex : Nat) (typeArgs : List Lean.Expr) : FromCanonicalM Lean.Expr

Builds an application of type type following the args

partial def Canonical.dePi (e : Lean.Expr) : Lean.Expr

Turn instances of Pi wrapper into native forallE.

def Canonical.canUnfoldDefault (cfg : Lean.Meta.Config) (info : Lean.ConstantInfo) : Lean.CoreM Bool

Lean's default unfolding predicate copied from Lean.Meta.GetUnfoldableConst.

Equations

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

def Canonical.canUnfold (e : Lean.Expr) : Lean.CoreM Bool

Custom unfolding predicate that unfolds definitions whose body is a forallE.

Equations

• Canonical.canUnfold (body.app arg) = Canonical.canUnfold body
• Canonical.canUnfold (Lean.Expr.lam binderName binderType body binderInfo) = Canonical.canUnfold body
• Canonical.canUnfold (Lean.Expr.letE declName type value body nonDep) = Canonical.canUnfold body
• Canonical.canUnfold (Lean.Expr.mdata data body) = Canonical.canUnfold body
• Canonical.canUnfold (Lean.Expr.forallE binderName binderType body binderInfo) = pure true
• Canonical.canUnfold e = pure false

structure Canonical.CanonicalConfig : Type

• count : USize

  Canonical produces count proofs.

• synth : Bool

  Guarantees completeness with respect to iota reduction.

• pi : Bool

  Provides (A → B) : Sort as an axiom to Canonical.

• debug : Bool
• refine : Bool

  Opens the refinement UI (beta).

def Canonical.canonicalConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM CanonicalConfig

Equations

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

def Canonical.checkInterrupted : Lean.CoreM Bool

A version of Core.checkInterrupted that does not crash.

Equations

• Canonical.checkInterrupted = do let __do_lift ← read match __do_lift.cancelTk? with | some tk => do let __do_lift ← liftM tk.isSet pure __do_lift | x => pure false

def Canonical.canonicalIO (type : Typ) (timeout : UInt64) (count : USize) (synth debug : Bool) : IO CanonicalResult

Equations

• Canonical.canonicalIO type timeout count synth debug = pure (Canonical.canonical type timeout count synth debug)

def refineWidget : Lean.Widget.Module

The widget for the refinement UI.

Equations

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

def canonicalRuleSeq : Lean.ParserDescr

Equations

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

def canonicalSeq : Lean.ParserDescr

Canonical exhaustively searches for terms in dependent type theory.

Equations

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