blob: 27845898aa28f56656fd231c81359b5662b0213d (
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
77
78
79
80
81
82
83
84
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
Require Import ZArith.
Require Import Int63.
Require Import ZifyBool.
Import ZifyClasses.
Lemma to_Z_bounded : forall x, (0 <= to_Z x < 9223372036854775808)%Z.
Proof. apply to_Z_bounded. Qed.
Instance Inj_int_Z : InjTyp int Z :=
mkinj _ _ to_Z (fun x => 0 <= x < 9223372036854775808)%Z to_Z_bounded.
Add Zify InjTyp Inj_int_Z.
Instance Op_max_int : CstOp max_int :=
{ TCst := 9223372036854775807 ; TCstInj := eq_refl }.
Add Zify CstOp Op_max_int.
Instance Op_digits : CstOp digits :=
{ TCst := 63 ; TCstInj := eq_refl }.
Add Zify CstOp Op_digits.
Instance Op_size : CstOp size :=
{ TCst := 63 ; TCstInj := eq_refl }.
Add Zify CstOp Op_size.
Instance Op_wB : CstOp wB :=
{ TCst := 2^63 ; TCstInj := eq_refl }.
Add Zify CstOp Op_wB.
Lemma ltb_lt : forall n m,
(n <? m)%int63 = (φ (n)%int63 <? φ (m)%int63)%Z.
Proof.
intros. apply Bool.eq_true_iff_eq.
rewrite ltb_spec. rewrite <- Z.ltb_lt.
apply iff_refl.
Qed.
Instance Op_ltb : BinOp ltb :=
{| TBOp := Z.ltb; TBOpInj := ltb_lt |}.
Add Zify BinOp Op_ltb.
Lemma leb_le : forall n m,
(n <=? m)%int63 = (φ (n)%int63 <=? φ (m)%int63)%Z.
Proof.
intros. apply Bool.eq_true_iff_eq.
rewrite leb_spec. rewrite <- Z.leb_le.
apply iff_refl.
Qed.
Instance Op_leb : BinOp leb :=
{| TBOp := Z.leb; TBOpInj := leb_le |}.
Add Zify BinOp Op_leb.
Lemma eqb_eq : forall n m,
(n =? m)%int63 = (φ (n)%int63 =? φ (m)%int63)%Z.
Proof.
intros. apply Bool.eq_true_iff_eq.
rewrite eqb_spec. rewrite Z.eqb_eq.
split ; intro H.
now subst; reflexivity.
now apply to_Z_inj in H.
Qed.
Instance Op_eqb : BinOp eqb :=
{| TBOp := Z.eqb; TBOpInj := eqb_eq |}.
Add Zify BinOp Op_eqb.
Lemma eq_int_inj : forall n m : int, n = m <-> (φ n = φ m)%int63.
Proof.
split; intro H.
rewrite H ; reflexivity.
apply to_Z_inj; auto.
Qed.
Instance Op_eq : BinRel (@eq int) :=
{| TR := @eq Z; TRInj := eq_int_inj |}.
Add Zify BinRel Op_eq.
Instance Op_add : BinOp add :=
{| TBOp := fun x y => (x + y) mod 9223372036854775808%Z; TBOpInj := add_spec |}%Z.
Add Zify BinOp Op_add.
Instance Op_sub : BinOp sub :=
{| TBOp := fun x y => (x - y) mod 9223372036854775808%Z; TBOpInj := sub_spec |}%Z.
Add Zify BinOp Op_sub.
Instance Op_opp : UnOp Int63.opp :=
{| TUOp := (fun x => (- x) mod 9223372036854775808)%Z; TUOpInj := (sub_spec 0) |}%Z.
Add Zify UnOp Op_opp.
Instance Op_oppcarry : UnOp oppcarry :=
{| TUOp := (fun x => 2^63 - x - 1)%Z; TUOpInj := oppcarry_spec |}%Z.
Add Zify UnOp Op_oppcarry.
Instance Op_succ : UnOp succ :=
{| TUOp := (fun x => (x + 1) mod 2^63)%Z; TUOpInj := succ_spec |}%Z.
Add Zify UnOp Op_succ.
Instance Op_pred : UnOp Int63.pred :=
{| TUOp := (fun x => (x - 1) mod 2^63)%Z; TUOpInj := pred_spec |}%Z.
Add Zify UnOp Op_pred.
Instance Op_mul : BinOp mul :=
{| TBOp := fun x y => (x * y) mod 9223372036854775808%Z; TBOpInj := mul_spec |}%Z.
Add Zify BinOp Op_mul.
Instance Op_gcd : BinOp gcd:=
{| TBOp := (fun x y => Zgcd_alt.Zgcdn (2 * 63)%nat y x) ; TBOpInj := to_Z_gcd |}.
Add Zify BinOp Op_gcd.
Instance Op_mod : BinOp Int63.mod :=
{| TBOp := Z.modulo ; TBOpInj := mod_spec |}.
Add Zify BinOp Op_mod.
Instance Op_subcarry : BinOp subcarry :=
{| TBOp := (fun x y => (x - y - 1) mod 2^63)%Z ; TBOpInj := subcarry_spec |}.
Add Zify BinOp Op_subcarry.
Instance Op_addcarry : BinOp addcarry :=
{| TBOp := (fun x y => (x + y + 1) mod 2^63)%Z ; TBOpInj := addcarry_spec |}.
Add Zify BinOp Op_addcarry.
Instance Op_lsr : BinOp lsr :=
{| TBOp := (fun x y => x / 2^ y)%Z ; TBOpInj := lsr_spec |}.
Add Zify BinOp Op_lsr.
Instance Op_lsl : BinOp lsl :=
{| TBOp := (fun x y => (x * 2^ y) mod 2^ 63)%Z ; TBOpInj := lsl_spec |}.
Add Zify BinOp Op_lsl.
Instance Op_lor : BinOp Int63.lor :=
{| TBOp := Z.lor ; TBOpInj := lor_spec' |}.
Add Zify BinOp Op_lor.
Instance Op_land : BinOp Int63.land :=
{| TBOp := Z.land ; TBOpInj := land_spec' |}.
Add Zify BinOp Op_land.
Instance Op_lxor : BinOp Int63.lxor :=
{| TBOp := Z.lxor ; TBOpInj := lxor_spec' |}.
Add Zify BinOp Op_lxor.
Instance Op_div : BinOp div :=
{| TBOp := Z.div ; TBOpInj := div_spec |}.
Add Zify BinOp Op_div.
Instance Op_bit : BinOp bit :=
{| TBOp := Z.testbit ; TBOpInj := bitE |}.
Add Zify BinOp Op_bit.
Instance Op_of_Z : UnOp of_Z :=
{ TUOp := (fun x => x mod 9223372036854775808)%Z; TUOpInj := of_Z_spec }.
Add Zify UnOp Op_of_Z.
Instance Op_to_Z : UnOp to_Z :=
{ TUOp := fun x => x ; TUOpInj := fun x : int => eq_refl }.
Add Zify UnOp Op_to_Z.
Instance Op_is_zero : UnOp is_zero :=
{ TUOp := (Z.eqb 0) ; TUOpInj := is_zeroE }.
Add Zify UnOp Op_is_zero.
Lemma is_evenE : forall x,
is_even x = Z.even φ (x)%int63.
Proof.
intros.
generalize (is_even_spec x).
rewrite Z_evenE.
destruct (is_even x).
symmetry. apply Z.eqb_eq. auto.
symmetry. apply Z.eqb_neq. congruence.
Qed.
Instance Op_is_even : UnOp is_even :=
{ TUOp := Z.even ; TUOpInj := is_evenE }.
Add Zify UnOp Op_is_even.
Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).
|
