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'" (t) :=
  let rec loop := (once t);try loop in loop.