Implemented distPos rule

Duper/Order.lean

@@ -85,7 +85,7 @@ def getHead (t : Expr) := match t with
 | Expr.forallE .. => mkConst ``FORALL
 | Expr.app (Expr.app (Expr.const ``Exists _) _) _  => mkConst ``EXISTS
 | Expr.mdata _ t => getHead t
-| _ => t.getAppFn
+| _ => t.getAppFn'
 
 def getArgs (t : Expr) := match t with
 | Expr.lam _ ty b _ => [ty, b]
@@ -396,7 +396,7 @@ def precCompare (f g : Expr) (symbolPrecMap : SymbolPrecMap) : MetaM Comparison
 /-- Overapproximation of being fluid -/
 def isFluid (t : Expr) :=
   let t := t.consumeMData
-  (t.isApp && t.getAppFn.isMVar') || (t.isLambda && t.hasMVar)
+  (t.isApp && t.getAppFn'.isMVar') || (t.isLambda && t.hasMVar)
 
 mutual
 

Duper/Rules/DatatypeDistinctness.lean

@@ -0,0 +1,89 @@
+import Duper.Simp
+import Duper.Util.ProofReconstruction
+
+namespace Duper
+open Std
+open RuleM
+open SimpResult
+open Lean
+open Meta
+
+initialize Lean.registerTraceClass `duper.rule.datatypeDistinctness
+
+def litEquatesDistinctConstructors (lit : Lit) : MetaM Bool := do
+  let litTyIsInductive ← matchConstInduct lit.ty.getAppFn' (fun _ => pure false) (fun _ _ => pure true)
+  if litTyIsInductive then
+    trace[duper.rule.datatypeDistinctness] "lit.ty {lit.ty} is an inductive datatype"
+    let lhsCtorOpt ← matchConstCtor lit.lhs.getAppFn' (fun _ => pure none) (fun cval lvls => pure (some (cval, lvls)))
+    let rhsCtorOpt ← matchConstCtor lit.rhs.getAppFn' (fun _ => pure none) (fun cval lvls => pure (some (cval, lvls)))
+    match lhsCtorOpt, rhsCtorOpt with
+    | some lhsCtor, some rhsCtor =>
+      trace[duper.rule.datatypeDistinctness] "Both lit.lhs {lit.lhs} and lit.rhs {lit.rhs} have constructors as heads"
+      return lhsCtor != rhsCtor
+    | _, _ =>
+      trace[duper.rule.datatypeDistinctness] "Either lit.lhs {lit.lhs} or lit.rhs {lit.rhs} does not have a constructor at its head"
+      return false
+  else -- `lit.ty` is not an inductive datatype so `lit` cannot be equating distinct constructors
+    trace[duper.rule.datatypeDistinctness] "lit.ty {lit.ty} is not an inductive datatype"
+    return false
+
+def mkDistPosProof (refs : List (Option Nat)) (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 (parentsLits, appliedPremises, transferExprs) ← instantiatePremises parents premises xs transferExprs
+    let parentLits := parentsLits[0]!
+    let appliedPremise := appliedPremises[0]!
+
+    let mut proofCases : Array Expr := Array.mkEmpty parentLits.size
+    for i in [:parentLits.size] do
+      let lit := parentLits[i]!
+      if ← litEquatesDistinctConstructors lit then
+        let matchConstInductK := (fun ival lvls => pure (some (ival.name, ival.numParams, lvls)))
+        let some (tyName, numParams, lvls) ← matchConstInduct lit.ty.getAppFn' (fun _ => pure none) matchConstInductK
+          | throwError "mkDistPosProof :: Failed to find the inductive datatype corresponding to {lit.ty}"
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          let noConfusionArgs := #[some (mkConst ``False), none, none, some h]
+          -- noConfusion first takes `numParams` arguments for parameters, so we need to add that many `none`s to the front of `noConfusionArgs`
+          let noConfusionArgs := (Array.range numParams).map (fun _ => none) ++ noConfusionArgs
+          let proofCase ← mkAppOptM' (mkConst (.str tyName "noConfusion") (0 :: lvls)) noConfusionArgs
+          let proofCase := mkApp2 (mkConst ``False.elim [levelZero]) body proofCase
+          Meta.mkLambdaFVars #[h] proofCase
+        proofCases := proofCases.push proofCase
+      else -- refs[i] should have the value (some j) where parentLits[i] == c[j]
+        match refs[i]! with
+        | none =>
+          panic! "There is a bug in mkDistPosProof (The refs invariant is not satisfied)"
+        | some j =>
+          let proofCase ← Meta.withLocalDeclD `h parentLits[i]!.toExpr fun h => do
+            Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) j h
+          proofCases := proofCases.push proofCase
+    let proof ← orCases (parentLits.map Lit.toExpr) proofCases
+    Meta.mkLambdaFVars xs $ mkApp proof appliedPremise
+
+/-- Implements the Dist-S⁺ rule described in https://arxiv.org/pdf/1611.02908 -/
+def distPos : MSimpRule := fun c => do
+  let c ← loadClause c
+  /- Spec for newLits and refs:
+     - If c.lits[i] equates distinct constructors (e.g. has the form `f s = g t` where `f` and `g` are constructors),
+       then refs[i] = none
+     - If c.lits[i] does not equate distinct constructors, then refs[i] = some j where newLits[j] = c.lits[i] -/
+  let mut newLits : List Lit := []
+  let mut refs : List (Option Nat) := []
+  for lit in c.lits do
+    if ← litEquatesDistinctConstructors lit then
+      refs := none :: refs
+    else
+      refs := (some newLits.length) :: refs
+      newLits := lit :: newLits
+  -- To achieve the desired spec for newLits and refs, I must reverse them
+  newLits := newLits.reverse
+  refs := refs.reverse
+  if (newLits.length = c.lits.size) then
+    return none
+  else
+    trace[duper.rule.datatypeDistinctness] "datatypeDistinctness applied with the newLits: {newLits}"
+    let yc ← yieldClause (MClause.mk newLits.toArray) "datatype dist-S+" (some (mkDistPosProof refs))
+    return some #[yc]
+
+end Duper

