From b1a964c9d754a19752da64b9815cd90f10dabd9f Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 31 Jan 2026 16:00:39 -0500 Subject: [PATCH 1/3] Resolve datatype distinctness bug --- Duper/Rules/DatatypeDistinctness.lean | 16 +++++++++++----- Duper/Saturate.lean | 12 ++++-------- Duper/Tests/test_regression.lean | 4 ---- 3 files changed, 15 insertions(+), 17 deletions(-) diff --git a/Duper/Rules/DatatypeDistinctness.lean b/Duper/Rules/DatatypeDistinctness.lean index 32b29b8..5159252 100644 --- a/Duper/Rules/DatatypeDistinctness.lean +++ b/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 diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean index 67b11a8..f26e69a 100644 --- a/Duper/Saturate.lean +++ b/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, diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index f85a3aa..435ab96 100644 --- a/Duper/Tests/test_regression.lean +++ b/Duper/Tests/test_regression.lean @@ -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 From 8cfd6c4c4b1695607c2d5941c729f1e11ab3b39d Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 2 Feb 2026 16:15:26 -0500 Subject: [PATCH 2/3] Resolve bug relating to unreduced let expressions --- Duper/Fingerprint.lean | 4 ++-- Duper/Tests/temp.lean | 37 ------------------------------------- Duper/Util/Reduction.lean | 17 +++++++++++------ 3 files changed, 13 insertions(+), 45 deletions(-) diff --git a/Duper/Fingerprint.lean b/Duper/Fingerprint.lean index 2636942..aebd6c0 100644 --- a/Duper/Fingerprint.lean +++ b/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 diff --git a/Duper/Tests/temp.lean b/Duper/Tests/temp.lean index d6f6286..3f7537b 100644 --- a/Duper/Tests/temp.lean +++ b/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 [*] diff --git a/Duper/Util/Reduction.lean b/Duper/Util/Reduction.lean index 8038bd2..999b150 100644 --- a/Duper/Util/Reduction.lean +++ b/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 From 82606cd26168cb5e30e8e47375f0b3f091e769e0 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Wed, 18 Feb 2026 22:42:29 -0500 Subject: [PATCH 3/3] Update to v4.28.0 --- Duper/Tests/test_regression.lean | 2 +- README.md | 8 ++++---- lake-manifest.json | 8 ++++---- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index 435ab96..5ddac53 100644 --- a/Duper/Tests/test_regression.lean +++ b/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] diff --git a/README.md b/README.md index 39f8724..a0660c0 100644 --- a/README.md +++ b/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. diff --git a/lake-manifest.json b/lake-manifest.json index 870ed41..da2367d 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lakefile.lean b/lakefile.lean index 092a77a..9cce340 100644 --- a/lakefile.lean +++ b/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 diff --git a/lean-toolchain b/lean-toolchain index 5249182..4c685fa 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0 +leanprover/lean4:v4.28.0