fix preprocessing bug in test code

leanprover-community · Nov 27, 2024 · 0867a4d · 0867a4d
1 parent 769fc6c
commit 0867a4d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 7 deletions.
diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean
@@ -39,7 +39,8 @@ def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : MetaM Resu
     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
+      let allLemmas ← (lctxLemmas ++ usedThms).mapM (Auto.unfoldConstAndPreprocessLemma #[])
+      let proofOfFalse ← Auto.runAuto declName? allLemmas inhLemmas
       Meta.mkLambdaFVars #[negGoalFVar] proofOfFalse
     let goal := mkApp2 (.const ``Classical.byContradiction []) body negGoalImpFalse
     Meta.mkLambdaFVars bs goal

diff --git a/Test/Bugs.lean b/Test/Bugs.lean
@@ -80,9 +80,3 @@ end Set
 example (x : Nat) (primeset : Nat → Prop) (dvd : Nat → Nat → Prop) :
   ((∃ (i : _) (i_1 : primeset i), dvd i x) ↔ (∃ p, primeset p ∧ dvd p x)) := by
   auto
-
--- bug
-set_option trace.auto.tactic true in
-#eval do
-  let m ← Auto.runAutoOnConst ``Nat.sub_one_lt_of_lt
-  trace[auto.tactic] m!"{m}"