proof trace basically working

leanprover-community · Jan 25, 2024 · d0bf6e4 · d0bf6e4
1 parent 6f72485
commit d0bf6e4
Show file tree

Hide file tree

Showing 10 changed files with 279 additions and 142 deletions.
diff --git a/Auto/Embedding/LamChecker.lean b/Auto/Embedding/LamChecker.lean
@@ -627,104 +627,190 @@ inductive ChkStep where
   | w : WFStep → ChkStep
   deriving Inhabited, Hashable, BEq, Lean.ToExpr
 
-def ConvStep.toString : ConvStep → String
-| .validOfHeadBeta pos => s!"validOfHeadBeta {pos}"
-| .validOfBetaBounded pos bound => s!"validOfBetaBounded {pos} {bound}"
-| .validOfExtensionalize pos => s!"validOfExtensionalize {pos}"
-| .validOfEqSymm pos => s!"validOfEqSymm {pos}"
-| .validOfMp pos rw => s!"validOfMp {pos} {rw}"
-| .validOfMpAll pos rw => s!"validOfMpAll {pos} {rw}"
-| .validOfCongrArg pos rw => s!"validOfCongrArg {pos} {rw}"
-| .validOfCongrFun pos rw => s!"validOfCongrFun {pos} {rw}"
-| .validOfCongr pos rwFn rwArg => s!"validOfCongr {pos} {rwFn} {rwArg}"
-| .validOfCongrArgs pos rws => s!"validOfCongrArgs {pos} {rws}"
-| .validOfCongrFunN pos rwFn n => s!"validOfCongrFunN {pos} {rwFn} {n}"
-| .validOfCongrs pos rwFn rwArgs => s!"validOfCongrs {pos} {rwFn} {rwArgs}"
-
-def ConvAtStep.toString : ConvAtStep → String
-| .validOfEtaExpand1At pos occ => s!"validOfEtaExpand1At {pos} {occ}"
-| .validOfEtaReduce1At pos occ => s!"validOfEtaReduce1At {pos} {occ}"
-| .validOfEtaExpandNAt pos n occ => s!"validOfEtaExpandNAt {pos} {n} {occ}"
-| .validOfEtaReduceNAt pos n occ => s!"validOfEtaReduceNAt {pos} {n} {occ}"
-| .validOfExtensionalizeEqAt pos occ => s!"validOfExtensionalizeEqAt {pos} {occ}"
-| .validOfExtensionalizeEqFNAt pos n occ => s!"validOfExtensionalizeEqFNAt {pos} {n} {occ}"
-| .validOfIntensionalizeEqAt pos occ => s!"validOfIntensionalizeEqAt {pos} {occ}"
-
-def EtomStep.toString : EtomStep → String
-| .skolemize pos => s!"skolemize {pos}"
-| .define t => s!"define {t}"
-
-def FactStep.toString : FactStep → String
-| .boolFacts => s!"boolFacts"
-| .iteSpec s => s!"iteSpec {s}"
-
-def InferenceStep.toString : InferenceStep → String
-| .validOfBVarLower pv pn => s!"validOfBVarLower {pv} {pn}"
-| .validOfBVarLowers pv pns => s!"validOfBVarLowers {pv} {pns}"
-| .validOfImp p₁₂ p₁ => s!"validOfImp {p₁₂} {p₁}"
-| .validOfImps imp ps => s!"validOfImps {imp} {ps}"
-| .validOfInstantiate1 pos arg => s!"validOfInstantiate1 {pos} {arg}"
-| .validOfInstantiate pos args => s!"validOfInstantiate {pos} {args}"
-| .validOfInstantiateRev pos args => s!"validOfInstantiateRev {pos} {args}"
-| .validOfEqualize pos occ => s!"validOfEqualize {pos} {occ}"
-| .validOfAndLeft pos occ => s!"validOfAndLeft {pos} {occ}"
-| .validOfAndRight pos occ => s!"validOfAndRight {pos} {occ}"
-
-def LCtxStep.toString : LCtxStep → String
-| .validOfIntro1F pos => s!"validOfIntro1F {pos}"
-| .validOfIntro1H pos => s!"validOfIntro1H {pos}"
-| .validOfIntros pos idx => s!"validOfIntros {pos} {idx}"
-| .validOfRevert pos => s!"validOfRevert {pos}"
-| .validOfReverts pos idx => s!"validOfReverts {pos} {idx}"
-| .validOfAppend pos ex => s!"validOfAppend {pos} {ex}"
-| .validOfPrepend pos ex => s!"validOfPrepend {pos} {ex}"
-
-def NonemptyStep.toString : NonemptyStep → String
-| .nonemptyOfAtom n => s!"nonemptyOfAtom {n}"
-| .nonemptyOfEtom n => s!"nonemptyOfEtom {n}"
-
-def PrepConvStep.toString : PrepConvStep → String
-| .validOfPropNeEquivEqNot => s!"validOfPropNeEquivEqNot"
-| .validOfTrueEqFalseEquivFalse => s!"validOfTrueEqFalseEquivFalse"
-| .validOfFalseEqTrueEquivFalse => s!"validOfFalseEqTrueEquivFalse"
-| .validOfEqTrueEquiv => s!"validOfEqTrueEquiv"
-| .validOfEqFalseEquiv => s!"validOfEqFalseEquiv"
-| .validOfNeTrueEquivEqFalse => s!"validOfNeTrueEquivEqFalse"
-| .validOfNeFalseEquivEqTrue => s!"validOfNeFalseEquivEqTrue"
-| .validOfNotEqTrueEquivEqFalse => s!"validOfNotEqTrueEquivEqFalse"
-| .validOfNotEqFalseEquivEqTrue => s!"validOfNotEqFalseEquivEqTrue"
-| .validOfNotNotEquiv => s!"validOfNotNotEquiv"
-| .validOfNotEqEquivEqNot => s!"validOfNotEqEquivEqNot"
-| .validOfNotEqNotEquivEq => s!"validOfNotEqNotEquivEq"
-| .validOfPropext => s!"validOfPropext"
-| .validOfNotAndEquivNotOrNot => s!"validOfNotAndEquivNotOrNot"
-| .validOfNotOrEquivNotAndNot => s!"validOfNotOrEquivNotAndNot"
-| .validOfImpEquivNotOr => s!"validOfImpEquivNotOr"
-| .validOfNotImpEquivAndNot => s!"validOfNotImpEquivAndNot"
-| .validOfPropEq => s!"validOfPropEq"
-| .validOfPropNe => s!"validOfPropNe"
-| .validOfPushBVCast => s!"validOfPushBVCast"
-
-def WFStep.toString : WFStep → String
-| .wfOfCheck lctx t => s!"wfOfCheck {lctx} {t}"
-| .wfOfAppend pos ex => s!"wfOfAppend {pos} {ex}"
-| .wfOfPrepend pos ex => s!"wfOfPrepend {pos} {ex}"
-| .wfOfHeadBeta pos => s!"wfOfHeadBeta {pos}"
-| .wfOfBetaBounded pos bound => s!"wfOfBetaBounded {pos} {bound}"
-
-def ChkStep.toString : ChkStep → String
-| .c s  => ConvStep.toString s
-| .ca s => ConvAtStep.toString s
-| .e s  => EtomStep.toString s
-| .f s  => FactStep.toString s
-| .i s  => InferenceStep.toString s
-| .l s  => LCtxStep.toString s
-| .n s  => NonemptyStep.toString s
-| .p s pos occ => s!"{PrepConvStep.toString s} {pos} {occ}"
-| .w s  => WFStep.toString s
-
-instance : ToString ChkStep where
-  toString := ChkStep.toString
+
+section ChkStepToString
+
+  def ConvStep.toString : ConvStep → String
+  | .validOfHeadBeta pos => s!"validOfHeadBeta {pos}"
+  | .validOfBetaBounded pos bound => s!"validOfBetaBounded {pos} {bound}"
+  | .validOfExtensionalize pos => s!"validOfExtensionalize {pos}"
+  | .validOfEqSymm pos => s!"validOfEqSymm {pos}"
+  | .validOfMp pos rw => s!"validOfMp {pos} {rw}"
+  | .validOfMpAll pos rw => s!"validOfMpAll {pos} {rw}"
+  | .validOfCongrArg pos rw => s!"validOfCongrArg {pos} {rw}"
+  | .validOfCongrFun pos rw => s!"validOfCongrFun {pos} {rw}"
+  | .validOfCongr pos rwFn rwArg => s!"validOfCongr {pos} {rwFn} {rwArg}"
+  | .validOfCongrArgs pos rws => s!"validOfCongrArgs {pos} {rws}"
+  | .validOfCongrFunN pos rwFn n => s!"validOfCongrFunN {pos} {rwFn} {n}"
+  | .validOfCongrs pos rwFn rwArgs => s!"validOfCongrs {pos} {rwFn} {rwArgs}"
+
+  def ConvAtStep.toString : ConvAtStep → String
+  | .validOfEtaExpand1At pos occ => s!"validOfEtaExpand1At {pos} {occ}"
+  | .validOfEtaReduce1At pos occ => s!"validOfEtaReduce1At {pos} {occ}"
+  | .validOfEtaExpandNAt pos n occ => s!"validOfEtaExpandNAt {pos} {n} {occ}"
+  | .validOfEtaReduceNAt pos n occ => s!"validOfEtaReduceNAt {pos} {n} {occ}"
+  | .validOfExtensionalizeEqAt pos occ => s!"validOfExtensionalizeEqAt {pos} {occ}"
+  | .validOfExtensionalizeEqFNAt pos n occ => s!"validOfExtensionalizeEqFNAt {pos} {n} {occ}"
+  | .validOfIntensionalizeEqAt pos occ => s!"validOfIntensionalizeEqAt {pos} {occ}"
+
+  def EtomStep.toString : EtomStep → String
+  | .skolemize pos => s!"skolemize {pos}"
+  | .define t => s!"define {t}"
+
+  def FactStep.toString : FactStep → String
+  | .boolFacts => s!"boolFacts"
+  | .iteSpec s => s!"iteSpec {s}"
+
+  def InferenceStep.toString : InferenceStep → String
+  | .validOfBVarLower pv pn => s!"validOfBVarLower {pv} {pn}"
+  | .validOfBVarLowers pv pns => s!"validOfBVarLowers {pv} {pns}"
+  | .validOfImp p₁₂ p₁ => s!"validOfImp {p₁₂} {p₁}"
+  | .validOfImps imp ps => s!"validOfImps {imp} {ps}"
+  | .validOfInstantiate1 pos arg => s!"validOfInstantiate1 {pos} {arg}"
+  | .validOfInstantiate pos args => s!"validOfInstantiate {pos} {args}"
+  | .validOfInstantiateRev pos args => s!"validOfInstantiateRev {pos} {args}"
+  | .validOfEqualize pos occ => s!"validOfEqualize {pos} {occ}"
+  | .validOfAndLeft pos occ => s!"validOfAndLeft {pos} {occ}"
+  | .validOfAndRight pos occ => s!"validOfAndRight {pos} {occ}"
+
+  def LCtxStep.toString : LCtxStep → String
+  | .validOfIntro1F pos => s!"validOfIntro1F {pos}"
+  | .validOfIntro1H pos => s!"validOfIntro1H {pos}"
+  | .validOfIntros pos idx => s!"validOfIntros {pos} {idx}"
+  | .validOfRevert pos => s!"validOfRevert {pos}"
+  | .validOfReverts pos idx => s!"validOfReverts {pos} {idx}"
+  | .validOfAppend pos ex => s!"validOfAppend {pos} {ex}"
+  | .validOfPrepend pos ex => s!"validOfPrepend {pos} {ex}"
+
+  def NonemptyStep.toString : NonemptyStep → String
+  | .nonemptyOfAtom n => s!"nonemptyOfAtom {n}"
+  | .nonemptyOfEtom n => s!"nonemptyOfEtom {n}"
+
+  def PrepConvStep.toString : PrepConvStep → String
+  | .validOfPropNeEquivEqNot => s!"validOfPropNeEquivEqNot"
+  | .validOfTrueEqFalseEquivFalse => s!"validOfTrueEqFalseEquivFalse"
+  | .validOfFalseEqTrueEquivFalse => s!"validOfFalseEqTrueEquivFalse"
+  | .validOfEqTrueEquiv => s!"validOfEqTrueEquiv"
+  | .validOfEqFalseEquiv => s!"validOfEqFalseEquiv"
+  | .validOfNeTrueEquivEqFalse => s!"validOfNeTrueEquivEqFalse"
+  | .validOfNeFalseEquivEqTrue => s!"validOfNeFalseEquivEqTrue"
+  | .validOfNotEqTrueEquivEqFalse => s!"validOfNotEqTrueEquivEqFalse"
+  | .validOfNotEqFalseEquivEqTrue => s!"validOfNotEqFalseEquivEqTrue"
+  | .validOfNotNotEquiv => s!"validOfNotNotEquiv"
+  | .validOfNotEqEquivEqNot => s!"validOfNotEqEquivEqNot"
+  | .validOfNotEqNotEquivEq => s!"validOfNotEqNotEquivEq"
+  | .validOfPropext => s!"validOfPropext"
+  | .validOfNotAndEquivNotOrNot => s!"validOfNotAndEquivNotOrNot"
+  | .validOfNotOrEquivNotAndNot => s!"validOfNotOrEquivNotAndNot"
+  | .validOfImpEquivNotOr => s!"validOfImpEquivNotOr"
+  | .validOfNotImpEquivAndNot => s!"validOfNotImpEquivAndNot"
+  | .validOfPropEq => s!"validOfPropEq"
+  | .validOfPropNe => s!"validOfPropNe"
+  | .validOfPushBVCast => s!"validOfPushBVCast"
+
+  def WFStep.toString : WFStep → String
+  | .wfOfCheck lctx t => s!"wfOfCheck {lctx} {t}"
+  | .wfOfAppend pos ex => s!"wfOfAppend {pos} {ex}"
+  | .wfOfPrepend pos ex => s!"wfOfPrepend {pos} {ex}"
+  | .wfOfHeadBeta pos => s!"wfOfHeadBeta {pos}"
+  | .wfOfBetaBounded pos bound => s!"wfOfBetaBounded {pos} {bound}"
+
+  def ChkStep.toString : ChkStep → String
+  | .c s  => ConvStep.toString s
+  | .ca s => ConvAtStep.toString s
+  | .e s  => EtomStep.toString s
+  | .f s  => FactStep.toString s
+  | .i s  => InferenceStep.toString s
+  | .l s  => LCtxStep.toString s
+  | .n s  => NonemptyStep.toString s
+  | .p s pos occ => s!"{PrepConvStep.toString s} {pos} {occ}"
+  | .w s  => WFStep.toString s
+
+  instance : ToString ChkStep where
+    toString := ChkStep.toString
+
+end ChkStepToString
+
+
+section ChkStepPremises
+
+  def ConvStep.premises : ConvStep → List Nat
+  | .validOfHeadBeta pos => [pos]
+  | .validOfBetaBounded pos _ => [pos]
+  | .validOfExtensionalize pos => [pos]
+  | .validOfEqSymm pos => [pos]
+  | .validOfMp pos rw => [pos, rw]
+  | .validOfMpAll pos rw => [pos, rw]
+  | .validOfCongrArg pos rw => [pos, rw]
+  | .validOfCongrFun pos rw => [pos, rw]
+  | .validOfCongr pos rwFn rwArg => [pos, rwFn, rwArg]
+  | .validOfCongrArgs pos rws => pos :: rws
+  | .validOfCongrFunN pos rwFn _ => [pos, rwFn]
+  | .validOfCongrs pos rwFn rwArgs => pos :: rwFn :: rwArgs
+
+  def ConvAtStep.premises : ConvAtStep → List Nat
+  | .validOfEtaExpand1At pos _ => [pos]
+  | .validOfEtaReduce1At pos _ => [pos]
+  | .validOfEtaExpandNAt pos _ _ => [pos]
+  | .validOfEtaReduceNAt pos _ _ => [pos]
+  | .validOfExtensionalizeEqAt pos _ => [pos]
+  | .validOfExtensionalizeEqFNAt pos _ _ => [pos]
+  | .validOfIntensionalizeEqAt pos _ => [pos]
+
+  def EtomStep.premises : EtomStep → List Nat
+  | .skolemize pos => [pos]
+  | .define _ => []
+
+  def FactStep.premises : FactStep → List Nat
+  | .boolFacts => []
+  | .iteSpec _ => []
+
+  def InferenceStep.premises : InferenceStep → List Nat
+  | .validOfBVarLower pv pn => [pv, pn]
+  | .validOfBVarLowers pv pns => pv :: pns
+  | .validOfImp p₁₂ p₁ => [p₁₂, p₁]
+  | .validOfImps imp ps => imp :: ps
+  | .validOfInstantiate1 pos _ => [pos]
+  | .validOfInstantiate pos _ => [pos]
+  | .validOfInstantiateRev pos _ => [pos]
+  | .validOfEqualize pos _ => [pos]
+  | .validOfAndLeft pos _ => [pos]
+  | .validOfAndRight pos _ => [pos]
+
+  def LCtxStep.premises : LCtxStep → List Nat
+  | .validOfIntro1F pos => [pos]
+  | .validOfIntro1H pos => [pos]
+  | .validOfIntros pos _ => [pos]
+  | .validOfRevert pos => [pos]
+  | .validOfReverts pos _ => [pos]
+  | .validOfAppend pos _ => [pos]
+  | .validOfPrepend pos _ => [pos]
+
+  def NonemptyStep.premises : NonemptyStep → List Nat
+  | .nonemptyOfAtom _ => []
+  | .nonemptyOfEtom _ => []
+
+  /--
+    Whether a term is well-formed or not does not depend
+      on assertions. So, the premises of a WFStep is
+      deemed empty (although for some `WFStep`s they seem
+      to have premise syntactically)
+  -/
+  def WFStep.premises (_ : WFStep) : List Nat := []
+
+  def ChkStep.premises : ChkStep → List Nat
+  | .c s  => ConvStep.premises s
+  | .ca s => ConvAtStep.premises s
+  | .e s  => EtomStep.premises s
+  | .f s  => FactStep.premises s
+  | .i s  => InferenceStep.premises s
+  | .l s  => LCtxStep.premises s
+  | .n s  => NonemptyStep.premises s
+  | .p _ pos _ => [pos]
+  | .w s  => WFStep.premises s
+
+end ChkStepPremises
+
 
 inductive EvalResult where
   | fail

