Documentation

CslibFrontier.Tactic.Degree

Degree certificates by composition #

degree proves a goal ComputableInDegree f encIn encOut d e from the fun_prop rules of the operations in f. It rewrites each match on an option to Option.elim, then runs fun_prop, which discharges the degree side conditions of its composition rules with lia.

Like fun_prop, it does not unfold definitions: unfold a definition first, or register a named certificate for it with fun_prop. On another goal it fails at once, and when the search fails the fun_prop error ends with a note saying so.

Main definitions #

source
def Turing.MultiTapeTM.degreeTac :
Lean.ParserDescr

Prove ComputableInDegree f encIn encOut d e by composing the fun_prop rules of the operations in f, after rewriting option matches to Option.elim.

Instances For
    source
    def Turing.MultiTapeTM.evalDegree :
    Lean.Elab.Tactic.Tactic

    Elaborate degree: check the goal, then compose with fun_prop.

    Instances For