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.

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

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

Lemma optionLift_cond X (a:bool) (b c :X):
62
  (if a then b else c) = match a with |true => b |false => c end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
63
Proof.
Heiko Becker's avatar
Heiko Becker committed
64
  reflexivity.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
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
  end.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
81
Ltac match_factorize :=
Heiko Becker's avatar
Heiko Becker committed
82 83
  match_factorize_asm ||
  match goal with
84 85
  | [ |- context [optionLift _ _ ?t _ _] ]
    => destruct t eqn:?; cbn; try congruence
86
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
87 88

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

93 94 95 96 97 98 99
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.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
100 101

Ltac match_simpl :=
102 103 104 105
  try remove_conds;
  try remove_matches;
  repeat match_factorize;
  try pair_factorize.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
106 107

Ltac bool_factorize :=
108 109 110
  match goal with
  | [H: _ = true |- _] => andb_to_prop H
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
111

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

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

128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
(* 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. *)
149 150 151 152

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

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.