[Merged by Bors] - feat(tactic/dependencies): add tactics to compute (reverse) dependencies #4602

JLimperg · 2020-10-13T09:49:45Z

These are the beginnings of an API about dependencies between expressions. For
now, we only deal with dependencies and reverse dependencies of hypotheses,
which are easy to compute.

Breaking change: tactic.revert_deps is renamed to
tactic.revert_reverse_dependencies_of_hyp for consistency. Its implementation
is completely new, but should be equivalent to the old one except for the order
in which hypotheses are reverted. (But the old implementation made no particular
guarantees about this order anyway.)

JLimperg · 2020-10-13T09:54:34Z

Design question: how do we compute dependencies between hypotheses in the presence of local defs?

The interesting case is this:

n : N
m : N := n
h : m > 0

Does h depend on n? Currently, this PR says no. This simplifies the implementation since "depends on" can be decided by a simple syntactic occurrence check. kdepends_on infamously ignores local defs altogether. However, I find all this semantically fishy.

eric-wieser · 2020-10-13T14:30:44Z

src/tactic/dependencies.lean

+    local_def_value_has_local_in h ns ]
+
+/--
+Given a hypothesis `h`, `hyp_depends_on_locals h ns` returns true iff `h`


Suggested change

Given a hypothesis `h`, `hyp_depends_on_locals h ns` returns true iff `h`

Given a hypothesis `h`, `hyp_depends_on_locals_inclusive h ns` returns true iff `h`

robertylewis · 2020-10-18T17:00:49Z

Does h depend on n?

Yes. The current implementation is clearly a "one-step" dependency relation. kdepends_on is probably an inappropriate name.

I think it's not horrible as long as doc strings are very clear that the notion of dependence is nontransitive. The library note is good but maybe we shouldn't rely on everyone reading that. Another way to clarify things would be to implement transitive versions of these tests. IIRC there's code for building transitive closures of directed graphs in the scc tactic, but I don't know if it's reusable here.

@gebner You commented in the Zulip thread about this question which didn't continue. (Sorry, I haven't been very active recently.) Any further thoughts?

robertylewis

I think these additions look very good!

robertylewis · 2020-10-18T17:02:36Z

src/tactic/dependencies.lean

+
+/--
+Given a hypothesis `h`, `hyp_depends_on_locals h ns` returns true iff `h`
+depends on a local constant whose unique name appears in `ns`. See note


Suggested change

depends on a local constant whose unique name appears in `ns`. See note

depends on a local constant whose unique name appears in `ns`. See Note

and below. I think the regex parser in doc gen only looks for capital Note [...].

robertylewis · 2020-10-18T17:04:43Z

src/tactic/dependencies.lean

+
+/--
+Given a hypothesis `h` and local constant `i`, `hyp_depends_on_local h i`
+checks whether `h` depends on `i`. See note [dependencies of hypotheses].


What is the behavior if i is not a local constant?

robertylewis · 2020-10-18T17:05:37Z

src/tactic/dependencies.lean

+  pure $ deps.insert h.local_uniq_name
+
+/--
+Given a hypothesis `h`, `dependencies_of_hyp_inclusive' h` returns the


Suggested change

Given a hypothesis `h`, `dependencies_of_hyp_inclusive' h` returns the

Given a hypothesis `h`, `dependencies_of_hyp_inclusive h` returns the

robertylewis · 2020-10-18T17:06:00Z

src/tactic/dependencies.lean

+hyp_depends_on_locals h (mk_name_set.insert i.local_uniq_name)
+
+/--
+Given a hypothesis `h` and local constant `i`, `hyp_depends_on_local h i`


Suggested change

Given a hypothesis `h` and local constant `i`, `hyp_depends_on_local h i`

Given a hypothesis `h` and local constant `i`, `hyp_depends_on_local_inclusive h i`

robertylewis · 2020-10-18T17:07:49Z

src/tactic/dependencies.lean

+  hs.foldl (λ ns h, ns.insert h.local_uniq_name) mk_name_set
+
+/--
+Revert the local constants whose unique names appear in `hs`, as well as any


Suggested change

Revert the local constants whose unique names appear in `hs`, as well as any

`revert_set hs` reverts the local constants whose unique names appear in `hs`, as well as any

and below

JLimperg · 2020-10-18T23:10:09Z

Thanks Rob and Eric! I'm currently implementing a new version of this code which makes the dependency relation transitive, since Gabriel and Mario requested it (and I also think that it's worth incurring minor performance costs for the sake of nice semantics). I'll ping you again when I'm done with that.

gebner · 2020-10-19T13:59:32Z

@gebner You commented in the Zulip thread about this question which didn't continue. (Sorry, I haven't been very active recently.) Any further thoughts?

My last word was that it should be transitive. I'm just waiting for Jannis to change this.

JLimperg · 2020-10-19T14:53:05Z

