Ltacs.v 2.86 KB
Newer Older
1
(** Ltac definitions **)
2 3
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
4

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

8 9 10 11 12 13 14 15 16 17 18 19
(** 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.

20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
Ltac canonize_Q_prop :=
  match goal with
  | [ H: Qle_bool ?a ?b = true |- _] => rewrite Qle_bool_iff in H
  | [ H: Qleb ?a ?b = true |- _ ] => rewrite Qle_bool_iff in H
  end.

Ltac canonize_Q_to_R :=
  match goal with
  | [ H: (?a <= ?b)%Q |- _ ] => apply Qle_Rle in H
  | [ H: context [Q2R 0] |- _ ] => rewrite Q2R0_is_0 in H
  | [ |- context [Q2R 0] ] => rewrite Q2R0_is_0
  end.

Ltac canonize_hyps := repeat canonize_Q_prop; repeat canonize_Q_to_R.

35 36 37 38 39 40 41 42 43 44 45 46
Ltac Q2R_to_head_step :=
  match goal with
  | [ H: context[Q2R ?a + Q2R ?b] |- _] => rewrite <- Q2R_plus in H
  | [ H: context[Q2R ?a - Q2R ?b] |- _] => rewrite <- Q2R_minus in H
  | [ H: context[Q2R ?a * Q2R ?b] |- _] => rewrite <- Q2R_minus in H
  | [ |- context[Q2R ?a + Q2R ?b]] => rewrite <- Q2R_plus
  | [ |- context[Q2R ?a - Q2R ?b]] => rewrite <- Q2R_minus
  | [ |- context[Q2R ?a * Q2R ?b]] => rewrite <- Q2R_minus
  end.

Ltac Q2R_to_head := repeat Q2R_to_head_step.

47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
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
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
  end.

Ltac match_simpl :=
  match goal with
  | [ H: ?t = ?u |- context [match ?t with _ => _ end]] => rewrite H; simpl
  end.

Ltac destruct_if :=
  match goal with
  | [H: (if ?c then ?a else ?b) = _ |- _ ] =>
    case_eq ?c;
    let name := fresh "cond" in
    intros name;
    rewrite name in *;
    try congruence
81 82 83 84 85 86 87 88 89 90
  end.

(* HOL4 Style patter matching tactics *)
Tactic Notation "lift " tactic(t) :=
  fun H => t H.

Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
  match goal with
  | [H: ?ty |- _ ] => unify pat ty; t H
  end.