Dev

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

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,125 @@ 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 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
+  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,
+    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. 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 × 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
+    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 ← isInductiveAndNonPropAndNotTypeClass fType
+        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"
+  | 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 ← isInductiveAndNonPropAndNotTypeClass fType
+      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.any (fun (t, _) => t == fType) then (fType, paramNames) :: datatypeList
+      else 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.any (fun (t', _) => t' == t) then (t, paramNames) :: datatypeList
+      else 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 paramNames
+    let mut datatypeArr := #[]
+    -- Remove freshMVar from all acquired datatypes
+    for (datatype, datatypeParams) in datatypeList do
+      if datatype.hasAnyMVar (fun mvarid => mvarid == freshMVarId) then
+        let datatype ← mkForallFVars #[freshMVar] datatype
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
+      else
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
+    pure (symbolFreqArityMap, datatypeArr.toList)
+  | Expr.forallE _ t b _ =>
+    let tIsInductive ← isInductiveAndNonPropAndNotTypeClass t
+    let datatypeList :=
+      if tIsInductive && !datatypeList.any (fun (t', _) => t' == t) then (t, paramNames) :: datatypeList
+      else 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 paramNames
+    let mut datatypeArr := #[]
+    -- Remove freshMVar from all acquired datatypes
+    for (datatype, datatypeParams) in datatypeList do
+      if datatype.hasAnyMVar (fun mvarid => mvarid == freshMVarId) then
+        let datatype ← mkForallFVars #[freshMVar] datatype
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
+      else
+        datatypeArr := datatypeArr.push (datatype, datatypeParams)
+    pure (symbolFreqArityMap, datatypeArr.toList)
+  | Expr.letE _ _ v b _ =>
+    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.any (fun (t, _) => t == fType) then
+      updateSymbolFreqArityMapAndDatatypeList b symbolFreqArityMap ((fType, paramNames) :: datatypeList) paramNames
+    else
+      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.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.any (fun (t, _) => t == fType) then
+      return (symbolFreqArityMap, (fType, paramNames) :: 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 +226,25 @@ 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. 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
+    trace[duper.collectDatatypes.debug] "Loaded clause c: {c.lits}"
+    for l in c.lits do
+      (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)
+
 /-- 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 +299,57 @@ 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.
+    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) := #[]
+  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)

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