Especially in the context of lia
, which can sometimes fail to prove a theorem in the form of
forall x, x <> 0 -> P x
but succeeds no problem with
forall x, x > 0 -> P x
I want to define a tactic that adds x > 0
for every hypothesis in the form of x <> 0
(and vice versa) for further automation of arithmetic proofs. I've tried the following but it (somewhat expectedly) loops:
Ltac aux :=
match goal with
| [ X : _ <> 0 |- _ ] => (
pose proof (ne_gt0 X);
aux
)
end.
I've also tried using the goal as temporary buffer but it only processes first (arbitrary?) hypothesis:
Ltac aux :=
match goal with
| [ X : _ <> 0 |- _ ] => (
pose proof (ne_gt0 X);
revert X;
aux;
intro
)
end.
Is it possible in Ltac? Related side question: I'd like to do this for many theorems in the form of P -> Q
. If possible, can the workload of writing many similar rules be simplified through some "higher-order tactic"?