7.4 Negation and contradiction
7.4.1 Absurd term
This tactic applies to any goal. The argument term is any proposition P of type Prop. This tactic applies False elimination, that is it deduces the current goal from False, and generates as subgoals ~P and P. It is very useful in proofs by cases, where some cases are impossible. In most cases, P or ~P is one of the hypotheses of the local context.7.4.2 Contradiction
This tactic applies to any goal. The Contradiction tactic attempts to find in the current context (after all Intros) one which is equivalent to False. It permits to prune irrelevant cases. This tactic is a macro for the tactics sequence Intros; ElimType False; Assumption.Error messages:
- No such assumption