From 383ac53216bb0ed54fa8f139f7ac96cc87b4ea0b Mon Sep 17 00:00:00 2001 From: Sreeram Date: Fri, 8 May 2026 15:21:52 -0400 Subject: [PATCH 1/2] Completed datatypeAcyclicity --- Duper/Rules/DatatypeAcyclicity.lean | 109 +++++++++++++++++++++++++++- 1 file changed, 106 insertions(+), 3 deletions(-) diff --git a/Duper/Rules/DatatypeAcyclicity.lean b/Duper/Rules/DatatypeAcyclicity.lean index 7fd6eda..e420753 100644 --- a/Duper/Rules/DatatypeAcyclicity.lean +++ b/Duper/Rules/DatatypeAcyclicity.lean @@ -13,6 +13,48 @@ open LitSide initialize Lean.registerTraceClass `duper.rule.datatypeAcyclicity +theorem one_add_ge (n : Nat) : 1 + n > n := by + let h1 := Nat.le_refl n + let h2 := Nat.lt_succ_of_le h1 + rw [Nat.succ_eq_one_add] at h2 + exact h2 + +def addAllRight (head : Expr) (xs : Array Expr) : MetaM Expr := do + xs.foldlM (init := head) fun acc lit => do mkAppM ``Nat.lt_add_right #[← mkAppM ``sizeOf #[lit], acc] + +def buildLeftSum (head : Expr) (xs : Array Expr) : MetaM Expr := + xs.foldlM (init := head) fun acc lit => mkAppM ``HAdd.hAdd #[acc, lit] + +def liftAddRight (eq s : Expr) : MetaM Expr := do + let f ← withLocalDeclD `t (mkConst ``Nat) fun t => do + mkLambdaFVars #[t] (← mkAppM ``HAdd.hAdd #[t, s]) + mkAppM ``congrArg #[f, eq] + +def flattenAddRight (head : Expr) (xs : Array Expr) : MetaM Expr := do + let n := xs.size + if n ≤ 1 then + return ← mkAppM ``Eq.refl #[← buildLeftSum head xs] + let innerSum ← buildLeftSum xs[0]! (xs.extract 1 n) + let lhs ← mkAppM ``HAdd.hAdd #[head, innerSum] + let mut eq ← mkAppM ``Eq.refl #[lhs] + for k in [:n - 1] do + let stillIn := xs.extract 0 (n - 1 - k) + let remaining ← buildLeftSum xs[0]! (stillIn.extract 1 stillIn.size) + let assocSymm ← mkAppM ``Eq.symm #[← mkAppM ``Nat.add_assoc #[head, remaining, xs[n - 1 - k]!]] + let alreadyOut := xs.extract (n - k) n + let lifted ← alreadyOut.foldlM (init := assocSymm) liftAddRight + eq ← mkAppM ``Eq.trans #[eq, lifted] + return eq + +partial def bubbleToLeft (spec : Expr) (sizes : Array Expr) (idx : Nat) : MetaM Expr := do + if idx = 0 then return spec + let prefixSum ← buildLeftSum (mkNatLit 1) (sizes.extract 0 (idx - 1)) + let comm ← mkAppM ``Nat.add_right_comm #[prefixSum, sizes[idx - 1]!, sizes[idx]!] + let suffix := sizes.extract (idx + 1) sizes.size + let lifted ← suffix.foldlM (init := comm) liftAddRight + let newSpec ← mkAppM ``Eq.trans #[spec, lifted] + bubbleToLeft newSpec (sizes.swapIfInBounds (idx - 1) idx) (idx - 1) + /-- Produces a list of (possibly duplicate) constructor subterms for `e` -/ partial def collectConstructorSubterms (e : Expr) : MetaM (Array Expr) := do let isConstructor ← matchConstCtor e.getAppFn' (fun _ => pure false) (fun _ _ => pure true) @@ -22,6 +64,61 @@ partial def collectConstructorSubterms (e : Expr) : MetaM (Array Expr) := do else return #[e] +/-- Builds a proof of `sizeOf lhs > sizeOf rhs` with `rhs` guaranteed to be a subterm of `lhs` -/ +partial def buildGtProof (lhs : Expr) (rhs : Expr) : MetaM Expr := do + let ctor := lhs.getAppFn + let some ctorName := ctor.constName? + | throwError "datatypeAcyclicity: lhs head is not a constant" + let ctorType ← inferType ctor + let explicitLhsArgs ← forallTelescopeReducing ctorType fun binders _ => + (binders.zip lhs.getAppArgs).filterMapM fun (b, a) => do + if (← b.fvarId!.getDecl).binderInfo.isExplicit then pure (some a) + else pure none + let specName := ctorName ++ `sizeOf_spec + unless (← getEnv).contains specName do throwError "datatypeAcyclicity: no sizeOf_spec for {ctorName}" + let specExpr ← mkConstWithFreshMVarLevels specName + let specImplicitCount ← forallTelescopeReducing (← inferType specExpr) fun binders _ => do + let mut count := 0 + for b in binders do + if !(← b.fvarId!.getDecl).binderInfo.isExplicit then + count := count + 1 + else + break + pure count + let nones := Array.replicate specImplicitCount none + let specApplied ← mkAppOptM specName (nones ++ explicitLhsArgs.map some) + let sizes ← explicitLhsArgs.mapM fun a => mkAppM ``sizeOf #[a] + match ← explicitLhsArgs.findIdxM? (fun a => isDefEq a rhs) with + | some rhsIdx => -- base case: `rhsIdx` is where `rhs` was found in the direct subterms of `lhs` + let rearranged ← bubbleToLeft specApplied sizes rhsIdx + let oneAddGe ← mkAppM ``one_add_ge #[← mkAppM ``sizeOf #[rhs]] + let lhsArgsExtra := explicitLhsArgs.eraseIdx! rhsIdx + let gtProof ← addAllRight oneAddGe lhsArgsExtra + let rearrangedSymm ← mkAppM ``Eq.symm #[rearranged] + let motive ← withLocalDeclD `y (mkConst ``Nat) fun y => do + mkLambdaFVars #[y] (← mkAppM ``LT.lt #[← mkAppM ``sizeOf #[rhs], y]) + mkAppOptM ``Eq.subst #[none, some motive, none, none, some rearrangedSymm, some gtProof] + | none => -- recursive case: `subtermIdx` is a direct subterm of `lhs` with `rhs` as a subterm + let some subtermIdx ← explicitLhsArgs.findIdxM? (fun term => do + let subterms ← collectConstructorSubterms term + subterms.anyM (fun s => isDefEq s rhs)) + | throwError "datatypeAcyclicity: rhs {rhs} not found among subterms" + let subterm := explicitLhsArgs[subtermIdx]! + let subProof ← buildGtProof subterm rhs + let lhsArgsExtra := explicitLhsArgs.eraseIdx! subtermIdx + let subProof ← addAllRight subProof lhsArgsExtra + let subProof ← mkAppM ``Nat.lt_add_left #[mkNatLit 1, subProof] + let rearranged ← bubbleToLeft specApplied sizes subtermIdx + let rearrangedSymm ← mkAppM ``Eq.symm #[rearranged] + let restInOrder := (sizes.extract 0 subtermIdx) ++ (sizes.extract (subtermIdx + 1) sizes.size) + let parenInner := #[sizes[subtermIdx]!] ++ restInOrder + let flattenEq ← flattenAddRight (mkNatLit 1) parenInner + let combined ← mkAppM ``Eq.trans #[flattenEq, rearrangedSymm] + let sizeOfRhs ← mkAppM ``sizeOf #[rhs] + let motive ← withLocalDeclD `y (mkConst ``Nat) fun y => do + mkLambdaFVars #[y] (← mkAppM ``LT.lt #[sizeOfRhs, y]) + mkAppOptM ``Eq.subst #[none, some motive, none, none, some combined, some subProof] + /-- Returns `none` if `lit` does not compare constructor subterms, and returns `some litside` if `lit.litside` is a subterm of the constructor it is being compared to. Note that `lit.litside` may not itself be a constructor (e.g. `xs` is a constructor subterm of `x :: xs`) -/ @@ -61,10 +158,16 @@ 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 sizeOfEq ← if lit.lhs.weight > lit.rhs.weight then + pure sizeOfEq + else + mkAppM ``Eq.symm #[sizeOfEq] + let lit := if lit.lhs.weight > lit.rhs.weight then lit else lit.symm 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 + let gtProof ← buildGtProof lit.lhs lit.rhs + let neProof ← mkAppM ``Nat.ne_of_gt #[gtProof] + sizeOfEqFalseMVarId.assign neProof 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}" @@ -86,7 +189,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" $ 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 From c6a42273b520991d01142cfe5d1c11a8bc2344ee Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 10 May 2026 22:38:21 -0400 Subject: [PATCH 2/2] Removing the no longer needed includeUnsafeAcyclicity option --- Duper/RuleM.lean | 12 ------- Duper/Rules/DatatypeAcyclicity.lean | 21 ++++++------ Duper/Saturate.lean | 53 ++--------------------------- Duper/Tests/test_regression.lean | 16 +++++++++ 4 files changed, 28 insertions(+), 74 deletions(-) diff --git a/Duper/RuleM.lean b/Duper/RuleM.lean index 291572a..830ac8a 100644 --- a/Duper/RuleM.lean +++ b/Duper/RuleM.lean @@ -38,11 +38,6 @@ register_option includeDatatypeRules : Bool := { descr := "Whether to include datatype rules (distinctness, injectivity, and acyclicity)" } -register_option includeUnsafeAcyclicity : Bool := { - defValue := false - descr := "Whether to include the unsafe datatype acyclicity rule" -} - def getInhabitationReasoning (opts : Options) : Bool := inhabitationReasoning.get opts @@ -58,9 +53,6 @@ def getIncludeExpensiveRules (opts : Options) : Bool := def getIncludeDatatypeRules (opts : Options) : Bool := includeDatatypeRules.get opts -def getIncludeUnsafeAcyclicity (opts : Options) : Bool := - includeUnsafeAcyclicity.get opts - def getInhabitationReasoningM : CoreM Bool := do let opts ← getOptions return getInhabitationReasoning opts @@ -81,10 +73,6 @@ def getIncludeDatatypeRulesM : CoreM Bool := do let opts ← getOptions return getIncludeDatatypeRules opts -def getIncludeUnsafeAcyclicityM : CoreM Bool := do - let opts ← getOptions - return getIncludeUnsafeAcyclicity opts - structure Context where order : Expr → Expr → Bool → MetaM Comparison symbolPrecMap : SymbolPrecMap diff --git a/Duper/Rules/DatatypeAcyclicity.lean b/Duper/Rules/DatatypeAcyclicity.lean index e420753..73e0d24 100644 --- a/Duper/Rules/DatatypeAcyclicity.lean +++ b/Duper/Rules/DatatypeAcyclicity.lean @@ -13,11 +13,7 @@ open LitSide initialize Lean.registerTraceClass `duper.rule.datatypeAcyclicity -theorem one_add_ge (n : Nat) : 1 + n > n := by - let h1 := Nat.le_refl n - let h2 := Nat.lt_succ_of_le h1 - rw [Nat.succ_eq_one_add] at h2 - exact h2 +theorem one_add_ge (n : Nat) : 1 + n > n := by grind def addAllRight (head : Expr) (xs : Array Expr) : MetaM Expr := do xs.foldlM (init := head) fun acc lit => do mkAppM ``Nat.lt_add_right #[← mkAppM ``sizeOf #[lit], acc] @@ -66,7 +62,7 @@ partial def collectConstructorSubterms (e : Expr) : MetaM (Array Expr) := do /-- Builds a proof of `sizeOf lhs > sizeOf rhs` with `rhs` guaranteed to be a subterm of `lhs` -/ partial def buildGtProof (lhs : Expr) (rhs : Expr) : MetaM Expr := do - let ctor := lhs.getAppFn + let ctor := lhs.getAppFn' let some ctorName := ctor.constName? | throwError "datatypeAcyclicity: lhs head is not a constant" let ctorType ← inferType ctor @@ -158,11 +154,14 @@ 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` - let sizeOfEq ← if lit.lhs.weight > lit.rhs.weight then - pure sizeOfEq - else - mkAppM ``Eq.symm #[sizeOfEq] - let lit := if lit.lhs.weight > lit.rhs.weight then lit else lit.symm + let sizeOfEq ← + match litSide with + | lhs => mkAppM ``Eq.symm #[sizeOfEq] + | rhs => pure sizeOfEq + let lit : Lit := + match litSide with + | lhs => lit.symm + | rhs => lit let sizeOfEqFalseMVar ← mkFreshExprMVar $ ← mkAppM ``Not #[← inferType sizeOfEq] -- Has the type `¬(sizeOf lit.lhs = sizeOf lit.rhs)` let sizeOfEqFalseMVarId := sizeOfEqFalseMVar.mvarId! let gtProof ← buildGtProof lit.lhs lit.rhs diff --git a/Duper/Saturate.lean b/Duper/Saturate.lean index f26e69a..8badb03 100644 --- a/Duper/Saturate.lean +++ b/Duper/Saturate.lean @@ -139,7 +139,7 @@ open SimpResult def forwardSimpRules : ProverM (Array SimpRule) := do let subsumptionTrie ← getSubsumptionTrie - if (← getIncludeExpensiveRulesM) && (← getIncludeDatatypeRulesM) && (← getIncludeUnsafeAcyclicityM) then + if (← getIncludeExpensiveRulesM) && (← getIncludeDatatypeRulesM) then return #[ betaEtaReduction.toSimpRule, clausificationStep.toSimpRule, @@ -164,31 +164,6 @@ def forwardSimpRules : ProverM (Array SimpRule) := do (forwardNegativeSimplifyReflect subsumptionTrie).toSimpRule, identBoolHoist.toSimpRule -- Higher order rule ] - else if (← getIncludeExpensiveRulesM) && (← getIncludeDatatypeRulesM) && !(← getIncludeUnsafeAcyclicityM) then - return #[ - betaEtaReduction.toSimpRule, - clausificationStep.toSimpRule, - syntacticTautologyDeletion1.toSimpRule, - syntacticTautologyDeletion2.toSimpRule, - boolSimp.toSimpRule, - syntacticTautologyDeletion3.toSimpRule, - elimDupLit.toSimpRule, - elimResolvedLit.toSimpRule, - destructiveEqualityResolution.toSimpRule, - identPropFalseElim.toSimpRule, - identBoolFalseElim.toSimpRule, - datatypeDistinctness.toSimpRule, -- Inductive datatype rule - datatypeInjectivity.toSimpRule, -- Inductive datatype rule - -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule - decElim.toSimpRule, - (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule, - (forwardClauseSubsumption subsumptionTrie).toSimpRule, - (forwardEqualitySubsumption subsumptionTrie).toSimpRule, - (forwardContextualLiteralCutting subsumptionTrie).toSimpRule, - (forwardPositiveSimplifyReflect subsumptionTrie).toSimpRule, - (forwardNegativeSimplifyReflect subsumptionTrie).toSimpRule, - identBoolHoist.toSimpRule -- Higher order rule - ] else if (← getIncludeExpensiveRulesM) && !(← getIncludeDatatypeRulesM) then return #[ betaEtaReduction.toSimpRule, @@ -211,7 +186,7 @@ def forwardSimpRules : ProverM (Array SimpRule) := do (forwardNegativeSimplifyReflect subsumptionTrie).toSimpRule, identBoolHoist.toSimpRule -- Higher order rule ] - else if !(← getIncludeExpensiveRulesM) && (← getIncludeDatatypeRulesM) && (← getIncludeUnsafeAcyclicityM) then + else if !(← getIncludeExpensiveRulesM) && (← getIncludeDatatypeRulesM) then return #[ betaEtaReduction.toSimpRule, clausificationStep.toSimpRule, @@ -235,30 +210,6 @@ def forwardSimpRules : ProverM (Array SimpRule) := do (forwardNegativeSimplifyReflect subsumptionTrie).toSimpRule, identBoolHoist.toSimpRule -- Higher order rule ] - else if !(← getIncludeExpensiveRulesM) && (← getIncludeDatatypeRulesM) && !(← getIncludeUnsafeAcyclicityM) then - return #[ - betaEtaReduction.toSimpRule, - clausificationStep.toSimpRule, - syntacticTautologyDeletion1.toSimpRule, - syntacticTautologyDeletion2.toSimpRule, - boolSimp.toSimpRule, - syntacticTautologyDeletion3.toSimpRule, - elimDupLit.toSimpRule, - elimResolvedLit.toSimpRule, - destructiveEqualityResolution.toSimpRule, - identPropFalseElim.toSimpRule, - identBoolFalseElim.toSimpRule, - datatypeDistinctness.toSimpRule, -- Inductive datatype rule - datatypeInjectivity.toSimpRule, -- Inductive datatype rule - -- datatypeAcyclicity.toSimpRule, -- Inductive datatype rule - (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule, - (forwardClauseSubsumption subsumptionTrie).toSimpRule, - (forwardEqualitySubsumption subsumptionTrie).toSimpRule, - (forwardContextualLiteralCutting subsumptionTrie).toSimpRule, - (forwardPositiveSimplifyReflect subsumptionTrie).toSimpRule, - (forwardNegativeSimplifyReflect subsumptionTrie).toSimpRule, - identBoolHoist.toSimpRule -- Higher order rule - ] else -- !(← getIncludeExpensiveRulesM) && !(← getIncludeDatatypeRulesM) return #[ betaEtaReduction.toSimpRule, diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index 5ddac53..4a713ff 100644 --- a/Duper/Tests/test_regression.lean +++ b/Duper/Tests/test_regression.lean @@ -784,3 +784,19 @@ example (t1 : Type 1) (t2 : Type 2) (x : myType4 t1 t2) : set_option duper.collectDatatypes true in example (P : α × β → Prop) (h : ∀ x : α, ∀ y : β, P (x, y)) : ∀ z : α × β, P z := by duper [*] {portfolioInstance := 7} + +example (x : List Nat) : x ≠ 0 :: x := by + duper [*] {portfolioInstance := 7} + +example (x : myType3) : const6 x ≠ x := by + duper + +inductive TriTree (t : Type _) where +| node : TriTree t → TriTree t → TriTree t → TriTree t +| leaf : t → TriTree t + +example (x y z : TriTree Nat) : x ≠ TriTree.node x y z := by + duper [*] {portfolioInstance := 7} + +example (x y z : TriTree Nat) : TriTree.node x y z ≠ z := by + duper [*]