diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean index 2247708..d176459 100644 --- 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 index a667780..a487b00 100644 --- 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}"