4
$\begingroup$

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

$\endgroup$

2 Answers 2

3
$\begingroup$
  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. 
$\endgroup$
1
  • $\begingroup$ Completely missed that, thank you so much! I typed the examples on mobile from memory so syntax errors are possible, sorry about that. $\endgroup$
    – shooqie
    Jul 14, 2023 at 5:41
3
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Jul 11, 2023 at 6:04
  • $\begingroup$ A little bit wordy when we want to write a single tactic for multiple such cases but elegant nonetheless, thank you! $\endgroup$
    – shooqie
    Jul 14, 2023 at 5:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.