begin prep proof tracing

Auto/Tactic.lean

@@ -140,36 +140,42 @@ 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"
     return lemmas
 
 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

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,18 +181,18 @@ 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⟩
 
 /--
   Only introduce leading non-prop binders
   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

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 :=

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

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}`"

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"

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) =>