RFC: making apply tactic more robust

[leodemoura]

As other proof assistants, the apply tactic will not create subgoals for dependent arguments.
See issue at: https://groups.google.com/forum/#!topic/lean-user/bhStu87PjiI

This decision minimizes the number of goals, but it may produce counter intuitive behavior where we finish a proof but still have unsolved metavariables.

I think we can avoid this issue by adding the subgoals for dependent arguments after the ones for non dependent arguments. That is, given the list of goals G_1, ..., G_n, by using apply, we would get N_1, ..., N_k, D_1, ..., D_m, G_2, ..., G_n, where Ns are subgoals for nondependent arguments and Ds are subgoals for dependent ones. In the current implementation, we get N_1, ..., N_k, G_2, ..., G_n.

The idea is: if solving the subgoals Ns we also solve the Ds (as expected when using apply), then we are fine, and Ds would be automatically removed. If they are not, then we would be forced to solve the Ds.
The tactic fapply would continue to work as it does now. The main difference between fapply and apply is that fapply does not move subgoals for dependent arguments are not moved after the ones for dependent ones.

[fpvandoorn]

I don't have a strong opinion about this change, but I think it is a good change.
Some related remarks from my experience:

• I think the fapply tactic should be the default apply. In my experience fapply is more often useful than apply (of course most of the time they will do the same thing). And maybe more important: I think fapply is less confusing for new users. But I think we've discussed this before, so if you don't agree, we don't have to discuss this again.
• Some related behavior which can be confusing (at least in Lean 2, but it's probably the same in Lean 3): if you (accidentally) write something like apply eq.trans _ H then Lean will accept the proof, but complain at the end that there is an unsolved metavariable. This can also confuse users.

Sorry I didn't have much to contribute to the question itself.

[leodemoura]

@fpvandoorn Thanks for the feedback. I'm happy to make fapply the default apply. My main concern is that this is not the default behavior in other proof assistants. Moreover, simple proofs like the following one would not work anymore.

example : ∃ x : nat, x = 0 :=
begin
  apply exists.intro,
  reflexivity
end

The user would have to swap the goals.

example : ∃ x : nat, x = 0 :=
begin
  apply exists.intro,
  swap,
  reflexivity
end

or provide the witness manually.

example : ∃ x : nat, x = 0 :=
begin
  apply exists.intro,
  exact 0,
  reflexivity
end

Do you think this is acceptable? Should we try to reorder the sub goals as suggested above? I'm concerned that reordering the new sub goals automatically may also generate confusion.

Some related behavior which can be confusing (at least in Lean 2, but it's probably the same in Lean 3): if you (accidentally) write something like apply eq.trans _ H

Should this be signed as an error?
If we include unsolved metavariables as new subgoals, do we put them first?

[fpvandoorn]

My main concern is that this is not the default behavior in other proof assistants.

But our current default behavior is already different than the behavior in Coq. In Coq, if I try

Definition foo : exists n, n = 0.
Proof.
apply ex_intro.

it fails, and eapply seems to have the same behavior as our current apply.

Moreover, simple proofs like the following one would not work anymore.

I do think it's good to have a variant of apply which has the same behavior as the current apply, so that you can still use that one if you want a short proof. With the current fapply you can also use fapply exists.intro _.

Note: we also should change constructor / fconstructor

Should this be signed as an error?
If we include unsolved metavariables as new subgoals, do we put them first?

Good question. If we include unsolved metavariables as new subgoals then we come really close to the refine tactic. I'm indifferent between adding them as subgoals or signing an error, but I think both of them are much better than the current behavior.
But if the unsolved metavariable still occurs in a generated subgoal (like in fapply exists.intro _), then no error should be signed (in this situation I'm indifferent between adding them as subgoal or keeping the current behavior).

[Kha]

Quick feedback: I wanted to test what breaks in library and library_dev if one redefines interactive.apply to fapply, but there was no fallout at all.

[avigad]

@Kha, as yet, that doesn't mean much: there aren't many tactic proofs in either yet. I can imagine that @fapply is more useful in HoTT-like situations, but in ordinary mathematical situations in Isabelle I often applied tactics that produced metavariables (like le_trans) with the intention of later applying another tactic that would fix the right instantiation.

So, we have three potential behaviors: (1) the current apply, (2) Leo's proposed apply, and (3) fapply. I don't have strong feelings as to which should be the default apply. I guess I vote for (2), leaving fapply alone, and using eapply for (1).

[avigad]

Here is another counterintuitive behavior:

example {α : Type} [weak_order α] (a : α) : a = a :=
begin
  apply le_antisymm,
  -- there are now three goals; the third is ⊢ weak_order α
  trace_state,
  -- class inference could fill the third 
  tactic.focus [tactic.skip, tactic.skip, tactic.apply_instance],
  apply le_refl,
  apply le_refl
end

The problem is that le_antisymm inserts two metavariables, one for the type and one for the type class. The apply tactic solves for the first, but class inference is not called on the second. As @gebner points out, apply @le_antisymm and apply @le_antisymm α _ both work: in the first case, the apply tactic calls class inference, and in the second, the elaborator does it successfully.
I don't know if there is a nice solution to this. We could have apply guess at which metavariable should be solved by class inference, but then there would be know way to suppress this behavior. At least, with the current behavior, there is an easy workaround (adding the @).