Skip to content

Merge changes from querySMT branch #76

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
JOSHCLUNE merged 10 commits into from
Apr 8, 2026
Merged

Merge changes from querySMT branch #76

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
29c514c
Modify lakefile to depend on querySMT branch of fork rather than main…
JOSHCLUNE Sep 27, 2025
a3f8ad4
Update lean-auto
JOSHCLUNE Sep 27, 2025
2277a82
Update lake-manifest
JOSHCLUNE Sep 30, 2025
27513c2
Update lake-manifest
JOSHCLUNE Sep 30, 2025
43faa09
Update lake-manifest
JOSHCLUNE Oct 1, 2025
42bfedc
Update lean-auto
JOSHCLUNE Oct 6, 2025
e4f158b
Modify derivInfo so that lemmas obtained from definitional equalities…
JOSHCLUNE Oct 7, 2025
073e08b
Merge branch 'dev' into querySMT
JOSHCLUNE Mar 28, 2026
b0098f6
Update lean-auto
JOSHCLUNE Apr 2, 2026
c65a3e7
Change lean-auto dependency to follow the hammer branch
JOSHCLUNE Apr 8, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions Duper/Interface.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down