From 1a6c36380a1713bd370099c24d59aac97a83e471 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Wed, 3 Jul 2024 16:49:58 -0400
Subject: [PATCH 01/10] Added (limited) ability to collect inductive datatypes
 for the purpose of generating datatype exhaustiveness facts

---
 Duper/Interface.lean                |  15 ++-
 Duper/Preprocessing.lean            | 164 ++++++++++++++++++++++++++++
 Duper/Rules/DatatypeAcyclicity.lean |   7 +-
 Duper/Saturate.lean                 |  18 ++-
 Main.lean                           |   3 +-
 5 files changed, 196 insertions(+), 11 deletions(-)

diff --git a/Duper/Interface.lean b/Duper/Interface.lean
index 4c46769..970b966 100644
--- a/Duper/Interface.lean
+++ b/Duper/Interface.lean
@@ -22,12 +22,20 @@ register_option duper.throwPortfolioErrors : Bool := {
   descr := "Whether to halt portfolio mode and throw an error if a subinstance throws an error"
 }
 
+register_option duper.collectDatatypes : Bool := {
+  defValue := false
+  descr := "Whether to collect inductive datatypes for the purpose of generating datatype exhaustiveness facts"
+}
+
 def getPrintPortfolioInstance (opts : Options) : Bool :=
   duper.printPortfolioInstance.get opts
 
 def getThrowPortfolioErrors (opts : Options) : Bool :=
   duper.throwPortfolioErrors.get opts
 
+def getCollectDataTypes (opts : Options) : Bool :=
+  duper.collectDatatypes.get opts
+
 def getPrintPortfolioInstanceM : CoreM Bool := do
   let opts ← getOptions
   return getPrintPortfolioInstance opts
@@ -36,6 +44,10 @@ def getThrowPortfolioErrorsM : CoreM Bool := do
   let opts ← getOptions
   return getThrowPortfolioErrors opts
 
+def getCollectDataTypesM : CoreM Bool := do
+  let opts ← getOptions
+  return getCollectDataTypes opts
+
 declare_syntax_cat Duper.bool_lit (behavior := symbol)
 
 syntax "true" : Duper.bool_lit
@@ -376,6 +388,7 @@ def formulasToMessageData : Expr × Expr × Array Name × Bool → MessageData
     then duper will run until it is timed out by the Core `maxHeartbeats` option). If Duper succeeds in deriving a contradiction and constructing
     a proof for it, then `runDuper` returns that proof as an expression. Otherwise, Duper will throw an error. -/
 def runDuper (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMaxHeartbeats : Nat) : MetaM Expr := do
+  let generateDatatypeExhaustivenessFacts ← getCollectDataTypesM
   let state ←
     withNewMCtxDepth do
       let formulas ← unfoldDefinitions formulas
@@ -387,7 +400,7 @@ def runDuper (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMax
         let skSorryName ← addSkolemSorry
         let (_, state) ←
           ProverM.runWithExprs (ctx := {}) (s := {instanceMaxHeartbeats := instanceMaxHeartbeats, skolemSorryName := skSorryName})
-            ProverM.saturateNoPreprocessingClausification
+            (ProverM.saturateNoPreprocessingClausification generateDatatypeExhaustivenessFacts)
             formulas
         pure state
   match state.result with
diff --git a/Duper/Preprocessing.lean b/Duper/Preprocessing.lean
index 63f24cb..bf927ce 100644
--- a/Duper/Preprocessing.lean
+++ b/Duper/Preprocessing.lean
@@ -16,6 +16,7 @@ open SimpResult
 
 initialize
   registerTraceClass `duper.unaryFirst.debug
+  registerTraceClass `duper.collectDatatypes.debug
 
 /-- Naively applies clausificationStep.toSimpRule to everything in the passive set (and everything produced by
     clausifying clauses in the passive set) without removing anything from the passive set. This preprocessing
@@ -94,6 +95,96 @@ partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : HashMap Sy
   | Expr.bvar .. => return symbolFreqArityMap
   | Expr.lit .. => return symbolFreqArityMap
 
+/-- Checks whether the type `t` is an inductive datatype that is not a type class-/
+def isInductiveAndNotTypeClass (t : Expr) : ProverM Bool := do
+  let isInductiveDatatype ← matchConstInduct t.getAppFn' (fun _ => pure false) (fun _ _ => pure true)
+  let isClass := Option.isSome $ ← isClass? t
+  return isInductiveDatatype && !isClass
+
+/-- Updates symbolFreqArityMap to increase the count of all symbols that appear in f (and if a symbol in f appears n
+    times, then updates f's result in symbolFreqMap to be n greater than it was originally). Note that as with Expr.weight,
+    this function may require revision to be more similar to Zipperposition's implementation once we actually start working
+    on higher order things. Additionally, updates datatypeList to make sure that all inductive datatypes that appear
+    in the problem are contained in the datatypeList. -/
+partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityMap : HashMap Symbol (Nat × Nat))
+  (datatypeList : List Expr) : ProverM (HashMap Symbol (Nat × Nat) × List Expr) := do
+  match f with
+  | Expr.fvar fVarId =>
+    let fSymbol := Symbol.FVarId fVarId
+    match symbolFreqArityMap.find? fSymbol with
+    | some (fFreq, fArity) => return (symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity), datatypeList)
+    | none =>
+      match (← getLCtx).fvarIdToDecl.find? fVarId with
+      | some fDecl =>
+        let fType := fDecl.type
+        let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+        if fTypeIsInductive && !datatypeList.contains fType then
+          return (symbolFreqArityMap.insert fSymbol (1, getArity fType), fType :: datatypeList)
+        else
+          return (symbolFreqArityMap.insert fSymbol (1, getArity fType), datatypeList)
+      | none => throwError s!"Unable to find {fVarId.name} in local context"
+  | Expr.const name _ =>
+    let fSymbol := Symbol.Const name
+    match symbolFreqArityMap.find? fSymbol with
+    | some (fFreq, fArity) => -- fSymbol has already been seen so datatypeList does not need to be updated
+      return (symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity), datatypeList)
+    | none =>
+      let fType ← inferType f
+      let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+      if fTypeIsInductive && !datatypeList.contains fType then
+        return (symbolFreqArityMap.insert fSymbol (1, getArity fType), fType :: datatypeList)
+      else
+        return (symbolFreqArityMap.insert fSymbol (1, getArity fType), datatypeList)
+  | Expr.app f1 f2 =>
+    let fType ← inferType f
+    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    let datatypeList :=
+      if fTypeIsInductive && !datatypeList.contains fType then fType :: datatypeList
+      else datatypeList
+    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList f1 symbolFreqArityMap datatypeList
+    updateSymbolFreqArityMapAndDatatypeList f2 symbolFreqArityMap' datatypeList'
+  | Expr.lam _ t b _ =>
+    let tIsInductive ← isInductiveAndNotTypeClass t
+    let datatypeList :=
+      if tIsInductive && !datatypeList.contains t then t :: datatypeList
+      else datatypeList
+    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
+    updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
+  | Expr.forallE _ t b _ =>
+    let tIsInductive ← isInductiveAndNotTypeClass t
+    let datatypeList :=
+      if tIsInductive && !datatypeList.contains t then t :: datatypeList
+      else datatypeList
+    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
+    updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
+  | Expr.letE _ _ v b _ =>
+    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList v symbolFreqArityMap datatypeList
+    updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
+  | Expr.proj _ _ b =>
+    let fType ← inferType f
+    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    if fTypeIsInductive && !datatypeList.contains fType then
+      updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap (fType :: datatypeList)
+    else
+      updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap datatypeList
+  | Expr.mdata _ b => updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap datatypeList
+  | Expr.sort .. => return (symbolFreqArityMap, datatypeList)
+  | Expr.mvar .. =>
+    let fType ← inferType f
+    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    if fTypeIsInductive && !datatypeList.contains fType then
+      return (symbolFreqArityMap, fType :: datatypeList)
+    else
+      return (symbolFreqArityMap, datatypeList)
+  | Expr.bvar .. => return (symbolFreqArityMap, datatypeList)
+  | Expr.lit .. =>
+    let fType ← inferType f
+    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    if fTypeIsInductive && !datatypeList.contains fType then
+      return (symbolFreqArityMap, fType :: datatypeList)
+    else
+      return (symbolFreqArityMap, datatypeList)
+
 /-- Builds a HashMap that maps each symbol to a tuple containing:
     - The number of times they appear in formulas
     - Its arity -/
