1 | open Preamble |
---|
2 | |
---|
3 | open Types |
---|
4 | |
---|
5 | open Bool |
---|
6 | |
---|
7 | open Relations |
---|
8 | |
---|
9 | open Nat |
---|
10 | |
---|
11 | open Hints_declaration |
---|
12 | |
---|
13 | open Core_notation |
---|
14 | |
---|
15 | open Pts |
---|
16 | |
---|
17 | open Logic |
---|
18 | |
---|
19 | open Positive |
---|
20 | |
---|
21 | open Z |
---|
22 | |
---|
23 | type natp = |
---|
24 | | Pzero |
---|
25 | | Ppos of Positive.pos |
---|
26 | |
---|
27 | (** val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **) |
---|
28 | let rec natp_rect_Type4 h_pzero h_ppos = function |
---|
29 | | Pzero -> h_pzero |
---|
30 | | Ppos x_4901 -> h_ppos x_4901 |
---|
31 | |
---|
32 | (** val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **) |
---|
33 | let rec natp_rect_Type5 h_pzero h_ppos = function |
---|
34 | | Pzero -> h_pzero |
---|
35 | | Ppos x_4905 -> h_ppos x_4905 |
---|
36 | |
---|
37 | (** val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **) |
---|
38 | let rec natp_rect_Type3 h_pzero h_ppos = function |
---|
39 | | Pzero -> h_pzero |
---|
40 | | Ppos x_4909 -> h_ppos x_4909 |
---|
41 | |
---|
42 | (** val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **) |
---|
43 | let rec natp_rect_Type2 h_pzero h_ppos = function |
---|
44 | | Pzero -> h_pzero |
---|
45 | | Ppos x_4913 -> h_ppos x_4913 |
---|
46 | |
---|
47 | (** val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **) |
---|
48 | let rec natp_rect_Type1 h_pzero h_ppos = function |
---|
49 | | Pzero -> h_pzero |
---|
50 | | Ppos x_4917 -> h_ppos x_4917 |
---|
51 | |
---|
52 | (** val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **) |
---|
53 | let rec natp_rect_Type0 h_pzero h_ppos = function |
---|
54 | | Pzero -> h_pzero |
---|
55 | | Ppos x_4921 -> h_ppos x_4921 |
---|
56 | |
---|
57 | (** val natp_inv_rect_Type4 : |
---|
58 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
59 | let natp_inv_rect_Type4 hterm h1 h2 = |
---|
60 | let hcut = natp_rect_Type4 h1 h2 hterm in hcut __ |
---|
61 | |
---|
62 | (** val natp_inv_rect_Type3 : |
---|
63 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
64 | let natp_inv_rect_Type3 hterm h1 h2 = |
---|
65 | let hcut = natp_rect_Type3 h1 h2 hterm in hcut __ |
---|
66 | |
---|
67 | (** val natp_inv_rect_Type2 : |
---|
68 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
69 | let natp_inv_rect_Type2 hterm h1 h2 = |
---|
70 | let hcut = natp_rect_Type2 h1 h2 hterm in hcut __ |
---|
71 | |
---|
72 | (** val natp_inv_rect_Type1 : |
---|
73 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
74 | let natp_inv_rect_Type1 hterm h1 h2 = |
---|
75 | let hcut = natp_rect_Type1 h1 h2 hterm in hcut __ |
---|
76 | |
---|
77 | (** val natp_inv_rect_Type0 : |
---|
78 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **) |
---|
79 | let natp_inv_rect_Type0 hterm h1 h2 = |
---|
80 | let hcut = natp_rect_Type0 h1 h2 hterm in hcut __ |
---|
81 | |
---|
82 | (** val natp_discr : natp -> natp -> __ **) |
---|
83 | let natp_discr x y = |
---|
84 | Logic.eq_rect_Type2 x |
---|
85 | (match x with |
---|
86 | | Pzero -> Obj.magic (fun _ dH -> dH) |
---|
87 | | Ppos a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
88 | |
---|
89 | (** val natp0 : natp -> natp **) |
---|
90 | let natp0 = function |
---|
91 | | Pzero -> Pzero |
---|
92 | | Ppos m -> Ppos (Positive.P0 m) |
---|
93 | |
---|
94 | (** val natp1 : natp -> natp **) |
---|
95 | let natp1 = function |
---|
96 | | Pzero -> Ppos Positive.One |
---|
97 | | Ppos m -> Ppos (Positive.P1 m) |
---|
98 | |
---|
99 | (** val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod **) |
---|
100 | let rec divide m n = |
---|
101 | match m with |
---|
102 | | Positive.One -> |
---|
103 | (match n with |
---|
104 | | Positive.One -> { Types.fst = (Ppos Positive.One); Types.snd = Pzero } |
---|
105 | | Positive.P1 x -> |
---|
106 | { Types.fst = Pzero; Types.snd = (Ppos Positive.One) } |
---|
107 | | Positive.P0 x -> |
---|
108 | { Types.fst = Pzero; Types.snd = (Ppos Positive.One) }) |
---|
109 | | Positive.P1 m' -> |
---|
110 | let { Types.fst = q; Types.snd = r } = divide m' n in |
---|
111 | (match r with |
---|
112 | | Pzero -> |
---|
113 | (match n with |
---|
114 | | Positive.One -> { Types.fst = (natp1 q); Types.snd = Pzero } |
---|
115 | | Positive.P1 x -> |
---|
116 | { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) } |
---|
117 | | Positive.P0 x -> |
---|
118 | { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) }) |
---|
119 | | Ppos r' -> |
---|
120 | (match Positive.partial_minus (Positive.P1 r') n with |
---|
121 | | Positive.MinusNeg -> |
---|
122 | { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P1 r')) } |
---|
123 | | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero } |
---|
124 | | Positive.MinusPos r'' -> |
---|
125 | { Types.fst = (natp1 q); Types.snd = (Ppos r'') })) |
---|
126 | | Positive.P0 m' -> |
---|
127 | let { Types.fst = q; Types.snd = r } = divide m' n in |
---|
128 | (match r with |
---|
129 | | Pzero -> { Types.fst = (natp0 q); Types.snd = Pzero } |
---|
130 | | Ppos r' -> |
---|
131 | (match Positive.partial_minus (Positive.P0 r') n with |
---|
132 | | Positive.MinusNeg -> |
---|
133 | { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P0 r')) } |
---|
134 | | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero } |
---|
135 | | Positive.MinusPos r'' -> |
---|
136 | { Types.fst = (natp1 q); Types.snd = (Ppos r'') })) |
---|
137 | |
---|
138 | (** val div : Positive.pos -> Positive.pos -> natp **) |
---|
139 | let div m n = |
---|
140 | (divide m n).Types.fst |
---|
141 | |
---|
142 | (** val mod0 : Positive.pos -> Positive.pos -> natp **) |
---|
143 | let mod0 m n = |
---|
144 | (divide m n).Types.snd |
---|
145 | |
---|
146 | (** val natp_plus : natp -> natp -> natp **) |
---|
147 | let rec natp_plus n m = |
---|
148 | match n with |
---|
149 | | Pzero -> m |
---|
150 | | Ppos n' -> |
---|
151 | (match m with |
---|
152 | | Pzero -> n |
---|
153 | | Ppos m' -> Ppos (Positive.plus n' m')) |
---|
154 | |
---|
155 | (** val natp_times : natp -> natp -> natp **) |
---|
156 | let rec natp_times n m = |
---|
157 | match n with |
---|
158 | | Pzero -> Pzero |
---|
159 | | Ppos n' -> |
---|
160 | (match m with |
---|
161 | | Pzero -> Pzero |
---|
162 | | Ppos m' -> Ppos (Positive.times n' m')) |
---|
163 | |
---|
164 | (** val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum **) |
---|
165 | let dec_divides m n = |
---|
166 | Types.prod_rect_Type0 (fun dv md -> |
---|
167 | match md with |
---|
168 | | Pzero -> |
---|
169 | (match dv with |
---|
170 | | Pzero -> (fun _ -> Obj.magic natp_discr (Ppos n) Pzero __ __) |
---|
171 | | Ppos dv' -> (fun _ -> Types.Inl __)) |
---|
172 | | Ppos x -> |
---|
173 | (match dv with |
---|
174 | | Pzero -> (fun md' _ -> Types.Inr __) |
---|
175 | | Ppos md' -> (fun dv' _ -> Types.Inr __)) x) (divide n m) __ |
---|
176 | |
---|
177 | (** val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum **) |
---|
178 | let dec_dividesZ p q = |
---|
179 | match p with |
---|
180 | | Z.OZ -> |
---|
181 | (match q with |
---|
182 | | Z.OZ -> Types.Inr __ |
---|
183 | | Z.Pos m -> Types.Inr __ |
---|
184 | | Z.Neg m -> Types.Inr __) |
---|
185 | | Z.Pos n -> |
---|
186 | (match q with |
---|
187 | | Z.OZ -> Types.Inl __ |
---|
188 | | Z.Pos auto -> dec_divides n auto |
---|
189 | | Z.Neg auto -> dec_divides n auto) |
---|
190 | | Z.Neg n -> |
---|
191 | (match q with |
---|
192 | | Z.OZ -> Types.Inl __ |
---|
193 | | Z.Pos auto -> dec_divides n auto |
---|
194 | | Z.Neg auto -> dec_divides n auto) |
---|
195 | |
---|
196 | (** val natp_to_Z : natp -> Z.z **) |
---|
197 | let natp_to_Z = function |
---|
198 | | Pzero -> Z.OZ |
---|
199 | | Ppos p -> Z.Pos p |
---|
200 | |
---|
201 | (** val natp_to_negZ : natp -> Z.z **) |
---|
202 | let natp_to_negZ = function |
---|
203 | | Pzero -> Z.OZ |
---|
204 | | Ppos p -> Z.Neg p |
---|
205 | |
---|
206 | (** val divZ : Z.z -> Z.z -> Z.z **) |
---|
207 | let divZ x y = |
---|
208 | match x with |
---|
209 | | Z.OZ -> Z.OZ |
---|
210 | | Z.Pos n -> |
---|
211 | (match y with |
---|
212 | | Z.OZ -> Z.OZ |
---|
213 | | Z.Pos m -> natp_to_Z (divide n m).Types.fst |
---|
214 | | Z.Neg m -> |
---|
215 | let { Types.fst = q; Types.snd = r } = divide n m in |
---|
216 | (match r with |
---|
217 | | Pzero -> natp_to_negZ q |
---|
218 | | Ppos x0 -> Z.zpred (natp_to_negZ q))) |
---|
219 | | Z.Neg n -> |
---|
220 | (match y with |
---|
221 | | Z.OZ -> Z.OZ |
---|
222 | | Z.Pos m -> |
---|
223 | let { Types.fst = q; Types.snd = r } = divide n m in |
---|
224 | (match r with |
---|
225 | | Pzero -> natp_to_negZ q |
---|
226 | | Ppos x0 -> Z.zpred (natp_to_negZ q)) |
---|
227 | | Z.Neg m -> natp_to_Z (divide n m).Types.fst) |
---|
228 | |
---|
229 | (** val modZ : Z.z -> Z.z -> Z.z **) |
---|
230 | let modZ x y = |
---|
231 | match x with |
---|
232 | | Z.OZ -> Z.OZ |
---|
233 | | Z.Pos n -> |
---|
234 | (match y with |
---|
235 | | Z.OZ -> Z.OZ |
---|
236 | | Z.Pos m -> natp_to_Z (divide n m).Types.snd |
---|
237 | | Z.Neg m -> |
---|
238 | let { Types.fst = q; Types.snd = r } = divide n m in |
---|
239 | (match r with |
---|
240 | | Pzero -> Z.OZ |
---|
241 | | Ppos x0 -> Z.zplus y (natp_to_Z r))) |
---|
242 | | Z.Neg n -> |
---|
243 | (match y with |
---|
244 | | Z.OZ -> Z.OZ |
---|
245 | | Z.Pos m -> |
---|
246 | let { Types.fst = q; Types.snd = r } = divide n m in |
---|
247 | (match r with |
---|
248 | | Pzero -> Z.OZ |
---|
249 | | Ppos x0 -> Z.zminus y (natp_to_Z r)) |
---|
250 | | Z.Neg m -> natp_to_Z (divide n m).Types.snd) |
---|
251 | |
---|