diff --git a/Duper/Interface.lean b/Duper/Interface.lean index d536851..3afcc4b 100644 --- a/Duper/Interface.lean +++ b/Duper/Interface.lean @@ -481,12 +481,16 @@ def formulasWithStringsToAutoLemmas (formulas : List (Expr × Expr × Array Name /-- Determines whether `lem`'s deriv info indicates that `lem` is part of the goal and should be included in the set of support. Note that `derivInfo` only works on lemmas generated from `formulasToAutoLemmas` or `formulasWithStringsToAutoLemmas`. In cases where the lemma was not generated from - `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. -/ + `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. The only exception to this + is if all leaves have exactly the form "termLikeDefEq", in which case `derivInfo` indicates that `isFromGoal` is `false`. -/ def derivInfo (lem : Auto.Lemma) : Bool × Bool := let derivLeaves := getLeavesFromDTr lem.deriv let matchesFormat := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l || "true, false".isPrefixOf l || "false, false".isPrefixOf l) if !matchesFormat then - (true, true) + if derivLeaves.all (fun l => l == "termLikeDefEq") then + (false, true) + else + (true, true) else let isFromGoal := derivLeaves.any (fun l => "true".isPrefixOf l) let includeInSetOfSupport := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l) diff --git a/lake-manifest.json b/lake-manifest.json index ac03469..50aa0ed 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d5600411d5e766a7cb1e47e3b3393ed64c42efc2", + "rev": "7f6aec42310efd5c3311e944fff95cdabef4556a", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-hammer", + "inputRev": "7f6aec42310efd5c3311e944fff95cdabef4556a", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 8aa415e..b597328 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.29.0-hammer" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"7f6aec42310efd5c3311e944fff95cdabef4556a" require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.29.0" package Duper {