Merge pull request #9 from leanprover-community/dev

Dev

Duper/Interface.lean

@@ -1,4 +1,3 @@
-import Std.Lean.CoreM
 import Duper.ProofReconstruction
 import Auto.Tactic
 
@@ -251,13 +250,13 @@ def mkDuperCallSuggestion (duperStxRef : Syntax) (origSpan : Syntax) (facts : Sy
   let configOptionsStx : Syntax.TSepArray `Duper.configOption "," := {elemsAndSeps := configOptionsArr}
   if withDuperStar && facts.elemsAndSeps.isEmpty then
     let suggestion ←`(tactic| duper [*] {$configOptionsStx,*})
-    Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
+    Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
   else if withDuperStar then
     let suggestion ←`(tactic| duper [*, $facts,*] {$configOptionsStx,*})
-    Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
+    Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
   else
     let suggestion ←`(tactic| duper [$facts,*] {$configOptionsStx,*})
-    Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
+    Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan)
 
 /-- We save the `CoreM` state. This is because we will add a constant `skolemSorry` to the environment to support skolem constants with
     universe levels. We want to erase this constant after the saturation procedure ends -/
@@ -328,9 +327,9 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name × Bool)) : M
     for (e, proof, paramNames, isFromGoal) in formulas do
       let update (ty lhs rhs : Expr) newFormulas (containedIn : Expr → Bool) : MetaM _ := do
         if containedIn rhs then pure newFormulas else
-          newFormulas.mapM fun (f, fproof, fparamNames) => do
+          newFormulas.mapM fun (f, fproof, fparamNames, fIsFromGoal) => do
             if !containedIn f then
-              return (f, fproof, fparamNames)
+              return (f, fproof, fparamNames, fIsFromGoal)
             else
               let us ← paramNames.mapM fun _ => mkFreshLevelMVar
               let lhs'   := lhs.instantiateLevelParamsArray paramNames us
@@ -342,11 +341,12 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name × Bool)) : M
               let f := abstracted.instantiate1 rhs'
               let fproof ← withTransparency .default do mkAppOptM ``Eq.ndrec #[none,
                 some lhs,
-                some $ mkLambda `x .default ty' (← Meta.mkAppM ``Eq #[abstracted, mkConst ``True]),
+                some (← Meta.withLocalDeclD `_ ty' fun fvar => do
+                  Meta.mkLambdaFVars #[fvar] $ ← Meta.mkAppM ``Eq #[abstracted.instantiate1 fvar, mkConst ``True]),
                 some fproof,
                 rhs',
                 proof']
-              return (f, ← instantiateMVars $ fproof, fparamNames)
+              return (f, ← instantiateMVars $ fproof, fparamNames, isFromGoal || fIsFromGoal)
       match e with
       | .app ( .app ( .app (.const ``Eq _) ty) (.fvar fid)) rhs =>
         let containedIn := fun e => (e.find? (· == .fvar fid)).isSome
@@ -409,18 +409,28 @@ def runDuper (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMax
    to be in alignment with how Auto stores lemmas to avoid the unnecessary cost of this conversion, but for now, it suffices to
    add or remove `eq_true` as needed) -/
 
-/-- Converts formulas/lemmas from the format used by Duper to the format used by Auto. -/
+partial def getLeavesFromDTr (t : Auto.DTr) : Array String :=
+  match t with
+  | Auto.DTr.node _ subTrees => (subTrees.map getLeavesFromDTr).flatten
+  | Auto.DTr.leaf s => #[s]
+
+/-- Converts formulas/lemmas from the format used by Duper to the format used by Auto. Duper uses Auto's deriv DTr to keep
+    track of `isFromGoal` information through the monomorphization procedure. -/
 def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name × Bool)) : MetaM (Array Auto.Lemma) :=
   formulas.toArray.mapM
     (fun (fact, proof, params, isFromGoal) => -- For now, isFromGoal is ignored
-      return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"❰{fact}❱")})
+      return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"{isFromGoal}")})
 
 /-- Converts formulas/lemmas from the format used by Auto to the format used by Duper. -/
 def autoLemmasToFormulas (lemmas : Array Auto.Lemma) : MetaM (List (Expr × Expr × Array Name × Bool)) :=
   /- Currently, we don't have any means of determining which lemmas are originally from the goal, so for now, we are
      indicating that all lemmas don't come from the goal. This behavior should be updated once we get a means of tracking
      that information through the monomorphization procedure. -/
-  lemmas.toList.mapM (fun lem => return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params, false))
+  lemmas.toList.mapM
+    (fun lem => do
+      let derivLeaves := getLeavesFromDTr lem.deriv
+      let isFromGoal := derivLeaves.contains "true"
+      return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params, isFromGoal))
 
 /-- Given `formulas`, `instanceMaxHeartbeats`, and an instance of Duper `inst`, runs `inst` with monomorphization preprocessing. -/
 def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMaxHeartbeats : Nat)
@@ -432,8 +442,8 @@ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array
   let prover : Array Auto.Lemma → MetaM Expr :=
     fun lemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
-      trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => f.1)}"
-      trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => f.1)}"
+      trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
+      trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => (f.1, f.2.2.2))}"
       inst monomorphizedFormulas instanceMaxHeartbeats
   Auto.monoInterface lemmas inhFacts prover
 
@@ -448,8 +458,8 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra
   let prover : Array Auto.Lemma → MetaM Expr :=
     fun lemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
-      trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => f.1)}"
-      trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => f.1)}"
+      trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
+      trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => (f.1, f.2.2.2))}"
       inst monomorphizedFormulas instanceMaxHeartbeats
   Auto.runNativeProverWithAuto declName? prover lemmas inhFacts
 

README.md

@@ -7,7 +7,7 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle
 To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add:
 
 ```lean
-require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.8"
+require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.10"
 ```
 
 Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [std4](https://github.com/leanprover/std4.git), then it uses the same version of std4 as the Duper branch of [Auto](https://github.com/leanprover-community/lean-auto.git). This step is necessary because Duper depends on Auto which depends on std4, so errors can arise if your project attempts to import a version of std4 different from the one imported by Duper.

lake-manifest.json

@@ -4,19 +4,19 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "b53593923a1423ae145c47c66306a68b6d0fbf44",
+   "rev": "1507142f79f05371e5eb25202eec6396bb940d72",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.6",
+   "inputRev": "1507142f79f05371e5eb25202eec6396bb940d72",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v0.0.6"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"1507142f79f05371e5eb25202eec6396bb940d72"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.7.0-rc2