expand_listfproofManagerLib.expand_listf : (list_tactic -> unit)Applies a list-tactic to the current goal, stacking the resulting subgoals.
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.
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.
Saving CPU time when doing goal-directed proofs, since the extra validation is not done. Redoing proofs quickly that are already known to work.
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.
proofManagerLib.set_goal,
proofManagerLib.restart,
proofManagerLib.backup,
proofManagerLib.redo,
proofManagerLib.restore,
proofManagerLib.save,
proofManagerLib.set_backup,
proofManagerLib.expand,
proofManagerLib.expandf,
proofManagerLib.expand_list,
proofManagerLib.p, proofManagerLib.top_thm,
proofManagerLib.top_goal