SPOSE_NOT_THEN

bossLib.SPOSE_NOT_THEN : (thm -> tactic) -> tactic

Initiate proof by contradiction.

SPOSE_NOT_THEN provides a flexible way to start a proof by contradiction. Simple tactics for contradiction proofs often simply negate the goal and place it on the assumption list. However, if the goal is quantified, as is often the case, then more processing is required in order to get it into a suitable form for subsequent work. SPOSE_NOT_THEN ttac negates the current goal, pushes the negation inwards, and applies ttac to it.

Failure

Never fails, unless ttac fails.

Example

Suppose we want to prove Euclid’s theorem.

   !m. ?n. prime n /\ m < n

The classic proof is by contradiction. However, if we start such a proof with CCONTR_TAC, we get the goal

   { ~!m. ?n. prime n /\ m < n } ?- F

and one would immediately want to simplify the assumption, which is a bit awkward. Instead, an invocation SPOSE_NOT_THEN ASSUME_TAC yields

   { ?m. !n. ~prime n \/ ~(m < n) } ?- F

and SPOSE_NOT_THEN STRIP_ASSUME_TAC results in

   { !n. ~prime n \/ ~(m < n) } ?- F

See also

Tactic.CCONTR_TAC, Tactic.CONTR_TAC, Tactic.ASSUME_TAC, Tactic.STRIP_ASSUME_TAC