Dev

Duper/Rules/DatatypeDistinctness.lean

@@ -12,6 +12,10 @@ open Meta
 
 initialize Lean.registerTraceClass `duper.rule.datatypeDistinctness
 
+-- **TODO** As of `v4.27.0`, proof reconstruction for this inference broke. This is due to a change in how Lean
+-- generates `noConfusion` theorems for inductive datatypes. Once `mkDatatypeDistinctnessProof` is corrected to
+-- match the new format, this inference can be re-enabled.
+
 /-- Returns `none` if `lit` does not compare distinct constructors, returns `some false` if `lit` says two distinct
     constructors are equal, and returns `some true` if `lit` says two distinct constructors are not equal. -/
 def litComparesDistinctConstructors (lit : Lit) : MetaM (Option Bool) := do
@@ -51,9 +55,22 @@ def mkDatatypeDistinctnessProof (refs : List (Option Nat)) (premises : List Expr
         let some (tyName, numParams, lvls) ← matchConstInduct lit.ty.getAppFn' (fun _ => pure none) matchConstInductK
           | throwError "mkDistPosProof :: Failed to find the inductive datatype corresponding to {lit.ty}"
         let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
-          let noConfusionArgs := #[some (mkConst ``False), none, none, some h]
-          -- noConfusion first takes `numParams` arguments for parameters, so we need to add that many `none`s to the front of `noConfusionArgs`
-          let noConfusionArgs := (Array.range numParams).map (fun _ => none) ++ noConfusionArgs
+          /- The strucure of `noConfusion`'s arguments is as follows (as of `v4.27.0`):
+              - `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 `(*)`
+              - `noConfusion` then takes in one element of the datatype instantiated with the previous `numParams` parameters.
+              - `noConfusion` then takes in another `numParams` arguments of the form `param : Type universe_param`. Call this list of parameters `(**)`
+              - `noConfusion` then takes in another element of the datatype instantiated with the previous `numParams` parameters.
+              - `noConfusion` then takes in `numParams` proofs that the `i`-th parameter from the first list `(*)` is equal to the `i`-th parameter
+                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 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,7 +152,8 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
+      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
@@ -177,7 +178,8 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
+      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
@@ -224,7 +226,8 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
+      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
@@ -248,7 +251,8 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
-      datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      -- **TODO** `datatypeDistinctness` can be re-added once the inference is updated to be compatible with `v4.27.0`
+      -- datatypeDistinctness.toSimpRule, -- Inductive datatype rule
       datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,

Duper/Tests/temp.lean

@@ -44,3 +44,40 @@ 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

@@ -713,6 +713,9 @@ 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
 
@@ -721,6 +724,7 @@ example : const3 (Type 8) ≠ const4 (Type 8) := by
 
 example : const5 ≠ const6 const5 := by
   duper
+-/
 
 example : [] ≠ [2] := by
   duper

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" @ "v4.26.0"
+require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.27.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": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
+   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e66058117f0d073914c2c1f674b880537d9eb2e",
+   "rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-hammer",
+   "inputRev": "v4.27.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.26.0-hammer"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.26.0"
+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"
 
 package Duper {
   precompileModules := true

lean-toolchain

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