Dev

Duper/Fingerprint.lean

@@ -138,7 +138,7 @@ def gfpf [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : ExprPos) : m Fingerpri
     we can add a step to the beginning to this function that converts e to η-long β-reduced normal form.
 
     Note: The output of this function is not guaranteed (or expected) to be well-formed. -/
-def transformToUntypedFirstOrderTerm [Monad m] [MonadLiftT MetaM m] (e : Expr) : m Expr := do
+partial def transformToUntypedFirstOrderTerm [Monad m] [MonadLiftT MetaM m] (e : Expr) : m Expr := do
   match e with
   | Expr.forallE _ _ b _ => transformToUntypedFirstOrderTerm b
   | Expr.lam _ _ b _ => transformToUntypedFirstOrderTerm b
@@ -159,7 +159,7 @@ def transformToUntypedFirstOrderTerm [Monad m] [MonadLiftT MetaM m] (e : Expr) :
      -/
     return .bvar bvarNum
   | Expr.mdata _ e => transformToUntypedFirstOrderTerm e
-  | Expr.letE _ _ _ _ _ => panic! s!"The letE expression {e} should have been removed by zeta reduction"
+  | Expr.letE _ _ v b _ => transformToUntypedFirstOrderTerm (b.instantiate1 v)
   -- Strip away levels
   | Expr.const name _ => return Expr.const name []
   | _ => return e -- Expr.fvar, Expr.mvar, Expr.lit, Expr.const, and Expr.sort cases

Duper/Rules/DatatypeDistinctness.lean