diff --git a/Auto/Solver/SMT.lean b/Auto/Solver/SMT.lean
@@ -9,6 +9,7 @@ initialize
   registerTraceClass `auto.smt.proof
   registerTraceClass `auto.smt.model
   registerTraceClass `auto.smt.stderr
+  registerTraceClass `auto.smt.unsatCore
 
 register_option auto.smt : Bool := {
   defValue := false
@@ -110,8 +111,24 @@ def getSexp (s : String) : MetaM (Sexp × String) :=
   | .incomplete _ _ => throwError s!"getSexp :: Incomplete input {s}"
   | .malformed => throwError s!"getSexp :: Malformed (prefix of) input {s}"
 
+/--
+  Recover id of valid facts from unsat core. Refer to `lamFOL2SMT`
+-/
+def validFactOfUnsatCore (unsatCore : Sexp) : MetaM (Array Nat) := do
+  let .app unsatCore := unsatCore
+    | throwError "validFactOfUnsatCore :: Malformed unsat core `{unsatCore}`"
+  let mut ret := #[]
+  for sexp in unsatCore do
+    let .atom (.symb name) := sexp
+      | continue
+    if name.take 11 == "valid_fact_" then
+      let .some n := (name.drop 11).toNat?
+        | throwError "validFactOfUnsatCore :: The id {name.drop 11} of {name} is invalid"
+      ret := ret.push n
+  return ret
+
 /-- Only put declarations in the query -/
-def querySolver (query : Array IR.SMT.Command) : MetaM (Option String) := do
+def querySolver (query : Array IR.SMT.Command) : MetaM (Option (Sexp × String)) := do
   if !(auto.smt.get (← getOptions)) then
     throwError "querySolver :: Unexpected error"
   if (auto.smt.solver.name.get (← getOptions) == .none) then
@@ -148,7 +165,7 @@ def querySolver (query : Array IR.SMT.Command) : MetaM (Option String) := do
     trace[auto.smt.result] "{name} says Unsat, unsat core:\n{unsatCore}"
     trace[auto.smt.proof] "Proof:\n{stdout}"
     trace[auto.smt.stderr] "stderr:\n{stderr}"
-    return .some stdout
+    return .some (unsatCore, stdout)
   | _ =>
     trace[auto.smt.result] "{name} produces unexpected check-sat response\n {checkSatResponse}"
     return .none

diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean
@@ -147,7 +147,8 @@ def collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array FVarId) : Tacti
 def collectUserLemmas (terms : Array Term) : TacticM (Array Lemma) :=
   Meta.withNewMCtxDepth do
     let mut lemmas := #[]
