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
|
Some hints for translation (DRAFT):
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".
If you really wish to keep the old meaning of "Set Implicit
Arguments", you have to replace every occurrence of it by
Set Implicit Arguments.
Unset Strict Implicits.
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.
II) Notations
---------
Grammar (on constr) and Syntax are no longer supported. Replace them by
Notation before translation.
Precedence levels are now from 0 to 250. Typical level are:
/\ : 60
\/ : 70
<-> : 80
~ : 50
=, <=, >=, <> : 50
+, - : 40
*, / : 30
The new scale can induce incompatibilities. To set the level an
operator should have after translation, use the V8only modifier of
Infix or Notation in the v7 file, as e.g.:
Infix 6 "<=" le V8only 50.
Notation "( x , y )" := (pair ? ? x y) V8only "x , y" (at level 0).
Infix 3 "*" mult : nat_scope V8only (left associativity).
The default for precedence is to multiply the level by 10. Notice
that you can change not only the precedence but also the
associativity and the syntax itself.
III) 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" -> "oldinduction"
"Destruct" -> "olddestruct"
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 3 1, d, e 4"
"Unfold 1 3 f 4 g" -> "unfold f 1 3, g 4"
"Simpl 1 3 e" -> "simpl e 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 simple quotes is:
"Quote any tactic in argument position and 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).
IV) Pitfalls
Type "entier" from fast_integer.v is renamed into "N" by the
translator. As a consequence, user-defined objects of same name "N"
can be hidden by the new "N" if the "Require ZArith" is not done soon
enough. The solution is to move the "Require ZArith" before users
modules. The same apply for names "GREATER", "EQUAL", "LESS",
etc... [COMPLETE LIST TO GIVE].
|