@@ -56,6 +56,11 @@ def mkDatatypeDistinctnessProof (refs : List (Option Nat)) (premises : List Expr
           | throwError "mkDistPosProof :: Failed to find the inductive datatype corresponding to {lit.ty}"
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
           /- The strucure of `noConfusion`'s arguments is as follows (as of `v4.27.0`):
+              If `lit.ty` has zero parameters then `noConfusion` takes exactly four arguments:
+              - `P : Sort u` which serves as the motive of the `noConfusionType`
+              - Two arguments with type `lit.ty`
+              - A final argument equating the two previous arguments
+              If `lit.ty` has one or more parameters then:
               - `noConfusion` first takes in `P : Sort u` which serves as the motive of the `noConfusionType`. The datatype distinctness inference
                 always instantiates `P` with `False`
               - `noConfusion` then takes in `numParams` arguments of the form `param : Type universe_param`. Call this list of parameters `(*)`
@@ -66,11 +71,12 @@ def mkDatatypeDistinctnessProof (refs : List (Option Nat)) (premises : List Expr
                 from the second list `(**)`. The datatype distinctness inference instantiates all of these with `rfl`.
               - `noConfusion` finally takes in a proof that the first element of the datatype is equal to the second element of the datatype (this is expressed
                 in terms of a heterogeneous equality). The datatype distinctness inference always instantiates this last argument with `heq_of_eq h`. -/
-          -- **TODO** Structure is different when the inductive datatype has no parameters to equate
-          -- **TODO** `rfl`'s type needs to be instantiated
-          let noConfusionArgs :=
-            #[some (mkConst ``False)] ++ (Array.range (2 * numParams + 2)).map (fun _ => none) ++
-            (← (Array.range (2 * numParams + 2)).mapM (fun _ => do pure $ some (← mkAppM ``rfl #[]))) ++ #[some (← mkAppM ``heq_of_eq #[h])]
+          let noConfusionArgs ←
+            if numParams = 0 then
+              pure $ #[some (mkConst ``False), none, none, some h]
+            else
+              pure $ #[some (mkConst ``False)] ++ (Array.range (2 * numParams + 2)).map (fun _ => none) ++
+                (← (Array.range numParams).mapM (fun x => do pure $ some (← mkAppOptM ``rfl #[none, some (lit.ty.getAppArgs[x]!)]))) ++ #[some (← mkAppM ``heq_of_eq #[h])]
           let proofCase ← mkAppOptM' (mkConst (.str tyName "noConfusion") (0 :: lvls)) noConfusionArgs
           let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
           Meta.mkLambdaFVars #[h] proofCase

Duper/Saturate.lean

@@ -152,8 +152,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
-      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
@@ -178,8 +177,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
-      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
@@ -226,8 +224,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
-      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
@@ -251,8 +248,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
-      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,

Duper/Tests/temp.lean

@@ -44,40 +44,3 @@ example (sum : myProd Int Int → Int)
     let _mk_sel0 : myProd Int Int → Int := myProd.rec (motive := fun _ => Int) fun arg0 arg1 => arg0
     _mk_sel0 x = 0 := sorry -- This triggers `unfoldProj :: myProd is not a structure`
   duper [*] {portfolioInstance := 1}
-
--- PANIC at Duper.RootCFPTrie.transformToUntypedFirstOrderTerm Duper.Fingerprint:162:27...
-example (x y : Nat) (hx : x ≤ 100) (hy : y ≤ 100)
-  (hxy : x * y ≥ 7625) : x + y ≥ 150 := by
-  have :
-    have _let_1 := Int.ofNat x + Int.ofNat y;
-    ¬Int.ofNat 150 ≤ _let_1 → ¬_let_1 ≥ Int.ofNat 150 :=
-    sorry
-  have :
-    (Eq (α := Nat → Prop) (fun (a : Nat) => True) fun (_n : Nat) => Int.ofNat _n ≥ Int.ofNat 0) ∧ (fun (a : Nat) => True) x →
-      Int.ofNat x ≥ Int.ofNat 0 :=
-    sorry
-  have : Int.ofNat y ≤ Int.ofNat 100 → ¬Int.ofNat y ≥ Int.ofNat 101 := sorry
-  have :
-    (Eq (α := Nat → Prop) (fun (a : Nat) => True) fun (_n : Nat) => Int.ofNat _n ≥ Int.ofNat 0) ∧ (fun (a : Nat) => True) y →
-      Int.ofNat y ≥ Int.ofNat 0 :=
-    sorry
-  have : Int.ofNat 7625 ≤ Int.ofNat x * Int.ofNat y → Int.ofNat x * Int.ofNat y ≥ Int.ofNat 7625 := sorry
-  have : Int.ofNat x ≤ Int.ofNat 100 → ¬Int.ofNat x ≥ Int.ofNat 101 := sorry
-  have : (¬Int.ofNat x ≥ Int.ofNat 0 ∨ Int.ofNat x = Int.ofNat 0) ∨ Int.ofNat x ≥ Int.ofNat 1 := sorry
-  have : Int.ofNat x > Int.ofNat 0 → Int.ofNat x ≥ Int.ofNat 1 := sorry
-  have :
-    have _let_1 := Int.ofNat x * Int.ofNat y;
-    ¬_let_1 ≥ Int.ofNat 7625 ∨ ¬_let_1 = Int.ofNat 0 :=
-    sorry
-  have : Int.ofNat y = Int.ofNat 0 → Int.ofNat x * Int.ofNat y = Int.ofNat 0 := sorry
-  have :
-    have _let_1 := Int.ofNat x * Int.ofNat y;
-    have _let_2 := -Int.ofNat 1 * _let_1;
-    (_let_1 ≥ Int.ofNat 7625 ∧ Int.ofNat 101 * Int.ofNat y + _let_2 ≥ Int.ofNat 1) ∧
-        Int.ofNat 101 * Int.ofNat x + _let_2 ≥ Int.ofNat 1 →
-      Int.ofNat x + Int.ofNat y ≥ Int.ofNat 150 :=
-    sorry
-  have : (¬Int.ofNat y ≥ Int.ofNat 0 ∨ Int.ofNat y = Int.ofNat 0) ∨ Int.ofNat y ≥ Int.ofNat 1 := sorry
-  have : Int.ofNat y > Int.ofNat 0 → Int.ofNat y ≥ Int.ofNat 1 := sorry
-  have : Int.ofNat x = Int.ofNat 0 → Int.ofNat x * Int.ofNat y = Int.ofNat 0 := sorry
-  duper [*]

Duper/Tests/test_regression.lean

@@ -604,7 +604,7 @@ end UniverseTest
 
 namespace RecursorTests
 
-inductive Color1 :=
+inductive Color1 where
 | red : Color1
 
 example : @Color1.rec (fun _ => Nat) a .red = a := by duper [Color1.rec]
@@ -713,9 +713,6 @@ inductive myEmpty (t1 : Type _) (t2 : Type _)
 
 open myType myType2 myType3 myType4
 
-/- **TODO** These tests require the datatypeDistinctness inference which is currently disabled
-   as of `v4.27.0` due to a change in how datatypes' `noConfusion` theorem is generated.
-   See Duper/Rules/DatatypeDistinctness.lean for more details.
 example : const1 ≠ const2 := by
   duper
 
@@ -724,7 +721,6 @@ example : const3 (Type 8) ≠ const4 (Type 8) := by
 
 example : const5 ≠ const6 const5 := by
   duper
--/
 
 example : [] ≠ [2] := by
   duper

Duper/Util/Reduction.lean

@@ -28,11 +28,12 @@ def getReduceInstancesM : CoreM Bool := do
 
 /-- This function is expensive and should only be used in preprocessing -/
 partial def preprocessFact (fact : Expr) : MetaM Expr := do
+  let red (e : Expr) : MetaM TransformStep := do
+    trace[duper.preprocessing.debug] "e before calling red: {e}"
+    let e := e.consumeMData
+    let e ← whnf e
+    return .continue e
   if (← getReduceInstancesM) then
-    let red (e : Expr) : MetaM TransformStep := do
-      let e := e.consumeMData
-      let e ← whnf e
-      return .continue e
     -- Reduce
     trace[duper.preprocessing.debug] "fact before preprocessing: {fact}"
     let fact ← withTransparency .instances <| Meta.transform fact (pre := red) (usedLetOnly := false)
@@ -48,8 +49,12 @@ partial def preprocessFact (fact : Expr) : MetaM Expr := do
     trace[duper.preprocessing.debug] "fact after preprocessing: {fact}"
     return fact
   else
-    trace[duper.preprocessing.debug] "reduceInstances option is set to false, only applying zeta reduction"
-    zetaReduce fact
+    trace[duper.preprocessing.debug] "reduceInstances option is set to false, only applying zeta reduction and reducing let expressions"
+    trace[duper.preprocessing.debug] "fact before preprocessing: {fact}"
+    let fact ← withTransparency .reducible <| Meta.transform fact (pre := red) (usedLetOnly := false)
+    let fact ← zetaReduce fact
+    trace[duper.preprocessing.debug] "fact after preprocessing: {fact}"
+    return fact
 
 /-- Eta-expand a beta-reduced expression. This function is currently unused -/
 partial def etaLong (e : Expr) : MetaM Expr := do

README.md

@@ -4,23 +4,23 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle
 
 ## Adding Duper to an existing project
 
-To add Duper for `v4.27.0` to an existing project with a `lakefile.toml` file, add the following dependency:
+To add Duper for `v4.28.0` to an existing project with a `lakefile.toml` file, add the following dependency:
 
 ```toml
 [[require]]
 name = "Duper"
 git = "https://github.com/leanprover-community/duper.git"
-rev = "v4.27.0"
+rev = "v4.28.0"
 ```
 The file `lean-toolchain` should contain the following:
 ```
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0
 ```
 
 If you have a project with a `lakefile.lean` instead of `lakefile.toml`, you can use this instead:
 
 ```lean
-require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.27.0"
+require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.28.0"
 ```
 
 Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [batteries](https://github.com/leanprover-community/batteries), then it uses the same version of batteries as Duper. This step is necessary because Duper depends on batteries, so errors can arise if your project attempts to import a version of batteries different from the one imported by Duper.

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3",
+   "rev": "1f8a3b2f31366ec7da2a160e634004c52be6631e",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-hammer",
+   "inputRev": "v4.28.0-hammer",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.27.0-hammer"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.27.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.28.0-hammer"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.28.0"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0