Semantics of "only" option of solve_by_elim

sacerdot commented 1 month ago

Prerequisites

Please put an X between the brackets as you perform the following steps:

[x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[ ] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

This is a request of changing the behavior of the "only" option to solve_by_elim in order to clarify the semantics, bring it in line with similar tactics in other systems (Coq/Matita/...) and make the tactic more useful.

solve_by_elim automatically introduces new hypotheses when proving implications/foralls. These new hypotheses are not automatically added to the set of "only" usable assumptions. Analogous tactics in every other system I am aware of have the opposite behavior, for good reasons that I explain here. First let's show an example

theorem iff_example: ∀A B: Prop, (A ↔ B) → (B ↔ A) := by
 intros A B U
 cases U
 case _ h1 h2 =>
  constructor
  . solve_by_elim [h2]             -- here it works without only
  . solve_by_elim only [h1]    -- but with only it does not work anymore

Reasons to change the semantics to always allow hypotheses introduced by the tactic itself:

[important] once solve_by_elim has found a proof using only lemmas l1 ... ln, with the new semantics "solve by elim only [l1,...,ln]" would be able to find the same proof reducing the search time. This is an important principle when reconstructing proofs found by hammers for example. However, as the example above shows, this is not the case with the current semantics
[minor] applications to didactics: "only" can be always automatically triggered (e.g. using a macro) to force students to list the lemmas that they think are necessary in a proof. However, as the example above shows, the current semantics does not allow that when (recursive) goals have implications

Context

See also the following conversation of Zulip

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/solve_by_elim.20.3A.20.22only.22weirdness

Steps to Reproduce

check the code above

Expected behavior: both calls to solve_by_elim should solve the goal

Actual behavior: only the first does because the implementation of the tactic starts introducing an hypothesis "a : A" that is not added to the list of usable hypotheses

Versions

4.9.0-rc3

sacerdot commented 1 month ago

The "bug" label was added automatically, but this is at most a documentation bug and more a request for improvement.

nomeata commented 1 month ago

Thanks for the suggestion. I guess it's more an RFC than a bug

semorrison commented 4 weeks ago

Thanks @sacerdot, I agree this would be a good change and I would like to see this fixed. I probably won't work on it in the short term, but if you or anyone else would like to, I would be happy to review a PR.

leanprover / lean4