Here's the new version which takes local defs fully into account. I'm afraid approximately all of the code has changed, so it'll need a full re-review. @robertylewis could you take another look? Sorry about the duplicate work.

…ies of hyps These are the beginnings of an API about dependencies between expressions. For now, we only deal with dependencies and reverse dependencies of hypotheses, which are easy to compute. Breaking change: `tactic.revert_deps` is renamed to `tactic.revert_reverse_dependencies_of_hyp` for consistency. Its implementation is completely new, but should be equivalent to the old one except for the order in which hypotheses are reverted. (But the old implementation made no particular guarantees about this order anyway.)

I thought these trivial variants would just clutter the API, but then I immediately needed a couple of them for another tactic.

robertylewis

@robertylewis could you take another look? Sorry about the duplicate work.

For future reference, please remove the awaiting-review tag and add WIP or awaiting-author if you have changes planned!

I see you're making edits now. Ping me when you're done and I'll review again.

src/meta/rb_map.lean

JLimperg · 2020-10-26T19:10:44Z

@robertylewis Yeah, sorry about the back-and-forth. The PR is now ready for review for real.

robertylewis

This looks useful and exhaustive. Thank you for filling out the full API here!

I have no major concerns. AFAIK all transitive checks go through context_dependencies, which computes the expr -> expr_set map for the entire context, right? It's not clear to me that doing this greedily is always ideal. There are certainly applications where keeping a graph representation and computing sets on demand would be more efficient, right? But presumably this approach is better at other times. I'm not sure how much to worry about this.

src/tactic/dependencies.lean

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

robertylewis · 2020-10-27T16:26:46Z

I have no major concerns. AFAIK all transitive checks go through context_dependencies, which computes the expr -> expr_set map for the entire context, right? It's not clear to me that doing this greedily is always ideal. There are certainly applications where keeping a graph representation and computing sets on demand would be more efficient, right? But presumably this approach is better at other times. I'm not sure how much to worry about this.

@gebner @digama0 thoughts here? Do you care? I'm okay merging as it is.

digama0 · 2020-10-27T16:48:54Z

I agree with both points: hyp_depends_on_local_name_set in particular can be implemented more efficiently by calculating the set of local defs and and doing a reachability test within those variables; and I don't think it matters. Maybe slap a TODO on there and come back to it if it's a bottleneck.

JLimperg · 2020-10-27T16:58:35Z

I'm writing a more efficient version right now, mostly for the sake of CS pride. ;)

…ultiple hyps; improve docs

JLimperg · 2020-10-28T15:16:25Z

I've now re-implemented the dependency search so that it only looks at relevant hypotheses. With the new implementation we can also efficiently find the dependencies of multiple hypotheses at once, so I've added tactics to do that as well. The tests still pass and I've been more careful than usual with the docs, so I hope this doesn't require yet another full review.

robertylewis · 2020-10-28T18:28:14Z

Thanks again! Looking good to me.

bors merge

bryangingechen · 2020-10-28T20:49:03Z

bors crashed, let's retry
bors r+

