Test code

Auto.lean

@@ -1,3 +1,4 @@
 import Auto.Tactic
+import Auto.EvaluateAuto.TestCode
 
-def hello := "world"
+def hello := "world"

Auto/EvaluateAuto/ConstAnalysis.lean

@@ -0,0 +1,127 @@
+import Lean
+
+open Lean
+
+namespace Auto
+
+def Name.getConstsOfModule (module : Name) : CoreM (Array Name) := do
+  let mFile ← findOLean module
+  unless (← mFile.pathExists) do
+    throwError s!"object file '{mFile}' of module {module} does not exist"
+  let (mod, _) ← readModuleData mFile
+  return mod.constNames
+
+/-- Used as a wrapper in other functions -/
+def Name.getCi (name : Name) (parentFunc : Name) : CoreM ConstantInfo := do
+  let .some ci := (← getEnv).find? name
+    | throwError "{parentFunc} :: Cannot find name {name}"
+  return ci
+
+/-- Used as a wrapper in other functions -/
+def Name.hasValue (name : Name) (parentFunc : Name) : CoreM Bool := do
+  return (← Name.getCi name parentFunc).value?.isSome
+
+/-- Used as a wrapper in other functions -/
+def Name.getValue (name : Name) (parentFunc : Name) : CoreM Expr := do
+  let .some v := (← Name.getCi name parentFunc).value?
+    | throwError "{parentFunc} :: {name} has no value"
+  return v
+
+def Name.isTheorem (name : Name) : CoreM Bool := do
+  let .some ci := (← getEnv).find? name
+    | throwError "Name.isTheorem :: Cannot find name {name}"
+  let .thmInfo _ := ci
+    | return false
+  return true
+
+/--
+  A constant is a human theorem iff it is a theorem and has a
+  declaration range. Roughly speaking, a constant have a declaration
+  range iff it is defined (presumably by a human) in a `.lean` file
+-/
+def Name.isHumanTheorem (name : Name) : CoreM Bool :=
+  return (← Lean.findDeclarationRanges? name).isSome && (← Name.isTheorem name)
+
+def allHumanTheorems : CoreM (Array Name) := do
+  let allConsts := (← getEnv).constants.toList.map Prod.fst
+  let allHumanTheorems ← allConsts.filterM Name.isHumanTheorem
+  return Array.mk allHumanTheorems
+
+/-- Return the theorems that occurs in an expression -/
+def Expr.getUsedTheorems (e : Expr) : CoreM (Array Name) :=
+  e.getUsedConstants.filterM Name.isTheorem
+
+/-- Return the theorems that are used in the declaration body of a constant -/
+def Name.getUsedTheorems (name : Name) : CoreM (Array Name) := do
+  let v ← Name.getValue name decl_name%
+  Expr.getUsedTheorems v
+
+/-- Return true if the expression `e` only uses constants present in `names` -/
+def Expr.onlyUsesConsts (e : Expr) (names : Array Name) : Bool :=
+  e.getUsedConstants.all (fun name => names.contains name)
+
+/-- Return true if the declaration body of `name` only
+  uses constants present in `names` -/
+def Name.onlyUsesConsts (name : Name) (names : Array Name) : CoreM Bool := do
+  let v ← Name.getValue name decl_name%
+  return Expr.onlyUsesConsts v names
+
+/-- Return true if the type `name` only uses constants present in `names` -/
+def Name.onlyUsesConstsInType (name : Name) (names : Array Name) : CoreM Bool := do
+  let ci ← Name.getCi name decl_name%
+  return Expr.onlyUsesConsts ci.type names
+
+/-- Used to filter out theorems known to SMT solvers and native provers-/
+def logicConsts : Array Name := #[
+    ``True, ``False,
+    ``Not, ``And, ``Or, ``Iff,
+    ``Eq
+  ]
+
+/-- Used to filter out theorems known to SMT solvers -/
+def boolConsts : Array Name := #[
+    ``Bool,
+    ``true, ``false,
+    ``Bool.and, ``Bool.or, ``Bool.xor, ``Bool.not,
+    ``BEq, ``BEq.beq, ``bne, ``instBEqOfDecidableEq, ``instDecidableEqBool,
+    ``ite, ``cond,
+    ``Decidable, ``Decidable.decide
+  ]
+
+/-- Used to filter out theorems known to SMT solvers -/
+def natConsts : Array Name := #[
+    ``Nat,
+    ``OfNat.ofNat, ``instOfNatNat,
+    ``Nat.add, ``Nat.sub, ``Nat.mul, ``Nat.div, ``Nat.mod,
+    ``HAdd, ``HAdd.hAdd, ``instHAdd, ``instAddNat,
+    ``HSub, ``HSub.hSub, ``instHSub, ``instSubNat,
+    ``HMul, ``HMul.hMul, ``instHMul, ``instMulNat,
+    ``HDiv, ``HDiv.hDiv, ``instHDiv, ``Nat.instDiv,
+    ``HMod, ``HMod.hMod, ``instHMod, ``Nat.instMod,
+    ``LE, ``LE.le, ``instLENat,
+    ``LT, ``LT.lt, ``instLTNat,
+    ``GE.ge, ``GT.gt
+  ]
+
+/- **TODO:** Int theorems -/
+
+def Name.onlyLogicInType (name : Name) :=
+  Name.onlyUsesConstsInType name logicConsts
+
+def Name.onlyBoolLogicInType (name : Name) :=
+  Name.onlyUsesConstsInType name (logicConsts ++ boolConsts)
+
+def Name.onlyNatBoolLogicInType (name : Name) :=
+  Name.onlyUsesConstsInType name (logicConsts ++ boolConsts ++ natConsts)
+
+/-- Obtain Logic, Bool and Nat theorems -/
+def analyze : CoreM (Array (Array Name)) := do
+  let a ← allHumanTheorems
+  let logicThms ← a.filterM Name.onlyLogicInType
+  let boolThms ← a.filterM (fun name =>
+    return (!(← Name.onlyLogicInType name)) && (← Name.onlyBoolLogicInType name))
+  let natThms ← a.filterM (fun name =>
+    return (!(← Name.onlyBoolLogicInType name)) && (← Name.onlyNatBoolLogicInType name))
+  return #[logicThms, boolThms, natThms]
+
+end Auto