@@ -106,6 +197,27 @@ partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (HashMap S
   trace[duper.unaryFirst.debug] "symbolFreqArityMap: {symbolFreqArityMap.toArray}"
   return symbolFreqArityMap
 
+/-- Builds:
+    - A HashMap that maps each symbol to a tuple containing:
+      - The number of times they appear in formulas
+      - Its arity
+    - A list containing every inductive datatype that appears in any clause
+    Note: The current code does not yet support polymorphic inductive datatypes -/
+partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat) × List Expr) := do
+  let mut symbolFreqArityMap := HashMap.empty
+  let mut datatypeList := []
+  for c in clauses do
+    -- In order to accurately collect inductive datatypes, I need to use mclauses rather than clauses.
+    -- This ensures, for instance, that polymorphic lists will appear as `List ?m` rather than `List #1`.
+    let c ← runRuleM $ loadClause c
+    trace[duper.collectDatatypes.debug] "Loaded clause c: {c.lits}"
+    for l in c.lits do
+      (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList l.lhs symbolFreqArityMap datatypeList
+      (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList l.rhs symbolFreqArityMap datatypeList
+  trace[duper.unaryFirst.debug] "symbolFreqArityMap: {symbolFreqArityMap.toArray}"
+  trace[duper.collectDatatypes.debug] "datatypeList collected by buildSymbolFreqArityMapAndDatatypeList: {datatypeList}"
+  return (symbolFreqArityMap, datatypeList)
+
 /-- Builds the symbolPrecMap from the input assumptions. Note that lower numbers in the symbol prec
     map correspond to higher precedences (so that symbol s is maximal iff s maps to 0).
 
@@ -160,3 +272,55 @@ def buildSymbolPrecMap (clauses : List Clause) : ProverM (SymbolPrecMap × Bool)
     counter := counter + 1
   trace[duper.unaryFirst.debug] "symbolPrecMap: {symbolPrecMap.toArray}"
   return (symbolPrecMap, highesetPrecSymbolHasArityZero)
+
+/-- Like `buildSymbolPrecMap` but it also returns a list of all inductive datatypes that appear in any clause.
+    Note: The current code does not yet support polymorphic inductive datatypes -/
+def buildSymbolPrecMapAndDatatypeList (clauses : List Clause) : ProverM (SymbolPrecMap × Bool × List Expr) := do
+  let (symbolFreqArityMap, datatypeList) ← buildSymbolFreqArityMapAndDatatypeList clauses
+  trace[duper.collectDatatypes.debug] "datatypeList collected by buildSymbolPrecMap: {datatypeList}"
+  let mut symbolPrecArr : Array (Symbol × Nat × Nat) := #[]
+  let lctx ← getLCtx
+  -- unaryFirstGt sorts implements the greater-than test for the unary_first precedence generation scheme
+  let unaryFirstGt : (Symbol × Nat × Nat) → (Symbol × Nat × Nat) → Bool :=
+    fun (s1, s1Freq, s1Arity) (s2, s2Freq, s2Arity) =>
+      if s1Arity == 1 && s2Arity != 1 then true
+      else if s2Arity == 1 && s1Arity != 1 then false
+      else if s1Arity > s2Arity then true
+      else if s2Arity > s1Arity then false
+      else -- s1Arity == s2Arity, so use frequency as a tie breaker (rarer symbols have greater precedence)
+        if s1Freq < s2Freq then true
+        else if s2Freq < s1Freq then false
+        else -- Array.binInsert requires the lt define a total (rather than merely partial) ordering, so tiebreak by symbol
+          match s1, s2 with
+          | Symbol.FVarId _, Symbol.Const _ => true
+          | Symbol.Const _, Symbol.FVarId _ => false
+          | Symbol.Const c1, Symbol.Const c2 => c1.toString < c2.toString
+          | Symbol.FVarId fVarId1, Symbol.FVarId fVarId2 =>
+              -- Tiebreaking fVarId1 and fVarId2 by name would cause duper's behavior to depend on the environment in unexpected ways,
+              -- so we instead tiebreak based on whether fVarId1 or fVarId2 appears first in the local context
+              let firstFVarIdInDecls :=
+                lctx.decls.findSome?
+                  (fun declOpt =>
+                    match declOpt with
+                    | some decl =>
+                        if decl.fvarId == fVarId1 || decl.fvarId == fVarId2 then some decl.fvarId
+                        else none
+                    | none => none)
+              match firstFVarIdInDecls with
+              | some firstFVarId =>
+                if firstFVarId == fVarId1 then true
+                else false
+              | none => false -- This case isn't possible because fVarId1 and fVarId2 must both appear in the local context
+  for (s, sFreq, sArity) in symbolFreqArityMap.toArray do
+    -- We use unaryFirstGt as the lt argument for binInsert so that symbols with higher precedence come first in symbolPrecArray
+    symbolPrecArr := symbolPrecArr.binInsert unaryFirstGt (s, sFreq, sArity)
+  trace[duper.unaryFirst.debug] "symbolPrecArr: {symbolPrecArr}"
+  let mut symbolPrecMap := HashMap.empty
+  let mut counter := 0
+  let mut highesetPrecSymbolHasArityZero := false
+  for (s, _, sArity) in symbolPrecArr do
+    if counter == 0 && sArity == 0 then highesetPrecSymbolHasArityZero := true
+    symbolPrecMap := symbolPrecMap.insert s counter -- Map s to its index in symbolPrecArr
+    counter := counter + 1
+  trace[duper.unaryFirst.debug] "symbolPrecMap: {symbolPrecMap.toArray}"
+  return (symbolPrecMap, highesetPrecSymbolHasArityZero, datatypeList)
diff --git a/Duper/Rules/DatatypeAcyclicity.lean b/Duper/Rules/DatatypeAcyclicity.lean
index 56ce345..193395b 100644
--- a/Duper/Rules/DatatypeAcyclicity.lean
+++ b/Duper/Rules/DatatypeAcyclicity.lean
@@ -59,11 +59,10 @@ def mkDatatypeAcyclicityProof (removedLitNum : Nat) (litSide : LitSide) (premise
           let litTyMVar ← mkFreshExprMVar lit.ty
           let abstrLam ← mkLambdaFVars #[litTyMVar] $ ← mkAppOptM ``sizeOf #[some lit.ty, some sizeOfInst, some litTyMVar]
           let sizeOfEq ← mkAppM ``congrArg #[abstrLam, h] -- Has the type `sizeOf lit.lhs = sizeOf lit.rhs`
+          -- Need to generate a term of type `¬(sizeOf lit.lhs = sizeOf lit.rhs)`
           let sizeOfEqFalseMVar ← mkFreshExprMVar $ ← mkAppM ``Not #[← inferType sizeOfEq] -- Has the type `¬(sizeOf lit.lhs = sizeOf lit.rhs)`
           let sizeOfEqFalseMVarId := sizeOfEqFalseMVar.mvarId!
-          -- **TODO**: Figure out how to assign `sizeOfEqFalseMVar` an actual term (ideally generated by `simp_arith`)
-          -- The below lines attempts to use the omega procedure to generate a term for `sizeOfEqFalseMVar`, but it doesn't work
-          Elab.Tactic.Omega.omega [] sizeOfEqFalseMVarId -- Use the `omega` tactic to prove `¬(sizeOf lit.lhs = sizeOf lit.rhs)`
+          -- **TODO**: Figure out how to assign `sizeOfEqFalseMVar` an actual term
           let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body $ mkApp sizeOfEqFalseMVar sizeOfEq -- Has the type `body`
           trace[duper.rule.datatypeAcyclicity] "lit: {lit}, lit.ty: {lit.ty}, sizeOfInst: {sizeOfInst}, abstrLam: {abstrLam}, sizeOfEq: {sizeOfEq}"
           trace[duper.rule.datatypeAcyclicity] "sizeOfEqFalseMVar: {sizeOfEqFalseMVar}, proofCase: {proofCase}"
@@ -85,7 +84,7 @@ def datatypeAcyclicity : MSimpRule := fun c => do
     | some side =>
       if lit.sign then -- `lit` is never true so `lit` can be removed from `c`
         let res := c.eraseIdx i
-        let yC ← yieldClause res "datatypeAcyclicity" none -- mkDatatypeAcyclicityProof i side
+        let yC ← yieldClause res "datatypeAcyclicity" none -- $ mkDatatypeAcyclicityProof i side
         trace[duper.rule.datatypeAcyclicity] "datatypeAcyclicity applied to {c.lits} to yield {yC.1}"
         return some #[yC]
       else -- `lit` is a tautology so the clause `c` can simply be removed
diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean
index cc87a7a..cf637f6 100644
--- a/Duper/Saturate.lean
+++ b/Duper/Saturate.lean
@@ -298,6 +298,8 @@ partial def saturate : ProverM Unit := do
       printTimeoutDebugStatements startTime
       throw e
 
+/-- Note: This definition is outdated (does not support datatype exhaustiveness reasoning). See `saturateNoPreprocessingClausification`
+    for additions that need to be made to make this usable. -/
 def clausifyThenSaturate : ProverM Unit := do
   Core.withCurrHeartbeats $
     preprocessingClausification;
@@ -306,12 +308,18 @@ def clausifyThenSaturate : ProverM Unit := do
     setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero;
     saturate
 
-def saturateNoPreprocessingClausification : ProverM Unit := do
+def saturateNoPreprocessingClausification (generateDatatypeExhaustivenessFacts : Bool) : ProverM Unit := do
   Core.withCurrHeartbeats $ do
-    let (symbolPrecMap, highesetPrecSymbolHasArityZero) ← buildSymbolPrecMap (← getPassiveSet).toList;
-    setSymbolPrecMap symbolPrecMap;
-    setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero;
-    saturate
+    if generateDatatypeExhaustivenessFacts then
+      let (symbolPrecMap, highesetPrecSymbolHasArityZero, datatypeList) ← buildSymbolPrecMapAndDatatypeList (← getPassiveSet).toList;
+      setSymbolPrecMap symbolPrecMap;
+      setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero;
+      saturate
+    else
+      let (symbolPrecMap, highesetPrecSymbolHasArityZero) ← buildSymbolPrecMap (← getPassiveSet).toList;
+      setSymbolPrecMap symbolPrecMap;
+      setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero;
+      saturate
 
 end ProverM
 
diff --git a/Main.lean b/Main.lean
index 67383e7..f7e7f36 100644
--- a/Main.lean
+++ b/Main.lean
@@ -15,6 +15,7 @@ open ProverM
     then duper will run until it is timed out by the Core `maxHeartbeats` option). If Duper succeeds in deriving a contradiction and constructing
     a proof for it, then `runDuper` returns that proof as an expression. Otherwise, Duper will throw an error. -/
 def runDuperOnTPTP (fileName : String) (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMaxHeartbeats : Nat) : MetaM Unit := do
+  let generateDatatypeExhaustivenessFacts ← getCollectDataTypesM
   let state ←
     withNewMCtxDepth do
       let formulas ← unfoldDefinitions formulas
@@ -25,7 +26,7 @@ def runDuperOnTPTP (fileName : String) (formulas : List (Expr × Expr × Array N
         let skSorryName ← addSkolemSorry
         let (_, state) ←
           ProverM.runWithExprs (ctx := {}) (s := {instanceMaxHeartbeats := instanceMaxHeartbeats, skolemSorryName := skSorryName})
-            ProverM.saturateNoPreprocessingClausification
+            (ProverM.saturateNoPreprocessingClausification generateDatatypeExhaustivenessFacts)
             formulas
         pure state
   match state.result with

From 2e837117e08e185da252d4dc15bf92b21de0a894 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Thu, 4 Jul 2024 22:10:54 -0400
Subject: [PATCH 02/10] Generate datatype exhaustiveness facts

Note: This commit does not include proof reconstruction for the
generated datatype exhaustiveness facts, and it also does not support
polymorphic inductive datatypes
---
 Duper/Rules/DatatypeExhaustiveness.lean | 67 +++++++++++++++++++++++++
 Duper/Saturate.lean                     | 18 ++++---
 2 files changed, 77 insertions(+), 8 deletions(-)
 create mode 100644 Duper/Rules/DatatypeExhaustiveness.lean

diff --git a/Duper/Rules/DatatypeExhaustiveness.lean b/Duper/Rules/DatatypeExhaustiveness.lean
new file mode 100644
index 0000000..1598ac1
--- /dev/null
+++ b/Duper/Rules/DatatypeExhaustiveness.lean
@@ -0,0 +1,67 @@
+import Duper.RuleM
+import Duper.Util.ProofReconstruction
+
+namespace Duper
+open ProverM RuleM Lean Meta
+
+initialize Lean.registerTraceClass `duper.rule.datatypeExhaustiveness
+
+/-- Given an expression `∀ x1 : t1, x2 : t2, ... xn : tn, b`, returns `[t1, t2, ..., tn]`. If the given expression is not
+    a forall expression, then `getForallArgumentTypes` just returns the empty list -/
+partial def getForallArgumentTypes (e : Expr) : List Expr :=
+  match e.consumeMData with
+  | Expr.forallE _ t b _ => t :: (getForallArgumentTypes b)
+  | _ => []
+
+/-- Creates the expression `(∃ fields, e = ctor.{lvls} params fields) = True` where `params` are the inductive datatype's parameters
+    and `fields` are arguments that need to be passed into `ctor` for the resulting expression to have the correct inductive type -/
+def makeConstructorEquality (e : Expr) (ctor : ConstructorVal) (lvls : List Level) (params : Array Expr) : MetaM Expr := do
+  if ctor.numFields = 0 then mkAppM ``Eq #[e, ← mkAppOptM' (mkConst ctor.name lvls) (params.map some)]
+  else
+    let ctorBeforeFields ← mkAppOptM' (mkConst ctor.name lvls) (params.map some)
+    let ctorType ← inferType ctorBeforeFields
+    let ctorArgTypes := getForallArgumentTypes ctorType
+    withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs => do
+      let mut res ← mkAppM ``Eq #[e, ← mkAppM' ctorBeforeFields ctorArgs]
+      for ctorArg in ctorArgs do
+        res ← mkLambdaFVars #[ctorArg] res
+        res ← mkAppM ``Exists #[res]
+      trace[duper.rule.datatypeExhaustiveness] "makeConstructorEquality :: Returning {res} from e {e} and ctor {ctor.name}"
+      mkAppM ``Eq #[res, mkConst ``True]
+
+/-- Given an inductive datatype `idt`, with constructors `ctor₁, ctor₂, ... ctorₙ`, generates a fact of the form
+    `∀ x : idt, x = ctor₁ ∨ x = ctor₂ ∨ ... x = ctorₙ` and adds it to the passive set. For example, if `idt = List Nat`,
+    then `generateDatatypeExhaustivenessFact` generates `∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l'`
+
+    Note: This code does not currently support polymorphic inductive datatypes, both because the arguments are not presently
+    collected properly, and because this code assumes that the generated clause has no parameters (which is not necessarily true
+    when `idt` is universe polymorphic) -/
+def generateDatatypeExhaustivenessFact (idt : Expr) : ProverM Unit := do
+  let some (idtIndVal, lvls) ← matchConstInduct idt.getAppFn' (fun _ => pure none) (fun ival lvls => pure (some (ival, lvls)))
+    | throwError "generateDatatypeExhaustivenessFact :: {idt} is not an inductive datatype"
+  let idtArgs := idt.getAppArgs
+  let constructors ← idtIndVal.ctors.mapM getConstInfoCtor
+  trace[duper.rule.datatypeExhaustiveness] "Inductive datatype {idt} with args {idtArgs} has constructors {constructors.map (fun x => x.name)}"
+  withLocalDeclD `_ idt fun idtFVar => do
+    match constructors with
+    | [] => -- `idt` is an inductive datatype with no constructors. This means that there cannot exist any elements of type `idt`
+      let cExp ← mkForallFVars #[idtFVar] $ mkConst ``False
+      let paramNames := #[] -- Assuming this is empty temporarily; This assumption does not hold if `idt` is universe polymorphic
+      let c := Clause.fromForallExpr paramNames cExp
+      let mkProof := fun _ _ _ _ => Lean.Meta.mkSorry cExp (synthetic := true)
+      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness (empty inductive datatype)", mkProof := mkProof} maxGoalDistance 0 #[]
+    | ctor1 :: restConstructors =>
+      let mut cBody ← makeConstructorEquality idtFVar ctor1 lvls idtArgs
+      for ctor in restConstructors do
+        let ctorEquality ← makeConstructorEquality idtFVar ctor lvls idtArgs
+        cBody ← mkAppM ``Or #[ctorEquality, cBody]
+      let cExp ← mkForallFVars #[idtFVar] cBody
+      let paramNames := #[] -- Assuming this is empty temporarily; This assumption does not hold if `idt` is universe polymorphic
+      let c := Clause.fromForallExpr paramNames cExp
+      let mkProof := fun _ _ _ _ => Lean.Meta.mkSorry cExp (synthetic := true)
+      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness", mkProof := mkProof} maxGoalDistance 0 #[]
+
+/-- For each inductive datatype in `inductiveDataTypes`, generates an exhaustiveness lemma
+    (e.g. `∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l'`) and adds it to the passive set -/
+partial def generateDatatypeExhaustivenessFacts (inductiveDataTypes : List Expr) : ProverM Unit :=
+  inductiveDataTypes.forM generateDatatypeExhaustivenessFact
diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean
index cf637f6..51e9fa1 100644
--- a/Duper/Saturate.lean
+++ b/Duper/Saturate.lean
@@ -30,6 +30,7 @@ import Duper.Rules.NeHoist
 import Duper.Rules.DatatypeDistinctness
 import Duper.Rules.DatatypeInjectivity
 import Duper.Rules.DatatypeAcyclicity
+import Duper.Rules.DatatypeExhaustiveness
 -- Higher order rules
 import Duper.Rules.ArgumentCongruence
 import Duper.Rules.FluidSup
@@ -308,17 +309,18 @@ def clausifyThenSaturate : ProverM Unit := do
     setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero;
     saturate
 
-def saturateNoPreprocessingClausification (generateDatatypeExhaustivenessFacts : Bool) : ProverM Unit := do
+def saturateNoPreprocessingClausification (withDatatypeExhaustivenessFacts : Bool) : ProverM Unit := do
   Core.withCurrHeartbeats $ do
-    if generateDatatypeExhaustivenessFacts then
-      let (symbolPrecMap, highesetPrecSymbolHasArityZero, datatypeList) ← buildSymbolPrecMapAndDatatypeList (← getPassiveSet).toList;
-      setSymbolPrecMap symbolPrecMap;
-      setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero;
+    if withDatatypeExhaustivenessFacts then
+      let (symbolPrecMap, highesetPrecSymbolHasArityZero, datatypeList) ← buildSymbolPrecMapAndDatatypeList (← getPassiveSet).toList
+      generateDatatypeExhaustivenessFacts datatypeList
+      setSymbolPrecMap symbolPrecMap
+      setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero
       saturate
     else
-      let (symbolPrecMap, highesetPrecSymbolHasArityZero) ← buildSymbolPrecMap (← getPassiveSet).toList;
-      setSymbolPrecMap symbolPrecMap;
-      setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero;
+      let (symbolPrecMap, highesetPrecSymbolHasArityZero) ← buildSymbolPrecMap (← getPassiveSet).toList
+      setSymbolPrecMap symbolPrecMap
+      setHighesetPrecSymbolHasArityZero highesetPrecSymbolHasArityZero
       saturate
 
 end ProverM

From da162858273949fab58542f3402d6a4569acba83 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Thu, 4 Jul 2024 22:42:41 -0400
Subject: [PATCH 03/10] mkEmptyDatatypeExhaustivenessProof

---
 Duper/Rules/DatatypeExhaustiveness.lean | 12 ++++++++++--
 Duper/Tests/test_regression.lean        | 10 ++++++++++
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/Duper/Rules/DatatypeExhaustiveness.lean b/Duper/Rules/DatatypeExhaustiveness.lean
index 1598ac1..27f70f4 100644
--- a/Duper/Rules/DatatypeExhaustiveness.lean
+++ b/Duper/Rules/DatatypeExhaustiveness.lean
@@ -6,6 +6,15 @@ open ProverM RuleM Lean Meta
 
 initialize Lean.registerTraceClass `duper.rule.datatypeExhaustiveness
 
+def mkEmptyDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr := do
+  Meta.forallTelescope c.toForallExpr fun xs body => do
+    let emptyTypeFVar := xs[xs.size - 1]!
+    let emptyType ← inferType emptyTypeFVar
+    let some (emptyTypeName, lvls) ← matchConstInduct emptyType.getAppFn' (fun _ => pure none) (fun ival lvls => pure (some (ival.name, lvls)))
+      | throwError "mkEmptyDatatypeExhaustivenessProof :: {emptyType} is not an inductive datatype"
+    let motive := .lam `_ emptyType (mkConst ``False) .default -- motive is `fun _ : emptyType => False`
+    mkLambdaFVars xs $ ← mkAppM' (mkConst (.str emptyTypeName "casesOn") (0 :: lvls)) #[motive, emptyTypeFVar]
+
 /-- Given an expression `∀ x1 : t1, x2 : t2, ... xn : tn, b`, returns `[t1, t2, ..., tn]`. If the given expression is not
     a forall expression, then `getForallArgumentTypes` just returns the empty list -/
 partial def getForallArgumentTypes (e : Expr) : List Expr :=
@@ -48,8 +57,7 @@ def generateDatatypeExhaustivenessFact (idt : Expr) : ProverM Unit := do
       let cExp ← mkForallFVars #[idtFVar] $ mkConst ``False
       let paramNames := #[] -- Assuming this is empty temporarily; This assumption does not hold if `idt` is universe polymorphic
       let c := Clause.fromForallExpr paramNames cExp
-      let mkProof := fun _ _ _ _ => Lean.Meta.mkSorry cExp (synthetic := true)
-      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness (empty inductive datatype)", mkProof := mkProof} maxGoalDistance 0 #[]
+      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness (empty inductive datatype)", mkProof := mkEmptyDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
     | ctor1 :: restConstructors =>
       let mut cBody ← makeConstructorEquality idtFVar ctor1 lvls idtArgs
       for ctor in restConstructors do
diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean
index 99efcaf..89ad6ec 100644
--- a/Duper/Tests/test_regression.lean
+++ b/Duper/Tests/test_regression.lean
@@ -709,6 +709,8 @@ inductive myType3
 inductive myType4 (t1 t2 : Type _)
 | const7 : t1 → t2 → myType4 t1 t2
 
+inductive myEmpty (t1 : Type _) (t2 : Type _)
+
 open myType myType2 myType3 myType4
 
 example : const1 ≠ const2 := by
@@ -738,3 +740,11 @@ example (a b x y : Nat) (f : Nat → Nat)
 
 example (x y : Nat) (h : [x] ≠ [y]) : x ≠ y := by
   duper [h] {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ¬∃ x : Empty, True := by
+  duper
+
+set_option duper.collectDatatypes true in
+example : ¬∃ x : (myEmpty Prop Type), True := by
+  duper

From 2afe812c37f008ac8a17eff0c654ca2306120eff Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Fri, 5 Jul 2024 20:00:32 -0400
Subject: [PATCH 04/10] Proof reconstruction for currently implemented datatype
 exhaustiveness fragment (still no polymorphism support)

---
 Duper/Rules/DatatypeExhaustiveness.lean | 82 ++++++++++++++++++++++---
 Duper/Tests/test_regression.lean        | 24 ++++++++
 2 files changed, 98 insertions(+), 8 deletions(-)

diff --git a/Duper/Rules/DatatypeExhaustiveness.lean b/Duper/Rules/DatatypeExhaustiveness.lean
index 27f70f4..b6edc45 100644
--- a/Duper/Rules/DatatypeExhaustiveness.lean
+++ b/Duper/Rules/DatatypeExhaustiveness.lean
@@ -6,6 +6,13 @@ open ProverM RuleM Lean Meta
 
 initialize Lean.registerTraceClass `duper.rule.datatypeExhaustiveness
 
+/-- Given an expression `∀ x1 : t1, x2 : t2, ... xn : tn, b`, returns `[t1, t2, ..., tn]`. If the given expression is not
+    a forall expression, then `getForallArgumentTypes` just returns the empty list -/
+partial def getForallArgumentTypes (e : Expr) : List Expr :=
+  match e.consumeMData with
+  | Expr.forallE _ t b _ => t :: (getForallArgumentTypes b)
+  | _ => []
+
 def mkEmptyDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr := do
   Meta.forallTelescope c.toForallExpr fun xs body => do
     let emptyTypeFVar := xs[xs.size - 1]!
@@ -15,12 +22,72 @@ def mkEmptyDatatypeExhaustivenessProof (premises : List Expr) (parents: List Pro
     let motive := .lam `_ emptyType (mkConst ``False) .default -- motive is `fun _ : emptyType => False`
     mkLambdaFVars xs $ ← mkAppM' (mkConst (.str emptyTypeName "casesOn") (0 :: lvls)) #[motive, emptyTypeFVar]
 
-/-- Given an expression `∀ x1 : t1, x2 : t2, ... xn : tn, b`, returns `[t1, t2, ..., tn]`. If the given expression is not
-    a forall expression, then `getForallArgumentTypes` just returns the empty list -/
-partial def getForallArgumentTypes (e : Expr) : List Expr :=
-  match e.consumeMData with
-  | Expr.forallE _ t b _ => t :: (getForallArgumentTypes b)
-  | _ => []
+def mkDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr := do
+  Meta.forallTelescope c.toForallExpr fun xs body => do
+    let cLits := c.lits.map (fun l => l.map (fun e => e.instantiateRev xs))
+    let idtFVar := xs[xs.size - 1]!
+    let idt ← inferType idtFVar
+    let some (idtIndVal, lvls) ← matchConstInduct idt.getAppFn' (fun _ => pure none) (fun ival lvls => pure (some (ival, lvls)))
+      | throwError "mkDatatypeExhaustivenessProof :: {idt} is not an inductive datatype"
+    let idtArgs := idt.getAppArgs.map some -- Mapping `some` to each element so it can be passed into `mkAppOptM'`
+    let constructors ← idtIndVal.ctors.mapM getConstInfoCtor
+    let motive ← mkLambdaFVars #[idtFVar] body
+    let mut casesOnArgs := #[] -- Each of these is an expression of type `∀ ctorFields, motive (ctor ctorFields)`
+    for ctor in constructors do
+      let orIdx := idtIndVal.numCtors - ctor.cidx - 1
+      let ctorBeforeFields ← mkAppOptM' (mkConst ctor.name lvls) idtArgs
+      let ctorType ← inferType ctorBeforeFields
+      let ctorArgTypes := getForallArgumentTypes ctorType
+      let curCasesOnArg ←
+        if ctorArgTypes.isEmpty then
+          let rflProof ← mkAppM ``Eq.refl #[ctorBeforeFields]
+          let idtFVarSubst := {map := AssocList.cons idtFVar.fvarId! ctorBeforeFields AssocList.nil}
+          let cLits := cLits.map (fun l => l.map (fun e => e.applyFVarSubst idtFVarSubst))
+          orIntro (cLits.map Lit.toExpr) orIdx rflProof
+        else
+          withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs => do
+            let fullyAppliedCtor ← mkAppM' ctorBeforeFields ctorArgs
+            let existsProof ←
+              withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs' => do
+                /-  Suppose ctorArgs = #[ctorArg0, ctorArg1] and ctorArgs' = #[ctorArg0', ctorArg1']
+                    Then we need to build:
+                    - @Exists.intro _ p1 ctorArg1 $ @Exists.intro _ p0 ctorArg0 $ Eq.refl (ctor ctorArg0 ctorArg1)
+                    Where:
+                    - p0 = `fun x => ctor ctorArg0 ctorArg1 = ctor x ctorArg1` (made via mkLambdaFVars #[ctorArg0']...)
+                    - p1 = `fun y => ∃ x : ctorArg1Type, ctor ctorArg0 ctorArg1 = ctor x y` -/
+                let mut rhsCtorArgs := ctorArgs
+                rhsCtorArgs := rhsCtorArgs.set! 0 ctorArgs'[0]!
+                let baseEquality ← mkAppM ``Eq #[fullyAppliedCtor, ← mkAppM' ctorBeforeFields rhsCtorArgs]
+                let existsIntroArg ← mkLambdaFVars #[ctorArgs'[0]!] baseEquality
+                let baseRflProof ← mkAppM ``Eq.refl #[fullyAppliedCtor]
+                let mut existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArgs[0]!, some baseRflProof]
+                let mut ctorArgNum := 0
+                trace[duper.rule.datatypeExhaustiveness] "Before entering loop, existsProof: {existsProof} (type: {← inferType existsProof})"
+                for (ctorArg, ctorArg') in ctorArgs.zip ctorArgs' do
+                  if ctorArgNum = 0 then
+                    ctorArgNum := 1
+                    continue
+                  rhsCtorArgs := rhsCtorArgs.set! ctorArgNum ctorArgs'[ctorArgNum]!
+                  let innerExistsProp ← do
+                    let mut innerExistsProp ← mkAppM ``Eq #[fullyAppliedCtor, ← mkAppM' ctorBeforeFields rhsCtorArgs]
+                    for i in [0:ctorArgNum] do
+                      innerExistsProp ← mkLambdaFVars #[ctorArgs'[i]!] innerExistsProp
+                      innerExistsProp ← mkAppM ``Exists #[innerExistsProp]
+                    pure innerExistsProp
+                  let existsIntroArg ← mkLambdaFVars #[ctorArg'] innerExistsProp
+                  existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArg, some existsProof]
+                  ctorArgNum := ctorArgNum + 1
+                  trace[duper.rule.datatypeExhaustiveness] "End of iteration {ctorArgNum} of loop"
+                  trace[duper.rule.datatypeExhaustiveness] "existsProof: {existsProof} (type: {← inferType existsProof})"
+                pure existsProof
+            let existsProof ← mkAppM ``eq_true #[existsProof]
+            let idtFVarSubst := {map := AssocList.cons idtFVar.fvarId! fullyAppliedCtor AssocList.nil}
+            let cLits := cLits.map (fun l => l.map (fun e => e.applyFVarSubst idtFVarSubst))
+            let orProof ← orIntro (cLits.map Lit.toExpr) orIdx existsProof
+            mkLambdaFVars ctorArgs orProof
+      trace[duper.rule.datatypeExhaustiveness] "casesOnArg for {ctor.name}: {curCasesOnArg} (type: {← inferType curCasesOnArg})"
+      casesOnArgs := casesOnArgs.push $ some curCasesOnArg
+    mkLambdaFVars xs $ ← mkAppOptM' (mkConst (.str idtIndVal.name "casesOn") (0 :: lvls)) (idtArgs ++ #[some motive, some idtFVar] ++ casesOnArgs)
 
 /-- Creates the expression `(∃ fields, e = ctor.{lvls} params fields) = True` where `params` are the inductive datatype's parameters
     and `fields` are arguments that need to be passed into `ctor` for the resulting expression to have the correct inductive type -/
@@ -66,8 +133,7 @@ def generateDatatypeExhaustivenessFact (idt : Expr) : ProverM Unit := do
       let cExp ← mkForallFVars #[idtFVar] cBody
       let paramNames := #[] -- Assuming this is empty temporarily; This assumption does not hold if `idt` is universe polymorphic
       let c := Clause.fromForallExpr paramNames cExp
-      let mkProof := fun _ _ _ _ => Lean.Meta.mkSorry cExp (synthetic := true)
-      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness", mkProof := mkProof} maxGoalDistance 0 #[]
+      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness", mkProof := mkDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
 
 /-- For each inductive datatype in `inductiveDataTypes`, generates an exhaustiveness lemma
     (e.g. `∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l'`) and adds it to the passive set -/
diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean
index 89ad6ec..9c4cc2c 100644
--- a/Duper/Tests/test_regression.lean
+++ b/Duper/Tests/test_regression.lean
@@ -748,3 +748,27 @@ example : ¬∃ x : Empty, True := by
 set_option duper.collectDatatypes true in
 example : ¬∃ x : (myEmpty Prop Type), True := by
   duper
+
+set_option duper.collectDatatypes true in
+example : ∀ x : myType, x = const1 ∨ x = const2 := by
+  duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ∀ x : Type 1, ∀ y : Type 2, ¬∃ z : (myEmpty y x), True := by
+  duper
+
+set_option duper.collectDatatypes true in
+example : ∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l' := by
+  duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ¬(∃ n : Nat, n ≠ 0 ∧ ∀ m : Nat, n ≠ m + 1) := by
+  duper [Nat.succ_eq_add_one] {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ∀ α : Type 2, ∀ x : myType2 α, ∃ t : α, x = const3 t ∨ ∃ t : α, x = const4 t := by
+  duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example (t1 : Type 1) (t2 : Type 2) (x : myType4 t1 t2) :
+  ∃ y : t1, ∃ z : t2, x = const7 y z := by duper {portfolioInstance := 7}

From dc83dfd0374303d4f58e9db26505dcd96a28b7c7 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Sat, 6 Jul 2024 15:37:36 -0400
Subject: [PATCH 05/10] Ignore propositions when collecting inductive datatypes

---
 Duper/Preprocessing.lean | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/Duper/Preprocessing.lean b/Duper/Preprocessing.lean
index bf927ce..357ba96 100644
--- a/Duper/Preprocessing.lean
+++ b/Duper/Preprocessing.lean
@@ -95,11 +95,12 @@ partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : HashMap Sy
   | Expr.bvar .. => return symbolFreqArityMap
   | Expr.lit .. => return symbolFreqArityMap
 
-/-- Checks whether the type `t` is an inductive datatype that is not a type class-/
-def isInductiveAndNotTypeClass (t : Expr) : ProverM Bool := do
+/-- Checks whether the type `t` is an inductive datatype that is neither a type class nor a Prop -/
+def isInductiveAndNonPropAndNotTypeClass (t : Expr) : ProverM Bool := do
   let isInductiveDatatype ← matchConstInduct t.getAppFn' (fun _ => pure false) (fun _ _ => pure true)
   let isClass := Option.isSome $ ← isClass? t
-  return isInductiveDatatype && !isClass
+  let isProp := (← inferType t).isProp
+  return isInductiveDatatype && !isClass && !isProp
 
 /-- Updates symbolFreqArityMap to increase the count of all symbols that appear in f (and if a symbol in f appears n
     times, then updates f's result in symbolFreqMap to be n greater than it was originally). Note that as with Expr.weight,
@@ -117,7 +118,7 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
       match (← getLCtx).fvarIdToDecl.find? fVarId with
       | some fDecl =>
         let fType := fDecl.type
-        let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+        let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
         if fTypeIsInductive && !datatypeList.contains fType then
           return (symbolFreqArityMap.insert fSymbol (1, getArity fType), fType :: datatypeList)
         else
@@ -130,28 +131,28 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
       return (symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity), datatypeList)
     | none =>
       let fType ← inferType f
-      let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+      let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
       if fTypeIsInductive && !datatypeList.contains fType then
         return (symbolFreqArityMap.insert fSymbol (1, getArity fType), fType :: datatypeList)
       else
         return (symbolFreqArityMap.insert fSymbol (1, getArity fType), datatypeList)
   | Expr.app f1 f2 =>
     let fType ← inferType f
-    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
     let datatypeList :=
       if fTypeIsInductive && !datatypeList.contains fType then fType :: datatypeList
       else datatypeList
     let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList f1 symbolFreqArityMap datatypeList
     updateSymbolFreqArityMapAndDatatypeList f2 symbolFreqArityMap' datatypeList'
   | Expr.lam _ t b _ =>
-    let tIsInductive ← isInductiveAndNotTypeClass t
+    let tIsInductive ← isInductiveAndNonPropAndNotTypeClass t
     let datatypeList :=
       if tIsInductive && !datatypeList.contains t then t :: datatypeList
       else datatypeList
     let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
     updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
   | Expr.forallE _ t b _ =>
-    let tIsInductive ← isInductiveAndNotTypeClass t
+    let tIsInductive ← isInductiveAndNonPropAndNotTypeClass t
     let datatypeList :=
       if tIsInductive && !datatypeList.contains t then t :: datatypeList
       else datatypeList
@@ -162,7 +163,7 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
     updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
   | Expr.proj _ _ b =>
     let fType ← inferType f
-    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
     if fTypeIsInductive && !datatypeList.contains fType then
       updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap (fType :: datatypeList)
     else
@@ -171,7 +172,7 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
   | Expr.sort .. => return (symbolFreqArityMap, datatypeList)
   | Expr.mvar .. =>
     let fType ← inferType f
-    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
     if fTypeIsInductive && !datatypeList.contains fType then
       return (symbolFreqArityMap, fType :: datatypeList)
     else
@@ -179,7 +180,7 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
   | Expr.bvar .. => return (symbolFreqArityMap, datatypeList)
   | Expr.lit .. =>
     let fType ← inferType f
-    let fTypeIsInductive ← isInductiveAndNotTypeClass fType
+    let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
     if fTypeIsInductive && !datatypeList.contains fType then
       return (symbolFreqArityMap, fType :: datatypeList)
     else

From 2a19ed208fbdfcd35d41bdfaef8d40db2dd3999e Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Mon, 8 Jul 2024 03:38:13 -0400
Subject: [PATCH 06/10] Update lean-auto

---
 lake-manifest.json | 4 ++--
 lakefile.lean      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 2d9a255..65493be 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "d90cb1aadbd52bf885958efa292ff4ef4f649732",
+   "rev": "7e475ff3bd5aa241b783546ca9700016e7a617ff",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d90cb1aadbd52bf885958efa292ff4ef4f649732",
+   "inputRev": "7e475ff3bd5aa241b783546ca9700016e7a617ff",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index 81dce70..beb19da 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"d90cb1aadbd52bf885958efa292ff4ef4f649732"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"7e475ff3bd5aa241b783546ca9700016e7a617ff"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.8.0"
 
 package Duper {

From 08180dde5e058ab85eef19bacd5aed20fd108301 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Wed, 17 Jul 2024 01:04:26 -0400
Subject: [PATCH 07/10] Working towards polymorphic datatype exhaustiveness
 support

---
 Duper/Preprocessing.lean                | 48 +++++++++++++++++++------
 Duper/Rules/DatatypeExhaustiveness.lean | 12 ++++++-
 2 files changed, 49 insertions(+), 11 deletions(-)

diff --git a/Duper/Preprocessing.lean b/Duper/Preprocessing.lean
index 357ba96..199701d 100644
--- a/Duper/Preprocessing.lean
+++ b/Duper/Preprocessing.lean
@@ -142,22 +142,48 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
     let datatypeList :=
       if fTypeIsInductive && !datatypeList.contains fType then fType :: datatypeList
       else datatypeList
-    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList f1 symbolFreqArityMap datatypeList
-    updateSymbolFreqArityMapAndDatatypeList f2 symbolFreqArityMap' datatypeList'
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList f1 symbolFreqArityMap datatypeList
+    updateSymbolFreqArityMapAndDatatypeList f2 symbolFreqArityMap datatypeList
   | Expr.lam _ t b _ =>
     let tIsInductive ← isInductiveAndNonPropAndNotTypeClass t
     let datatypeList :=
       if tIsInductive && !datatypeList.contains t then t :: datatypeList
       else datatypeList
-    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
-    updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
+    -- Modify `b` to not contain loose bvars
+    let freshMVar ← mkFreshExprMVar t
+    let freshMVarId := freshMVar.mvarId!
+    let b' := b.instantiate1 freshMVar
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList b' symbolFreqArityMap datatypeList
+    let mut datatypeArr := #[]
+    -- Remove freshMVar from all acquired datatypes
+    for datatype in datatypeList do
+      if datatype.hasAnyMVar (fun mvarid => mvarid == freshMVarId) then
+        let datatype ← mkLambdaFVars #[freshMVar] datatype
+        datatypeArr := datatypeArr.push datatype
+      else
+        datatypeArr := datatypeArr.push datatype
+    pure (symbolFreqArityMap, datatypeArr.toList)
   | Expr.forallE _ t b _ =>
     let tIsInductive ← isInductiveAndNonPropAndNotTypeClass t
     let datatypeList :=
       if tIsInductive && !datatypeList.contains t then t :: datatypeList
       else datatypeList
-    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
-    updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
+    -- Modify `b` to not contain loose bvars
+    let freshMVar ← mkFreshExprMVar t
+    let freshMVarId := freshMVar.mvarId!
+    let b' := b.instantiate1 freshMVar
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList b' symbolFreqArityMap datatypeList
+    let mut datatypeArr := #[]
+    -- Remove freshMVar from all acquired datatypes
+    for datatype in datatypeList do
+      if datatype.hasAnyMVar (fun mvarid => mvarid == freshMVarId) then
+        let datatype ← mkLambdaFVars #[freshMVar] datatype
+        datatypeArr := datatypeArr.push datatype
+      else
+        datatypeArr := datatypeArr.push datatype
+    pure (symbolFreqArityMap, datatypeArr.toList)
   | Expr.letE _ _ v b _ =>
     let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList v symbolFreqArityMap datatypeList
     updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
@@ -202,14 +228,15 @@ partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (HashMap S
     - A HashMap that maps each symbol to a tuple containing:
       - The number of times they appear in formulas
       - Its arity
-    - A list containing every inductive datatype that appears in any clause
-    Note: The current code does not yet support polymorphic inductive datatypes -/
+    - A list containing every inductive datatype that appears in any clause. Polymorphic inductive datatypes are represented
+      as lambdas from parameters to the overall inductive type. For example, the polymorphic list datatype is represented
+      via `fun x => List x` -/
 partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat) × List Expr) := do
   let mut symbolFreqArityMap := HashMap.empty
   let mut datatypeList := []
   for c in clauses do
     -- In order to accurately collect inductive datatypes, I need to use mclauses rather than clauses.
-    -- This ensures, for instance, that polymorphic lists will appear as `List ?m` rather than `List #1`.
+    -- This specifically ensures that level parameters are replaced with fresh level metavariables
     let c ← runRuleM $ loadClause c
     trace[duper.collectDatatypes.debug] "Loaded clause c: {c.lits}"
     for l in c.lits do
@@ -275,7 +302,8 @@ def buildSymbolPrecMap (clauses : List Clause) : ProverM (SymbolPrecMap × Bool)
   return (symbolPrecMap, highesetPrecSymbolHasArityZero)
 
 /-- Like `buildSymbolPrecMap` but it also returns a list of all inductive datatypes that appear in any clause.
-    Note: The current code does not yet support polymorphic inductive datatypes -/
+    Polymorphic inductive datatypes are represented as lambdas from parameters to the overall inductive type.
+    For example, the polymorphic list datatype is represented via `fun x => List x`-/
 def buildSymbolPrecMapAndDatatypeList (clauses : List Clause) : ProverM (SymbolPrecMap × Bool × List Expr) := do
   let (symbolFreqArityMap, datatypeList) ← buildSymbolFreqArityMapAndDatatypeList clauses
   trace[duper.collectDatatypes.debug] "datatypeList collected by buildSymbolPrecMap: {datatypeList}"
diff --git a/Duper/Rules/DatatypeExhaustiveness.lean b/Duper/Rules/DatatypeExhaustiveness.lean
index b6edc45..8b1e31e 100644
--- a/Duper/Rules/DatatypeExhaustiveness.lean
+++ b/Duper/Rules/DatatypeExhaustiveness.lean
@@ -13,6 +13,15 @@ partial def getForallArgumentTypes (e : Expr) : List Expr :=
   | Expr.forallE _ t b _ => t :: (getForallArgumentTypes b)
   | _ => []
 
+/-- Given an expression `λ x1 : t1, x2 : t2, ... xn : tn => b`, returns `[t1, t2, ..., tn]` and `b`. If the given expression is not
+    a lambda expression, then `getLambdaArgumentTypes` just returns the empty list and `e` -/
+partial def getLambdaArgumentTypesAndBody (e : Expr) : List Expr × Expr :=
+  match e.consumeMData with
+  | Expr.lam _ t b _ =>
+    let (args, b) := getLambdaArgumentTypesAndBody b
+    (t :: args, b)
+  | _ => ([], e)
+
 def mkEmptyDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr := do
   Meta.forallTelescope c.toForallExpr fun xs body => do
     let emptyTypeFVar := xs[xs.size - 1]!
@@ -113,11 +122,12 @@ def makeConstructorEquality (e : Expr) (ctor : ConstructorVal) (lvls : List Leve
     collected properly, and because this code assumes that the generated clause has no parameters (which is not necessarily true
     when `idt` is universe polymorphic) -/
 def generateDatatypeExhaustivenessFact (idt : Expr) : ProverM Unit := do
+  let (idtParams, idt) := getLambdaArgumentTypesAndBody idt
   let some (idtIndVal, lvls) ← matchConstInduct idt.getAppFn' (fun _ => pure none) (fun ival lvls => pure (some (ival, lvls)))
     | throwError "generateDatatypeExhaustivenessFact :: {idt} is not an inductive datatype"
   let idtArgs := idt.getAppArgs
   let constructors ← idtIndVal.ctors.mapM getConstInfoCtor
-  trace[duper.rule.datatypeExhaustiveness] "Inductive datatype {idt} with args {idtArgs} has constructors {constructors.map (fun x => x.name)}"
+  trace[duper.rule.datatypeExhaustiveness] "Inductive datatype {idt} with params {idtParams} and args {idtArgs} has constructors {constructors.map (fun x => x.name)}"
   withLocalDeclD `_ idt fun idtFVar => do
     match constructors with
     | [] => -- `idt` is an inductive datatype with no constructors. This means that there cannot exist any elements of type `idt`

From fd54083e79da68dbc099a3dcf41e8c64eddbe5b2 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Wed, 17 Jul 2024 14:46:46 -0400
Subject: [PATCH 08/10] Generate exhaustiveness facts for polymorphic inductive
 datatypes

Note: duper.collectDatatypes is still disabled by default because
test_regression.lean has some problems that fail when
duper.collectDatatypes is enabled. After those issues are resolved,
there will be a future commit that enables duper.collectDatatypes by
default (or gets rid of this option altogether)
---
 Duper/Preprocessing.lean                | 90 ++++++++++++-------------
 Duper/Rules/DatatypeExhaustiveness.lean | 68 +++++++------------
 Duper/Tests/test_regression.lean        | 12 ++++
 3 files changed, 83 insertions(+), 87 deletions(-)

diff --git a/Duper/Preprocessing.lean b/Duper/Preprocessing.lean
index 199701d..b85ff9a 100644
--- a/Duper/Preprocessing.lean
+++ b/Duper/Preprocessing.lean
@@ -106,9 +106,11 @@ def isInductiveAndNonPropAndNotTypeClass (t : Expr) : ProverM Bool := do
     times, then updates f's result in symbolFreqMap to be n greater than it was originally). Note that as with Expr.weight,
     this function may require revision to be more similar to Zipperposition's implementation once we actually start working
     on higher order things. Additionally, updates datatypeList to make sure that all inductive datatypes that appear
-    in the problem are contained in the datatypeList. -/
+    in the problem are contained in the datatypeList. The format in which inductive datatypes are recorded as elements of
+    type `Expr × Array Name` is described in the comment above `buildSymbolFreqArityMapAndDatatypeList` -/
 partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityMap : HashMap Symbol (Nat × Nat))
-  (datatypeList : List Expr) : ProverM (HashMap Symbol (Nat × Nat) × List Expr) := do
+  (datatypeList : List (Expr × Array Name)) (paramNames : Array Name) :
+  ProverM (HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
   match f with
   | Expr.fvar fVarId =>
     let fSymbol := Symbol.FVarId fVarId
@@ -119,8 +121,8 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
       | some fDecl =>
         let fType := fDecl.type
         let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
-        if fTypeIsInductive && !datatypeList.contains fType then
-          return (symbolFreqArityMap.insert fSymbol (1, getArity fType), fType :: datatypeList)
+        if fTypeIsInductive && !datatypeList.any (fun (t, _) => t == fType) then
+          return (symbolFreqArityMap.insert fSymbol (1, getArity fType), (fType, paramNames) :: datatypeList)
         else
           return (symbolFreqArityMap.insert fSymbol (1, getArity fType), datatypeList)
       | none => throwError s!"Unable to find {fVarId.name} in local context"
@@ -132,83 +134,83 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
     | none =>
       let fType ← inferType f
       let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
-      if fTypeIsInductive && !datatypeList.contains fType then
-        return (symbolFreqArityMap.insert fSymbol (1, getArity fType), fType :: datatypeList)
+      if fTypeIsInductive && !datatypeList.any (fun (t, _) => t == fType) then
+        return (symbolFreqArityMap.insert fSymbol (1, getArity fType), (fType, paramNames) :: datatypeList)
       else
         return (symbolFreqArityMap.insert fSymbol (1, getArity fType), datatypeList)
   | Expr.app f1 f2 =>
     let fType ← inferType f
     let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
     let datatypeList :=
-      if fTypeIsInductive && !datatypeList.contains fType then fType :: datatypeList
+      if fTypeIsInductive && !datatypeList.any (fun (t, _) => t == fType) then (fType, paramNames) :: datatypeList
       else datatypeList
-    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList f1 symbolFreqArityMap datatypeList
-    updateSymbolFreqArityMapAndDatatypeList f2 symbolFreqArityMap datatypeList
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList f1 symbolFreqArityMap datatypeList paramNames
+    updateSymbolFreqArityMapAndDatatypeList f2 symbolFreqArityMap datatypeList paramNames
   | Expr.lam _ t b _ =>
     let tIsInductive ← isInductiveAndNonPropAndNotTypeClass t
     let datatypeList :=
-      if tIsInductive && !datatypeList.contains t then t :: datatypeList
+      if tIsInductive && !datatypeList.any (fun (t', _) => t' == t) then (t, paramNames) :: datatypeList
       else datatypeList
-    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList paramNames
     -- Modify `b` to not contain loose bvars
     let freshMVar ← mkFreshExprMVar t
     let freshMVarId := freshMVar.mvarId!
     let b' := b.instantiate1 freshMVar
-    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList b' symbolFreqArityMap datatypeList
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList b' symbolFreqArityMap datatypeList paramNames
     let mut datatypeArr := #[]
     -- Remove freshMVar from all acquired datatypes
-    for datatype in datatypeList do
+    for (datatype, datatypeParams) in datatypeList do
       if datatype.hasAnyMVar (fun mvarid => mvarid == freshMVarId) then
-        let datatype ← mkLambdaFVars #[freshMVar] datatype
-        datatypeArr := datatypeArr.push datatype
+        let datatype ← mkForallFVars #[freshMVar] datatype
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
       else
-        datatypeArr := datatypeArr.push datatype
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
     pure (symbolFreqArityMap, datatypeArr.toList)
   | Expr.forallE _ t b _ =>
     let tIsInductive ← isInductiveAndNonPropAndNotTypeClass t
     let datatypeList :=
-      if tIsInductive && !datatypeList.contains t then t :: datatypeList
+      if tIsInductive && !datatypeList.any (fun (t', _) => t' == t) then (t, paramNames) :: datatypeList
       else datatypeList
-    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList t symbolFreqArityMap datatypeList paramNames
     -- Modify `b` to not contain loose bvars
     let freshMVar ← mkFreshExprMVar t
     let freshMVarId := freshMVar.mvarId!
     let b' := b.instantiate1 freshMVar
-    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList b' symbolFreqArityMap datatypeList
+    let (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList b' symbolFreqArityMap datatypeList paramNames
     let mut datatypeArr := #[]
     -- Remove freshMVar from all acquired datatypes
-    for datatype in datatypeList do
+    for (datatype, datatypeParams) in datatypeList do
       if datatype.hasAnyMVar (fun mvarid => mvarid == freshMVarId) then
-        let datatype ← mkLambdaFVars #[freshMVar] datatype
-        datatypeArr := datatypeArr.push datatype
+        let datatype ← mkForallFVars #[freshMVar] datatype
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
       else
-        datatypeArr := datatypeArr.push datatype
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
     pure (symbolFreqArityMap, datatypeArr.toList)
   | Expr.letE _ _ v b _ =>
-    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList v symbolFreqArityMap datatypeList
-    updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList'
+    let (symbolFreqArityMap', datatypeList') ← updateSymbolFreqArityMapAndDatatypeList v symbolFreqArityMap datatypeList paramNames
+    updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap' datatypeList' paramNames
   | Expr.proj _ _ b =>
     let fType ← inferType f
     let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
-    if fTypeIsInductive && !datatypeList.contains fType then
-      updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap (fType :: datatypeList)
+    if fTypeIsInductive && !datatypeList.any (fun (t, _) => t == fType) then
+      updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap ((fType, paramNames) :: datatypeList) paramNames
     else
-      updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap datatypeList
-  | Expr.mdata _ b => updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap datatypeList
+      updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap datatypeList paramNames
+  | Expr.mdata _ b => updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap datatypeList paramNames
   | Expr.sort .. => return (symbolFreqArityMap, datatypeList)
   | Expr.mvar .. =>
     let fType ← inferType f
     let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
-    if fTypeIsInductive && !datatypeList.contains fType then
-      return (symbolFreqArityMap, fType :: datatypeList)
+    if fTypeIsInductive && !datatypeList.any (fun (t, _) => t == fType) then
+      return (symbolFreqArityMap, (fType, paramNames) :: datatypeList)
     else
       return (symbolFreqArityMap, datatypeList)
   | Expr.bvar .. => return (symbolFreqArityMap, datatypeList)
   | Expr.lit .. =>
     let fType ← inferType f
     let fTypeIsInductive ← isInductiveAndNonPropAndNotTypeClass fType
-    if fTypeIsInductive && !datatypeList.contains fType then
-      return (symbolFreqArityMap, fType :: datatypeList)
+    if fTypeIsInductive && !datatypeList.any (fun (t, _) => t == fType) then
+      return (symbolFreqArityMap, (fType, paramNames) :: datatypeList)
     else
       return (symbolFreqArityMap, datatypeList)
 
@@ -228,20 +230,17 @@ partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (HashMap S
     - A HashMap that maps each symbol to a tuple containing:
       - The number of times they appear in formulas
       - Its arity
-    - A list containing every inductive datatype that appears in any clause. Polymorphic inductive datatypes are represented
-      as lambdas from parameters to the overall inductive type. For example, the polymorphic list datatype is represented
-      via `fun x => List x` -/
-partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat) × List Expr) := do
+    - A list containing every inductive datatype that appears in any clause. Polymorphic inductive datatypes are represented as universally
+    quantified types paired with an array of parameters that can appear in the inductive datatype. For example, the polymorphic list datatype
+    `List α` of where `α : Type u` is represented via `((∀ (α : Type u), List α), #[u])` -/
+partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
   let mut symbolFreqArityMap := HashMap.empty
   let mut datatypeList := []
   for c in clauses do
-    -- In order to accurately collect inductive datatypes, I need to use mclauses rather than clauses.
-    -- This specifically ensures that level parameters are replaced with fresh level metavariables
-    let c ← runRuleM $ loadClause c
     trace[duper.collectDatatypes.debug] "Loaded clause c: {c.lits}"
     for l in c.lits do
-      (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList l.lhs symbolFreqArityMap datatypeList
-      (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList l.rhs symbolFreqArityMap datatypeList
+      (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList l.lhs symbolFreqArityMap datatypeList c.paramNames
+      (symbolFreqArityMap, datatypeList) ← updateSymbolFreqArityMapAndDatatypeList l.rhs symbolFreqArityMap datatypeList c.paramNames
   trace[duper.unaryFirst.debug] "symbolFreqArityMap: {symbolFreqArityMap.toArray}"
   trace[duper.collectDatatypes.debug] "datatypeList collected by buildSymbolFreqArityMapAndDatatypeList: {datatypeList}"
   return (symbolFreqArityMap, datatypeList)
@@ -302,9 +301,10 @@ def buildSymbolPrecMap (clauses : List Clause) : ProverM (SymbolPrecMap × Bool)
   return (symbolPrecMap, highesetPrecSymbolHasArityZero)
 
 /-- Like `buildSymbolPrecMap` but it also returns a list of all inductive datatypes that appear in any clause.
-    Polymorphic inductive datatypes are represented as lambdas from parameters to the overall inductive type.
-    For example, the polymorphic list datatype is represented via `fun x => List x`-/
-def buildSymbolPrecMapAndDatatypeList (clauses : List Clause) : ProverM (SymbolPrecMap × Bool × List Expr) := do
+    Polymorphic inductive datatypes are represented as universally quantified types paired with an array of parameters
+    that can appear in the inductive datatype. For example, the polymorphic list datatype `List α` of where `α : Type u`
+    is represented via `((∀ (α : Type u), List α), #[u])` -/
+def buildSymbolPrecMapAndDatatypeList (clauses : List Clause) : ProverM (SymbolPrecMap × Bool × List (Expr × Array Name)) := do
   let (symbolFreqArityMap, datatypeList) ← buildSymbolFreqArityMapAndDatatypeList clauses
   trace[duper.collectDatatypes.debug] "datatypeList collected by buildSymbolPrecMap: {datatypeList}"
   let mut symbolPrecArr : Array (Symbol × Nat × Nat) := #[]
diff --git a/Duper/Rules/DatatypeExhaustiveness.lean b/Duper/Rules/DatatypeExhaustiveness.lean
index 8b1e31e..b3d9774 100644
--- a/Duper/Rules/DatatypeExhaustiveness.lean
+++ b/Duper/Rules/DatatypeExhaustiveness.lean
@@ -13,15 +13,6 @@ partial def getForallArgumentTypes (e : Expr) : List Expr :=
   | Expr.forallE _ t b _ => t :: (getForallArgumentTypes b)
   | _ => []
 
-/-- Given an expression `λ x1 : t1, x2 : t2, ... xn : tn => b`, returns `[t1, t2, ..., tn]` and `b`. If the given expression is not
-    a lambda expression, then `getLambdaArgumentTypes` just returns the empty list and `e` -/
-partial def getLambdaArgumentTypesAndBody (e : Expr) : List Expr × Expr :=
-  match e.consumeMData with
-  | Expr.lam _ t b _ =>
-    let (args, b) := getLambdaArgumentTypesAndBody b
-    (t :: args, b)
-  | _ => ([], e)
-
 def mkEmptyDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofParent) (transferExprs : Array Expr) (c : Clause) : MetaM Expr := do
   Meta.forallTelescope c.toForallExpr fun xs body => do
     let emptyTypeFVar := xs[xs.size - 1]!
@@ -71,7 +62,6 @@ def mkDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofPar
                 let baseRflProof ← mkAppM ``Eq.refl #[fullyAppliedCtor]
                 let mut existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArgs[0]!, some baseRflProof]
                 let mut ctorArgNum := 0
-                trace[duper.rule.datatypeExhaustiveness] "Before entering loop, existsProof: {existsProof} (type: {← inferType existsProof})"
                 for (ctorArg, ctorArg') in ctorArgs.zip ctorArgs' do
                   if ctorArgNum = 0 then
                     ctorArgNum := 1
@@ -86,15 +76,12 @@ def mkDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofPar
                   let existsIntroArg ← mkLambdaFVars #[ctorArg'] innerExistsProp
                   existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArg, some existsProof]
                   ctorArgNum := ctorArgNum + 1
-                  trace[duper.rule.datatypeExhaustiveness] "End of iteration {ctorArgNum} of loop"
-                  trace[duper.rule.datatypeExhaustiveness] "existsProof: {existsProof} (type: {← inferType existsProof})"
                 pure existsProof
             let existsProof ← mkAppM ``eq_true #[existsProof]
             let idtFVarSubst := {map := AssocList.cons idtFVar.fvarId! fullyAppliedCtor AssocList.nil}
             let cLits := cLits.map (fun l => l.map (fun e => e.applyFVarSubst idtFVarSubst))
             let orProof ← orIntro (cLits.map Lit.toExpr) orIdx existsProof
             mkLambdaFVars ctorArgs orProof
-      trace[duper.rule.datatypeExhaustiveness] "casesOnArg for {ctor.name}: {curCasesOnArg} (type: {← inferType curCasesOnArg})"
       casesOnArgs := casesOnArgs.push $ some curCasesOnArg
     mkLambdaFVars xs $ ← mkAppOptM' (mkConst (.str idtIndVal.name "casesOn") (0 :: lvls)) (idtArgs ++ #[some motive, some idtFVar] ++ casesOnArgs)
 
@@ -111,41 +98,38 @@ def makeConstructorEquality (e : Expr) (ctor : ConstructorVal) (lvls : List Leve
       for ctorArg in ctorArgs do
         res ← mkLambdaFVars #[ctorArg] res
         res ← mkAppM ``Exists #[res]
-      trace[duper.rule.datatypeExhaustiveness] "makeConstructorEquality :: Returning {res} from e {e} and ctor {ctor.name}"
       mkAppM ``Eq #[res, mkConst ``True]
 
 /-- Given an inductive datatype `idt`, with constructors `ctor₁, ctor₂, ... ctorₙ`, generates a fact of the form
     `∀ x : idt, x = ctor₁ ∨ x = ctor₂ ∨ ... x = ctorₙ` and adds it to the passive set. For example, if `idt = List Nat`,
     then `generateDatatypeExhaustivenessFact` generates `∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l'`
 
-    Note: This code does not currently support polymorphic inductive datatypes, both because the arguments are not presently
-    collected properly, and because this code assumes that the generated clause has no parameters (which is not necessarily true
-    when `idt` is universe polymorphic) -/
-def generateDatatypeExhaustivenessFact (idt : Expr) : ProverM Unit := do
-  let (idtParams, idt) := getLambdaArgumentTypesAndBody idt
-  let some (idtIndVal, lvls) ← matchConstInduct idt.getAppFn' (fun _ => pure none) (fun ival lvls => pure (some (ival, lvls)))
-    | throwError "generateDatatypeExhaustivenessFact :: {idt} is not an inductive datatype"
-  let idtArgs := idt.getAppArgs
-  let constructors ← idtIndVal.ctors.mapM getConstInfoCtor
-  trace[duper.rule.datatypeExhaustiveness] "Inductive datatype {idt} with params {idtParams} and args {idtArgs} has constructors {constructors.map (fun x => x.name)}"
-  withLocalDeclD `_ idt fun idtFVar => do
-    match constructors with
-    | [] => -- `idt` is an inductive datatype with no constructors. This means that there cannot exist any elements of type `idt`
-      let cExp ← mkForallFVars #[idtFVar] $ mkConst ``False
-      let paramNames := #[] -- Assuming this is empty temporarily; This assumption does not hold if `idt` is universe polymorphic
-      let c := Clause.fromForallExpr paramNames cExp
-      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness (empty inductive datatype)", mkProof := mkEmptyDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
-    | ctor1 :: restConstructors =>
-      let mut cBody ← makeConstructorEquality idtFVar ctor1 lvls idtArgs
-      for ctor in restConstructors do
-        let ctorEquality ← makeConstructorEquality idtFVar ctor lvls idtArgs
-        cBody ← mkAppM ``Or #[ctorEquality, cBody]
-      let cExp ← mkForallFVars #[idtFVar] cBody
-      let paramNames := #[] -- Assuming this is empty temporarily; This assumption does not hold if `idt` is universe polymorphic
-      let c := Clause.fromForallExpr paramNames cExp
-      addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness", mkProof := mkDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
+    Polymorphic inductive datatypes are represented as universally quantified types paired with an array of parameters
+    that can appear in the inductive datatype. For example, the polymorphic list datatype `List α` of where `α : Type u`
+    is represented via `idt` `∀ (α : Type u), List α` and `paramNames` `#[u]` -/
+def generateDatatypeExhaustivenessFact (idt : Expr) (paramNames : Array Name) : ProverM Unit := do
+  forallTelescope idt fun idtParams idtBody => do
+    let some (idtIndVal, lvls) ← matchConstInduct idtBody.getAppFn' (fun _ => pure none) (fun ival lvls => pure (some (ival, lvls)))
+      | throwError "generateDatatypeExhaustivenessFact :: {idt} is not an inductive datatype"
+    let idtArgs := idtBody.getAppArgs
+    let constructors ← idtIndVal.ctors.mapM getConstInfoCtor
+    withLocalDeclD `_ idtBody fun idtFVar => do
+      match constructors with
+      | [] => -- `idtBody` is an inductive datatype with no constructors. This means that there cannot exist any elements of type `idtBody`
+        let cExp ← mkForallFVars (idtParams.push idtFVar) $ mkConst ``False
+        let c := Clause.fromForallExpr paramNames cExp
+        addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness (empty inductive datatype)", mkProof := mkEmptyDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
+      | ctor1 :: restConstructors =>
+        let mut cBody ← makeConstructorEquality idtFVar ctor1 lvls idtArgs
+        for ctor in restConstructors do
+          let ctorEquality ← makeConstructorEquality idtFVar ctor lvls idtArgs
+          cBody ← mkAppM ``Or #[ctorEquality, cBody]
+        let cExp ← mkForallFVars (idtParams.push idtFVar) cBody
+        let c := Clause.fromForallExpr paramNames cExp
+        trace[duper.rule.datatypeExhaustiveness] "About to add {c} to passive set"
+        addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness", mkProof := mkDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
 
 /-- For each inductive datatype in `inductiveDataTypes`, generates an exhaustiveness lemma
     (e.g. `∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l'`) and adds it to the passive set -/
-partial def generateDatatypeExhaustivenessFacts (inductiveDataTypes : List Expr) : ProverM Unit :=
-  inductiveDataTypes.forM generateDatatypeExhaustivenessFact
+partial def generateDatatypeExhaustivenessFacts (inductiveDataTypes : List (Expr × Array Name)) : ProverM Unit :=
+  inductiveDataTypes.forM (fun x => generateDatatypeExhaustivenessFact x.1 x.2)
diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean
index 9c4cc2c..82ba924 100644
--- a/Duper/Tests/test_regression.lean
+++ b/Duper/Tests/test_regression.lean
@@ -761,6 +761,14 @@ set_option duper.collectDatatypes true in
 example : ∀ l : List Nat, l = [] ∨ ∃ n : Nat, ∃ l' : List Nat, l = n :: l' := by
   duper {portfolioInstance := 7}
 
+set_option duper.collectDatatypes true in
+example : ∀ l : List α, l = [] ∨ ∃ x : α, ∃ l' : List α, l = x :: l' := by
+  duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example : ∀ α : Type u, ∀ x : α × Int, ∃ y : α, ∃ z : Int, x = (y, z) := by
+  duper [*] {portfolioInstance := 7}
+
 set_option duper.collectDatatypes true in
 example : ¬(∃ n : Nat, n ≠ 0 ∧ ∀ m : Nat, n ≠ m + 1) := by
   duper [Nat.succ_eq_add_one] {portfolioInstance := 7}
@@ -772,3 +780,7 @@ example : ∀ α : Type 2, ∀ x : myType2 α, ∃ t : α, x = const3 t ∨ ∃
 set_option duper.collectDatatypes true in
 example (t1 : Type 1) (t2 : Type 2) (x : myType4 t1 t2) :
   ∃ y : t1, ∃ z : t2, x = const7 y z := by duper {portfolioInstance := 7}
+
+set_option duper.collectDatatypes true in
+example (P : α × β → Prop) (h : ∀ x : α, ∀ y : β, P (x, y)) : ∀ z : α × β, P z := by
+  duper [*] {portfolioInstance := 7}

From d800617693b2ed27ae16064f925df1e702b571dc Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Thu, 18 Jul 2024 09:08:54 -0400
Subject: [PATCH 09/10] Modifying DatatypeExhaustiveness.lean to support
 dependent types

Note: duper.collectDatatypes is still disabled by default because there
remain tests in test_regression.lean that fail when it is enabled. At
least some of these tests fail due to unrelated issues that are exposed by
enabling duper.collectDatatypes. After these issues are resolved, the
duper.collectDatatypes option can be removed or folded into portfolio mode's
includeExpensiveRules option
---
 Duper/Rules/DatatypeExhaustiveness.lean | 37 +++++++++++++------------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/Duper/Rules/DatatypeExhaustiveness.lean b/Duper/Rules/DatatypeExhaustiveness.lean
index b3d9774..126276c 100644
--- a/Duper/Rules/DatatypeExhaustiveness.lean
+++ b/Duper/Rules/DatatypeExhaustiveness.lean
@@ -45,37 +45,39 @@ def mkDatatypeExhaustivenessProof (premises : List Expr) (parents: List ProofPar
           let cLits := cLits.map (fun l => l.map (fun e => e.applyFVarSubst idtFVarSubst))
           orIntro (cLits.map Lit.toExpr) orIdx rflProof
         else
-          withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs => do
+          withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun prevArgs => pure (ty.instantiate prevArgs))).toArray fun ctorArgs => do
             let fullyAppliedCtor ← mkAppM' ctorBeforeFields ctorArgs
             let existsProof ←
-              withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs' => do
+              withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun prevArgs => pure (ty.instantiate prevArgs))).toArray fun ctorArgs' => do
                 /-  Suppose ctorArgs = #[ctorArg0, ctorArg1] and ctorArgs' = #[ctorArg0', ctorArg1']
                     Then we need to build:
-                    - @Exists.intro _ p1 ctorArg1 $ @Exists.intro _ p0 ctorArg0 $ Eq.refl (ctor ctorArg0 ctorArg1)
+                    - @Exists.intro _ p0 ctorArg0 $ @Exists.intro _ p1 ctorArg1 $ Eq.refl (ctor ctorArg0 ctorArg1)
                     Where:
-                    - p0 = `fun x => ctor ctorArg0 ctorArg1 = ctor x ctorArg1` (made via mkLambdaFVars #[ctorArg0']...)
-                    - p1 = `fun y => ∃ x : ctorArg1Type, ctor ctorArg0 ctorArg1 = ctor x y` -/
+                    - p1 = `fun x => ctor ctorArg0 ctorArg1 = ctor ctorArg0 x` (made via mkLambdaFVars #[ctorArg1']...)
+                    - p0 = `fun y => ∃ x : ctorArg1Type, ctor ctorArg0 ctorArg1 = ctor y x` -/
                 let mut rhsCtorArgs := ctorArgs
-                rhsCtorArgs := rhsCtorArgs.set! 0 ctorArgs'[0]!
+                let numCtorArgs := ctorArgs.size -- ctorArgs.size = ctorArgs'.size
+                rhsCtorArgs := rhsCtorArgs.set! (numCtorArgs - 1) ctorArgs'[numCtorArgs - 1]!
                 let baseEquality ← mkAppM ``Eq #[fullyAppliedCtor, ← mkAppM' ctorBeforeFields rhsCtorArgs]
-                let existsIntroArg ← mkLambdaFVars #[ctorArgs'[0]!] baseEquality
+                let existsIntroArg ← mkLambdaFVars #[ctorArgs'[numCtorArgs - 1]!] baseEquality
                 let baseRflProof ← mkAppM ``Eq.refl #[fullyAppliedCtor]
-                let mut existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArgs[0]!, some baseRflProof]
-                let mut ctorArgNum := 0
-                for (ctorArg, ctorArg') in ctorArgs.zip ctorArgs' do
-                  if ctorArgNum = 0 then
-                    ctorArgNum := 1
+                let mut existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArgs[numCtorArgs - 1]!, some baseRflProof]
+                let mut ctorArgNum := numCtorArgs - 1
+                for (ctorArg, ctorArg') in (ctorArgs.zip ctorArgs').reverse do
+                  if ctorArgNum = numCtorArgs - 1 then
+                    ctorArgNum := ctorArgNum - 1
                     continue
                   rhsCtorArgs := rhsCtorArgs.set! ctorArgNum ctorArgs'[ctorArgNum]!
                   let innerExistsProp ← do
                     let mut innerExistsProp ← mkAppM ``Eq #[fullyAppliedCtor, ← mkAppM' ctorBeforeFields rhsCtorArgs]
-                    for i in [0:ctorArgNum] do
-                      innerExistsProp ← mkLambdaFVars #[ctorArgs'[i]!] innerExistsProp
+                    for i in [ctorArgNum + 1:numCtorArgs] do
+                      let j := numCtorArgs - i
+                      innerExistsProp ← mkLambdaFVars #[ctorArgs'[j]!] innerExistsProp
                       innerExistsProp ← mkAppM ``Exists #[innerExistsProp]
                     pure innerExistsProp
                   let existsIntroArg ← mkLambdaFVars #[ctorArg'] innerExistsProp
                   existsProof ← mkAppOptM ``Exists.intro #[none, some existsIntroArg, some ctorArg, some existsProof]
-                  ctorArgNum := ctorArgNum + 1
+                  ctorArgNum := ctorArgNum - 1
                 pure existsProof
             let existsProof ← mkAppM ``eq_true #[existsProof]
             let idtFVarSubst := {map := AssocList.cons idtFVar.fvarId! fullyAppliedCtor AssocList.nil}
@@ -93,9 +95,9 @@ def makeConstructorEquality (e : Expr) (ctor : ConstructorVal) (lvls : List Leve
     let ctorBeforeFields ← mkAppOptM' (mkConst ctor.name lvls) (params.map some)
     let ctorType ← inferType ctorBeforeFields
     let ctorArgTypes := getForallArgumentTypes ctorType
-    withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun _ => pure ty)).toArray fun ctorArgs => do
+    withLocalDeclsD (ctorArgTypes.map fun ty => (`_, fun prevArgs => pure (ty.instantiate prevArgs))).toArray fun ctorArgs => do
       let mut res ← mkAppM ``Eq #[e, ← mkAppM' ctorBeforeFields ctorArgs]
-      for ctorArg in ctorArgs do
+      for ctorArg in ctorArgs.reverse do -- Need to reverse `ctorArgs` to support arguments that depend on previous arguments
         res ← mkLambdaFVars #[ctorArg] res
         res ← mkAppM ``Exists #[res]
       mkAppM ``Eq #[res, mkConst ``True]
@@ -118,6 +120,7 @@ def generateDatatypeExhaustivenessFact (idt : Expr) (paramNames : Array Name) :
       | [] => -- `idtBody` is an inductive datatype with no constructors. This means that there cannot exist any elements of type `idtBody`
         let cExp ← mkForallFVars (idtParams.push idtFVar) $ mkConst ``False
         let c := Clause.fromForallExpr paramNames cExp
+        trace[duper.rule.datatypeExhaustiveness] "About to add {c} to passive set"
         addNewToPassive c {parents := #[], ruleName := "datatypeExhaustiveness (empty inductive datatype)", mkProof := mkEmptyDatatypeExhaustivenessProof} maxGoalDistance 0 #[]
       | ctor1 :: restConstructors =>
         let mut cBody ← makeConstructorEquality idtFVar ctor1 lvls idtArgs

From 34330cf3110706fc50d5e48e8f3b0ecbea0035a3 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Sat, 20 Jul 2024 01:27:12 -0400
Subject: [PATCH 10/10] Update to lean v4.9.1

---
 lake-manifest.json | 8 ++++----
 lakefile.lean      | 4 ++--
 lean-toolchain     | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index bbbf7bf..8cf38cb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,19 +4,19 @@
  [{"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "542821345b1e8eb8e244dacafa96d677d0a55340",
+   "rev": "bfb20f93b4e67029b977f218c67d8ca87ca09c9a",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "542821345b1e8eb8e244dacafa96d677d0a55340",
+   "inputRev": "bfb20f93b4e67029b977f218c67d8ca87ca09c9a",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
+   "rev": "dcea9ce8aba248927fb2ea8d5752bfe1e3fe7b44",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.9.0",
+   "inputRev": "v4.9.1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",
diff --git a/lakefile.lean b/lakefile.lean
index b5805ff..18facb8 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"@"542821345b1e8eb8e244dacafa96d677d0a55340"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.9.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"bfb20f93b4e67029b977f218c67d8ca87ca09c9a"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.9.1"
 
 package Duper {
   precompileModules := true
diff --git a/lean-toolchain b/lean-toolchain
index 4ef27c4..acd5c69 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.9.1