----------------------------------------------------------------------
suffices_by                                                  (bossLib)
----------------------------------------------------------------------
op suffices_by : term quotation * tactic -> tactic

SYNOPSIS
Replace the goal’s conclusion with a sufficient alternative.

KEYWORDS
declarative theorem-proving

DESCRIBE
A call to the tactic {q suffices_by tac} will first attempt to parse
the quotation {q} in the context of the current goal. Assuming this
generates a term {qt} of boolean type, it will then generate two
sub-goals. Assuming the current goal is {asl ?- g}, the first new
sub-goal will be that {qt} implies {g}, thus {asl ?- qt ==> g}. The
second goal will be {asl ?- qt}.

The system next applies {tac} to the first sub-goal (the implication).
If {tac} solves the goal (the common or at least, desired, case), the
user will then be presented with one goal, where the original {g} has
been replaced with {qt}. In this way, the user has adjusted the goal,
replacing the old {g} with a {qt} that is sufficient to prove it.

FAILURE
A call to {q suffices_by tac} will fail if the quotation {q} does not
parse to a term of boolean type. This parsing is done in the context
of the whole goal {(asl,g)}, using the {parse_in_context} function.
The call will also fail if {tac} does not solve the newly generated
subgoal.

EXAMPLE
If the current goal is

   f n m = f m n
   ------------------------------------
     0.  m <= n
     1.  n <= m

then the tactic {`m = n` suffices_by SIMP_TAC bool_ss []} will result in the goal

   m = n
   ------------------------------------
     0.  m <= n
     1.  n <= m

where the call to {SIMP_TAC} has successfully proved the theorem

   |- (m = n) ==> (f m n = f n m)

eliminating the first of the two sub-goals that was generated.

COMMENTS
The tactic {suffices_by} is designed to support a backwards style of
reasoning. Superficially, it appears to be dual to the tactic {by},
which provides a forward-reasoning facility. In fact, both are
implementing a backwards application of the sequent calculus’s “cut”
rule; the difference is which of the two premises to the rule is
worked on by the provided tactics.

SEEALSO
bossLib.by, Parse.parse_in_context, Tactic.SUFF_TAC.

----------------------------------------------------------------------