/
qoc_jisuanji_environmental_parametrized_module.html
492 lines (376 loc) · 16.4 KB
/
qoc_jisuanji_environmental_parametrized_module.html
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
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
<!--
This sample contains two very simple introductory exercises of
interactive proofs in Coq, one with natural numbers and one with lists.
It can be used as a gentle landing page, which requires no knowledge
of math-comp.
-->
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<meta name="description" content="An Online IDE for the Coq Theorem Prover" />
<title>Use Coq in Your Browser: The Js Coq Theorem Prover Online IDE!</title>
</head>
<body>
<div id="ide-wrapper" class="toggled">
<div id="code-wrapper">
<div id="document">
<p>
+ Thursday, Apriil 4, 2019, 20:20:00
<br/> OOO1337777 , COQ , 鸡算计 , mathematics , 数学 - environmental parametrized module 1 - 环境的 参数化了 包裹 1
<br/> https://www.bilibili.com/video/av48293615/
</p>
<p>
+ Friday, April 5, 2019, 22:22:00
<br/> OOO1337777 , COQ , 鸡算计 , mathematics , 数学 - environmental parametrized module 2 - 环境的 参数化了 包裹 2
<br/> https://www.bilibili.com/video/av48424625/
</p>
<p>
+ Friday, April 5, 2019, 22:44:00
<br/> OOO1337777 , COQ , 鸡算计 , mathematics , 数学 - environmental parametrized module 3 - 环境的 参数化了 包裹 3
<br/> https://www.bilibili.com/video/av48426398/
</p>
<p>
Alt+↑/↓ – move through proof; Alt+→ or Alt+⏎ – go to cursor. <br/>
Alt+hover executed sentences to watch intermediate steps. <br/>
Hover identifiers in goals to view their types. Alt+hover to view definitions.<br/>
<i style="color: rgb(51, 51, 150)">Company-coq</i> addon is enabled: it will auto-complete names of tactics and lemmas
from the standard library, and also show types of lemmas in the right pane.
</p>
<p>
“Alt +↑/↓” : 通过证明。 “Alt +→”或“Alt +⏎” : 转到光标。
<br/> “Alt +”悬停执行句子以观察中间步骤。
<br/> 将目标中的标识符悬停在其中以查看其类型。 “Alt +”悬停以查看定义。
<br/> 启用“Company-coq”加载项：它将自动完成标准库中的策略和引理名称，并在右侧窗格中显示引导类型。
</p>
<textarea id="workspace">
From Qoc Require Import Jisuanji .
(**MEMO:
短 :: 一些参数“p”参数化许多定义和引理“d”和“l”都可以打包成一个;然后可以实例化该参数“p”以产生实例化的定义和引理：“Q.d”和“Q.l”，其新名称以任何选择的前缀名称“Q”作为前缀 ...
Short :: some parameter "p" which parametrizes many definitions and lemmas "d" and "l" may all be packaged into one ; and then later this parameter "p" may be instantiated to produce the instantiated definitions and lemmas : "Q.d" and "Q.l" whose new names are prefixed by any chosen prefix name "Q" ...
Outline ::
* PART 1 : SIMPLE PARAMETRIZATION
* PART 2 : SIMPLE ENVIRONMENT
* PART 3 : COMPLEX ENVIRONMENTAL PARAMETRIZATION
*)
(** PART 1 : SIMPLE PARAMETRIZATION *)
模块 p_dl.
(** Bāoguǒ p_dl. *)
参数 p : 类型 .
(** Cānshù p: Lèixíng. *)
定义 d := prod p p .
(** Dìngyì d:= Prod p p. *)
定义 l : p -> d .
(** Dìngyì l: P -> d. *)
证明.
(** Zhèngmíng.*)
移动外 x.
(** Jièshàomen x. *)
确切 (pair x x).
(** Quèqiè (pair x x). *)
定义了.
(** Dìngyìle. *)
结束 p_dl.
(** Jiéshù p_dl. *)
模块 词头了 参数 nat_dl : p_dl 跟 定义 p := nat.
(** Bāoguǒ cítóule cānshù nat_dl: P_dl gēn dìngyì p:= Nat. *)
打印 nat_dl.l.
(** Dǎyìn nat_dl.L. *)
计算 (nat_dl.l 3).
(** Jìsuàn (nat_dl.L 3). *)
模块 词头了 参数 bool_dl : 让 定义 p := bool 在 p_dl .
(** Bāoguǒ cítóule cānshù bool_dl: Ràng dìngyì p:= Bool zài p_dl. *)
计算 (bool_dl.l false).
(** Jìsuàn (bool_dl.L false). *)
模块 词头了 别号 NN := nat_dl .
(** Bāoguǒ cítóule bié hào NN:= Nat_dl. *)
打印 NN.l.
(** Dǎyìn NN.L. *)
(** ---------------------------------------------------- *)
Reset p_dl .
Modular p_dl.
Parameter p : Type .
Definition d := prod p p .
Definition l : p -> d .
Proof.
intros x.
exact (pair x x).
Defined.
End p_dl.
Modular Prefixed Parameter nat_dl : (p_dl with Definition p := nat).
Print nat_dl.l.
Compute (nat_dl.l 3).
Modular Prefixed Parameter bool_dl : (let Definition p := bool in p_dl).
Compute (bool_dl.l false).
Modular Prefixed Alias NN := nat_dl .
Print NN.l.
(** --------------------------------------------- *)
(** PART 2 : SIMPLE ENVIRONMENT *)
(** This does not lack to touch/call the Coq file [goptions.ml] ;
it is hardcoded into the grammar *)
Print Table Implicit Arguments .
Set Implicit Arguments .
设置 隐含 键入 .
打印 表格 隐含 键入 .
未设置 隐含 键入.
打印 表格 隐含 键入.
Print Table Printing Let.
Add Printing Let prod.
加 打印 让 prod.
Print Table Printing Notations.
设置 打印 符号 .
未设置 打印 符号 .
打印 表格 Ssr识别号 .
Reset p_dl .
(** --------------------------------------------- *)
(** PART 3 : COMPLEX ENVIRONMENTAL PARAMETRIZATION *)
(** Module without parameters . This is precisely for the prefix [M] below .*)
模块 MOD_T'nat_x'0_y'true.
定义 T := nat.
定义 x := 0.
定义 y : bool.
证明.
确切 true.
定义了.
结束 MOD_T'nat_x'0_y'true.
模块 词头了 参数 M : MOD_T'nat_x'0_y'true .
(** Module with 2 inner-parameters and with some environment which is enabled . *)
模块 MOD_T_x.
参数 T : Set.
(** [Export] keyword says that this environment will be imported when this module is imported . *)
出口 设置 打印 符号.
符号 _carrier := T.
(** [本地] keyword says this identifier will never be imported .
[将展开] keyword says that this component of any prefixed-module input
will be unfolded in the output module during any outer/functor instantiation/application *)
本地 参数 将展开 x : T.
结束 MOD_T_x.
(** Module instantiated and prefixed by the name [B] . *)
模块 词头了 参数 B : (MOD_T_x 跟 定义 T := bool).
(** Another different instantiation . Module instantiated and prefixed by the name [N] . *)
模块 词头了 参数 N : (MOD_T_x 跟 定义 T := nat) .
打印 N.T.
打印 N.x.
(** No more instantiation of [M] is possible. Oneself can only alias (here rename) , then check the precision . *)
模块 词头了 别号 M' <: (MOD_T_x 跟 定义 T := nat) := M .
模块 MOD_z (M'' : MOD_T'nat_x'0_y'true).
定义 z : nat := 1 + M''.x .
结束 MOD_z.
(** Another form of the command to (anonymously) present the module components and to prefix the module at the same time (and also to check the precision). *)
模块 词头了 别号 M_z <: (MOD_T_x 跟 定义 T := nat).
包括 M.
Fail 定义 x := 1 .
(** may be bad *)
定义 z : nat := 1 + M.x . 打印 z.
Reset z.
包括 (MOD_z M). 打印 z.
Reset z.
定义 z : nat := 1 + x . 打印 z.
Reset z.
包括 MOD_z. 打印 z.
结束 M_z.
打印 M_z.T.
打印 M_z.x.
(** Module with one outer-parameter [X]] . This module has also one inner-parameter [Y] , which will also be component of the result *)
模块 MODPARAMS (X : MOD_T_x) <: MOD_T_x .
模块 词头了 参数 Y : (MOD_T_x 跟 定义 T := X.T) .
打印 X.x.
打印 Y.x.
Fail 打印 X.y.
Fail 打印 Y.y.
定义 T := (prod X.T Y.T)%type.
Reset T.
(** Notation _carrier is not yet imported *)
Fail 校验 _carrier.
(** Disable the printing of notations for now *)
未设置 打印 符号.
进口 Y.
(** Y.T is imported *)
打印 T.
(** Notation _carrier is imported *)
校验 _carrier.
(** Export Set Printing Notation is imported *)
校验 T. (** output: _carrier : Set *)
(** [x] is 本地 and therefore not imported *)
Fail 打印 x.
(** Same as above because the Notation is imported *)
定义 T := (prod X.T _carrier)%type.
(** The imported [Y.T] is now masked *)
打印 T .
Reset T .
(** Same as above because the sharing constraint says that [ X.T = Y.T ( = _carrier )] *)
定义 T := (prod _carrier _carrier)%type.
定义 x : T := (pair X.x Y.x) .
结束 MODPARAMS.
打印 模块 MODPARAMS.
(** Fails because the sharing constraints are not satisfied *)
Fail 模块 词头了 参数 P : ((MODPARAMS N) 跟 模块 词头了 Y := B) .
Fail 模块 词头了 参数 P : ((MODPARAMS B) 跟 模块 词头了 Y := N) .
(** In this section : [X = M , Y = N] *)
模块 词头了 参数 R : ((MODPARAMS M) 跟 模块 词头了 Y := N) .
打印 模块 词头了 R .
打印 R.x. (** M.x is unfolded in ( R.x = ( 0 (** M.x *) , R.Y.x) ) because the component x of MOD_T_x is inlined ;
and certainly R.Y.x ( = N.x ) will not be unfolded because Y is some inner (not-outer) parameter of MODPARAMS *)
计算 ( fst R.x + snd R.x ).
模块 词头了 参数 S : (** HERE !!! *) ! ( (MODPARAMS M) 跟 模块 词头了 Y := N ) .
(** [M.x]] is not unfolded in [ R.x = (M.x , S.Y.x) ] because the inlining of the component [x] of [MOD_T_x] is disabled by the command [!] *)
打印 S.x.
计算 ( fst S.x + snd S.x ).
(** In this section : [X = N , Y = M] *)
模块 词头了 参数 U : ((MODPARAMS N) 跟 模块 词头了 Y := M) .
(** In [ U.x = (N.x , U.Y.x) ] , certainly [N.x] is already not unfoldable *)
打印 U.x .
计算 ( snd U.x + fst U.x ) .
(** This section shows how the inner-parameter [Y] of the module [MODPARAMS] may be moved outside as some outer-parameter .
Also the permutation of the sequence of the outer-parameters is possible . *)
模块 MODPARAMS_Y_X (Y : MOD_T_x) (X : MOD_T_x 跟 定义 T := Y.T)
:= 让 模块 词头了 Y := Y 在 (MODPARAMS X) .
打印 模块 MODPARAMS_Y_X.
模块 词头了 参数 V_Y'M_X'N : (MODPARAMS_Y_X M N) .
Reset V_Y'M_X'N . (** same : *)
模块 词头了 参数 V_Y_X (Y : MOD_T_x) (X : (MOD_T_x 跟 定义 T := Y.T))
: (MODPARAMS_Y_X Y X) .
模块 词头了 别号 V_Y'M_X'N <: (MODPARAMS_Y_X M N) := (V_Y_X M N) .
(** [V_Y'M_X'N.Y.x] is unfolded in [ V_Y'M_X'N.x = (N.x , 0 (* V_Y'M_X'N.Y.x *) ) ] ,
because the component [x] of [MOD_T_x] is inlined
and the instantiation by [M] of the module [MODPARAMS_Y_X] or the prefixed-module [V_Y_X] to get the instance [V_Y'M_X'N]
is via the (module or prefixed-module) outer/functor instantiation/application *)
打印 V_Y'M_X'N.x .
计算 ( snd V_Y'M_X'N.x + fst V_Y'M_X'N.x ) .
(** ---------------------------------------------------- *)
Reset MOD_T'nat_x'0_y'true.
(** Module without parameters . This is precisely for the prefix [M] below .*)
Modular MOD_T'nat_x'0_y'true.
Definition T := nat.
Definition x := 0.
Definition y : bool.
Proof.
exact true.
Defined.
End MOD_T'nat_x'0_y'true.
Modular Prefixed Parameter M : MOD_T'nat_x'0_y'true .
(** Module with 2 inner-parameters and with some environment which is enabled . *)
Modular MOD_T_x.
Parameter T : Set.
(** [Export] keyword says that this environment will be imported when this module is imported . *)
Export Set Printing Notations.
Notation _carrier := T.
(** [Local] keyword says this identifier will never be imported .
[Inline] keyword says that this component of any prefixed-module input
will be unfolded in the output module during any outer/functor instantiation/application *)
Local Parameter Inline x : T.
End MOD_T_x.
(** Module instantiated and prefixed by the name [B] . *)
Modular Prefixed Parameter B : (MOD_T_x with Definition T := bool).
(** Another different instantiation . Module instantiated and prefixed by the name [N] . *)
Modular Prefixed Parameter N : (MOD_T_x with Definition T := nat) .
Print N.T.
Print N.x.
(** No more instantiation of [M] is possible. Oneself can only alias (here rename) , then check the precision . *)
Modular Prefixed Alias M' <: (MOD_T_x with Definition T := nat) := M .
Modular MOD_z (M'' : MOD_T'nat_x'0_y'true).
Definition z : nat := 1 + M''.x .
End MOD_z.
(** Another form of the command to (anonymously) present the module components and to prefix the module at the same time (and also to check the precision). *)
Modular Prefixed Alias M_z <: (MOD_T_x with Definition T := nat).
Include M.
Fail Definition x := 1 .
(** may be bad *)
Definition z : nat := 1 + M.x . Print z.
Reset z.
Include (MOD_z M). Print z.
Reset z.
Definition z : nat := 1 + x . Print z.
Reset z.
Include MOD_z. Print z.
End M_z.
Print M_z.T.
Print M_z.x.
(** Module with one outer-parameter [X]] . This module has also one inner-parameter [Y] , which will also be component of the result *)
Modular MODPARAMS (X : MOD_T_x) <: MOD_T_x .
Modular Prefixed Parameter Y : (MOD_T_x with Definition T := X.T) .
Print X.x.
Print Y.x.
Fail Print X.y.
Fail Print Y.y.
Definition T := (prod X.T Y.T)%type.
Reset T.
(** Notation _carrier is not yet imported *)
Fail Check _carrier.
(** Disable the printing of notations for now *)
Unset Printing Notations.
Import Y.
(** Y.T is imported *)
Print T.
(** Notation _carrier is imported *)
Check _carrier.
(** Export Set Printing Notation is imported *)
Check T. (** output: _carrier : Set *)
(** [x] is Local and therefore not imported *)
Fail Print x.
(** Same as above because the Notation is imported *)
Definition T := (prod X.T _carrier)%type.
(** The imported [Y.T] is now masked *)
Print T .
Reset T .
(** Same as above because the sharing constraint says that [ X.T = Y.T ( = _carrier )] *)
Definition T := (prod _carrier _carrier)%type.
Definition x : T := (pair X.x Y.x) .
End MODPARAMS.
Print Modular MODPARAMS.
(** Fails because the sharing constraints are not satisfied *)
Fail Modular Prefixed Parameter P : ((MODPARAMS N) with Modular Prefixed Y := B) .
Fail Modular Prefixed Parameter P : ((MODPARAMS B) with Modular Prefixed Y := N) .
(** In this section : [X = M , Y = N] *)
Modular Prefixed Parameter R : ((MODPARAMS M) with Modular Prefixed Y := N) .
Print Modular Prefixed R .
Print R.x. (** M.x is unfolded in ( R.x = ( 0 (** M.x *) , R.Y.x) ) because the component x of MOD_T_x is inlined ;
and certainly R.Y.x ( = N.x ) will not be unfolded because Y is some inner (not-outer) parameter of MODPARAMS *)
Compute ( fst R.x + snd R.x ).
Modular Prefixed Parameter S : (** HERE !!! *) ! ( (MODPARAMS M) with Modular Prefixed Y := N ) .
(** [M.x]] is not unfolded in [ R.x = (M.x , S.Y.x) ] because the inlining of the component [x] of [MOD_T_x] is disabled by the command [!] *)
Print S.x.
Compute ( fst S.x + snd S.x ).
(** In this section : [X = N , Y = M] *)
Modular Prefixed Parameter U : ((MODPARAMS N) with Modular Prefixed Y := M) .
(** In [ U.x = (N.x , U.Y.x) ] , certainly [N.x] is already not unfoldable *)
Print U.x .
Compute ( snd U.x + fst U.x ) .
(** This section shows how the inner-parameter [Y] of the module [MODPARAMS] may be moved outside as some outer-parameter .
Also the permutation of the sequence of the outer-parameters is possible . *)
Modular MODPARAMS_Y_X (Y : MOD_T_x) (X : MOD_T_x with Definition T := Y.T)
:= let Modular Prefixed Y := Y in (MODPARAMS X) .
Print Modular MODPARAMS_Y_X.
Modular Prefixed Parameter V_Y'M_X'N : (MODPARAMS_Y_X M N) .
Reset V_Y'M_X'N . (** same : *)
Modular Prefixed Parameter V_Y_X (Y : MOD_T_x) (X : (MOD_T_x with Definition T := Y.T))
: (MODPARAMS_Y_X Y X) .
Modular Prefixed Alias V_Y'M_X'N <: (MODPARAMS_Y_X M N) := (V_Y_X M N) .
(** [V_Y'M_X'N.Y.x] is unfolded in [ V_Y'M_X'N.x = (N.x , 0 (* V_Y'M_X'N.Y.x *) ) ] ,
because the component [x] of [MOD_T_x] is inlined
and the instantiation by [M] of the modular [MODPARAMS_Y_X] or the modular prefixed [V_Y_X] to get the instance [V_Y'M_X'N]
is via the (modular or modular prefixed) outer/functor instantiation/application *)
Print V_Y'M_X'N.x .
Compute ( snd V_Y'M_X'N.x + fst V_Y'M_X'N.x ) .
</textarea>
</div> <!-- /#document -->
</div> <!-- /#code-wrapper -->
</div> <!-- /#ide-wrapper -->
<script src="../ui-js/jscoq-loader.js" type="text/javascript"></script>
<script type="text/javascript">
var jscoq_ids = ['workspace'];
var jscoq_opts = {
prelude: true,
base_path: '../',
init_pkgs: ['init', 'qoc'],
all_pkgs: ['init', 'qoc', 'coq-base', 'coq-collections', 'coq-arith', 'coq-reals', 'math-comp'],
implicit_libs: true,
editor: { mode: { 'company-coq': true }, keyMap: 'default' }
};
/* Global reference */
var coq;
loadJsCoq(jscoq_opts.base_path)
.then( () => coq = new CoqManager(jscoq_ids, jscoq_opts) );
</script>
</body>
</html>