- STRUCTURE
- SYNOPSIS
Applies a list-tactic to the current goal, stacking the resulting subgoals.
- DESCRIPTION
The function expand_listf is a faster version of expand_list.
It does not use a validated version of the list-tactic.
That is, no check is made that the justification of the list-tactic
does prove the goals from the subgoals it generates.
If an invalid list-tactic is used,
the theorem ultimately proved may not match the goal originally set.
Alternatively, failure may occur when the justifications
are applied in which case the theorem would not be proved. For a description of
the subgoal package, see under set_goal.
- FAILURE
Calling expand_listf ltac fails if the list-tactic ltac fails
for the current goal list. It will diverge if the list-tactic diverges
for the goals. It will fail if there are no
unproven goals. This could be because no goal has been set using set_goal or
because the last goal set has been completely proved. If an invalid tactic,
whose justification actually fails, has been used earlier in the proof,
expand_listf ltac may succeed in applying ltac and apparently prove
the current goals. It may then fail as it applies the justifications
of the tactics applied earlier.
- USES
Saving CPU time when doing goal-directed proofs, since the extra validation is
not done. Redoing proofs quickly that are already known to work.
- COMMENTS
The CPU time saved may cause misery later.
If an invalid tactic or list-tactic is used, this
will only be discovered when the proof has apparently been finished and the
justifications are applied.
- SEEALSO
set_goal,
restart,
backup,
restore,
save,
set_backup,
expand,
expandf,
expand_list,
p,
top_thm,
top_goal