Closed leodemoura closed 7 years ago
I don't have a strong opinion about this change, but I think it is a good change. Some related remarks from my experience:
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.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.
@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?
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).
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.
@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).
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 @
).
I think that the current apply
is the best (the one that I'll use most often) default apply
.
eapply
is pretty confusing, to a Coq user, however. In Coq at least, the e stands for existential, and is a reference to the metavariables that eapply creates. I might suggest renaming eapply
to sapply
(for strict) or anything other than eapply
really.
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/bhStu87PjiIThis 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 usingapply
, we would getN_1, ..., N_k, D_1, ..., D_m, G_2, ..., G_n
, whereN
s are subgoals for nondependent arguments andD
s are subgoals for dependent ones. In the current implementation, we getN_1, ..., N_k, G_2, ..., G_n
.The idea is: if solving the subgoals
N
s we also solve theD
s (as expected when usingapply
), then we are fine, andD
s would be automatically removed. If they are not, then we would be forced to solve theD
s. The tacticfapply
would continue to work as it does now. The main difference betweenfapply
andapply
is thatfapply
does not move subgoals for dependent arguments are not moved after the ones for dependent ones.