numpairScript.sml

1Theory numpair[bare]
2Ancestors
3  arithmetic
4Libs
5  HolKernel boolLib Parse BasicProvers TotalDefn numSimps numLib
6  simpLib metisLib
7
8fun fs ths = FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) ths
9fun simp ths = ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) ths
10val metis_tac = METIS_TAC
11
12(* ----------------------------------------------------------------------
13    Triangular numbers
14   ---------------------------------------------------------------------- *)
15
16Definition tri_def[nocompute,simp]:
17  (tri 0 = 0) /\
18  (tri (SUC n) = SUC n + tri n)
19End
20
21Theorem twotri_formula:
22    2 * tri n = n * (n + 1)
23Proof
24  Induct_on `n` THEN
25  SRW_TAC [ARITH_ss][tri_def, MULT_CLAUSES, LEFT_ADD_DISTRIB]
26QED
27
28Theorem tri_formula[compute]:
29  tri n = (n * (n + 1)) DIV 2
30Proof
31  ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC DIV_UNIQUE THEN
32  Q.EXISTS_TAC `0` THEN SRW_TAC [ARITH_ss][twotri_formula]
33QED
34
35Theorem tri_eq_0[simp]:
36  ((tri n = 0) <=> (n = 0)) /\ ((0 = tri n) <=> (n = 0))
37Proof
38  Cases_on `n` THEN SRW_TAC [ARITH_ss][tri_def]
39QED
40
41val DECIDE_TAC = SRW_TAC [ARITH_ss][]
42Theorem tri_LT_I:
43    !n m. n < m ==> tri n < tri m
44Proof
45  Induct THEN Cases_on `m` THEN SRW_TAC [ARITH_ss][tri_def] THEN
46  RES_TAC THEN DECIDE_TAC
47QED
48
49Theorem tri_LT[simp]:
50  !n m. tri n < tri m <=> n < m
51Proof
52  SRW_TAC [][EQ_IMP_THM, tri_LT_I] THEN
53  SPOSE_NOT_THEN ASSUME_TAC THEN
54  `(n = m) \/ m < n` by DECIDE_TAC THEN1 FULL_SIMP_TAC (srw_ss()) [] THEN
55  METIS_TAC [prim_recTheory.LESS_REFL, tri_LT_I, LESS_TRANS]
56QED
57
58Theorem tri_11[simp]:
59  !m n. (tri m = tri n) <=> (m = n)
60Proof
61  SRW_TAC [][EQ_IMP_THM] THEN
62  `m < n \/ n < m \/ (m = n)` by DECIDE_TAC THEN
63  METIS_TAC [tri_LT_I, prim_recTheory.LESS_REFL]
64QED
65
66Theorem tri_LE[simp]:
67  !m n. tri m <= tri n <=> m <= n
68Proof
69  SRW_TAC [][LESS_OR_EQ]
70QED
71
72Definition invtri0_def:
73  invtri0 n a = if n < a + 1 then (n,a)
74                else invtri0 (n - (a + 1)) (a + 1)
75End
76
77Definition invtri_def:  invtri n = SND (invtri0 n 0)
78End
79val _ = Unicode.unicode_version {tmnm = "invtri",
80                                 u = "tri"^UnicodeChars.sup_minus^
81                                     UnicodeChars.sup_1}
82
83Theorem invtri0_thm:
84    !n a. tri (SND (invtri0 n a)) + FST (invtri0 n a) = n + tri a
85Proof
86  HO_MATCH_MP_TAC (theorem "invtri0_ind") THEN SRW_TAC [][] THEN
87  Cases_on `n < a + 1` THEN
88  ONCE_REWRITE_TAC [invtri0_def] THEN SRW_TAC [ARITH_ss][] THEN
89  SRW_TAC [ARITH_ss][GSYM ADD1, tri_def]
90QED
91
92Theorem SND_invtri0:
93    !n a. FST (invtri0 n a) < SUC (SND (invtri0 n a))
94Proof
95  HO_MATCH_MP_TAC (theorem "invtri0_ind") THEN SRW_TAC [][] THEN
96  Cases_on `n < a + 1` THEN ONCE_REWRITE_TAC [invtri0_def] THEN
97  SRW_TAC [ARITH_ss][]
98QED
99
100Theorem invtri_lower:
101    tri (invtri n) <= n
102Proof
103  SRW_TAC [][invtri_def] THEN
104  Q.SPECL_THEN [`n`, `0`] MP_TAC invtri0_thm THEN
105  SRW_TAC [ARITH_ss][tri_def]
106QED
107
108Theorem invtri_upper:
109    n < tri (invtri n + 1)
110Proof
111  SRW_TAC [][invtri_def, GSYM ADD1, tri_def] THEN
112  Q.SPECL_THEN [`n`, `0`] MP_TAC invtri0_thm THEN
113  Q.SPECL_THEN [`n`, `0`] MP_TAC SND_invtri0 THEN
114  SRW_TAC [ARITH_ss][tri_def]
115QED
116
117Theorem invtri_linverse[simp]:
118  invtri (tri n) = n
119Proof
120  MAP_EVERY (MP_TAC o Q.INST [`n` |-> `tri n`])
121            [invtri_upper, invtri_lower] THEN
122  SRW_TAC [ARITH_ss][]
123QED
124
125Theorem invtri_unique:
126    tri y <= n /\ n < tri (y + 1) ==> (invtri n = y)
127Proof
128  STRIP_TAC THEN MAP_EVERY ASSUME_TAC [invtri_lower, invtri_upper] THEN
129  `invtri n < y \/ (invtri n = y) \/ y < invtri n` by DECIDE_TAC THENL [
130     `invtri n + 1 <= y` by DECIDE_TAC THEN
131     `tri (invtri n + 1) <= tri y` by SRW_TAC [][] THEN
132     DECIDE_TAC,
133     `y + 1 <= invtri n` by DECIDE_TAC THEN
134     `tri (y + 1) <= tri (invtri n)` by SRW_TAC [][] THEN
135     DECIDE_TAC
136  ]
137QED
138
139Theorem invtri_linverse_r:
140    y <= x ==> (invtri (tri x + y) = x)
141Proof
142  STRIP_TAC THEN MATCH_MP_TAC invtri_unique THEN
143  SRW_TAC [ARITH_ss][GSYM ADD1, tri_def]
144QED
145
146Theorem tri_le:
147    n <= tri n
148Proof
149  Induct_on `n` THEN SRW_TAC [][tri_def]
150QED
151
152Theorem invtri_le:
153    invtri n <= n
154Proof
155  Q_TAC SUFF_TAC `tri (invtri n) <= tri n` THEN1 SRW_TAC [][] THEN
156  METIS_TAC [tri_le, invtri_lower, arithmeticTheory.LESS_EQ_TRANS]
157QED
158
159
160
161
162
163(* ----------------------------------------------------------------------
164    Numeric pair, fst and snd -- Cantor's encoding
165   ---------------------------------------------------------------------- *)
166
167Definition npair_def:
168  npair m n = tri (m + n) + n
169End
170
171val _ = set_fixity "*," (Infixr 601)
172val _ = Unicode.unicode_version {tmnm = "*,", u = UTF8.chr 0x2297 (* \otimes *)}
173Overload "*," = ``npair``
174val _ = TeX_notation {TeX = ("\\ensuremath{\\otimes}", 1), hol = "*,"}
175val _ = TeX_notation {TeX = ("\\ensuremath{\\otimes}", 1),
176                      hol = UTF8.chr 0x2297}
177
178
179Definition nfst_def:
180  nfst n = tri (invtri n) + invtri n - n
181End
182
183Definition nsnd_def:
184  nsnd n = n - tri (invtri n)
185End
186
187Theorem nfst_npair[simp]:
188  nfst (x *, y) = x
189Proof
190  SRW_TAC [][nfst_def, npair_def] THEN
191  SRW_TAC [ARITH_ss][invtri_linverse_r]
192QED
193
194Theorem nsnd_npair[simp]:
195  nsnd (x *, y) = y
196Proof
197  SRW_TAC [][nsnd_def, npair_def] THEN
198  SRW_TAC [ARITH_ss][invtri_linverse_r]
199QED
200
201Theorem npair_cases:
202    !n. ?x y. n = (x *, y)
203Proof
204  STRIP_TAC THEN MAP_EVERY Q.EXISTS_TAC [`nfst n`, `nsnd n`] THEN
205  SRW_TAC [][nsnd_def, nfst_def, npair_def] THEN
206  `n <= tri (invtri n) + invtri n`
207     by (ASSUME_TAC invtri_upper THEN
208         FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [GSYM ADD1, tri_def]) THEN
209  ASSUME_TAC invtri_lower THEN
210  ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) []
211QED
212
213Theorem npair[simp]:
214  !n. (nfst n *, nsnd n) = n
215Proof
216  STRIP_TAC THEN Q.SPEC_THEN `n` STRUCT_CASES_TAC npair_cases THEN
217  SRW_TAC [][]
218QED
219
220Theorem npair_11[simp]:
221  (x1 *, y1 = x2 *, y2) <=> (x1 = x2) /\ (y1 = y2)
222Proof
223  SRW_TAC [][EQ_IMP_THM] THENL [
224    POP_ASSUM (MP_TAC o Q.AP_TERM `nfst`) THEN SRW_TAC [][],
225    POP_ASSUM (MP_TAC o Q.AP_TERM `nsnd`) THEN SRW_TAC [][]
226  ]
227QED
228
229Theorem nfst_le:
230    nfst n <= n
231Proof
232  SRW_TAC [][nfst_def] THEN
233  MAP_EVERY ASSUME_TAC [invtri_lower, invtri_le] THEN
234  DECIDE_TAC
235QED
236Theorem nsnd_le:   nsnd n <= n
237Proof SRW_TAC [][nsnd_def]
238QED
239
240Theorem npair00[simp]:
241  npair 0 0 = 0
242Proof
243  SIMP_TAC (srw_ss()) [npair_def]
244QED
245
246Theorem npair_EQ_0[simp]:
247  !x y. (npair x y = 0) <=> (x = 0) /\ (y = 0)
248Proof
249  METIS_TAC[npair00,npair_11]
250QED
251
252Theorem nfst0[simp]:
253  nfst 0 = 0
254Proof
255  METIS_TAC[nfst_npair, npair00, npair_11]
256QED
257
258Theorem nsnd0[simp]:
259  nsnd 0 = 0
260Proof
261  METIS_TAC[nsnd_npair, npair00, npair_11]
262QED
263
264Theorem nfst_le_npair[simp]:
265  !m n. n <= npair n m
266Proof
267  rpt gen_tac \\
268  `n = nfst (npair n m)` by simp[GSYM nfst_npair] >>
269  `nfst (npair n m) <= npair n m` by simp[nfst_le] >> fs[]
270QED
271
272Theorem nsnd_le_npair[simp]:
273  !m n. m <= npair n m
274Proof
275  rpt gen_tac \\
276  `m = nsnd (npair n m)` by simp[GSYM nsnd_npair] >>
277  `nsnd (npair n m) <= npair n m` by simp[nsnd_le] >> fs[]
278QED
279
280Theorem npair2_lt_E:
281  !n n1 n2. npair n n1 < npair n n2 ==> n1 < n2
282Proof
283  rpt gen_tac
284  >> simp[npair_def] >> strip_tac >> SPOSE_NOT_THEN ASSUME_TAC
285  >> `n1 >= n2` by simp[]
286  >> `n + n1 >= n + n2` by simp[]
287  >> `n + n2 <= n + n1` by simp[]
288  >> `tri (n + n2) <= tri (n + n1)` by metis_tac[tri_LE]
289  >> `n2 <= n1` by simp[]
290  >> `n2 + tri (n + n2) <= n1 + tri (n + n1)` by simp[]
291  >> fs[]
292QED
293
294Theorem npair2_lt_I:
295  !n n1 n2. n1 < n2 ==> npair n n1 < npair n n2
296Proof
297  rpt strip_tac >> simp[npair_def] >>
298  `n + n1 < n + n2` by simp[] >>
299  `tri (n + n1) < tri (n + n2)` by simp[tri_LT] >> simp[]
300QED
301
302Theorem npair2_lt[simp]:
303  !n n1 n2. npair n n1 < npair n n2 <=> n1 < n2
304Proof
305  metis_tac[npair2_lt_E, npair2_lt_I]
306QED
307
308(* slightly more general than npair2_lt_I *)
309Theorem npairs_lt_I :
310  !a b c d. a <= b /\ c < d ==> npair a c < npair b d
311Proof
312    rpt STRIP_TAC
313 >> `(a = b) \/ a < b` by SRW_TAC [ARITH_ss] []
314 >- (ASM_REWRITE_TAC [] \\
315     MATCH_MP_TAC npair2_lt_I >> simp [])
316 >> MATCH_MP_TAC LESS_TRANS
317 >> Q.EXISTS_TAC ‘npair a d’
318 >> CONJ_TAC >- (MATCH_MP_TAC npair2_lt_I >> ASM_REWRITE_TAC [])
319 >> REWRITE_TAC [npair_def]
320 >> Q_TAC SUFF_TAC `tri (a + d) < tri (b + d)`
321 >- SRW_TAC [ARITH_ss] []
322 >> MATCH_MP_TAC tri_LT_I
323 >> SRW_TAC [ARITH_ss] []
324QED