-    for ⟨⟨proof, type, deriv⟩, params⟩ in ← terms.mapM Prep.elabLemma do
+    for term in terms do
+      let ⟨⟨proof, type, deriv⟩, params⟩ ← Prep.elabLemma term (.leaf s!"❰{term}❱")
       if ← Prep.isNonemptyInhabited type then
         throwError "invalid lemma {type}, lemmas should not be inhabitation facts"
       else if ← Meta.isProp type then
@@ -293,8 +294,13 @@ def querySMT (exportFacts : Array REntry) (exportInds : Array MutualIndInfo) : L
     trace[auto.smt.printCommands] "{cmd}"
   if (auto.smt.save.get (← getOptions)) then
     Solver.SMT.saveQuery commands
-  let .some proof ← Solver.SMT.querySolver commands
+  let .some (unsatCore, proof) ← Solver.SMT.querySolver commands
     | return .none
+  for id in ← Solver.SMT.validFactOfUnsatCore unsatCore do
+    let .some t := exportLamTerms[id]?
+      | throwError "runAuto :: Index {id} of `exportLamTerm` out of range"
+    let vderiv ← LamReif.collectDerivFor (.valid [] t)
+    trace[auto.smt.unsatCore] "valid_fact_{id}: {vderiv}"
   if auto.smt.rconsProof.get (← getOptions) then
     let (_, _) ← Solver.SMT.getSexp proof
     logWarning "Proof reconstruction is not implemented."