Duper/Saturate.lean

@@ -26,6 +26,8 @@ import Duper.Rules.EqHoist
 import Duper.Rules.ExistsHoist
 import Duper.Rules.ForallHoist
 import Duper.Rules.NeHoist
+-- Inductive datatype rules
+import Duper.Rules.DatatypeDistinctness
 -- Higher order rules
 import Duper.Rules.ArgumentCongruence
 import Duper.Rules.FluidSup
@@ -66,15 +68,15 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
+      distPos.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
       (forwardEqualitySubsumption subsumptionTrie).toSimpRule,
       (forwardContextualLiteralCutting subsumptionTrie).toSimpRule,
       (forwardPositiveSimplifyReflect subsumptionTrie).toSimpRule,
       (forwardNegativeSimplifyReflect subsumptionTrie).toSimpRule,
-      -- Higher order rules
-      identBoolHoist.toSimpRule
+      identBoolHoist.toSimpRule -- Higher order rule
     ]
   else
     return #[
@@ -89,14 +91,14 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       destructiveEqualityResolution.toSimpRule,
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
+      distPos.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
       (forwardEqualitySubsumption subsumptionTrie).toSimpRule,
       (forwardContextualLiteralCutting subsumptionTrie).toSimpRule,
       (forwardPositiveSimplifyReflect subsumptionTrie).toSimpRule,
       (forwardNegativeSimplifyReflect subsumptionTrie).toSimpRule,
-      -- Higher order rules
-      identBoolHoist.toSimpRule
+      identBoolHoist.toSimpRule -- Higher order rule
     ]
 
 -- The first `Clause` is the given clause

Duper/Tests/test_regression.lean

@@ -690,3 +690,32 @@ example (a b : Nat) (matrix : Fin a → Fin b → Nat)
   (h : ∀ n : Nat, ∀ m : Nat, (fun x => transpose n m (transpose m n x)) = (fun x => x)) :
   transpose b a (transpose a b matrix) = matrix := by
   duper [h]
+
+--###############################################################################################################################
+-- Inductive datatype tests
+
+inductive myType
+| const1 : myType
+| const2 : myType
+
+inductive myType2 (t : Type _)
+| const3 : t → myType2 t
+| const4 : t → myType2 t
+
+inductive myType3
+| const5 : myType3
+| const6 : myType3 → myType3
+
+open myType myType2 myType3
+
+example : const1 ≠ const2 := by
+  duper
+
+example : const3 (Type 8) ≠ const4 (Type 8) := by
+  duper
+
+example : const5 ≠ const6 const5 := by
+  duper
+
+example : [] ≠ [2] := by
+  duper