solve_by_elim : "only"weirdness

Stream: metaprogramming / tactics

[Claudio Sacerdoti Coen]

"solve_by_elim only L" cannot prove some goals that "solve_by_elim L" can prove without using any lemmas outside L.
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
  . solve_by_elim only [h1]    -- with only it does not

My wild guess is that one of the following two things happens:

1. "only" disallows introducing hypotheses (i.e. intro)
2. hypotheses are introduced, but they are not added to the list L of usable hypotheses, like it should IMHO

Is this a known issue? Is there a simple workaround and/or could/should solve_by_elim being patched?

[Claudio Sacerdoti Coen]

Followup: looking at the solve_by_elim code the cause is clearly hypothesis 2.

[Damiano Testa]

Using show_term shows indeed an unexpected (by me) behaviour:

example {A B : Prop} (U : (A ↔ B)) : (B ↔ A) := by
  cases U
  case _ h1 h2 =>
    constructor
    . -- clear h1 -- if you uncomment `clear h1`, `solve_by_elim` finds `exact fun a => h2 a`
      show_term solve_by_elim -- a detour `exact fun a => h2 (h1 (h2 a))`
    . sorry

If it can go on a detour, it does.

[Claudio Sacerdoti Coen]

@Damiano Testa the detour is not nice, but it is unrelated to what I am reporting. Indeed

solve_by_elim only [h1,h2]

also fails to find a proof, even if the ingredients for the detour are there. The problem is that the tactic starts doing "intro a" but NOT adding "a" to the list of lemmas and therefore after applying "h2" it cannot conclude

[Damiano Testa]

I agree, but I imagine that this could be expected behaviour: when you use only you have not specified using the introduced variable (and you probably have no way of doing that, since it is not available to begin with).

* gives you access to everything and then you can prevent the detour using solve_by_elim only [*, h2, -h1] (the -h1 is in fact not really needed).

[Claudio Sacerdoti Coen]

1. The behaviour is not expected from equivalent tactics in other systems (Coq/Matita): there every additional hypotheses introduced by the tactic itself is allowed. This also allows the natural specification "the tactic solves the goal using only iff it solves the goal without only using only the listed lemmas"
2. My expected behaviour is the useful one for reconstructing proofs found by external provers and to speed up proof search: once you find the proof the first time (or an external proof does), you cut down using "only" on the only lemmas that are required. But this requires my semantics
3. In my particular case I am writing a macro used in teaching that forces the students to write explicitly the hypotheses that are required. If the hypotheses introduced by the tactic itself are not considered, then I canno tuse solve_by_elim for this and I need to duplicate the code of solve_by_elim to impose my semantics. (And I am not even sure if the code lives all in user space)

[Claudio Sacerdoti Coen]

Finally, I do not see any advantages of the current semantics of "only". Can you see any?

[Damiano Testa]

I was using "expected behaviour" to mean "this is what the tactic might be expected to do", with no connotation of whether this was desirable or not. I imagine that limiting the hypotheses to the ones initially available may make the tactic more performant. I can also imagine that this is an oversight and the authors intended the only flag to just shield the initially available hypotheses, but not also "new" ones. For this, we probably have to wait for the authors of the tactic to comment, I guess.

[Damiano Testa]

I, for one, would not have expected the tactic to use more hypotheses than the ones that I would give it, when using the only flag, but I do not have any experience with other proof assistants.

[Kim Morrison]

In fact, solve_by_elim introducing hypotheses at all came after the implementation of only, so this is just an oversight.

[Kim Morrison]

I think I agree that even with only, introduced hypotheses should be used.

[Kim Morrison]

@Claudio Sacerdoti Coen, I'm not sure if you're interested in investigating, but I'd be open to reviewing a change to the tactic implementation to this effect.

[Kim Morrison]

Otherwise, you could open an issue! No promises for fast action on this one, however.

[Claudio Sacerdoti Coen]

Hi @Kim Morrison I had opened the RFC https://github.com/leanprover/lean4/issues/4870