aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/translate.txt
blob: 5b372c96c3508eaac9a3d6243c77bde0a9d4c435 (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
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
493
494
495

                 How to use the translator
                 =========================

       (temporary version to be included in the official
           TeX document describing the translator)

The translator is a smart, robust and powerful tool to improve the
readibility of your script. The current document describes the
possibilities of the translator.

In case of problem recompiling the translated files, don't waste time
to modify the translated file by hand, read first the following
document telling on how to modify the original files to get a smooth
uniform safe translation. All 60000 lines of Coq lines on our
user-contributions server have been translated without any change
afterwards, and 0,5 % of the lines of the original files (mainly
notations) had to be modified beforehand to get this result.

Table of contents
-----------------

I) Implicit Arguments
 1) Strict Implicit Arguments 
 2) Implicit Arguments in standard library

II) Notations
 1) Translating a V7 notation as it was
 2) Translating a V7 notation which conflicts with the new syntax
  a) Associativity conflicts
  b) Conflicts with other notations
   b1) A notation hides another notation 
   b2) A notation conflicts with the V8 grammar
   b3) My notation is already defined at another level
  c) How to use V8only with Distfix ?
  d) Can I overload a notation in V8, e.g. use "*" and "+" ?
 3) Using the translator to have simplest notations
 4) Setting the translator to automatically use new notations that
    wasn't used in old syntax
 5) Defining a construction and its notation simultaneously

III) Various pitfalls
 1) New keywords
 2) Old "Case" and "Match"
 3) Change of definition or theorem names
 4) Change of tactic names

---------------------------------------------------------------------

I) Implicit Arguments
   ------------------

1) Strict Implicit Arguments 

  "Set Implicit Arguments" changes its meaning in V8: the default is
to turn implicit only the arguments that are _strictly_ implicit (or
rigid), i.e. that remains inferable whatever the other arguments
are. E.g "x" inferable from "P x" is not strictly inferable since it
can disappears if "P" is instanciated by a term which erase "x".

  To respect the old semantics, the default behaviour of the
translator is to replace each occurrence "Set Implicit Arguments" by

  Set Implicit Arguments.
  Unset Strict Implicits.

  However, you may wish to adopt the new semantics of "Set Implicit
Arguments" (for instance because you think that the choice of
arguments it setsimplicit is more "natural" for you). In this case,
add the option -strict-implicit to the translator.

  Warning: Changing the number of implicit arguments can break the
notations.  Then use the V8only modifier of Notations.

2) Implicit Arguments in standard library

  Main definitions of standard library have now implicit
arguments. These arguments are dropped in the translated files. This
can exceptionally be a source of incompatibilities which has to be
solved by hand (it typically happens for polymorphic functions applied
to "nil" or "None").

II) Notations
    ---------

  Grammar (on constr) and Syntax are no longer supported. Replace them by
Notation before translation.

  Precedence levels are now from 0 to 200. In V8, the precedence and
associativity of an operator cannot be redefined. Typical level are
(refer to the chapter on notations in the Reference Manual for the
full list):

  <-> : 95                    (no associativity)
  -> : 90                     (right associativity)
  \/ : 85                     (right associativity)
  /\ : 80                     (right associativity)
  ~ : 75                      (right associativity)
  =, <, >, <=, >=, <> : 70    (no associativity)
  +, - : 50                   (left associativity)
  *, / : 40                   (left associativity)
  ^ : 30                      (right associativity)

1) Translating a V7 notation as it was

  By default, the translator keeps the associativity given in V7 while
the levels are mapped according to the following table:
 
  the V7 levels             [  0;  1;  2;  3;  4;  5;  6;  7;  8;  9;  10]
  are resp. mapped in V8 to [  0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100]
  with predefined assoc     [ No;  L;  R;  L;  L; No;  R;  R;  R; No;   L]

  If this is OK for you, just simply apply the translator.

2) Translating a V7 notation which conflicts with the new syntax

a) Associativity conflict

  Since the associativity of the levels obtained by translating a V7
level (as shown on table above) cannot be changed, you have to choose
another level with a compatible associativity.

  You can choose any level between 0 and 200, knowing that the
standard operators are already set at the levels shown on the list
above. 

Example 1: Assume you have a notation

Infix NONA 2 "=_S" my_setoid_eq.

By default, the translator moves it to level 30 which is right
associative, hence a conflict with the expected no associativity.

To solve the problem, just add the "V8only" modifier to reset the
level and enforce the associativity as follows:

Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).

The translator now knows that it has to translate "=_S" at level 70
with no associativity.

Rem: 70 is the "natural" level for relations, hence the choice of 70
here, but any other level accepting a no-associativity would have been
OK.

