more defeq options

leanprover-community · Dec 19, 2024 · bf88b6e · bf88b6e
1 parent c5d2731
commit bf88b6e
Show file tree

Hide file tree

Showing 3 changed files with 69 additions and 59 deletions.
diff --git a/Auto/Lib/MetaState.lean b/Auto/Lib/MetaState.lean
@@ -105,6 +105,9 @@ def isDefEq (t s : Expr) : MetaStateM Bool := runMetaM (Meta.isDefEq t s)
 
 def isDefEqRigid (t s : Expr) : MetaStateM Bool := runMetaM (Meta.withNewMCtxDepth (Meta.isDefEq s t))
 
+def isDefEqRigidWith (t s : Expr) (mode : Meta.TransparencyMode) : MetaStateM Bool :=
+  runMetaM (Meta.withTransparency mode <| Meta.withNewMCtxDepth (Meta.isDefEq s t))
+
 def isLevelDefEq (u v : Level) : MetaStateM Bool := runMetaM (Meta.isLevelDefEq u v)
 
 def isLevelDefEqRigid (u v : Level) : MetaStateM Bool := runMetaM (Meta.withNewMCtxDepth (Meta.isLevelDefEq u v))

diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean
@@ -451,61 +451,62 @@ def dirtyTryRflInRunAuto (lemmas : Array Lemma) : MetaM (Option Lemma) := do
   Run `auto`'s monomorphization and preprocessing, then send the problem to different solvers
 -/
 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
