(** Ltac definitions **)
Require Import Coq.Bool.Bool Coq.Reals.Reals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet.


Ltac iv_assert iv name:=
  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).

(** Automatic translation and destruction of conjuctinos with andb into Props **)
Ltac andb_to_prop H :=
  apply Is_true_eq_left in H;
  apply andb_prop_elim in H;
  let Left := fresh "L" in
  let Right := fresh "R" in
  destruct H as [Left Right];
  apply Is_true_eq_true in Left;
  apply Is_true_eq_true in Right;
  try andb_to_prop Left;
  try andb_to_prop Right.

Ltac NatSet_simp hyp :=
  try rewrite NatSet.mem_spec in hyp;
  try rewrite NatSet.equal_spec in hyp;
  try rewrite NatSet.subset_spec in hyp;
  try rewrite NatSet.empty_spec in hyp;
  try rewrite NatSet.is_empty_spec in hyp;
  try rewrite NatSet.add_spec in hyp;
  try rewrite NatSet.remove_spec in hyp;
  try rewrite NatSet.singleton_spec in hyp;
  try rewrite NatSet.union_spec in hyp;
  try rewrite NatSet.inter_spec in hyp;
  try rewrite NatSet.diff_spec in hyp.

Ltac NatSet_prop :=
  match goal with
  | [ H : true = true |- _ ] => clear H; NatSet_prop
  | [ H: ?T = true |- _ ] => NatSet_simp H;
                           (apply Is_true_eq_left in H; NatSet_prop; apply Is_true_eq_true in H) || NatSet_prop
  | _ => try auto
  end.