From 6f72485740144d3ec5f2346875a9498699a144ce Mon Sep 17 00:00:00 2001 From: IndPrinciple Date: Thu, 25 Jan 2024 00:07:36 +0800 Subject: [PATCH] begin prep proof tracing --- Auto/Tactic.lean | 24 +++++--- Auto/Translation/Assumptions.lean | 80 +++++++++++++++----------- Auto/Translation/Inhabitation.lean | 7 ++- Auto/Translation/Lam2D.lean | 5 +- Auto/Translation/LamReif.lean | 4 +- Auto/Translation/Monomorphization.lean | 6 +- Auto/Translation/Preprocessing.lean | 12 +++- README.md | 9 +++ 8 files changed, 91 insertions(+), 56 deletions(-) diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean index 1cae160..e6341e1 100644 --- a/Auto/Tactic.lean +++ b/Auto/Tactic.lean @@ -140,17 +140,18 @@ def collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array FVarId) : Tacti if ← Prep.isNonemptyInhabited type then continue if ¬ decl.isAuxDecl ∧ (← Meta.isProp type) then - lemmas := lemmas.push ⟨mkFVar fVarId, type, #[]⟩ + let name ← fVarId.getUserName + lemmas := lemmas.push ⟨⟨mkFVar fVarId, type, .leaf s!"lctxLem {name}"⟩, #[]⟩ return lemmas def collectUserLemmas (terms : Array Term) : TacticM (Array Lemma) := Meta.withNewMCtxDepth do let mut lemmas := #[] - for ⟨proof, type, params⟩ in ← terms.mapM Prep.elabLemma do + for ⟨⟨proof, type, deriv⟩, params⟩ in ← terms.mapM Prep.elabLemma do if ← Prep.isNonemptyInhabited type then throwError "invalid lemma {type}, lemmas should not be inhabitation facts" else if ← Meta.isProp type then - lemmas := lemmas.push ⟨proof, ← instantiateMVars type, params⟩ + lemmas := lemmas.push ⟨⟨proof, ← instantiateMVars type, deriv⟩, params⟩ else -- **TODO**: Relax condition? throwError "invalid lemma {type} for auto, proposition expected" @@ -158,18 +159,23 @@ def collectUserLemmas (terms : Array Term) : TacticM (Array Lemma) := def collectHintDBLemmas (names : Array Name) : TacticM (Array Lemma) := do let mut hs : HashSet Name := HashSet.empty + let mut ret : Array Lemma := #[] for name in names do let .some db ← findLemDB name | throwError "unknown lemma database {name}" - hs := mergeHashSet hs (← db.toHashSet) - liftM <| hs.toArray.mapM Lemma.ofConst + let lemNames ← db.toHashSet + for lname in lemNames do + if !hs.contains lname then + hs := hs.insert lname + ret := ret.push (← Lemma.ofConst lname (.leaf s!"lemdb {name} {lname}")) + return ret def collectDefeqLemmas (names : Array Name) : TacticM (Array Lemma) := Meta.withNewMCtxDepth do let lemmas ← names.concatMapM Prep.elabDefEq - lemmas.mapM (fun (⟨proof, type, params⟩ : Lemma) => do + lemmas.mapM (fun (⟨⟨proof, type, deriv⟩, params⟩ : Lemma) => do let type ← instantiateMVars type - return ⟨proof, type, params⟩) + return ⟨⟨proof, type, deriv⟩, params⟩) def unfoldConstAndPreprocessLemma (unfolds : Array Prep.ConstUnfoldInfo) (lem : Lemma) : MetaM Lemma := do let type ← prepReduceExpr (← instantiateMVars lem.type) @@ -350,10 +356,10 @@ def runNativeProverWithAuto def runAuto (declName? : Option Name) (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM Expr := do -- Simplify `ite` - let ite_simp_lem ← Lemma.ofConst ``Auto.Bool.ite_simp + let ite_simp_lem ← Lemma.ofConst ``Auto.Bool.ite_simp (.leaf "hw Auto.Bool.ite_simp") let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem ite_simp_lem) -- Simplify `decide` - let decide_simp_lem ← Lemma.ofConst ``Auto.Bool.decide_simp + let decide_simp_lem ← Lemma.ofConst ``Auto.Bool.decide_simp (.leaf "hw Auto.Bool.decide_simp") let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem decide_simp_lem) let afterReify (uvalids : Array UMonoFact) (uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM Expr := (do let exportFacts ← LamReif.reifFacts uvalids diff --git a/Auto/Translation/Assumptions.lean b/Auto/Translation/Assumptions.lean index 19bf5d4..c9b058e 100644 --- a/Auto/Translation/Assumptions.lean +++ b/Auto/Translation/Assumptions.lean @@ -3,64 +3,73 @@ import Std.Data.Array.Basic import Auto.Lib.BoolExtra import Auto.Lib.MessageData import Auto.Lib.ExprExtra +import Auto.Lib.ListExtra import Auto.Lib.Containers import Auto.Lib.AbstractMVars open Lean namespace Auto -structure Lemma where - proof : Expr -- Proof of the lemma - type : Expr -- The statement of the lemma - params : Array Name -- Universe Levels +/-- Proof Tree -/ +inductive DTr where + | node : String → Array DTr → DTr + | leaf : String → DTr deriving Inhabited, Hashable, BEq -instance : ToMessageData Lemma where - toMessageData lem := MessageData.compose - m!"⦗⦗ {lem.proof} : {lem.type} @@ " (.compose (MessageData.array lem.params toMessageData) m!" ⦘⦘") - /-- Universe monomprphic facts User-supplied facts should have their universe level parameters instantiated before being put into `Reif.State.facts` - The first `Expr` is the proof, and the second `Expr` is the fact -/ -abbrev UMonoFact := Expr × Expr +structure UMonoFact where + proof : Expr + type : Expr + deriv : DTr +deriving Inhabited, Hashable, BEq + +structure Lemma extends UMonoFact where + params : Array Name -- Universe Levels +deriving Inhabited, Hashable, BEq + +instance : ToMessageData Lemma where + toMessageData lem := MessageData.compose + m!"⦗⦗ {lem.proof} : {lem.type} @@ " (.compose (MessageData.array lem.params toMessageData) m!" ⦘⦘") -def Lemma.ofUMonoFact (fact : UMonoFact) : Lemma := ⟨fact.fst, fact.snd, #[]⟩ +def Lemma.ofUMonoFact (fact : UMonoFact) : Lemma := { fact with params := #[] } def Lemma.toUMonoFact? (lem : Lemma) : Option UMonoFact := match lem.params with - | ⟨.nil⟩ => .some ⟨lem.proof, lem.type⟩ + | ⟨.nil⟩ => .some lem.toUMonoFact | ⟨_::_⟩ => .none def Lemma.instantiateLevelParamsArray (lem : Lemma) (lvls : Array Level) : Lemma := - let ⟨proof, type, params⟩ := lem - ⟨proof.instantiateLevelParamsArray params lvls, + let ⟨⟨proof, type, deriv⟩, params⟩ := lem + ⟨⟨proof.instantiateLevelParamsArray params lvls, type.instantiateLevelParamsArray params lvls, + deriv⟩, params[lvls.size:]⟩ def Lemma.instantiateLevelParams (lem : Lemma) (lvls : List Level) : Lemma := Lemma.instantiateLevelParamsArray lem ⟨lvls⟩ def Lemma.instantiateMVars (lem : Lemma) : MetaM Lemma := do - let ⟨proof, type, params⟩ := lem + let ⟨⟨proof, type, deriv⟩, params⟩ := lem let proof ← Lean.instantiateMVars proof let type ← Lean.instantiateMVars type - return ⟨proof, type, params⟩ + return ⟨⟨proof, type, deriv⟩, params⟩ def Lemma.betaReduceType (lem : Lemma) : CoreM Lemma := do - let ⟨proof, type, params⟩ := lem + let ⟨⟨proof, type, deriv⟩, params⟩ := lem let type ← Core.betaReduce type - return ⟨proof, type, params⟩ + return ⟨⟨proof, type, deriv⟩, params⟩ /-- Create a `Lemma` out of a constant, given the name of the constant -/ -def Lemma.ofConst (name : Name) : CoreM Lemma := do +def Lemma.ofConst (name : Name) (deriv : DTr) : CoreM Lemma := do let .some decl := (← getEnv).find? name | throwError "Lemma.ofConst :: Unknown constant {name}" let type := decl.type let params := decl.levelParams - return ⟨.const name (params.map Level.param), type, ⟨params⟩⟩ + return ⟨⟨.const name (params.map Level.param), type, deriv⟩, ⟨params⟩⟩ /-- Check whether `lem₁` subsumes `lem₂` -/ def Lemma.subsumeQuick (lem₁ lem₂ : Lemma) : MetaM Bool := Meta.withNewMCtxDepth <| do @@ -95,7 +104,7 @@ def Lemma.reorderForallInstDep (lem : Lemma) : MetaM Lemma := do let proof := Expr.headBeta (Lean.mkAppN lem.proof xs) let proof ← Meta.mkLambdaFVars prec (← Meta.mkLambdaFVars trail proof) let type ← Meta.mkForallFVars prec (← Meta.mkForallFVars trail body) - return ⟨proof, type, lem.params⟩ + return ⟨⟨proof, type, lem.deriv⟩, lem.params⟩ /-- Rewrite using a universe-monomorphic rigid equality @@ -104,10 +113,10 @@ def Lemma.reorderForallInstDep (lem : Lemma) : MetaM Lemma := do · If `lhs` does not occur in `lem.type`, return `.none` -/ def Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) : MetaM (Option Lemma) := do - let (rwproof, rwtype) := rw + let ⟨rwproof, rwtype, rwDeriv⟩ := rw let .some (α, lhs, rhs) ← Meta.matchEq? rwtype | throwError "Lemma.rewriteUMonoRigid :: {rwtype} is not an equality" - let ⟨proof, e, params⟩ := lem + let ⟨⟨proof, e, lemDeriv⟩, params⟩ := lem let eAbst ← Meta.kabstract e lhs unless eAbst.hasLooseBVars do return .none @@ -116,7 +125,7 @@ def Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) : MetaM (Option Lemm unless (← Meta.isTypeCorrect motive) do throwError "Lemma.rewriteUMonoRigid :: Motive {motive} is not type correct" let eqPrf ← Meta.mkEqNDRec motive proof rwproof - return .some ⟨eqPrf, eNew, params⟩ + return .some ⟨⟨eqPrf, eNew, .node "rw" #[lemDeriv, rwDeriv]⟩, params⟩ /-- Exhaustively rewrite using a universe-polymorphic rigid equality @@ -172,10 +181,10 @@ structure LemmaInst extends Lemma where deriving Inhabited, Hashable, BEq def LemmaInst.ofLemma (lem : Lemma) : MetaM LemmaInst := do - let ⟨proof, type, params⟩ := lem + let ⟨⟨proof, type, deriv⟩, params⟩ := lem Meta.forallTelescope type fun xs _ => do let proof ← Meta.mkLambdaFVars xs (mkAppN proof xs) - let lem' : Lemma := ⟨proof, type, params⟩ + let lem' : Lemma := ⟨⟨proof, type, deriv⟩, params⟩ return ⟨lem', xs.size, xs.size⟩ /-- @@ -183,7 +192,7 @@ def LemmaInst.ofLemma (lem : Lemma) : MetaM LemmaInst := do But, if a prop-binder is an instance binder, we still introduce it -/ def LemmaInst.ofLemmaHOL (lem : Lemma) : MetaM LemmaInst := do - let ⟨proof, type, params⟩ := lem + let ⟨⟨proof, type, deriv⟩, params⟩ := lem Meta.forallTelescope type fun xs _ => do let mut xs' := #[] for x in xs do @@ -192,17 +201,17 @@ def LemmaInst.ofLemmaHOL (lem : Lemma) : MetaM LemmaInst := do break xs' := xs'.push x let proof ← Meta.mkLambdaFVars xs' (mkAppN proof xs') - let lem' : Lemma := ⟨proof, type, params⟩ + let lem' : Lemma := ⟨⟨proof, type, deriv⟩, params⟩ return ⟨lem', xs'.size, xs'.size⟩ def LemmaInst.ofLemmaLeadingDepOnly (lem : Lemma) : MetaM LemmaInst := do - let ⟨proof, type, params⟩ := lem + let ⟨⟨proof, type, deriv⟩, params⟩ := lem let nld := Expr.numLeadingDepArgs type Meta.forallBoundedTelescope type nld fun xs _ => do if xs.size != nld then throwError "LemmaInst.ofLemmaLeadingDepOnly :: Unexpected error" let proof ← Meta.mkLambdaFVars xs (mkAppN proof xs) - let lem' : Lemma := ⟨proof, type, params⟩ + let lem' : Lemma := ⟨⟨proof, type, deriv⟩, params⟩ return ⟨lem', xs.size, xs.size⟩ /-- Get the proof of the lemma that `li` is an instance of -/ @@ -253,6 +262,7 @@ structure MLemmaInst where origProof : Expr args : Array Expr type : Expr + deriv : DTr deriving Inhabited, Hashable, BEq instance : ToMessageData MLemmaInst where @@ -262,7 +272,7 @@ instance : ToMessageData MLemmaInst where m!" : {mi.type} ⦘⦘") def MLemmaInst.ofLemmaInst (li : LemmaInst) : MetaM (Array Level × Array Expr × MLemmaInst) := do - let ⟨proof, type, params⟩ := li.toLemma + let ⟨⟨proof, type, deriv⟩, params⟩ := li.toLemma let lvls ← params.mapM (fun _ => Meta.mkFreshLevelMVar) let proof := proof.instantiateLevelParamsArray params lvls let type := type.instantiateLevelParamsArray params lvls @@ -273,10 +283,10 @@ def MLemmaInst.ofLemmaInst (li : LemmaInst) : MetaM (Array Level × Array Expr if args.size != li.nargs then throwError "MLemmaInst.ofLemmaInst :: Unexpected error" let type ← Meta.instantiateForall type mvars - return (lvls, mvars, ⟨origProof, args, type⟩) + return (lvls, mvars, ⟨origProof, args, type, deriv⟩) def LemmaInst.ofMLemmaInst (mi : MLemmaInst) : MetaM LemmaInst := do - let ⟨origProof, args, type⟩ := mi + let ⟨origProof, args, type, deriv⟩ := mi let origProof ← instantiateMVars origProof let args ← args.mapM instantiateMVars let type ← instantiateMVars type @@ -289,7 +299,7 @@ def LemmaInst.ofMLemmaInst (mi : MLemmaInst) : MetaM LemmaInst := do let nargs := args.size let proof := s.lctx.mkLambda s.fvars proof let type := s.lctx.mkForall s.fvars type - let lem : Lemma := ⟨proof, type, s.paramNames⟩ + let lem : Lemma := ⟨⟨proof, type, deriv⟩, s.paramNames⟩ return ⟨lem, nbinders, nargs⟩ partial def collectUniverseLevels : Expr → MetaM (HashSet Level) @@ -323,7 +333,7 @@ partial def collectUniverseLevels : Expr → MetaM (HashSet Level) | .proj .. => throwError "Please unfold projections before collecting universe levels" def computeMaxLevel (facts : Array UMonoFact) : MetaM Level := do - let levels ← facts.foldlM (fun hs (_, ty) => do + let levels ← facts.foldlM (fun hs ⟨_, ty, _⟩ => do let tyUs ← collectUniverseLevels ty return mergeHashSet tyUs hs) HashSet.empty -- Compute the universe level that we need to lift to diff --git a/Auto/Translation/Inhabitation.lean b/Auto/Translation/Inhabitation.lean index af4cce4..b401db5 100644 --- a/Auto/Translation/Inhabitation.lean +++ b/Auto/Translation/Inhabitation.lean @@ -82,7 +82,8 @@ def getInhFactsFromLCtx : MetaM (Array Lemma) := withNewMCtxDepth do if ← isDefEq lem.type ty then new := false; break if !new then continue - ret := ret.push ⟨proof, ty, #[]⟩ + let name ← fid.getUserName + ret := ret.push ⟨⟨proof, ty, .leaf s!"lctxInh {name}"⟩, #[]⟩ return ret private def inhFactMatchAtomTysAux (inhTy : Lemma) (atomTys : Array Expr) : MetaM LemmaInsts := @@ -114,11 +115,11 @@ def inhFactMatchAtomTys (inhTys : Array Lemma) (atomTys : Array Expr) : MetaM (A if li.params.size != 0 || li.nbinders != 0 then continue let mut new? := true let canTy ← canonicalize li.type atomTys - for (_, ty) in ret do + for ⟨_, ty, _⟩ in ret do if canTy == ty then new? := false if !new? then continue - ret := ret.push ⟨li.proof, canTy⟩ + ret := ret.push ⟨li.proof, canTy, li.deriv⟩ return ret where canonicalize (inhTy : Expr) (atomTys : Array Expr) : MetaM Expr := diff --git a/Auto/Translation/Lam2D.lean b/Auto/Translation/Lam2D.lean index a74581e..7973e7a 100644 --- a/Auto/Translation/Lam2D.lean +++ b/Auto/Translation/Lam2D.lean @@ -354,7 +354,10 @@ private def callNativeExternMAction trace[auto.printHyps] "{hyp}" let hyps ← runMetaM <| hyps.mapM (fun e => Core.betaReduce e) let hypFvars ← withHyps hyps - let lemmas : Array Lemma := (hyps.zip hypFvars).map (fun (ty, proof) => ⟨.fvar proof, ty, #[]⟩) + -- debug + -- **TODO: Specify origin** + let lemmas : Array Lemma := (hyps.zip hypFvars).map (fun (ty, proof) => + ⟨⟨.fvar proof, ty, .leaf "?callNativeExternMAction"⟩, #[]⟩) -- Note that we're not introducing bound variables into local context -- in the above action, so it's reasonable to use `runMetaM` let atomsToAbstract ← getAtomsToAbstract diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean index a869fc5..ea8c8b0 100644 --- a/Auto/Translation/LamReif.lean +++ b/Auto/Translation/LamReif.lean @@ -1620,7 +1620,7 @@ def reifTermCheckType (e : Expr) : ReifM (LamSort × LamTerm) := do /-- Return the positions of the reified and `resolveImport`-ed facts within the `validTable` -/ def reifFacts (facts : Array UMonoFact) : ReifM (Array LamTerm) := - facts.mapM (fun (proof, ty) => do + facts.mapM (fun ⟨proof, ty, _⟩ => do let (s, lamty) ← reifTermCheckType ty if s != .base .prop then throwError "reifFacts :: Fact {lamty} is not of type `prop`" @@ -1629,7 +1629,7 @@ def reifFacts (facts : Array UMonoFact) : ReifM (Array LamTerm) := return lamty) def reifInhabitations (inhs : Array UMonoFact) : ReifM (Array LamSort) := - inhs.mapM (fun (inhTy, ty) => do + inhs.mapM (fun ⟨inhTy, ty, _⟩ => do let s ← reifType ty newInhabitation inhTy s trace[auto.lamReif.printResult] "Successfully reified inhabitation proof of {ty} to λsort `{s}`" diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean index 1dc5601..8b2d25a 100644 --- a/Auto/Translation/Monomorphization.lean +++ b/Auto/Translation/Monomorphization.lean @@ -741,7 +741,7 @@ def monomorphize (lemmas : Array Lemma) (inhFacts : Array Lemma) (k : Reif.State -- Lemma instances let lis := monoSt.lisArr.concatMap id let fvarRepMFactAction : FVarRep.FVarRepM (Array UMonoFact) := - lis.mapM (fun li => do return ⟨li.proof, ← FVarRep.replacePolyWithFVar li.type⟩) + lis.mapM (fun li => do return ⟨li.proof, ← FVarRep.replacePolyWithFVar li.type, li.deriv⟩) let fvarRepMInductAction (ivals : Array (Array SimpleIndVal)) : FVarRep.FVarRepM (Array (Array SimpleIndVal)) := ivals.mapM (fun svals => svals.mapM (fun ⟨name, type, ctors, projs⟩ => do FVarRep.processType type @@ -754,7 +754,7 @@ def monomorphize (lemmas : Array Lemma) (inhFacts : Array Lemma) (k : Reif.State return ⟨name, type, ctors, projs⟩)) let metaStateMAction : MetaState.MetaStateM (Array FVarId × Reif.State) := (do let (uvalids, s) ← fvarRepMFactAction.run { ciMap := monoSt.ciMap } - for (proof, ty) in uvalids do + for ⟨proof, ty, _⟩ in uvalids do trace[auto.mono.printResult] "Monomorphized :: {proof} : {ty}" let exlis := s.exprMap.toList.map (fun (e, id) => (id, e)) let cilis ← s.ciIdMap.toList.mapM (fun (ci, id) => do return (id, ← MetaState.runMetaM ci.toExpr)) @@ -765,7 +765,7 @@ def monomorphize (lemmas : Array Lemma) (inhFacts : Array Lemma) (k : Reif.State let mut tyCanInhs := #[] for e in tyCans do if let .some inh ← MetaState.runMetaM <| Meta.withNewMCtxDepth <| Meta.trySynthInhabited e then - tyCanInhs := tyCanInhs.push ⟨inh, e⟩ + tyCanInhs := tyCanInhs.push ⟨inh, e, .leaf "tyCanInh"⟩ let inhMatches ← MetaState.runMetaM (Inhabitation.inhFactMatchAtomTys inhFacts tyCans) let inhs := tyCanInhs ++ inhMatches trace[auto.mono] "Monomorphizing inhabitation facts took {(← IO.monoMsNow) - startTime}ms" diff --git a/Auto/Translation/Preprocessing.lean b/Auto/Translation/Preprocessing.lean index 0f9e8ca..da8f6e0 100644 --- a/Auto/Translation/Preprocessing.lean +++ b/Auto/Translation/Preprocessing.lean @@ -12,7 +12,10 @@ namespace Auto namespace Prep -/-- From a user-provided term `stx`, produce a lemma -/ +/-- + From a user-provided term `stx`, produce a lemma + Note that the `deriv` of the lemma is left unspecified +-/ def elabLemma (stx : Term) : TacticM Lemma := -- elaborate term as much as possible and abstract any remaining mvars: Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do @@ -22,7 +25,7 @@ def elabLemma (stx : Term) : TacticM Lemma := let abstres ← Auto.abstractMVars e let e := abstres.expr let paramNames := abstres.paramNames - return Lemma.mk e (← inferType e) paramNames + return Lemma.mk ⟨e, ← inferType e, .leaf "?elabLemma"⟩ paramNames def addRecAsLemma (recVal : RecursorVal) : MetaM (Array Lemma) := do let some (.inductInfo indVal) := (← getEnv).find? recVal.getInduct @@ -44,13 +47,16 @@ def addRecAsLemma (recVal : RecursorVal) : MetaM (Array Lemma) := do return (← mkLambdaFVars ys proof, ← mkForallFVars ys eq) let proof ← instantiateMVars (← mkLambdaFVars xs proof) let eq ← instantiateMVars (← mkForallFVars xs eq) - return ⟨proof, eq, recVal.levelParams.toArray⟩ + return ⟨⟨proof, eq, .leaf s!"rec {recVal.name}.{ctorName}"⟩, recVal.levelParams.toArray⟩ for lem in res do let ty' ← Meta.inferType lem.proof if !(← Meta.isDefEq ty' lem.type) then throwError "addRecAsLemma :: Application type mismatch" return Array.mk res +/-- + Note that the `deriv` of the lemmas are left unspecified +-/ def elabDefEq (name : Name) : TacticM (Array Lemma) := do match (← getEnv).find? name with | some (.recInfo val) => diff --git a/README.md b/README.md index d3bd594..ab5e0d9 100644 --- a/README.md +++ b/README.md @@ -71,3 +71,12 @@ Lean-auto is still under development, but it's already able to solve nontrivial ## Checker * The checker is based on a deep embedding of simply-typed lambda calculus into dependent type theory. * The checker is slow on large input. For example, it takes ```6s``` to typecheck the final example in ```BinderComplexity.lean```. However, this is probably acceptable for mathlib usages, because e.g ```Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean``` has two theorems that take ```4s``` to compile (but a large portion of the ```4s``` are spent on typeclass inference) + +## Rules in Proof Tree +* `?`: Not specified, generated in function ``. This is for debug purpose only. +* `hw `: Lemmas hard-wired into Lean-auto +* `lctxInh`: Inhabitation fact from local context +* `lctxLem`: Lemma from local context +* `rec .` +* `rw [0, 1]`: Rewrite `0` using `1` (`1` must be an equality) +* `tyCanInh`: Inhabitation instance synthesized for canonicalized type \ No newline at end of file