…ies (#4602) These are the beginnings of an API about dependencies between expressions. For now, we only deal with dependencies and reverse dependencies of hypotheses, which are easy to compute. Breaking change: `tactic.revert_deps` is renamed to `tactic.revert_reverse_dependencies_of_hyp` for consistency. Its implementation is completely new, but should be equivalent to the old one except for the order in which hypotheses are reverted. (But the old implementation made no particular guarantees about this order anyway.)

bors · 2020-10-28T23:34:17Z

Pull request successfully merged into master.

Build succeeded:

…ies (leanprover-community#4602) These are the beginnings of an API about dependencies between expressions. For now, we only deal with dependencies and reverse dependencies of hypotheses, which are easy to compute. Breaking change: `tactic.revert_deps` is renamed to `tactic.revert_reverse_dependencies_of_hyp` for consistency. Its implementation is completely new, but should be equivalent to the old one except for the order in which hypotheses are reverted. (But the old implementation made no particular guarantees about this order anyway.)

JLimperg added awaiting-review The author would like community review of the PR RFC Request for comment labels Oct 13, 2020

eric-wieser reviewed Oct 13, 2020

View reviewed changes

bryangingechen added the t-meta Tactics, attributes or user commands label Oct 13, 2020

urkud assigned robertylewis Oct 17, 2020

robertylewis reviewed Oct 18, 2020

View reviewed changes

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 18, 2020

JLimperg marked this pull request as draft October 18, 2020 23:10

JLimperg added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes RFC Request for comment labels Oct 19, 2020

JLimperg marked this pull request as ready for review October 19, 2020 14:51

JLimperg added 5 commits October 26, 2020 14:22

Make 'depends on' relation transitive when there are local defs

d8a4c23

Add tests

c51ca7f

Placate the linter

d68e4b3

Add variants for list expr, name_set and expr_set for all functions

25ea5bd

I thought these trivial variants would just clutter the API, but then I immediately needed a couple of them for another tactic.

JLimperg force-pushed the dependencies branch from f0f9895 to 25ea5bd Compare October 26, 2020 16:06

JLimperg added 2 commits October 26, 2020 17:09

Fix type errors

e44313d

Add dependency_set_of_hyp_inclusive and variants

87a1e0d

robertylewis reviewed Oct 26, 2020

View reviewed changes

src/meta/rb_map.lean Show resolved Hide resolved

Add doc string

b33d5d7

robertylewis reviewed Oct 26, 2020

View reviewed changes

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 26, 2020

JLimperg and others added 4 commits October 27, 2020 02:18

Apply suggestions from code review

d572ac3

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Make local_list_to_name_set public

94c9e03

Make performance warning more explicit

7f89c3e

Add 'transitive' to heading for grepability

c77eac2

gebner added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 27, 2020

robertylewis added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Oct 27, 2020

Reimplement dependency search; add functions to get dependencies of m…

f6f9fad

…ultiple hyps; improve docs

JLimperg added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Oct 28, 2020

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 28, 2020

bors bot changed the title ~~feat(tactic/dependencies): add tactics to compute (reverse) dependencies~~ [Merged by Bors] - feat(tactic/dependencies): add tactics to compute (reverse) dependencies Oct 28, 2020

bors bot closed this Oct 28, 2020

bors bot deleted the dependencies branch October 28, 2020 23:34

bryangingechen mentioned this pull request Oct 28, 2020

bors crashing with "Cannot change the base branch of a closed pull request" bors-ng/bors-ng#1067

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(tactic/dependencies): add tactics to compute (reverse) dependencies #4602

[Merged by Bors] - feat(tactic/dependencies): add tactics to compute (reverse) dependencies #4602

JLimperg commented Oct 13, 2020

JLimperg commented Oct 13, 2020

eric-wieser Oct 13, 2020

robertylewis commented Oct 18, 2020

robertylewis left a comment

robertylewis Oct 18, 2020

robertylewis Oct 18, 2020

robertylewis Oct 18, 2020

robertylewis Oct 18, 2020

robertylewis Oct 18, 2020

JLimperg commented Oct 18, 2020

gebner commented Oct 19, 2020

JLimperg commented Oct 19, 2020

robertylewis left a comment

JLimperg commented Oct 26, 2020

robertylewis left a comment

robertylewis commented Oct 27, 2020

digama0 commented Oct 27, 2020

JLimperg commented Oct 27, 2020

JLimperg commented Oct 28, 2020

robertylewis commented Oct 28, 2020

bryangingechen commented Oct 28, 2020

bors bot commented Oct 28, 2020

	Given a hypothesis `h`, `hyp_depends_on_locals h ns` returns true iff `h`
	Given a hypothesis `h`, `hyp_depends_on_locals_inclusive h ns` returns true iff `h`

	depends on a local constant whose unique name appears in `ns`. See note
	depends on a local constant whose unique name appears in `ns`. See Note

	Given a hypothesis `h`, `dependencies_of_hyp_inclusive' h` returns the
	Given a hypothesis `h`, `dependencies_of_hyp_inclusive h` returns the

	Given a hypothesis `h` and local constant `i`, `hyp_depends_on_local h i`
	Given a hypothesis `h` and local constant `i`, `hyp_depends_on_local_inclusive h i`

	Revert the local constants whose unique names appear in `hs`, as well as any
	`revert_set hs` reverts the local constants whose unique names appear in `hs`, as well as any

[Merged by Bors] - feat(tactic/dependencies): add tactics to compute (reverse) dependencies #4602

[Merged by Bors] - feat(tactic/dependencies): add tactics to compute (reverse) dependencies #4602

Conversation

JLimperg commented Oct 13, 2020

JLimperg commented Oct 13, 2020

eric-wieser Oct 13, 2020

Choose a reason for hiding this comment

robertylewis commented Oct 18, 2020

robertylewis left a comment

Choose a reason for hiding this comment

robertylewis Oct 18, 2020

Choose a reason for hiding this comment

robertylewis Oct 18, 2020

Choose a reason for hiding this comment

robertylewis Oct 18, 2020

Choose a reason for hiding this comment

robertylewis Oct 18, 2020

Choose a reason for hiding this comment

robertylewis Oct 18, 2020

Choose a reason for hiding this comment

JLimperg commented Oct 18, 2020

gebner commented Oct 19, 2020

JLimperg commented Oct 19, 2020

robertylewis left a comment

Choose a reason for hiding this comment

JLimperg commented Oct 26, 2020

robertylewis left a comment

Choose a reason for hiding this comment

robertylewis commented Oct 27, 2020

digama0 commented Oct 27, 2020

JLimperg commented Oct 27, 2020

JLimperg commented Oct 28, 2020

robertylewis commented Oct 28, 2020

bryangingechen commented Oct 28, 2020

bors bot commented Oct 28, 2020