blob: 901cfde88cc13c1b6098d942786109b62d07d8a0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
Require Import Coq.omega.Omega.
Require Import Coq.ZArith.BinInt.
Ltac rewrite_min_max_side_condition_t := omega.
Ltac revert_min_max :=
repeat match goal with
| [ H : context[Z.min _ _] |- _ ] => revert H
| [ H : context[Z.max _ _] |- _ ] => revert H
end.
Ltac rewrite_min_max_step_fast :=
match goal with
| [ H : (?a <= ?b)%Z |- context[Z.max ?a ?b] ]
=> rewrite (Z.max_r a b) by assumption
| [ H : (?b <= ?a)%Z |- context[Z.max ?a ?b] ]
=> rewrite (Z.max_l a b) by assumption
| [ H : (?a <= ?b)%Z |- context[Z.min ?a ?b] ]
=> rewrite (Z.min_l a b) by assumption
| [ H : (?b <= ?a)%Z |- context[Z.min ?a ?b] ]
=> rewrite (Z.min_r a b) by assumption
end.
Ltac rewrite_min_max_step :=
match goal with
| _ => rewrite_min_max_step_fast
| [ |- context[Z.max ?a ?b] ]
=> first [ rewrite (Z.max_l a b) by rewrite_min_max_side_condition_t
| rewrite (Z.max_r a b) by rewrite_min_max_side_condition_t ]
| [ |- context[Z.min ?a ?b] ]
=> first [ rewrite (Z.min_l a b) by rewrite_min_max_side_condition_t
| rewrite (Z.min_r a b) by rewrite_min_max_side_condition_t ]
end.
Ltac only_split_min_max_step :=
match goal with
| _ => revert_min_max; progress repeat apply Z.min_case_strong; intros
| _ => revert_min_max; progress repeat apply Z.max_case_strong; intros
end.
Ltac split_min_max_step :=
match goal with
| _ => rewrite_min_max_step
| _ => only_split_min_max_step
end.
Ltac split_min_max := repeat split_min_max_step.
|
