(** 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.