Example 2: Assume you have a notation

Infix RIGHTA 1 "o" my_comp.

By default, the translator moves it to level 20 which is left
associative, hence a conflict with the expected right associativity.

To solve the problem, just add the "V8only" modifier to reset the
level and enforce the associativity as follows:

Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).

The translator now knows that it has to translate "o" at level 20
which has the correct "right associativity".

Rem: We assumed here that the user wants a strong precedence for
composition, in such a way, say, that "f o g + h" is parsed as
"(f o g) + h". To get "o" binding less than the arithmetical operators,
an appropriated level would have been close of 70, and below, e.g. 65.

b) Conflicts with other notations

Since the new syntax comes with new keywords and new predefined
symbols, new conflicts can occur. Again, you can use the option V8only
to inform the translator of the new syntax to use.

b1) A notation hides another notation 

Rem: use Print Grammar constr in V8 to diagnose the overlap and see the
section on factorization in the chapter on notations of the Reference
Manual for hints on how to factorize.

Example:

Notation "{ x }" := (my_embedding x) (at level 1).

overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at
level 99. The conflicts can be solved by left-factorizing the notation
as follows:

Notation "{ x }" := (my_embedding x) (at level 1)
  V8only (at level 0, x at level 99).

b2) A notation conflicts with the V8 grammar.

Again, use the V8only modifier to tell the translator to automatically
take in charge the new syntax.

Example:

Infix 3 "@" app.

Since "@" is used in the new syntax for deactivating the implicit
arguments, another symbol has to be used, e.g. "@@". This is done via
the V8only option as follows:

Infix 3 "@" app V8only "@@" (at level 40, left associativity).

or, alternatively by

Notation "x @ y" := (app x y) (at level 3, left associativity)
  V8only "x @@ y" (at level 40, left associativity).

b3) My notation is already defined at another level (or with another
associativity)

In V8, the level and associativity of a given notation can no longer
be changed. Then, either you adopt the standard reserved levels and
associativity for this notation (as given on the list above) or you
change your notation.

- To change the notation, follow the directions in section b2.

- To adopt the standard level, just use V8only without any argument.

Example.

Infix 6 "*" my_mult.

is not accepted as such in V8. Write

Infix 6 "*" my_mult V8only.

to tell the translator to use "*" at the reserved level (i.e. 40 with
left associativity). Even better, use interpretation scopes (look at
the Reference Manual).

c) How to use V8only with Distfix ?

You can't, use Notation instead of Distfix.

d) Can I overload a notation in V8, e.g. use "*" and "+" for my own
algebraic operations ?

Yes, using interpretation scopes (see the corresponding chapter in the
Reference Manual).

3) Using the translator to have simplest notations

Thanks to the new syntax, * has now the expected left associativity,
and the symbols <, >, <= and >= are now available.

Thanks to the interpretation scopes, you can overload the
interpretation of these operators with the default interpretation
provided in Coq.

This may be a motivation to use the translator to automatically change
the notations while switching to the new syntax.

See sections b) and d) above for examples.

4) Setting the translator to automatically use new notations that
wasn't used in old syntax

Thanks to the "Notation" mechanism, defining symbolic notations is
simpler than in the previous versions of Coq.

Thanks to the new syntax and interpretation scopes, new symbols and
overloading is available.

This may be a motivation for using the translator to automatically change
the notations while switching to the new syntax.

Use for that the commands V8Notation and V8Infix.

Examples:

V8Infix "==>" my_relation (at level 65, right associativity).

tells the translator to write an infix "==>" instead of my_relation in
the translated files.

V8Infix ">=" my_ge.

tells the translator to write an infix ">=" instead of my_ge in the
translated files and that the level and associativity are the standard
one (as defined in the chart above).

V8Infix ">=" my_ge : my_scope.

tells the translator to write an infix ">=" instead of my_ge in the
translated files, that the level and associativity are the standard
one (as defined in the chart above), but only if scope my_scope is
open or if a delimiting key is available for "my_scope" (see the
Reference Manual).

5) Defining a construction and its notation simultaneously

This is permitted by the new syntax. Look at the Reference Manual for
explanation. The translator is not fully able to take this in charge...

III) Various pitfalls
    ----------------

1) New keywords

  The following identifiers are new keywords

  "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
  "else"; "return"; "mod"; "at"; "let"; "_"; ".("

  The translator automatically add a "_" to names clashing with a
keyword, except for files. Hence users may need to rename the files
whose name clashes with a keyword.

  Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type"
  were already keywords

