Ltacs.v 7.26 KB
Newer Older
1
(** Ltac definitions **)
2 3 4 5
From Coq
     Require Import Bool.Bool Reals.Reals QArith.QArith QArith.Qreals micromega.Psatz.
From Flover.Infra
     Require Import RealSimps NatSet RationalSimps RealRationalProps Results.
6

7
Global Set Implicit Arguments.
8

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

12 13 14 15 16 17 18 19 20 21 22 23
(** 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.

24 25 26 27 28 29 30 31 32
Ltac split_bool :=
  match goal with
  | [|- (_ && _) = true ] => apply Is_true_eq_true;
                             apply andb_prop_intro;
                             split;
                             apply Is_true_eq_left
  | _ => fail "Cannot case split on non-boolean conjunction"
  end.

33 34 35 36
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
37
  | [ H: Qeq_bool ?a ?b = true |- _] => rewrite Qeq_bool_iff in H
38 39 40 41 42
  end.

Ltac canonize_Q_to_R :=
  match goal with
  | [ H: (?a <= ?b)%Q |- _ ] => apply Qle_Rle in H
43
  | [ H: (?a == ?b)%Q |- _ ] => apply Qeq_eqR in H
44 45 46 47 48 49
  | [ 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.

50 51 52 53 54 55 56 57 58 59 60 61
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.

62 63 64 65 66 67
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
  match v with
  | Some v => f v
  | None => e
  end.

68 69 70 71 72 73 74 75 76
Definition resultBind (X:Type) (r:result X) (f: X  -> result X) :result X :=
  match r with
  | Succes res => f res
  | _ => r
  end.

Definition resultReturn (X:Type) (r:X) :=
  Succes r.

77 78 79 80
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None)
                                       (only parsing, at level 0, t at level 200).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False)
                                       (only parsing, at level 0, t at level 200).
81 82 83 84
Notation "'rlet' x ':=' u 'in' t" := (resultBind u (fun x => t))
                                       (only parsing, at level 0, t at level 200).
Notation "'ret' x" := (resultReturn x) (only parsing, at level 0 ).

85 86
Ltac optionD :=
  match goal with
87 88
  |H: context[resultBind ?v ?f] |- _ =>
   destruct v eqn:?
89
  |H: context[optionBind ?v ?default ?f] |- _ =>
90
   destruct v eqn:?
91 92
  end.

93 94
Lemma optionBind_eq (X Y: Type) v (f: X -> Y) (e: Y):
  match v with |Some val => f val | None => e end = optionBind v f e.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
95
Proof.
Heiko Becker's avatar
Heiko Becker committed
96
  reflexivity.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
97 98
Qed.

99
Lemma optionBind_cond X (a:bool) (b c: X):
100
  (if a then b else c) = match a with |true => b |false => c end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
101
Proof.
Heiko Becker's avatar
Heiko Becker committed
102
  reflexivity.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
103 104
Qed.

105
Ltac remove_matches := rewrite optionBind_eq in *.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
106

107 108
Ltac remove_matches_asm := rewrite optionBind_eq in * |- .

109
Ltac remove_conds := rewrite <- andb_lazy_alt in *.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
110

111
Ltac remove_conds_asm := rewrite <- andb_lazy_alt in * |- .
112

113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
Ltac result_factorize_asm :=
  match goal with
  | [ H: ?t = ?u |- context [resultBind ?t _ ]]
    => rewrite H; cbn
  | [ H1: ?t = ?u, H2: context [resultBind ?t _] |- _ ]
    => rewrite H1 in H2; cbn in H2
  | [ H: context [resultBind ?t _ ] |- _ ]
    => destruct t eqn:?; cbn in H; try congruence
  end.

Ltac result_factorize :=
  result_factorize_asm ||
  match goal with
  | [ |- context [resultBind ?t _] ]
    => destruct t eqn:?; cbn; try congruence
  end.

Heiko Becker's avatar
Heiko Becker committed
130
Ltac match_factorize_asm :=
131
  match goal with
132
  | [ H: ?t = ?u |- context [optionBind ?t _ _]]
133
    => rewrite H; cbn
134
  | [ H1: ?t = ?u, H2: context [optionBind ?t _ _] |- _ ]
135
    => rewrite H1 in H2; cbn in H2
136
  | [ H: context [optionBind ?t _ _] |- _ ]
137
    => destruct t eqn:?; cbn in H; try congruence
Heiko Becker's avatar
Heiko Becker committed
138 139
  end.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
140
Ltac match_factorize :=
Heiko Becker's avatar
Heiko Becker committed
141 142
  match_factorize_asm ||
  match goal with
143
  | [ |- context [optionBind ?t _ _] ]
144
    => destruct t eqn:?; cbn; try congruence
145
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
146 147

Ltac pair_factorize :=
148
  match goal with
149 150 151
  | [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
  end.

152 153 154 155 156 157 158
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
159 160

Ltac match_simpl :=
161 162 163
  try remove_conds;
  try remove_matches;
  repeat match_factorize;
164
  repeat result_factorize;
165
  try pair_factorize.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
166 167

Ltac bool_factorize :=
168 169 170
  match goal with
  | [H: _ = true |- _] => andb_to_prop H
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
171

172
Ltac Flover_compute_asm :=
Heiko Becker's avatar
Heiko Becker committed
173
  repeat (
174 175
      (try remove_conds_asm;
       try remove_matches_asm;
Heiko Becker's avatar
Heiko Becker committed
176
       repeat match_factorize_asm;
177
       repeat result_factorize_asm;
Heiko Becker's avatar
Heiko Becker committed
178 179
       try pair_factorize) ||
      bool_factorize).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
180

181
Ltac Flover_compute :=
Heiko Becker's avatar
Heiko Becker committed
182 183 184 185
  repeat (
      (try remove_conds;
      try remove_matches;
      repeat match_factorize;
186
      repeat result_factorize;
Heiko Becker's avatar
Heiko Becker committed
187 188
      try pair_factorize) ||
      bool_factorize).
189

190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
(* 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 *)
208
(*   | H: context [optionBind (FloverMap.find ?k ?M) _ _] |- _ => *)
209
(*     destruct (FloverMap.find (elt:=intv * error) k M); idtac H *)
210
(*   end. *)
211 212 213 214

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
215
  end.
Heiko Becker's avatar
Heiko Becker committed
216 217 218 219 220 221 222 223

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.
224

225 226 227 228
(* Takes a field-structure equality expression, tries to rewrite the *)
(* the left side in the goal with right if the equality holds        *)
Ltac field_rewrite H :=
  let tmp := fresh "tmp" in
229
  assert H as tmp by (try field; try lra); rewrite tmp; clear tmp.
230

231 232 233 234 235 236 237 238 239 240
Ltac destruct_ex H pat :=
  match type of H with
  | exists v, ?H' =>
               let vFresh:=fresh v in
               let fN := fresh "ex" in
               destruct H as [vFresh fN];
               destruct_ex fN pat
  | _ => destruct H as pat
  end.

241
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
242 243 244 245 246 247 248 249 250 251

(* Debugging tactics, if scripts fail *)
Ltac debug_term t :=
  let name := fresh "debug" in
  let res := (eval compute in t) in
  assert (t = res) as name by (vm_compute; auto);
  rewrite name; clear name.

Ltac step f :=
  cbn iota beta delta [f].