Require Import Undecidability.Shared.Libs.PSL.Base Lia Ring.
Tactic Notation "destruct" "_":=
match goal with
| [ |- context[match ?X with _ => _ end] ] => destruct X
end.
Tactic Notation "destruct" "_" "eqn" ":" ident(E) :=
match goal with
| [ |- context[match ?X with _ => _ end] ] => destruct X eqn:E
end.
Tactic Notation "destruct" "*" :=
repeat destruct _.
Ltac dec :=
match goal with
| [ |- context[Dec ?X] ] => decide X
end.
Ltac trace :=
match goal with
|- ?G => idtac "Trace:";idtac G
end.
Require Export ZArith.
Ltac leq_crossout :=
try zify;try apply Zle_0_minus_le; ring_simplify;
repeat eapply Z.add_nonneg_nonneg;try now (repeat eapply Z.mul_nonneg_nonneg;easy).
Tactic Notation (at level 3) "repeat'" tactic3(t) :=
let rec loop := (once t);try loop in loop.
Tactic Notation "destruct" "_":=
match goal with
| [ |- context[match ?X with _ => _ end] ] => destruct X
end.
Tactic Notation "destruct" "_" "eqn" ":" ident(E) :=
match goal with
| [ |- context[match ?X with _ => _ end] ] => destruct X eqn:E
end.
Tactic Notation "destruct" "*" :=
repeat destruct _.
Ltac dec :=
match goal with
| [ |- context[Dec ?X] ] => decide X
end.
Ltac trace :=
match goal with
|- ?G => idtac "Trace:";idtac G
end.
Require Export ZArith.
Ltac leq_crossout :=
try zify;try apply Zle_0_minus_le; ring_simplify;
repeat eapply Z.add_nonneg_nonneg;try now (repeat eapply Z.mul_nonneg_nonneg;easy).
Tactic Notation (at level 3) "repeat'" tactic3(t) :=
let rec loop := (once t);try loop in loop.