2) Old "Case" and "Match"

  "Case" and "Match" are normally automatically translated into
  "match" or "match" and "fix", but sometimes it fails to do so. It
  typically fails when the Case or Match is argument of a tactic whose
  typing context is unknown because of a preceding Intro/Intros, as e.g. in 

     Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)

  The solution is then to replace the invocation of the sequence of
  tactics into several invocation of the elementary tactics as follows

     Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
          ^^^

3) Change of definition or theorem names

  Type "entier" from fast_integer.v is renamed into "N" by the
translator. As a consequence, user-defined objects of same name "N"
are systematically qualified even tough it may not be necessary.  The
same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
TO GIVE].

4) Change of tactics names

  Since tactics names are now lowercase, this can clash with
user-defined tactic definitions. To pally this, clashing names are
renamed by adding an extra "_" to their name.

======================================================================
Main examples for new syntax
----------------------------

1) Constructions

  Applicative terms don't any longer require to be surrounded by parentheses as
e.g in

  "x = f y -> S x = S (f y)"


  Product is written

     "forall x y : T, U"
     "forall x y, U"
     "forall (x y : T) z (v w : V), U"
     etc.

  Abstraction is written

     "fun x y : T, U"
     "fun x y, U"
     "fun (x y : T) z (v w : V), U"
     etc.

  Pattern-matching is written

     "match x with c1 x1 x2 => t | c2 y as z => u end"
     "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end"
     "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with
         c1 x1 x2, _ => t | c2 y, d z => u end"

     The last example is the new form of what was written

    "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of
         (c1 x1 x2) _ => t | (c2 y) (d z) => u end"

  Pattern-matching of type with one constructors and no dependencies
of the arguments in the resulting type can be written

    "let (x,y,z) as u return P u := t in v"
     
  Local fixpoints are written

    "fix f (n m:nat) z (x : X) {struct m} : nat := ...
     with ..."

    and "struct" tells which argument is structurally decreasing.

  Explicitation of implicit arguments is written

     "f @1:=u v @3:=w t"
     "@f u v w t"

2) Tactics

  The main change is that tactics names are now lowercase. Besides
this, the following renaming are applied:

  "NewDestruct" -> "destruct"
  "NewInduction" -> "induction"
  "Induction" -> "simple induction"
  "Destruct" -> "simple destruct"

  For tactics with occurrences, the occurrences now comes after and
  repeated use is separated by comma as in

  "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4"
  "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4"
  "Simpl 1 3 e" -> "simpl e at 1 3"

3) Tactic language

  Definitions are now introduced with keyword "Ltac" (instead of
"Tactic"/"Meta" "Definition") and are implicitly recursive
("Recursive" is no longer used).

  The new rule for distinguishing terms from ltac expressions is:

  Write "ltac:" in front of any tactic in argument position and
  "constr:" in front of any construction in head position

4) Vernacular language

a) Assumptions

  The syntax for commands is mainly unchanged. Declaration of
assumptions is now done as follows

  Variable m : t.
  Variables m n p : t.
  Variables (m n : t) (u v : s) (w : r).
  
b) Definitions

  Definitions are done as follows

  Definition f m n : t := ... .
  Definition f m n := ... .
  Definition f m n := ... : t.
  Definition f (m n : u) : t := ... .
  Definition f (m n : u) := ... : t.
  Definition f (m n : u) := ... .
  Definition f a b (p q : v) r s (m n : t) : t := ... .
  Definition f a b (p q : v) r s (m n : t) := ... .
  Definition f a b (p q : v) r s (m n : t) := ... : t.

c) Fixpoints

  Fixpoints are done this way
  
  Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... .
  Fixpoint f x : v := ... .
  Fixpoint f (x : t) : v := ... .

  It is possible to give a concrete notation to a fixpoint as follows

  Fixpoint plus (n m:nat) {struct n} : nat as "n + m" :=
    match n with
    | O => m
    | S p => S (p + m)
    end.

d) Inductive types

  The syntax for inductive types is as follows

  Inductive t (a b : u) (d : e) : v :=
     c1 : w1 | c2 : w2 | ... .

  Inductive t (a b : u) (d : e) : v :=
     c1 : w1 | c2 : w2 | ... .

  Inductive t (a b : u) (d : e) : v :=
     c1 (x y : t) : w1 | c2 (z : r) : w2 | ... .

  As seen in the last example, arguments of the constructors can be
given before the colon. If the type itself is omitted (allowed only in
case the inductive type has no real arguments), this yields an
ML-style notation as follows

  Inductive nat : Set := O | S (n:nat).
  Inductive bool : Set := true | false.

  It is even possible to define a syntax at the same time, as follows:

  Inductive or (A B:Prop) : Prop as "A \/ B":=
    | or_introl (a:A) : A \/ B 
    | or_intror (b:B) : A \/ B.

  Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).