exact? / apply? / rw? / ... feature requests

Stream: mathlib4

[Michael Stoll]

1. The following shows one success and three failures of exact?:

import Mathlib

example {p : ℕ} (h : p.Prime) : 1 < p := by
  exact? says exact Nat.Prime.one_lt h

example (p : ℕ) [Fact p.Prime] : 1 < p := by
  -- exact? -- `exact?` could not close the goal.
  sorry

example {p : ℕ} (h : p.Prime ∧ p ≠ 2) : 1 < p := by
  -- exact? -- `exact?` could not close the goal.
  sorry

example {p : ℕ} (h : p.Prime) : 1 ≤ p := by
  -- exact? -- `exact?` could not close the goal.
  sorry

Would it be possible to extend exact? so that

• it also considers components of hypotheses in the context (like Fact.out or h.1), so that it would solve the first two of the failing cases above;
• it also considers strict inequalities when asked to solve goals involving ≤ or ≠ (similar to what I think it already does regarding symmetry of equalities), so that it would solve the last example?

Or would this be too much of "mission creep"?

2. When I have a goal that is an equality or an equivalence, apply? tends to produce a quite long list of generic statements about equalities or equivalences that are rarely, if ever, useful, and maybe only fairly far down shows some more specific suggestions. Would it be possible to filter the lemmas that apply?considers (and similarly for rw?) by providing a list of constants (like ZMod or Finset.sum) that should appear in the lemma statement and/or a list of terms (e.g., local hypotheses or statements derived from them) that should be used as arguments? Usually I have an idea of what I want to do and what I want to use as input, so being able to transmit this information to apply? would result in a much more targeted list of suggestions.

[Yakov Pechersky]

A related issue that maybe gets at the underlying issue is that solve_by_elim doesn't use TC hyps:

import Mathlib

example {p : ℕ} (h : p.Prime) : 1 < p := by
  apply Nat.Prime.one_lt
  solve_by_elim

example (p : ℕ) [h : Fact p.Prime] : 1 < p := by
  apply Nat.Prime.one_lt
  solve_by_elim -- failed

[Kim Morrison]

Regarding using projections of local facts:

This would be a change to solve_by_elim, and I think would be very useful. It could be done either as the default behaviour, or under a flag, and exact? could use it either way.

[Kim Morrison]

Regarding inequalities, I think unfortunately this is scope creep into the "hammer" realm.

[Kim Morrison]

Regarding question 2, have you tried out apply? using x? This requires that x appears as a subexpression of any reported result.

[Kim Morrison]

@Yakov Pechersky, I don't think this is about typeclasses at all, but rather than Fact is a one-field structure, and we would need to project using Fact.out to get the thing that solve_by_elim needs to finish:

example (p : ℕ) [h : Fact p.Prime] : 1 < p := by
  apply Nat.Prime.one_lt
  solve_by_elim [Fact.out] -- works!

[Yakov Pechersky]

What if the Fact hyp is unnamed?

[Kim Morrison]

Doesn't (couldn't!) make any difference whether it has a user facing name.

[Kim Morrison]

Does anyone see a quick way to generate all the projections of an Expr? I'm not sure how to look up all the projections associated to the Name of the structure. getProjectionFnInfo? is looking up in the other direction.

[Kyle Miller]

There are a couple ways to get all the fields here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Metaprogramming.20a.20structure.20declaration/near/369266959

[Kim Morrison]

Ah, just found getStructureInfo?

[Kyle Miller]

That's not the projections yet (edit: never mind, it appears to be the projections)

[Kyle Miller]

There's a chance you want docs#Lean.getStructureFieldsFlattened so you can get the fields even if a structure extends another structure

[Michael Stoll]

Scott Morrison said:

Regarding question 2, have you tried out apply? using x? This requires that x appears as a subexpression of any reported result.

Is this documented somewhere? (Hovering over "apply?" in VSCode shows the list of suggestions (if there are any) plus "A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics. Delimiter-free indentation is determined by the first tactic of the sequence.")

The following does not work, though:

import Mathlib

example {p : ℕ} (h : p.Prime ∧ p ≠ 2) : 1 < p := by
  apply? using h.1 --unexpected term 'h.left'; expected single reference to variable

