discriminate

discriminate solves goals that are trivial inequalities (something of the form x <> y)*. This tactic will fail if the goal is not an inequality or is non-trivial.

* Keep in mind that x <> y is actually shorthand for x = y -> False! This means that discriminate actually searches for trivial inequalities in assumptions.

Syntax

(* Simple usage *)
discriminate.

Examples

Before

=========================
1/1
1 <> 2

discriminate.

After

No more goals.

Before

=========================
1/1
"hello" <> "world"

discriminate.

After

No more goals.

Before

H: S n = O
==========================
1/1
False

discriminate.

After

No more goals.

Resources

Reference Documentation

---