Ltac - run tactic for each hypothesis of given pattern

Question

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

Answer 1

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. 
Admitted. 

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.
Admitted. 

Answer 2

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.
Admitted. 

Here, fail 1 causes the failure to go up one level, causing the mach with ?n <> 0 to fail. So, we're checking for every hypothesis of the form ?n <> 0 and, for each of those checking to make sure that we don't already have the fact that n < 0 recorded. If we don't, then we record it.