feat(tactic): add various tactics about local definitions #1953

fpvandoorn · 2020-02-04T17:45:12Z

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

src/data/option/defs.lean

fpvandoorn · 2020-02-05T06:17:09Z

@cipher1024: What does the following tactic do?

mathlib/src/tactic/monotonicity/interactive.lean

Lines 406 to 408 in 253f75c

    
           /-- tactic-facing function, similar to `interactive.tactic.generalize` with the 
        
           exception that meta variables -/ 
        
           meta def generalize' (h : name) (v : expr) (x : name) : tactic (expr × expr) :=

The docstring is a sentence fragment. Can I rename it to monotonicity.generalize'?

Also, many of the declarations in that file are not interactive tactics at all...

src/tactic/core.lean

src/tactic/interactive.lean

src/tactic/core.lean

robertylewis · 2020-02-05T12:09:53Z

src/tactic/core.lean

+
+/-- `local_def_value e` returns the value of the expression `e`, assuming that `e` has been defined
+locally using a `let` expression. Otherwise it fails. -/
+meta def local_def_value (e : expr) : tactic expr :=


Would this and the following be better implemented in C++? IIRC local definitions are stored in the type context, right? @EdAyers exposed some of the type context to the tactic monad in 3.5c. Rather than this kind of hackish way to get the local def value, maybe there should be a function to query the type context directly.

Yes, it would almost certainly be better to implement this in C++.
I don't know how to do that, though.

Shall merge this PR and change it until we've exposed it from the C++ side?

I think this is already implemented:

tactic.unsafe.type_context.run $ do lctx <- get_local_context, some ldecl <- pure (lctx.get_local_decl e.local_uniq_name), some let_val <- pure ldecl.value, pure let_val

Nice! Do you know if it possible to run tactic.pp inside the type_context monad (for error message handling)?

I didn't find anything, and I don't think there is a way to run tactics from the type context monad.

src/tactic/core.lean

gebner · 2020-02-10T17:47:13Z

src/tactic/core.lean

+
+/-- `local_def_value e` returns the value of the expression `e`, assuming that `e` has been defined
+locally using a `let` expression. Otherwise it fails. -/
+meta def local_def_value (e : expr) : tactic expr :=


I think this is already implemented:

tactic.unsafe.type_context.run $ do lctx <- get_local_context, some ldecl <- pure (lctx.get_local_decl e.local_uniq_name), some let_val <- pure ldecl.value, pure let_val

src/tactic/core.lean

src/tactic/monotonicity/interactive.lean

src/tactic/interactive.lean

gebner · 2020-02-11T13:01:34Z

I don't think we need to change local_def_value and is_local_def to use the type_context monad. The current implementation seems robust enough. But please try it out if you think it's fun.

fpvandoorn · 2020-02-20T18:32:23Z

I updated local_def_value to use the type_context. is_local_def is a one-liner, and I kept it the same. I also added tests to check that it works.

gebner · 2020-02-21T19:23:49Z

src/tactic/core.lean

+
+/-- `local_def_value e` returns the value of the expression `e`, assuming that `e` has been defined
+locally using a `let` expression. Otherwise it fails. -/
+meta def local_def_value (e : expr) : tactic expr :=


I didn't find anything, and I don't think there is a way to run tactics from the type context monad.

gebner · 2020-02-21T19:24:57Z

src/tactic/interactive.lean

+`generalize'` is similar to `generalize`. The difference is that `generalize' : e = x` also succeeds when `e`
+  does not occur in the goal. It is similar to `set`, but the resulting hypothesis `x` is not a local definition.
+-/
+meta def generalize' (h : parse ident?) (_ : parse $ tk ":") (p : parse generalize_arg_p) : tactic unit :=


This should probably go into Lean 3.6.

…-community#1953) * feat(tactic): add various tactics about local definitions * remove {α β} * rename generalize' in monotonicity. * updates after reviews Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

fpvandoorn force-pushed the local_def_tactics branch from fb26435 to e7df2cb Compare February 4, 2020 17:54

urkud reviewed Feb 4, 2020

View reviewed changes

src/data/option/defs.lean Outdated Show resolved Hide resolved

robertylewis reviewed Feb 5, 2020

View reviewed changes

robertylewis added the awaiting-author A reviewer has asked the author a question or requested changes label Feb 5, 2020

gebner reviewed Feb 10, 2020

View reviewed changes

robertylewis assigned gebner Feb 11, 2020

gebner requested changes Feb 11, 2020

View reviewed changes

fpvandoorn added 4 commits February 20, 2020 12:50

feat(tactic): add various tactics about local definitions

6df1c26

remove {α β}

e401749

rename generalize' in monotonicity.

447c37a

updates after reviews

46d6854

fpvandoorn force-pushed the local_def_tactics branch from 5236932 to 46d6854 Compare February 20, 2020 18:29

fpvandoorn 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 Feb 20, 2020

fpvandoorn requested a review from gebner February 21, 2020 18:49

gebner approved these changes Feb 21, 2020

View reviewed changes

gebner 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 Feb 21, 2020

mergify bot added 3 commits February 21, 2020 19:26

Merge branch 'master' into local_def_tactics

594d2ad

Merge branch 'master' into local_def_tactics

06b5c2e

Merge branch 'master' into local_def_tactics

1f4467b

mergify bot merged commit ffb6d6e into master Feb 21, 2020

mergify bot deleted the local_def_tactics branch February 21, 2020 22:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(tactic): add various tactics about local definitions #1953

feat(tactic): add various tactics about local definitions #1953

fpvandoorn commented Feb 4, 2020

fpvandoorn commented Feb 5, 2020 •

edited

robertylewis Feb 5, 2020

fpvandoorn Feb 10, 2020 •

edited

gebner Feb 10, 2020

fpvandoorn Feb 20, 2020

gebner Feb 21, 2020

gebner Feb 10, 2020

gebner commented Feb 11, 2020

fpvandoorn commented Feb 20, 2020

gebner Feb 21, 2020

gebner Feb 21, 2020

feat(tactic): add various tactics about local definitions #1953

feat(tactic): add various tactics about local definitions #1953

Conversation

fpvandoorn commented Feb 4, 2020

fpvandoorn commented Feb 5, 2020 • edited

robertylewis Feb 5, 2020

Choose a reason for hiding this comment

fpvandoorn Feb 10, 2020 • edited

Choose a reason for hiding this comment

gebner Feb 10, 2020

Choose a reason for hiding this comment

fpvandoorn Feb 20, 2020

Choose a reason for hiding this comment

gebner Feb 21, 2020

Choose a reason for hiding this comment

gebner Feb 10, 2020

Choose a reason for hiding this comment

gebner commented Feb 11, 2020

fpvandoorn commented Feb 20, 2020

gebner Feb 21, 2020

Choose a reason for hiding this comment

gebner Feb 21, 2020

Choose a reason for hiding this comment

fpvandoorn commented Feb 5, 2020 •

edited

fpvandoorn Feb 10, 2020 •

edited