remove reorderForallInstDep

leanprover-community · Nov 21, 2024 · 91e5820 · 91e5820
1 parent 420bc92
commit 91e5820
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 3 deletions.
diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean
@@ -184,7 +184,6 @@ def unfoldConstAndPreprocessLemma (unfolds : Array Prep.ConstUnfoldInfo) (lem :
   let type := Prep.unfoldConsts unfolds type
   let type ← Core.betaReduce (← instantiateMVars type)
   let lem := {lem with type := type}
-  let lem ← lem.reorderForallInstDep
   return lem
 
 /--
@@ -202,7 +201,6 @@ def unfoldConstAndprepReduceDefeq (unfolds : Array Prep.ConstUnfoldInfo) (lem :
   let type := Prep.unfoldConsts unfolds type
   let type ← Core.betaReduce (← instantiateMVars type)
   let lem := {lem with type := type}
-  let lem ← lem.reorderForallInstDep
   return lem
 
 def traceLemmas (pre : String) (lemmas : Array Lemma) : TacticM Unit := do

diff --git a/Auto/Translation/Assumptions.lean b/Auto/Translation/Assumptions.lean
@@ -97,7 +97,9 @@ def Lemma.equivQuick (lem₁ lem₂ : Lemma) : MetaM Bool := do
   let s₂₁ ← Lemma.subsumeQuick lem₂ lem₁
   return s₁₂ && s₂₁
 
-/-- Reorder top-level `∀` so that (non-prop / dependent) ones precede other ones -/
+/- **TODO:** Determine whether this is useful -/
+/- Reorder top-level `∀` so that (non-prop / dependent) ones precede other ones -/
+/-
 def Lemma.reorderForallInstDep (lem : Lemma) : MetaM Lemma := do
   let depargs := HashSet.empty.insertMany (Expr.depArgs lem.type)
   Meta.forallTelescope lem.type fun xs body => do
@@ -112,6 +114,7 @@ def Lemma.reorderForallInstDep (lem : Lemma) : MetaM Lemma := do
     let proof ← Meta.mkLambdaFVars prec (← Meta.mkLambdaFVars trail proof)
     let type ← Meta.mkForallFVars prec (← Meta.mkForallFVars trail body)
     return ⟨⟨proof, type, lem.deriv⟩, lem.params⟩
+-/
 
 /--
   Rewrite using a universe-monomorphic rigid equality

diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
@@ -17,6 +17,7 @@ initialize
   registerTraceClass `auto.mono.printLemmaInst
   registerTraceClass `auto.mono.printConstInst
   registerTraceClass `auto.mono.printResult
+  registerTraceClass `auto.mono.printInputLemmas
 
 register_option auto.mono.saturationThreshold : Nat := {
   defValue := 250
@@ -903,6 +904,8 @@ def intromono (lemmas : Array Lemma) (mvarId : MVarId) : MetaM MVarId := do
     return mvar.mvarId!)
 
 def monomorphize (lemmas : Array Lemma) (inhFacts : Array Lemma) (k : Reif.State → MetaM α) : MetaM α := do
+  for h in lemmas do
+    trace[auto.mono.printInputLemmas] "Monomorphization got input lemma :: {h.type}"
   let (inductiveVals, monoSt) ← monoMAction.run {}
   MetaState.runWithIntroducedFVars (metaStateMAction inductiveVals monoSt) k
 where

diff --git a/Test/SmtTranslation/Trigger.lean b/Test/SmtTranslation/Trigger.lean
@@ -17,3 +17,8 @@ axiom fGreater : forall x, trigger (f x) (f x > x)
 
 set_option trace.auto.lamFOL2SMT.nameSuggestion true
 theorem fPlusOneGreater : forall x, (f x) + 1 > x := by auto [fGreater] u[]
+
+axiom fTrueGreater : true → ∀ x, trigger (f x) (f x > x)
+
+set_option trace.auto.printLemmas true
+theorem fTrueGreaterTr : true → forall x, f x > x := by auto [fTrueGreater] u[]