From 1aea756894f3bb070e439ef2215f6c6941f9d4ac Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Wed, 19 Jun 2024 20:20:02 -0400 Subject: [PATCH] Datatype injectivity rules --- Duper/Rules/BoolSimp.lean | 13 +- Duper/Rules/DatatypeDistinctness.lean | 2 +- Duper/Rules/DatatypeInjectivity.lean | 173 ++++++++++++++++++++++++++ Duper/Saturate.lean | 3 + Duper/Tests/test_regression.lean | 21 +++- Duper/Util/ProofReconstruction.lean | 36 +++++- 6 files changed, 234 insertions(+), 14 deletions(-) create mode 100644 Duper/Rules/DatatypeInjectivity.lean diff --git a/Duper/Rules/BoolSimp.lean b/Duper/Rules/BoolSimp.lean index 00b154f..feb2da8 100644 --- a/Duper/Rules/BoolSimp.lean +++ b/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 diff --git a/Duper/Rules/DatatypeDistinctness.lean b/Duper/Rules/DatatypeDistinctness.lean index 37efbeb..200e589 100644 --- a/Duper/Rules/DatatypeDistinctness.lean +++ b/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) diff --git a/Duper/Rules/DatatypeInjectivity.lean b/Duper/Rules/DatatypeInjectivity.lean new file mode 100644 index 0000000..9aff72f --- /dev/null +++ b/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 diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean index 59d79b6..b0bf767 100644 --- a/Duper/Saturate.lean +++ b/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, diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index 9aa6832..99efcaf 100644 --- a/Duper/Tests/test_regression.lean +++ b/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} diff --git a/Duper/Util/ProofReconstruction.lean b/Duper/Util/ProofReconstruction.lean index 1641ea0..8dfe840 100644 --- a/Duper/Util/ProofReconstruction.lean +++ b/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