# Ltac - run tactic for each hypothesis of given pattern

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"?

1. Perhaps the base case is just missing in your implementations as recursive tactics.
Lemma ne_gt0 {x} : x <> 0 -> 0 < x.
Proof. intro; now apply Nat.neq_0_lt_0.  Qed.

Ltac aux_rec :=
match goal with
| [ X : _ <> 0 |- _ ] => (
pose proof (ne_gt0  X);
revert X;
aux_rec
)
| [ |- _] => idtac
end.

Goal forall x y z, x <> 0 -> y <> 0 -> z <> 0 -> x+y+z <> 0.
intros. aux_rec.


In your post, you put a question mark on the X hypothesis name, which caused a syntax error.

(EDITED)

Here's is another solution, which doesn't change hypothesis names in the current context (contrary to the previous one).

It uses the LibHyps library:

From LibHyps Require Import LibHyps.

Ltac aux_no_rename :=
onAllHyps (fun h =>
match type of h with
| (?n <> 0) => assert (0 < n) by now apply (ne_gt0 h)
| _ => idtac
end).

Goal forall x y z, x <> 0 -> y <> 0 -> z <> 0 -> x+y+z <> 0.
intros x y z Hx Hy Hz; aux_no_rename.

• Completely missed that, thank you so much! I typed the examples on mobile from memory so syntax errors are possible, sorry about that. Commented Jul 14, 2023 at 5:41

Another way to do this is to check for the hypothesis that you're inserting. I use this pattern pretty commonly.

Ltac aux :=
repeat match goal with
| [X: ?n <> 0 |- _] =>
match goal with
| [ _ :  0 < n |- _ ] => fail 1
| _ => pose proof (ne_gt0 X)
end
end.

Goal forall x y z, x <> 0 -> y <> 0 -> 0 < y -> z <> 0 -> x+y+z <> 0.
intros x y z Hx Hy Hy'  Hz; aux.

• It may be interesting to note that your tactic can be easily adapted to LibHyps. The outer match becomes an onAllHyps loop, and the fail 1 an idtac. Commented Jul 11, 2023 at 6:04