Ltacs.v 4.58 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
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
24
  | [ H: Qeq_bool ?a ?b = true |- _] => rewrite Qeq_bool_iff in H
25 26 27 28 29
  end.

Ltac canonize_Q_to_R :=
  match goal with
  | [ H: (?a <= ?b)%Q |- _ ] => apply Qle_Rle in H
30
  | [ H: (?a == ?b)%Q |- _ ] => apply Qeq_eqR in H
31 32 33 34 35 36
  | [ 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.

37 38 39 40 41 42 43 44 45 46 47 48
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.

49 50 51 52
Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
  match v with
  |Some val => f val
  | None => e
53 54
  end.

55 56 57
Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
  match v with |Some val => f val | None => e end = optionLift X Y v f e.
Proof.
Heiko Becker's avatar
Heiko Becker committed
58
  reflexivity.
59 60 61 62 63
Qed.

Lemma optionLift_cond X (a:bool) (b c :X):
  (if a then b else c) = match a with |true => b |false => c end.
Proof.
Heiko Becker's avatar
Heiko Becker committed
64
  reflexivity.
65 66 67 68 69 70
Qed.

Ltac remove_matches := rewrite optionLift_eq in *.

Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.

Heiko Becker's avatar
Heiko Becker committed
71
Ltac match_factorize_asm :=
72
  match goal with
73 74 75 76 77 78
  | [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
    => rewrite H; cbn
  | [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
    => rewrite H1 in H2; cbn in H2
  | [ H: context [optionLift _ _ ?t _ _] |- _ ]
    => destruct t eqn:?; cbn in H; try congruence
Heiko Becker's avatar
Heiko Becker committed
79 80 81 82 83 84
  end.


Ltac match_factorize :=
  match_factorize_asm ||
  match goal with
85 86
  | [ |- context [optionLift _ _ ?t _ _] ]
    => destruct t eqn:?; cbn; try congruence
87 88
  end.

89
Ltac pair_factorize :=
90
  match goal with
91 92 93
  | [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
  end.

94 95 96 97 98 99 100 101
Ltac destr_factorize :=
  match goal with
  | [H1: _ ?v = Some ?a, H2: _ ?v = Some ?b |- _]
      => rewrite H1 in H2; inversion H2; subst; clear H2
  | [H1:  _ ?k ?M = Some ?a, H2: _ ?k ?M = Some ?b |- _]
    => rewrite H1 in H2; inversion H2; subst; clear H2
  end.

102 103 104 105 106 107
Ltac match_simpl :=
  try remove_conds;
  try remove_matches;
  repeat match_factorize;
  try pair_factorize.

108 109 110 111 112
Ltac bool_factorize :=
  match goal with
  | [H: _ = true |- _] => andb_to_prop H
  end.

Heiko Becker's avatar
Heiko Becker committed
113 114 115 116 117 118 119 120
Ltac Daisy_compute_asm :=
  repeat (
      (try remove_conds;
       try remove_matches;
       repeat match_factorize_asm;
       try pair_factorize) ||
      bool_factorize).

121
Ltac Daisy_compute :=
Heiko Becker's avatar
Heiko Becker committed
122 123 124 125 126 127
  repeat (
      (try remove_conds;
      try remove_matches;
      repeat match_factorize;
      try pair_factorize) ||
      bool_factorize).
128

129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149
(* 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 *)
(*   | [H: _ |- if ?c then ?a else ?b = _] => *)
(*       case_eq ?c; *)
(*       let name := fresh "cond" in *)
(*       intros name; *)
(*       rewrite name in *; *)
(*       try congruence *)
(*       end. *)

(* Ltac match_destr t:= *)
(*   match goal with *)
(*   | H: context [optionLift (DaisyMap.find ?k ?M) _ _] |- _ => *)
(*     destruct (DaisyMap.find (elt:=intv * error) k M); idtac H *)
(*   end. *)
150 151 152 153

Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
  match goal with
  | [H: ?ty |- _ ] => unify pat ty; t H
Heiko Becker's avatar
Heiko Becker committed
154 155 156 157 158 159 160 161 162
  end.

Ltac telling_rewrite pat hyp :=
  match goal with
  | [H: context[pat] |- _ ] => rewrite hyp in H; constr:(H)
  end.

Tactic Notation "unify asm" open_constr(pat) hyp(H):=
  telling_rewrite pat H.