RFC: making apply tactic more robust #1342
Comments
I don't have a strong opinion about this change, but I think it is a good change.
Sorry I didn't have much to contribute to the question itself. |
@fpvandoorn Thanks for the feedback. I'm happy to make example : ∃ x : nat, x = 0 :=
begin
apply exists.intro,
reflexivity
end The user would have to 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.
Should this be signed as an error? |
But our current default behavior is already different than the behavior in Coq. In Coq, if I try
it fails, and
I do think it's good to have a variant of Note: we also should change
Good question. If we include unsolved metavariables as new subgoals then we come really close to the |
Quick feedback: I wanted to test what breaks in |
@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 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 |
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 |
See issue leanprover#1342 Support for auto_param and opt_param has not been implemented yet. @johoelzl The coinductive.lean test is not working anymore. As discussed at leanprover#1342, I added `eapply` which should behave like the old `apply`. I also added `eapplyc` (to simulate the old `applyc`) and `econstructor`. I tried to use these tactics at coinductive_predicate.lean, but it didn't help. I'm assuming that `coinductive_predicate.lean` depends on some other tactic that depends on `apply`. I spent a few hours trying to fix `coinductive.lean`, but I don't know what is going on. I also tried to comment line 158 at apply_tactic.cpp collect_metavars(e, e_metas); By commenting this line, we disable a feature requested by @fpvandoorn. Second bullet at leanprover#1342 (comment) I thought the new goals could be confusing your tactics, but it didn't help. I'm still getting the same error. I would really appreciate if you could take a look. All other tests are passing. Thanks, Leo
See issue #1342 Support for auto_param and opt_param have not been implemented yet.
I think that the current
|
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 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 tactic
fapply
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.The text was updated successfully, but these errors were encountered: