Return to Answer

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

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. 

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) => 
                   let Y:= fresh in assert (Y: 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. aux_no_rename.
Admitted. 

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

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.

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) => 
                   let Y:= fresh in assert (Y: 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. aux_no_rename.
Admitted.