@@ -314,7 +320,7 @@ def queryNative
   (prover? : Option (Array Lemma → MetaM Expr) := .none) : LamReif.ReifM (Option Expr) := do
   let (proof, proofLamTerm, usedEtoms, usedInhs, unsatCore) ←
     Lam2D.callNative_checker exportInhs exportFacts (prover?.getD Solver.Native.queryNative)
-  LamReif.newAssertion proof proofLamTerm
+  LamReif.newAssertion proof (.leaf "by_native::queryNative") proofLamTerm
   let etomInstantiated ← LamReif.validOfInstantiateForall (.valid [] proofLamTerm) (usedEtoms.map .etom)
   let forallElimed ← LamReif.validOfElimForalls etomInstantiated usedInhs
   let contra ← LamReif.validOfImps forallElimed unsatCore
@@ -436,8 +442,7 @@ def evalIntromono : Tactic
 | _ => throwUnsupportedSyntax
 
 /--
-  A monomorphization interface that can be invoked by repos dependent
-    on `lean-auto`.
+  A monomorphization interface that can be invoked by repos dependent on `lean-auto`.
   **TODO: Change `prover : Array Lemma → MetaM Expr` to have type `proverName : String`**
 -/
 def monoInterface

diff --git a/Auto/Translation/Assumptions.lean b/Auto/Translation/Assumptions.lean
@@ -16,6 +16,14 @@ inductive DTr where
   | leaf : String → DTr
 deriving Inhabited, Hashable, BEq
 
+partial def DTr.toString : DTr → String
+| .node s dtrs =>
+  s ++ " [" ++ String.intercalate ", " (dtrs.map DTr.toString).data ++ "]"
+| .leaf s => s
+
+instance : ToString DTr where
+  toString := DTr.toString
+
 /--
   Universe monomprphic facts
   User-supplied facts should have their universe level parameters