[Kim Morrison]

Ah, yes, it only accepts a list of variables, not arbitrary terms. That could probably be fixed easily.

[Kim Morrison]

@Michael Stoll, @Yakov Pechersky,

example (p : ℕ) [Fact p.Prime] : 1 < p := by exact?

works after std#549.

[Kim Morrison]

(Although it's not entirely clear that we actually want that change; it works by saturating the context with projections of hypotheses, which is potentially an explosive thing to do.)

[Kim Morrison]

@Michael Stoll, fair criticism about the lack of documentation. PRs of course very very welcome, and it's a great way to get into metaprogramming. :-)

We're in the midst of replacing exact? with a rewrite that is now in Std, so documentation will be in flux, hopefully improving!

[Michael Stoll]

I saw that in the other thread. My question (regarding documentation) was basically if I should have known about apply? using, but I guess the answer is "No". I'll probably look into metaprogramming at some point, but not in the immediate future.

[Kim Morrison]

One good method for learning about tactics with poor documentation is to read their test files. These are often very helpful (and in particular using is "documented" in test/LibrarySearch/basic.lean).

[Kim Morrison]

But yeah... the missing doc-string is pretty bad.

[Michael Stoll]

Here is a failure of apply? using:

import Mathlib

example {x : ℝ} (h : x ≠ 0) : 2 * x ≠ 0 := by
  -- apply? -- `Try this: refine mul_ne_zero ?ha h` is no. 4 in the list
  -- apply? using h -- apply? didn't find any relevant lemmas
  exact mul_ne_zero two_ne_zero h

@Scott Morrison

[Michael Stoll]

... and here is a failure of rw?.

import Mathlib

example : (0 : ℝ) ∈ closure (Set.Ioi 0) := by
  -- rw? -- does not suggest the following
  rw [closure_Ioi]
  exact Set.left_mem_Ici

[Kim Morrison]

Michael Stoll said:

Here is a failure of apply? using:

import Mathlib

example {x : ℝ} (h : x ≠ 0) : 2 * x ≠ 0 := by
  -- apply? -- `Try this: refine mul_ne_zero ?ha h` is no. 4 in the list
  -- apply? using h -- apply? didn't find any relevant lemmas
  exact mul_ne_zero two_ne_zero h

Scott Morrison

@Michael Stoll, several drafts into an explanation of why this was going to be hard to fix, I came up with an easy fix: std4#554

[Kim Morrison]

(This will fix std_apply?, not apply?, but hopefully the switch will happen soon enough.)

[Kim Morrison]

Regarding the rw? question, set_option trace.Tactic.rewrites.lemmas true shows that at least it is finding closure_Ioi in its index.

[Kim Morrison]

I think the only probably here is that we restrict rw? to a max of 20 outputs, and it just hasn't got there yet. Can we do better? Suggestions welcome.

[Michael Stoll]

It lists 18 ...mem_closure_iff... lemmas and then Set.mem_def and Set.mem_iff_boolIndicator.

How does rw? sort its output currently? (I seem to remember that there was a discussion at some point (maybe about apply?), but I don't recall if anything came out of it.) Maybe it would help to sort according to a weighted sum of

• number of remaining goals and
• (total) length (or complexity measured in some other resaonable way) of these goals.

The goal ⊢ 0 ∈ Set.Ici 0 remaining after rw [closure_Ioi] is shorter than basically anything offered by rw?.

Rationale: Usually we want to obtain "simpler" goals after the rewrite, and the number and length of the remaining goals should be a reasonably good proxy for measuring simplicity.

[Michael Stoll]

Scott Morrison said:

(This will fix std_apply?, not apply?, but hopefully the switch will happen soon enough.)

It doesn't look like it, but does this also make it allow more general terms after using?

[Kevin Buzzard]

My memory of the sorting discussion was "if you know how to sort them so the right thing appears at the top, you've just written an extremely powerful tactic; hence sorting must be hard"

[Michael Stoll]

There are NP-hard problems that allow for efficient good approximations, though.
I think some reasonable way of sorting here is better than none.