Auto/EvaluateAuto/EnvAnalysis.lean

@@ -0,0 +1,11 @@
+import Lean
+
+open Lean
+
+namespace Auto
+
+def mathlibModules : CoreM (Array Name) := do
+  let u := (← getEnv).header.moduleNames
+  return u.filter (fun name => name.components[0]? == .some `Mathlib)
+
+end Auto

Auto/EvaluateAuto/TestCode.lean

@@ -0,0 +1,72 @@
+import Lean
+import Auto.EvaluateAuto.ConstAnalysis
+import Auto.EvaluateAuto.EnvAnalysis
+import Auto.Tactic
+
+open Lean
+
+namespace Auto
+
+inductive Result
+  | success
+  | nonProp
+  | typeCheckFail
+  | typeUnequal
+  | autoException (e : Exception)
+
+instance : ToMessageData Result where
+  toMessageData : Result → MessageData
+  | .success         => "Result.success"
+  | .nonProp         => "Result.nonProp"
+  | .typeCheckFail   => "Result.typeCheckFail"
+  | .typeUnequal     => "Result.typeUnequal"
+  | .autoException e => m!"Result.autoException :: {e.toMessageData}"
+
+/--
+  Run `Lean-auto` on `lem.type`, using premises collected from `lem.proof`
+  Premises which only contain logic constants are filtered because they
+    are assumed to be known by the prover
+-/
+def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : MetaM Result := do
+  if !(← Meta.isProp lem.type) then
+    return .nonProp
+  -- **TODO: Aux theorem like those ending in `.proof_1`**
+  let usedThmNames ← (← Expr.getUsedTheorems lem.proof).filterM (fun name =>
+    return !(← Name.onlyLogicInType name))
+  let usedThms ← usedThmNames.mapM (fun n => Lemma.ofConst n (.leaf "collected by hammertest"))
+  let autoProofFn : MetaM Expr := Meta.forallTelescope lem.type fun bs body => do
+    let negGoal := Expr.app (.const ``Not []) body
+    let negGoalImpFalse ← Meta.withLocalDeclD `negGoal negGoal fun negGoalFVar => do
+      let inhLemmas ← Auto.Inhabitation.getInhFactsFromLCtx
+      let lctxLemmas ← Auto.collectLctxLemmas true #[]
+      let proofOfFalse ← Auto.runAuto declName? (lctxLemmas ++ usedThms) inhLemmas
+      Meta.mkLambdaFVars #[negGoalFVar] proofOfFalse
+    let goal := mkApp2 (.const ``Classical.byContradiction []) body negGoalImpFalse
+    Meta.mkLambdaFVars bs goal
+  let mut autoProof : Expr := Expr.sort .zero
+  try
+    autoProof ← autoProofFn
+  catch e =>
+    return .autoException e
+  match Kernel.check (← getEnv) {} autoProof with
+  | Except.ok autoProofType =>
+    match Kernel.isDefEq (← getEnv) {} autoProofType lem.type with
+    | Except.ok true => return .success
+    | _ => return .typeUnequal
+  | Except.error _ => return .typeCheckFail
+
+/--
+  Run `Lean-auto` on the type of ``name``, using premises collected
+    from the proof of `name`
+  Premises which only contain logic constants are filtered because they
+    are assumed to be known by the prover
+-/
+def runAutoOnConst (name : Name) : MetaM Result := do
+  let ci ← Name.getCi name decl_name%
+  let .some v := ci.value?
+    | throwError "{decl_name%} :: {name} has no value"
+  let lemmaPre ← Auto.Lemma.ofConst name (.leaf "ofConst")
+  let lemmaV := {lemmaPre with proof := v}
+  runAutoOnAutoLemma (.some name) lemmaV
+
+end Auto

Auto/Tactic.lean

@@ -10,6 +10,7 @@ initialize
   registerTraceClass `auto.tactic
   registerTraceClass `auto.tactic.printProof
   registerTraceClass `auto.printLemmas
+  registerTraceClass `auto.runAuto.printLemmas
 
 namespace Auto
 
@@ -203,13 +204,14 @@ def unfoldConstAndprepReduceDefeq (unfolds : Array Prep.ConstUnfoldInfo) (lem :
   let lem := {lem with type := type}
   return lem
 
-def traceLemmas (pre : String) (lemmas : Array Lemma) : TacticM Unit := do
+def traceLemmas (traceClass : Name) (pre : String) (lemmas : Array Lemma) : CoreM Unit := do
   let mut cnt : Nat := 0
   let mut mdatas : Array MessageData := #[]
   for lem in lemmas do
     mdatas := mdatas.push m!"\n{cnt}: {lem}"
     cnt := cnt + 1
-  trace[auto.printLemmas] mdatas.foldl MessageData.compose pre
+  if ← isTracingEnabledFor traceClass then
+    addTrace traceClass (mdatas.foldl MessageData.compose pre)
 
 def checkDuplicatedFact (terms : Array Term) : TacticM Unit :=
   let n := terms.size
@@ -236,19 +238,19 @@ def collectAllLemmas
   let startTime ← IO.monoMsNow
   let lctxLemmas ← collectLctxLemmas inputHints.lctxhyps ngoalAndBinders
   let lctxLemmas ← lctxLemmas.mapM (m:=MetaM) (unfoldConstAndPreprocessLemma unfoldInfos)
-  traceLemmas "Lemmas collected from local context:" lctxLemmas
+  traceLemmas `auto.printLemmas "Lemmas collected from local context:" lctxLemmas
   checkDuplicatedFact inputHints.terms
   checkDuplicatedLemmaDB inputHints.lemdbs
   let userLemmas := (← collectUserLemmas inputHints.terms) ++ (← collectHintDBLemmas inputHints.lemdbs)
   let userLemmas ← userLemmas.mapM (m:=MetaM) (unfoldConstAndPreprocessLemma unfoldInfos)
-  traceLemmas "Lemmas collected from user-provided terms:" userLemmas
+  traceLemmas `auto.printLemmas "Lemmas collected from user-provided terms:" userLemmas
   let defeqLemmas ← collectDefeqLemmas defeqNames
   let defeqLemmas ← defeqLemmas.mapM (m:=MetaM) (unfoldConstAndprepReduceDefeq unfoldInfos)
-  traceLemmas "Lemmas collected from user-provided defeq hints:" defeqLemmas
+  traceLemmas `auto.printLemmas "Lemmas collected from user-provided defeq hints:" defeqLemmas
   trace[auto.tactic] "Preprocessing took {(← IO.monoMsNow) - startTime}ms"
   let inhFacts ← Inhabitation.getInhFactsFromLCtx
   let inhFacts ← inhFacts.mapM (m:=MetaM) (unfoldConstAndPreprocessLemma unfoldInfos)
-  traceLemmas "Inhabitation lemmas :" inhFacts
+  traceLemmas `auto.printLemmas "Inhabitation lemmas :" inhFacts
   return (lctxLemmas ++ userLemmas ++ defeqLemmas, inhFacts)
 
 open Embedding.Lam in
@@ -431,6 +433,7 @@ def queryNative
 -/
 def runAuto
   (declName? : Option Name) (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM Expr := do
+  traceLemmas `auto.runAuto.printLemmas s!"All lemmas received by {decl_name%}:" lemmas
   -- Simplify `ite`
   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)