blob: df6eae383ded2c873d7f34ebc8be074d28e2cf5c (
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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.Bool.
Local Open Scope Z_scope.
Module Z.
Lemma eqb_cases x y : if x =? y then x = y else x <> y.
Proof.
pose proof (Z.eqb_spec x y) as H.
inversion H; trivial.
Qed.
Lemma geb_spec0 : forall x y : Z, Bool.reflect (x >= y) (x >=? y).
Proof.
intros x y; pose proof (Zge_cases x y) as H; destruct (Z.geb x y); constructor; omega.
Qed.
Lemma gtb_spec0 : forall x y : Z, Bool.reflect (x > y) (x >? y).
Proof.
intros x y; pose proof (Zgt_cases x y) as H; destruct (Z.gtb x y); constructor; omega.
Qed.
Ltac ltb_to_lt_with_hyp H lem :=
let H' := fresh in
rename H into H';
pose proof lem as H;
rewrite H' in H;
clear H'.
Ltac ltb_to_lt_in_goal b' lem :=
refine (proj1 (@reflect_iff_gen _ _ lem b') _);
cbv beta iota.
Ltac ltb_to_lt_hyps_step :=
match goal with
| [ H : (?x <? ?y) = ?b |- _ ]
=> ltb_to_lt_with_hyp H (Zlt_cases x y)
| [ H : (?x <=? ?y) = ?b |- _ ]
=> ltb_to_lt_with_hyp H (Zle_cases x y)
| [ H : (?x >? ?y) = ?b |- _ ]
=> ltb_to_lt_with_hyp H (Zgt_cases x y)
| [ H : (?x >=? ?y) = ?b |- _ ]
=> ltb_to_lt_with_hyp H (Zge_cases x y)
| [ H : (?x =? ?y) = ?b |- _ ]
=> ltb_to_lt_with_hyp H (eqb_cases x y)
end.
Ltac ltb_to_lt_goal_step :=
match goal with
| [ |- (?x <? ?y) = ?b ]
=> ltb_to_lt_in_goal b (Z.ltb_spec0 x y)
| [ |- (?x <=? ?y) = ?b ]
=> ltb_to_lt_in_goal b (Z.leb_spec0 x y)
| [ |- (?x >? ?y) = ?b ]
=> ltb_to_lt_in_goal b (Z.gtb_spec0 x y)
| [ |- (?x >=? ?y) = ?b ]
=> ltb_to_lt_in_goal b (Z.geb_spec0 x y)
| [ |- (?x =? ?y) = ?b ]
=> ltb_to_lt_in_goal b (Z.eqb_spec x y)
end.
Ltac ltb_to_lt_step :=
first [ ltb_to_lt_hyps_step
| ltb_to_lt_goal_step ].
Ltac ltb_to_lt := repeat ltb_to_lt_step.
Section R_Rb.
Local Ltac t := intros ? ? []; split; intro; ltb_to_lt; omega.
Local Notation R_Rb Rb R nR := (forall x y b, Rb x y = b <-> if b then R x y else nR x y).
Lemma ltb_lt_iff : R_Rb Z.ltb Z.lt Z.ge. Proof. t. Qed.
Lemma leb_le_iff : R_Rb Z.leb Z.le Z.gt. Proof. t. Qed.
Lemma gtb_gt_iff : R_Rb Z.gtb Z.gt Z.le. Proof. t. Qed.
Lemma geb_ge_iff : R_Rb Z.geb Z.ge Z.lt. Proof. t. Qed.
Lemma eqb_eq_iff : R_Rb Z.eqb (@Logic.eq Z) (fun x y => x <> y). Proof. t. Qed.
End R_Rb.
Hint Rewrite ltb_lt_iff leb_le_iff gtb_gt_iff geb_ge_iff eqb_eq_iff : ltb_to_lt.
Ltac ltb_to_lt_in_context :=
repeat autorewrite with ltb_to_lt in *;
cbv beta iota in *.
End Z.
|
