Revisions to Ltac - run tactic for each hypothesis of given pattern

Fix a few minor typos (syntax).

Source Link

edited Jul 10, 2023 at 21:54

304
1
6

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.

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.

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.

Fix a few minor typos (syntax).

Source Link

edit approved Jul 10, 2023 at 21:54

Pierre Castéran

673
2
5

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[X: ?n <> 0) |- _] =>
           match goal with
           | (n[ <_ :  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.

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
           | (n < 0) => fail 1
           | _ => pose proof (ne_gt0 X)
           end
         end.

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.

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.

Source Link

created Jul 10, 2023 at 14:33

Andrew K. Hirsch

304
1
6

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
           | (n < 0) => fail 1
           | _ => pose proof (ne_gt0 X)
           end
         end.

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.

Stack Exchange Network

Return to Answer