From ae9bb8b2a104772aa3dd890b8b576c926bf38a85 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 4 Oct 2022 16:09:59 -0700 Subject: [PATCH 1/3] feat(tactic/recommend): `recommend` tactic based on premise selection --- docs/references.bib | 12 +++++++ src/tactic/interactive.lean | 1 + src/tactic/recommend.lean | 71 +++++++++++++++++++++++++++++++++++++ 3 files changed, 84 insertions(+) create mode 100644 src/tactic/recommend.lean diff --git a/docs/references.bib b/docs/references.bib index fffe6800f3a4e..132bef68a98c8 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -527,6 +527,18 @@ @Book{ coxlittleoshea1997 isbn = {978-0-387-94680-1} } +@Article{ czajka2018, + author = {Lukasz Czajka and Cezary Kaliszyk}, + title = {Hammer for Coq: Automation for Dependent Type Theory}, + journal = {Journal of Automated Reasoning}, + volume = {61}, + number = {1-4}, + pages = {423--453}, + year = {2018}, + url = {https://doi.org/10.1007/s10817-018-9458-4}, + doi = {10.1007/s10817-018-9458-4} +} + @Book{ davey_priestley, author = {Davey, B. A. and Priestley, H. A.}, title = {Introduction to lattices and order}, diff --git a/src/tactic/interactive.lean b/src/tactic/interactive.lean index 462543ebd069c..802d3c4564509 100644 --- a/src/tactic/interactive.lean +++ b/src/tactic/interactive.lean @@ -6,6 +6,7 @@ Authors: Mario Carneiro, Simon Hudon, Sébastien Gouëzel, Scott Morrison import logic.nonempty import tactic.lint import tactic.dependencies +import tactic.recommend setup_tactic_parser diff --git a/src/tactic/recommend.lean b/src/tactic/recommend.lean new file mode 100644 index 0000000000000..d23594262a89f --- /dev/null +++ b/src/tactic/recommend.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner +-/ +import tactic.core + +/-! +# `recommend` + +The `recommend` tactic searches for lemmas in the current environment +that look like they could be useful to prove the current goal. + +It is based on premise selection heuristic used in [CoqHammer][czajka2018], +with a preprocessing step that removes type arguments, type class instances, etc. +This heuristic analyzes the proofs of the theorems in the environment: +it will suggest lemmas that have been used in proofs of +similar theorems as the current goal. + +The heuristic is completely syntactic; +it won't unfold definitions during the search, +and doesn't know about types and type classes. +-/ + +namespace tactic + +open feature_search + +/-- Attribute that marks a theorem to be ignored by the `recommend` tactic. -/ +@[user_attribute] +meta def recommend_ignore_attr : user_attribute := +{ name := `recommend_ignore, descr := "Marks a theorem to be ignored by the `recommend` tactic." } + +attribute [recommend_ignore] eq.mpr eq.rec id_tag nat eq + has_zero.zero has_one.one has_lt.lt has_le.le + +/-- Returns true if `rw [const]` succeeds (or `rw [← const]` if `symm` is true). -/ +meta def can_rw_with_at_goal (const : name) (symm : bool) : tactic bool := +retrieve' $ succeeds $ interactive.rw + { rules := [{ pos := default, symm := symm, rule := expr.const const [] }], end_pos := none } + (interactive.loc.ns [none]) + +/-- +`recommend` is a tactic to search for existing lemmas in the library +that could be useful to close the current goal. + +The `recommend` tactic does not unfold any definitions. +-/ +meta def interactive.recommend (max_results := 30) : tactic unit := do +tgt ← retrieve' $ revert_all >> target, +env ← get_env, +let cfg : feature_cfg := {}, +let pred := env.mk_predictor {.. cfg}, +let fv := feature_vec.of_expr env tgt cfg, +let results := pred.predict fv max_results, +ignored ← attribute.get_instances recommend_ignore_attr.name, +let results := results.filter (λ res, res.1 ∉ ignored), +results.mmap' (λ res : name × native.float, do + mwhen (retrieve' $ succeeds $ applyc res.1) $ trace!"Try this: apply {res.1}", + mwhen (can_rw_with_at_goal res.1 ff) $ trace!"Try this: rw {res.1}", + mwhen (can_rw_with_at_goal res.1 tt) $ trace!"Try this: rw ← {res.1}"), +trace "\nOther useful lemmas:", +results.mmap' (λ res, trace!"{res.1} (score: {res.2})") + +add_tactic_doc +{ name := "recommend", + category := doc_category.tactic, + decl_names := [``interactive.recommend], + tags := ["search", "Try this"] } + +end tactic From 7a5a624e234ed41e1757eec1b69da3e6a6b18f78 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 4 Oct 2022 16:19:23 -0700 Subject: [PATCH 2/3] Simplify proof using `recommend`. --- src/algebra/ring/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean index 956571775f59d..24c99006ba6b8 100644 --- a/src/algebra/ring/basic.lean +++ b/src/algebra/ring/basic.lean @@ -863,7 +863,7 @@ by simp only [divp, add_mul, units.mul_inv_cancel_right] @[field_simps] lemma divp_sub (a b : α) (u : αˣ) : a /ₚ u - b = (a - b * u) /ₚ u := begin simp only [divp, sub_mul, sub_right_inj], - assoc_rw [units.mul_inv, mul_one], + rw units.mul_inv_cancel_right end end units From d6c1473cf22e9df624af99dd383f5cf383bec88a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 4 Oct 2022 21:52:18 -0700 Subject: [PATCH 3/3] Golf. --- src/algebra/ring/basic.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean index 24c99006ba6b8..1f0cead3e2cb5 100644 --- a/src/algebra/ring/basic.lean +++ b/src/algebra/ring/basic.lean @@ -861,10 +861,7 @@ by simp only [divp, sub_mul, units.mul_inv_cancel_right] by simp only [divp, add_mul, units.mul_inv_cancel_right] @[field_simps] lemma divp_sub (a b : α) (u : αˣ) : a /ₚ u - b = (a - b * u) /ₚ u := -begin - simp only [divp, sub_mul, sub_right_inj], - rw units.mul_inv_cancel_right -end +by simp only [divp, sub_mul, units.mul_inv_cancel_right] end units