The order tactic
This tactic is designed to solve systems of (in)equations
involving
eq,
lt,
le and
~eq on some type. This tactic is
domain-agnostic; it will only use equivalence+order axioms, and
not analyze elements of the domain. Hypothesis or goal of the form
~lt or
~le are initially turned into
le and
lt, other
parts of the goal are ignored. This initial preparation of the
goal is the only moment where totality is used. In particular,
the core of the tactic only proceeds by saturation of transitivity
and similar properties, and does not perform case splitting.
The tactic will fail if it doesn't solve the goal.
An abstract vision of the predicates. This allows a one-line
statement for interesting transitivity properties: for instance
trans_ord OLE OLE = OLE will imply later
le x y -> le y z -> le x z.
order_eq : replace x by y in all (in)equations hyps thanks
to equality EQ (where eq has been hidden in order to avoid
self-rewriting), then discard EQ.
Goal preparation : We turn all negative hyps into positive ones
and try to prove False from the inverse of the current goal.
These steps require totality of our order. After this preparation,
order only deals with the context, and tries to prove False.
Hypotheses of the form A -> False are also folded in ~A
for convenience (i.e. cope with the mess left by intuition).
The complete tactic.