Ltacs.v 3.62 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 58 59 60 61 62 63 64 65 66 67 68 69 70 71
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.
  cbv; auto.
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.
  cbv; auto.
Qed.

Ltac remove_matches := rewrite optionLift_eq in *.

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

Ltac match_factorize :=
72
  match goal with
73 74 75 76 77 78 79 80
  | [ 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
  | [ |- context [optionLift _ _ ?t _ _] ]
    => destruct t eqn:?; cbn; try congruence
81 82
  end.

83
Ltac pair_factorize :=
84
  match goal with
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
  | [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
  end.

Ltac match_simpl :=
  try remove_conds;
  try remove_matches;
  repeat match_factorize;
  try pair_factorize.

(* 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. *)
115 116 117 118 119

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