Datatype injectivity rules

Duper/Rules/BoolSimp.lean

@@ -223,19 +223,10 @@ partial def mkRule26Theorem (e : Expr) (counter : Nat) (i : Nat) (j : Nat) : Met
     let iIdx := (counter - 1) - i
     orIntro goals j (Expr.bvar iIdx)
 
-/-- Assuming e has the form e1 ∧ e2 ∧ ... ∧ en, returns an array #[e1, e2, ... en].
-    Note: If e has the form (e1a ∧ e1b) ∧ e2 ∧ ... ∧ en, then the conjunction (e1a ∧ e1b) will
-    be considered e1 (and the conjunction e1 will not be broken down further). This decision is made
-    to reflect the form of the conjunction assumed by ProofReconstruction.lean's `andGet` -/
-partial def getConjunctiveHypotheses (e : Expr) (hyps : Array Expr) : Array Expr :=
-  match e.consumeMData with
-  | Expr.app (Expr.app (Expr.const ``And _) e1) e2 => getConjunctiveHypotheses e2 (hyps.push e1)
-  | _ => hyps.push e
-
 partial def mkRule27Theorem (e : Expr) (i : Nat) (j : Nat) : MetaM Expr := do
   match e.consumeMData with
   | Expr.forallE _ t b _ =>