-  -- **TODO:** This is a dirty trick
-  let lemmas ← (do
-    match ← dirtyTryRflInRunAuto lemmas with
-    | .some lem => return lemmas.push lem
-    | .none => return 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)
-  -- Simplify `cond`
-  let cond_simp_lem ← Lemma.ofConst ``Auto.Bool.cond_simp (.leaf "hw Auto.Bool.cond_simp")
-  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem cond_simp_lem)
-  -- Simplify `decide`
-  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
-    let mut exportFacts := exportFacts.map (Embedding.Lam.REntry.valid [])
-    let _ ← LamReif.reifInhabitations uinhs
-    let exportInhs := (← LamReif.getRst).nonemptyMap.toArray.map
-      (fun (s, _) => Embedding.Lam.REntry.nonempty s)
-    let exportInds ← LamReif.reifMutInds minds
-    LamReif.printValuation
-    -- **Preprocessing in Verified Checker**
-    let (exportFacts', exportInds) ← LamReif.preprocess exportFacts exportInds
-    exportFacts := exportFacts'
-    -- **TPTP invocation and Premise Selection**
-    if auto.tptp.get (← getOptions) then
-      let (proof, unsatCore) ← queryTPTP exportFacts
-      if let .some proof := proof then
-        return proof
-      let premiseSel? := auto.tptp.premiseSelection.get (← getOptions)
-      if premiseSel? then
-        if let .some unsatCore := unsatCore then
-          exportFacts := unsatCore
-    -- **SMT**
-    if auto.smt.get (← getOptions) then
-      let (proof, _) ← querySMT exportFacts exportInds
-      if let .some proof := proof then
-        return proof
-    -- **Native Prover**
-    exportFacts := exportFacts.append (← LamReif.auxLemmas exportFacts)
-    if auto.native.get (← getOptions) then
-      if let .some proof ← queryNative declName? exportFacts exportInhs then
-        return proof
-    throwError "Auto failed to find proof"
-    )
-  let (proof, _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM Expr) do
-    let s ← get
-    let u ← computeMaxLevel s.facts
-    (afterReify s.facts s.inhTys s.inds).run' {u := u})
-  trace[auto.tactic] "Auto found proof of {← Meta.inferType proof}"
-  trace[auto.tactic.printProof] "{proof}"
-  return proof
+  (declName? : Option Name) (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM Expr :=
+  Meta.withDefault do
+    traceLemmas `auto.runAuto.printLemmas s!"All lemmas received by {decl_name%}:" lemmas
+    -- **TODO:** This is a dirty trick
+    let lemmas ← (do
+      match ← dirtyTryRflInRunAuto lemmas with
+      | .some lem => return lemmas.push lem
+      | .none => return 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)
+    -- Simplify `cond`
+    let cond_simp_lem ← Lemma.ofConst ``Auto.Bool.cond_simp (.leaf "hw Auto.Bool.cond_simp")
+    let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem cond_simp_lem)
+    -- Simplify `decide`
+    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
+      let mut exportFacts := exportFacts.map (Embedding.Lam.REntry.valid [])
+      let _ ← LamReif.reifInhabitations uinhs
+      let exportInhs := (← LamReif.getRst).nonemptyMap.toArray.map
+        (fun (s, _) => Embedding.Lam.REntry.nonempty s)
+      let exportInds ← LamReif.reifMutInds minds
+      LamReif.printValuation
+      -- **Preprocessing in Verified Checker**
+      let (exportFacts', exportInds) ← LamReif.preprocess exportFacts exportInds
+      exportFacts := exportFacts'
+      -- **TPTP invocation and Premise Selection**
+      if auto.tptp.get (← getOptions) then
+        let (proof, unsatCore) ← queryTPTP exportFacts
+        if let .some proof := proof then
+          return proof
+        let premiseSel? := auto.tptp.premiseSelection.get (← getOptions)
+        if premiseSel? then
+          if let .some unsatCore := unsatCore then
+            exportFacts := unsatCore
+      -- **SMT**
+      if auto.smt.get (← getOptions) then
+        let (proof, _) ← querySMT exportFacts exportInds
+        if let .some proof := proof then
+          return proof
+      -- **Native Prover**
+      exportFacts := exportFacts.append (← LamReif.auxLemmas exportFacts)
+      if auto.native.get (← getOptions) then
+        if let .some proof ← queryNative declName? exportFacts exportInhs then
+          return proof
+      throwError "Auto failed to find proof"
+      )
+    let (proof, _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM Expr) do
+      let s ← get
+      let u ← computeMaxLevel s.facts
+      (afterReify s.facts s.inhTys s.inds).run' {u := u})
+    trace[auto.tactic] "Auto found proof of {← Meta.inferType proof}"
+    trace[auto.tactic.printProof] "{proof}"
+    return proof
 
 @[tactic auto]
 def evalAuto : Tactic

diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
@@ -39,9 +39,14 @@ register_option auto.mono.ciInstDefEq.mode : Meta.TransparencyMode := {
     " arising from instance relations between `ConstInst`s"
 }
 
-register_option auto.mono.tyCan.mode : Meta.TransparencyMode := {
+register_option auto.mono.tyRed.mode : Meta.TransparencyMode := {
   defValue := .reducible
-  descr := "Transparency level used when canonicalizing types"
+  descr := "Transparency level used when reducing types"
+}
+
+register_option auto.mono.tyDefEq.mode : Meta.TransparencyMode := {
+  defValue := .default
+  descr := "Transparency level used when testing definitional equality of types"
 }
 
 namespace Auto
@@ -758,7 +763,7 @@ namespace FVarRep
 
   /-- Return : (reduce(e), whether reduce(e) contain bfvars) -/
   def processType (e : Expr) : FVarRepM (Expr × Bool) := do
-    let mode := auto.mono.tyCan.mode.get (← getOptions)
+    let mode := auto.mono.tyRed.mode.get (← getOptions)
     let e ← MetaState.runMetaM <| prepReduceExprWithMode e mode
     let bfvarSet ← getBfvarSet
     -- If `e` contains no bound variables
@@ -783,7 +788,8 @@ namespace FVarRep
       if (← getTyCanMap).contains e then
         return
       for (e', ec) in (← getTyCanMap).toList do
-        if ← MetaState.isDefEqRigid e e' then
+        let mode := auto.mono.tyDefEq.mode.get (← getOptions)
+        if ← MetaState.isDefEqRigidWith e e' mode then
           setTyCanMap ((← getTyCanMap).insert e ec)
           return
       setTyCanMap ((← getTyCanMap).insert e e)