A new tactic

Stream: mathlib4

[Scott Morrison]

I have a new tactic, which is a forwards-reasoning analogue of the backwards-reasoning library_search.

It is tentatively called propose at the moment, but suggestions are welcome. (One option would be to fold it into library_search.)

Here are two examples:

import Std.Data.List.Basic
import Mathlib.Tactic.Propose

example (K L M : List α) (w : L.Disjoint M) (m : K ⊆ L) : True := by
  propose using w
  have : K.Disjoint M := by assumption -- `propose` added the hypothesis `List.disjoint_of_subset_left m w`
  trivial

import Mathlib.Tactic.Propose
import Mathlib.Algebra.Associated

-- From Mathlib.Algebra.Associated:
variable {α : Type} [CommMonoidWithZero α]
open Prime in
theorem dvd_of_dvd_pow (hp : Prime p) {a : α} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a := by
  induction' n with n ih
  · rw [pow_zero] at h
    -- In mathlib, we proceed by two `have` statements:
    -- have := isUnit_of_dvd_one  h
    -- have := not_unit hp
    -- `propose` successfully guesses them both:
    propose using h
    propose using hp
    contradiction
  rw [pow_succ] at h
  cases' dvd_or_dvd hp h with dvd_a dvd_pow
  · assumption
  exact ih dvd_pow

[Scott Morrison]

How does it work? It's pretty simple. Just like library_search, we traverse all declarations in the environment, and stick them into a discrimination tree, but this time indexed by (each of the) hypotheses, rather than by the conclusion. As with library_search after !4#2888, we discard any where the discrimination key is just #[*]. Now, when the user calls propose using a, b, c, we retrieve a list of all the lemmas that take as an argument something of shape a (notice the first argument after using is treated specially). Now, for each such lemma, we use solve_by_elim (augmented by typeclass search) to try to fill in all the arguments. We only accept solutions that use each of a, b, c, backtracking as necessary. Finally, we add up to 10 successful results as new hypotheses.

[Scott Morrison]

This is not intended as a "leave in place" tactic: you should replace it with a have statement, and probably we should add some Try this: functionality.

[Scott Morrison]

I haven't done a lot of testing (the two examples!) but it seems to work pretty nicely, and seems useful when you know that some handful of hypotheses should be useful together, but you're not quite sure how (or maybe you are, and just want to know the name).

[Scott Morrison]

One question: should this be a separate tactic?

[Scott Morrison]

Or just roll it into library_search at a, b, c?

[Mario Carneiro]

I don't like the idea of using something other than a location after the at keyword

[Scott Morrison]

Oh, I intended here that a, b, c are each hypotheses?

[Mario Carneiro]

well there wouldn't be commas at least

[Mario Carneiro]

if you do use the location grammar, does at h |- and at * make sense?

[Scott Morrison]

Ah. It could still be a location, I guess. If it includes ⊢, it would use the usual backwards-reasoning library_search (and require that any named hypotheses are used in the result, like the current library_search using).

[Scott Morrison]

If it doesn't include ⊢, it would use the new forwards-reasoning search.

[Scott Morrison]

I worry that it would be confusing that library_search at a b c (i.e. without an ⊢) would not be looking at the goal at all.

[Mario Carneiro]

that's not too unusual for other tactics using at h

[Scott Morrison]

indeed

[Mario Carneiro]

what is more unusual is that it doesn't modify those hypotheses

[Jireh Loreaux]

Why not library_search using a b c?

[Adam Topaz]

I would prefer to leave it as a separate tactic. And I think propose is a good name.

[Mario Carneiro]

and also that it treats the first hyp specially

[Scott Morrison]

@Jireh Loreaux, that already means something: it says "find me a lemma that closes the goal, but only if you can do so in a way that we use a b c as arguments to that lemma"

[Scott Morrison]

e.g.

example (l : List α) (f : α → β ⊕ γ) : List β × List γ := by library_search using f -- partitionMap f l

[Mario Carneiro]

maybe propose should consider the goal for relevance filtering purposes?

[Jireh Loreaux]

Ah good to know, obviously I haven't used library_search that much, but hopefully it becomes useful again with Lean 4 and your recent speedup.

[Scott Morrison]

Considering the goal for relevance sounds awesome, but maybe for later. :-)

[Mario Carneiro]

maybe propose shouldn't actually change the goal state at all, but only give a bunch of "try this" style suggestions

[Adam Topaz]

Personally I find it easier to remember what different tactics with different names do as opposed to remembering what different grammars do for a single tactic

[Mario Carneiro]

as described it is almost impossible to guess what the state looks like after propose

[Mario Carneiro]

and you also can't name the introduced variables

[Scott Morrison]

I agree that it should just give Try this.

[Scott Morrison]

Harder to write the tests :-)

[Mario Carneiro]

propose (im_feeling_lucky := true)

[Scott Morrison]

Okay, propose now generates have : t := e suggestions. (I think having the type in the suggestion is very helpful for deciding if you like the suggestion! A user can remove it if they like.)

[Scott Morrison]

There's also propose! for "I'm feeling lucky". It still prints the suggestions, so it will always be noisy.

[Scott Morrison]

Some further features: you can write things like propose : X using Y, Z, and it will only return lemmas whose type matches X (which may contain metavariables).

[Siddhartha Gadgil]

A minor comment: is this exactly instantiation by the given hypothesis where applicable? If so:

• is instantiate a better name?
• why not allow terms, not just hypotheses : instantiate [n, m + n]?
• can one use a slug of the type as a name?

[Johan Commelin]

Scott Morrison said:

Some further features: you can write things like propose : X using Y, Z, and it will only return lemmas whose type matches X (which may contain metavariables).

That sounds a lot like the observe that I hacked together for ml3.

[James Gallicchio]

(can I request this get into Std? would be super super useful for program verification stuff I'm playing around with!)

[Scott Morrison]

@Siddhartha Gadgil, yes, you can use terms. I'm not sure why instantiate would be relevant/helpful here. It's going and finding some lemma from the lemma, whose arguments can be filled by local hypotheses (perhaps recursively).

And I'm not sure what slug means here?

[Scott Morrison]

re: Std, I think it's best that it has a shake out period in mathlib initially. library_search should also move to Std eventually.

[Siddhartha Gadgil]

Yes, it is really the dual of instantiate (or use as in the tactic), i.e., one is finding a lemma which can be instantiated. So instantiate_with may be better but not that good and a little long.

By slug I mean something that is done by, for example, static site generators where a sentence is converted into a legal identifier, url in that case (also mapped to lowercase etc) as in https://jekyllrb.com/docs/liquid/filters/. It seems nice to have in some cases, typically if a proof is auto-generated by forward reasoning then it can be named by slugifying the type.

[Mario Carneiro]

Scott Morrison said:

re: Std, I think it's best that it has a shake out period in mathlib initially. library_search should also move to Std eventually.

I agree with this. As long as the implementation doesn't impose a cost for people who don't use it, I think it would be nice to have library_search available in Std.

[Trebor Huang]

Why not add an alias couse or library_cosearch for duality enthusiasts?

[Thomas Murrills]

library_searchᵒᵖ