Ltacs.v 5.22 KB
Newer Older
1
(** Ltac definitions **)
2
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
3
Require Import Flover.Infra.RealSimps Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.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
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.

29
30
31
32
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
33
  | [ H: Qeq_bool ?a ?b = true |- _] => rewrite Qeq_bool_iff in H
34
35
36
37
38
  end.

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

46
47
48
49
50
51
52
53
54
55
56
57
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
58
Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
59
60
61
  match v with
  |Some val => f val
  | None => e
62
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
63
64

Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
65
  match v with |Some val => f val | None => e end = optionLift X Y v f e.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
66
Proof.
Heiko Becker's avatar
Heiko Becker committed
67
  reflexivity.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
68
69
70
Qed.

Lemma optionLift_cond X (a:bool) (b c :X):
71
  (if a then b else c) = match a with |true => b |false => c end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
72
Proof.
Heiko Becker's avatar
Heiko Becker committed
73
  reflexivity.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
74
75
76
77
78
79
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
80
Ltac match_factorize_asm :=
81
  match goal with
82
83
84
85
86
87
  | [ 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
88
89
  end.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
90
Ltac match_factorize :=
Heiko Becker's avatar
Heiko Becker committed
91
92
  match_factorize_asm ||
  match goal with
93
94
  | [ |- context [optionLift _ _ ?t _ _] ]
    => destruct t eqn:?; cbn; try congruence
95
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
96
97

Ltac pair_factorize :=
98
  match goal with
99
100
101
  | [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
  end.

102
103
104
105
106
107
108
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
109
110

Ltac match_simpl :=
111
112
113
114
  try remove_conds;
  try remove_matches;
  repeat match_factorize;
  try pair_factorize.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
115
116

Ltac bool_factorize :=
117
118
119
  match goal with
  | [H: _ = true |- _] => andb_to_prop H
  end.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
120

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

129
Ltac Flover_compute :=
Heiko Becker's avatar
Heiko Becker committed
130
131
132
133
134
135
  repeat (
      (try remove_conds;
      try remove_matches;
      repeat match_factorize;
      try pair_factorize) ||
      bool_factorize).
136

137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
(* 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 *)
155
156
(*   | H: context [optionLift (FloverMap.find ?k ?M) _ _] |- _ => *)
(*     destruct (FloverMap.find (elt:=intv * error) k M); idtac H *)
157
(*   end. *)
158
159
160
161

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
162
  end.
Heiko Becker's avatar
Heiko Becker committed
163
164
165
166
167
168
169
170

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.
171
172
173
174
175
176
177
178
179
180
181
182

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.

Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.