-    let hyps := (getConjunctiveHypotheses t #[]).toList
+    let hyps := getConjunctiveHypotheses t
     let goals := getDisjunctiveGoals b #[]
     let iHypProof ← andGet hyps i (Expr.bvar 0)
     let innerBody ← orIntro goals j iHypProof
@@ -547,7 +538,7 @@ partial def applyRule27 (e : Expr) : RuleM (Option (Nat × Nat)) := do
   | e@(Expr.forallE ..) => Meta.forallBoundedTelescope e (some 1) fun xs b => do
     if !(← inferType b).isProp then return none -- Prevents applying rule27 to expressions like Nat → Nat
     let t ← inferType xs[0]!
-    let hyps := getConjunctiveHypotheses t #[]
+    let hyps := getConjunctiveHypothesesHelper t
     let goals := getDisjunctiveGoals b #[]
     let mut goalIdx := 0
     for goal in goals do

Duper/Rules/DatatypeDistinctness.lean

@@ -10,7 +10,7 @@ open Meta
 
 initialize Lean.registerTraceClass `duper.rule.datatypeDistinctness
 
-/-- Returns `none` if `lit` does not compare distinct instructors, returns `some false` if `lit` says two distinct
+/-- Returns `none` if `lit` does not compare distinct constructors, returns `some false` if `lit` says two distinct
     constructors are equal, and returns `some true` if `lit` says two distinct constructors are not equal. -/
 def litComparesDistinctConstructors (lit : Lit) : MetaM (Option Bool) := do
   let litTyIsInductive ← matchConstInduct lit.ty.getAppFn' (fun _ => pure false) (fun _ _ => pure true)

Duper/Rules/DatatypeInjectivity.lean

@@ -0,0 +1,173 @@
+import Duper.Simp
+import Duper.Util.ProofReconstruction
+
+namespace Duper
+open Std
+open RuleM
+open SimpResult
+open Lean
+open Meta
+
+initialize Lean.registerTraceClass `duper.rule.datatypeInjectivity
+
+/-- Returns `none` if `lit` does not compare identical constructors, returns `some true` if `lit` says two identical
+    constructors are equal, and returns `some false` if `lit` says two identical constructors are not equal. -/
+def litComparesIdenticalConstructors (lit : Lit) : MetaM (Option Bool) := do
+  let litTyIsInductive ← matchConstInduct lit.ty.getAppFn' (fun _ => pure false) (fun _ _ => pure true)
+  if litTyIsInductive then
+    trace[duper.rule.datatypeInjectivity] "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.datatypeInjectivity] "Both lit.lhs {lit.lhs} and lit.rhs {lit.rhs} have constructors as heads"
+      if lhsCtor == rhsCtor then return lit.sign
+      else return none
+    | _, _ => -- `lit` is not comparing two constructors
+      trace[duper.rule.datatypeInjectivity] "Either lit.lhs {lit.lhs} or lit.rhs {lit.rhs} does not have a constructor at its head"
+      return none
+  else -- `lit.ty` is not an inductive datatype so `lit` cannot be comparing identical constructors
+    trace[duper.rule.datatypeInjectivity] "lit.ty {lit.ty} is not an inductive datatype"
+    return none
+
+def mkDatatypeInjectivityPosProof (removedLitNum ctorArgNum : 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 i == removedLitNum then -- `lit` is the constructor equality to be replaced with the argument equality
+        let matchConstCtorK := (fun cval lvls => pure (some (cval, lvls)))
+        let some (sharedCtor, sharedCtorLvls) ← matchConstCtor lit.lhs.getAppFn' (fun _ => pure none) matchConstCtorK
+          | throwError "mkDatatypeInjectivityPosProof :: Failed to find the constructor at the head of both sides of {lit}"
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          /- injEq first takes `numParams` arguments for the inductive datatype's parameters, then the lhs constructor's arguments
+             (not including the datatype's parameter arguments), and finally, rhs constructor's arguments (again not including the
+             datatype's parameter arguments) -/
+          let datatypeParamArgs := (Array.range sharedCtor.numParams).map (fun _ => none)
+          let lhsArgs := (lit.lhs.consumeMData.getAppArgs.toList.drop sharedCtor.numParams).map (fun x => some x)
+          let rhsArgs := (lit.rhs.consumeMData.getAppArgs.toList.drop sharedCtor.numParams).map (fun x => some x)
+          let injEqArgs := datatypeParamArgs ++ lhsArgs.toArray ++ rhsArgs.toArray
+          let proofCase ← mkAppOptM' (mkConst (.str sharedCtor.name "injEq") sharedCtorLvls) injEqArgs
+          let proofCase ← Meta.mkAppM ``Eq.mp #[proofCase, h]
+          let proofCase ← andGet (getConjunctiveHypotheses (← inferType proofCase)) ctorArgNum proofCase
+          Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i proofCase
+        proofCases := proofCases.push proofCase
+      else -- `lit` is not the constructor equality that is currently being modified
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i h
+        proofCases := proofCases.push proofCase
+    let proof ← orCases (parentLits.map Lit.toExpr) proofCases
+    Meta.mkLambdaFVars xs $ mkApp proof appliedPremise
+
+/- Note: This proof reconstruction procedure will fail if it is run on a constructor inequality where the constructor
+   contains zero arguments (e.g. `[] ≠ []`). However, this should never occur so long as Saturate.lean's `forwardSimpRules`
+   array contains `elimResolvedLit` before `datatypeInjectivity` -/
+def mkDatatypeInjectivityNegProof (removedLitNum : 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 i == removedLitNum then -- `lit` is the constructor inequality to be replaced with the argument inequality disjunction
+        let matchConstCtorK := (fun cval lvls => pure (some (cval, lvls)))
+        let some (sharedCtor, sharedCtorLvls) ← matchConstCtor lit.lhs.getAppFn' (fun _ => pure none) matchConstCtorK
+          | throwError "mkDatatypeInjectivityNegProof :: Failed to find the constructor at the head of both sides of {lit}"
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          /- injEq first takes `numParams` arguments for the inductive datatype's parameters, then the lhs constructor's arguments
+             (not including the datatype's parameter arguments), and finally, rhs constructor's arguments (again not including the
+             datatype's parameter arguments) -/
+          let datatypeParamArgs := (Array.range sharedCtor.numParams).map (fun _ => none)
+          let lhsArgs := (lit.lhs.consumeMData.getAppArgs.toList.drop sharedCtor.numParams).map (fun x => some x)
+          let rhsArgs := (lit.rhs.consumeMData.getAppArgs.toList.drop sharedCtor.numParams).map (fun x => some x)
+          let injEqArgs := datatypeParamArgs ++ lhsArgs.toArray ++ rhsArgs.toArray
+          let injEq ← mkAppOptM' (mkConst (.str sharedCtor.name "injEq") sharedCtorLvls) injEqArgs
+          -- `injEq : (constructor x1 y1 = constructor x2 y2) = (x1 = x2 ∧ y1 = y2)`
+          let argEqualities ←
+            match ← inferType injEq with
+            | Expr.app (Expr.app (Expr.app (Expr.const ``Eq [_]) _) _) e2 => pure e2
+            | _ => throwError "mkDatatypeInjectivityNegProof :: Type of {injEq} is not an equality as expected"
+          let propMVar ← mkFreshExprMVar (mkSort levelZero)
+          let abstrLam ← mkLambdaFVars #[propMVar] $ ← mkAppM ``Eq #[← mkAppM ``Not #[propMVar], ← mkAppM ``Not #[argEqualities]]
+          let proofCase ← mkAppM ``Eq.mpr #[← mkAppM ``congrArg #[abstrLam, injEq], ← mkAppM ``Eq.refl #[← mkAppM ``Not #[argEqualities]]]
+          let proofCase ← mkAppM ``Eq.mp #[proofCase, h]
+          let proofCase ← notAndDistribute (← inferType proofCase) proofCase
+          Meta.mkLambdaFVars #[h] $ ← orSubclause (cLits.map Lit.toExpr) (1 + cLits.size - parentLits.size) proofCase
+        proofCases := proofCases.push proofCase
+      else -- `lit` is not the constructor inequality that is currently being modified
+        let proofCase ← Meta.withLocalDeclD `h lit.toExpr fun h => do
+          Meta.mkLambdaFVars #[h] $ ← orIntro (cLits.map Lit.toExpr) i h
+        proofCases := proofCases.push proofCase
+    let proof ← orCases (parentLits.map Lit.toExpr) proofCases
+    Meta.mkLambdaFVars xs $ mkApp proof appliedPremise
+
+/-- Implements the injectivity rules described in section 6.3 of https://arxiv.org/pdf/1611.02908 -/
+def datatypeInjectivity : MSimpRule := fun c => do
+  let c ← loadClause c
+  for i in [:c.lits.size] do
+    let lit := c.lits[i]!
+    match ← litComparesIdenticalConstructors lit with
+    | some true => -- datatypeInjectivity⁺ (the first of the rules described in above paper)
+      let lhsArgs := lit.lhs.consumeMData.getAppArgs
+      let rhsArgs := lit.rhs.consumeMData.getAppArgs
+      let numArgs ←
+        if lhsArgs.size != rhsArgs.size then
+          throwError "datatypeInjectivity: The same constructor takes different numbers of arguments in {lit.lhs} and {lit.rhs}"
+        else pure lhsArgs.size
+      let numTyParams ← matchConstInduct lit.ty.getAppFn' (fun _ => pure 0) (fun ival _ => pure ival.numParams)
+      -- Create `numArgs` conclusions each of the form `cWithoutLit ∨ lhsArgs[k] = rhsArgs[k]` (where `numTyParams ≤ k < numArgs`)
+      let mut conclusions : Array (Clause × Proof) := #[]
+      for k in [numTyParams:numArgs] do --Iterate over actual constructor arguments (skipping the inductive datatype's parameters)
+        let lhsArg := lhsArgs[k]!
+        let rhsArg := rhsArgs[k]!
+        let ty ← inferType lhsArg
+        let tyLvl := (← inferType ty).sortLevel!
+        let argEqLit : Lit := {
+          sign := true,
+          lvl := tyLvl,
+          ty := ty,
+          lhs := lhsArg,
+          rhs := rhsArg
+        }
+        let mclause := MClause.mk $ c.lits.set! i argEqLit
+        conclusions := conclusions.push $ ← yieldClause mclause "datatypeInjectivity+" $ mkDatatypeInjectivityPosProof i (k - numTyParams)
+      trace[duper.rule.datatypeInjectivity] "datatypeInjectivity+ applied to {c.lits} to create conclusions {conclusions.map (fun x => x.1)}"
+      return some conclusions
+    | some false => -- datatypeInjectivity⁻ (the second of the rules described in above paper)
+      let lhsArgs := lit.lhs.consumeMData.getAppArgs
+      let rhsArgs := lit.rhs.consumeMData.getAppArgs
+      let numArgs ←
+        if lhsArgs.size != rhsArgs.size then
+          throwError "datatypeInjectivity: The same constructor takes different numbers of arguments in {lit.lhs} and {lit.rhs}"
+        else pure lhsArgs.size
+      let mut res : Array Lit := #[]
+      for j in [:c.lits.size] do
+        if i != j then res := res.push c.lits[j]!
+      let numTyParams ← matchConstInduct lit.ty.getAppFn' (fun _ => pure 0) (fun ival _ => pure ival.numParams)
+      -- For each `k` such that `numTyParams ≤ k < numArgs`, add the literal `lhsArgs[k] ≠ rhsArgs[k]` onto `res`
+      for k in [numTyParams:numArgs] do
+        let lhsArg := lhsArgs[k]!
+        let rhsArg := rhsArgs[k]!
+        let ty ← inferType lhsArg
+        let tyLvl := (← inferType ty).sortLevel!
+        let kLit : Lit := {
+          sign := false,
+          lvl := tyLvl,
+          ty := ty,
+          lhs := lhsArg,
+          rhs := rhsArg
+        }
+        res := res.push kLit
+      let yC ← yieldClause (MClause.mk res) "datatypeInjectivity-" $ mkDatatypeInjectivityNegProof i
+      trace[duper.rule.datatypeInjectivity] "datatypeInjectivity- applied to {c.lits} to yield {yC.1}"
+      return some #[yC]
+    | none => continue
+  return none

Duper/Saturate.lean

@@ -28,6 +28,7 @@ import Duper.Rules.ForallHoist
 import Duper.Rules.NeHoist
 -- Inductive datatype rules
 import Duper.Rules.DatatypeDistinctness
+import Duper.Rules.DatatypeInjectivity
 -- Higher order rules
 import Duper.Rules.ArgumentCongruence
 import Duper.Rules.FluidSup
@@ -69,6 +70,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
       datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       decElim.toSimpRule,
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
@@ -92,6 +94,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       identPropFalseElim.toSimpRule,
       identBoolFalseElim.toSimpRule,
       datatypeDistinctness.toSimpRule, -- Inductive datatype rule
+      datatypeInjectivity.toSimpRule, -- Inductive datatype rule
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
       (forwardEqualitySubsumption subsumptionTrie).toSimpRule,

Duper/Tests/test_regression.lean

@@ -706,7 +706,10 @@ inductive myType3
 | const5 : myType3
 | const6 : myType3 → myType3
 
-open myType myType2 myType3
+inductive myType4 (t1 t2 : Type _)
+| const7 : t1 → t2 → myType4 t1 t2
+
+open myType myType2 myType3 myType4
 
 example : const1 ≠ const2 := by
   duper
@@ -719,3 +722,19 @@ example : const5 ≠ const6 const5 := by
 
 example : [] ≠ [2] := by
   duper
+
+example (p : Prop) (t1 t2 : Type a) (t3 t4 : Type b) (h : p = True ∨ const7 t1 t3 = const7 t2 t4) :
+  ¬p → t1 = t2 ∧ t3 = t4 := by
+  duper [h]
+
+example (p : Prop) (a b c : Nat) (h : [0, 1, 2] = [a, b, c] ∨ p = True) :
+  ¬p → 0 = a ∧ 1 = b ∧ 2 = c := by duper [h]
+
+example (a b x y : Nat) (f : Nat → Nat)
+  (h1 : ∀ z1 z2 : Nat, z1 ≠ z2 → f z1 ≠ f z2)
+  (h2 : [0, a, x, 3] ≠ [0, b, y, 3]) :
+  f a ≠ f b ∨ f x ≠ f y := by
+  duper [h1, h2] {portfolioInstance := 7}
+
+example (x y : Nat) (h : [x] ≠ [y]) : x ≠ y := by
+  duper [h] {portfolioInstance := 7}

Duper/Util/ProofReconstruction.lean

@@ -6,6 +6,7 @@ import Duper.Util.Misc
 namespace Duper
 open RuleM
 open Lean
+open Meta
 
 initialize Lean.registerTraceClass `duper.instantiatePremises
 
@@ -89,7 +90,7 @@ def andBuild (l : List Expr) : MetaM Expr :=
   | l1 :: List.nil => return l1
   | l1 :: restL => return mkApp2 (mkConst ``And) l1 $ ← andBuild restL
 
-/-- Given a proof of `l[0] ∧ ... ∧ l[n]`, constructs a proof of `l[i]` -/
+/-- Given a proof of a conjunction with `n` conjuncts, constructs a proof of `i`-th conjunct -/
 def andGet (l : List Expr) (i : Nat) (proof : Expr) : MetaM Expr := do
   match l with
   | List.nil => throwError "andGet index {i} out of bound (l is {l})"
@@ -100,4 +101,37 @@ def andGet (l : List Expr) (i : Nat) (proof : Expr) : MetaM Expr := do
     if i == 0 then return mkApp3 (mkConst ``And.left) l1 (← andBuild restL) proof
     else andGet restL (i - 1) $ mkApp3 (mkConst ``And.right) l1 (← andBuild restL) proof
 
+/-- Assuming `e` has the form `e1 ∧ e2 ∧ ... ∧ en`, returns an array `#[e1, e2, ... en]`.
+    Note: If e has the form `(e1a ∧ e1b) ∧ e2 ∧ ... ∧ en`, then the conjunction `(e1a ∧ e1b)` will
+    be considered `e1` (and the conjunction e1 will not be broken down further). This decision is made
+    to reflect the form of the conjunction assumed by `andGet` -/
+partial def getConjunctiveHypothesesHelper (e : Expr) (hyps : Array Expr := #[]) : Array Expr :=
+  match e.consumeMData with
+  | Expr.app (Expr.app (Expr.const ``And _) e1) e2 => getConjunctiveHypothesesHelper e2 (hyps.push e1)
+  | _ => hyps.push e
+
+/-- Assuming `e` has the form `e1 ∧ e2 ∧ ... ∧ en`, returns a list `[e1, e2, ... en]`.
+    Note: If `e` has the form `(e1a ∧ e1b) ∧ e2 ∧ ... ∧ en`, then the conjunction `(e1a ∧ e1b)` will
+    be considered `e1` (and the conjunction `e1` will not be broken down further). This decision is made
+    to reflect the form of the conjunction assumed by `andGet` -/
+def getConjunctiveHypotheses (e : Expr) : List Expr := (getConjunctiveHypothesesHelper e #[]).toList
+
+theorem not_and_or (p q : Prop) : ¬(p ∧ q) ↔ ¬p ∨ ¬q := by
+  have : Decidable p := Classical.propDecidable p
+  exact Decidable.not_and_iff_or_not_not
+
+/-- Given a proof `prf` of type `e` which has the form `¬(p1 ∧ p2 ∧ ... pn)`, constructs a proof of `¬p1 ∨ ¬p2 ∨ ... ¬pn` -/
+partial def notAndDistribute (e prf : Expr) : MetaM Expr := do
+  match e.consumeMData with
+  | Expr.app (Expr.const ``Not _) (Expr.app (Expr.app (Expr.const ``And _) e1) e2) =>
+    let prf ← mkAppM ``Iff.mp #[mkApp2 (mkConst ``not_and_or) e1 e2, prf]
+    let rightMVar ← mkFreshExprMVar $ ← mkAppM ``Not #[e2]
+    let distributedE2Prf ← notAndDistribute e2 rightMVar
+    let distributedE2Type ← inferType distributedE2Prf
+    let rightPrf ← mkLambdaFVars #[rightMVar] $ ← mkAppOptM ``Or.inr #[some (← mkAppM ``Not #[e1]), none, some (← notAndDistribute e2 rightMVar)]
+    let leftMVar ← mkFreshExprMVar $ ← mkAppM ``Not #[e1]
+    let leftPrf ← mkLambdaFVars #[leftMVar] $ ← mkAppOptM ``Or.inl #[none, some distributedE2Type, some leftMVar]
+    mkAppM ``Or.elim #[prf, leftPrf, rightPrf]
+  | _ => pure prf
+
 end Duper