seance6-english.v 13.4 KB
Newer Older
Pierre Letouzey's avatar
Pierre Letouzey committed
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

(** * Session 6 : more modules, records, extraction *)

Require Import List.
Import ListNotations.

(** * Part 1 : Modules *)

(** Example of "Module Type", also known as a signature, or
    an interface. *)

Module Type Foo.
 Parameter t : Type -> Type.
 Parameter empty : forall A, t A.
 Parameter cons : forall A, A -> t A -> t A.
 Parameter decons : forall A, t A -> option (A * t A).
 Parameter length : forall A, t A -> nat.
End Foo.

(** Example of an implementation of this signature.

    With the "<:" syntax below, Coq checks that the definitions
    in module Bar are compatibles with Foo.
    But Bar is left unrestricted afterwards.
*)

Module Bar <: Foo.
 Definition t := list.
 Definition empty {A} : list A := [].
 Definition cons := @List.cons.
 Definition decons {A} (l:list A) :=
  match l with
  | [] => None
  | x::l => Some (x,l)
  end.
 (* Note: the implementation can contain extra stuff not mentionned in Foo. *)
 Definition truc := 1 + 2.
 Definition length := @List.length.
End Bar.

Print Bar.t.

Compute (Bar.cons _ 1 Bar.empty).

(** Now, if we use the syntax ":" below instead of "<:" in the definition
    of a module, all internal details will be masked afterwards, hidden
    by Foo, and only the information given by Foo will be available.
    In particular, this will prevent here any computation, since
    the body of the definitions will be inaccessible.
    So in Coq this ":" is usually far too restrictive, unlike in
    languages like OCaml.
*)

Module RestrictedBar : Foo := Bar.

Print RestrictedBar.t.

Compute (RestrictedBar.cons _ 1 (RestrictedBar.empty _)).


Pierre Letouzey's avatar
Pierre Letouzey committed
61
(** A "functor" ("foncteur" in French) is a module parametrized
Pierre Letouzey's avatar
Pierre Letouzey committed
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
    by another module.
*)


(** Example: starting from [Foo], one may propose some [head] and
    [tail] functions. *)

Module HeadTail (M:Foo).
  Definition head {A} : M.t A -> option A :=
    fun l => match M.decons _ l with None => None | Some (x,l') => Some x end.
  Definition tail {A} : M.t A -> option (M.t A) :=
    fun l => match M.decons _ l with None => None | Some (x,l') => Some l' end.
End HeadTail.

(** For now, this does not create any new concrete functions. *)

Fail Print HeadTail.head.

(** But we can use this in a generic way on any implementation of Foo. *)

Module BarHdTl := HeadTail(Bar).
Print BarHdTl.head.
Compute BarHdTl.head [1;2].

(** We can even extend a module, via a notion of inclusion. *)

Module Bar2.
 Include Bar.
 Include HeadTail(Bar).
End Bar2.

(** Lighter syntax for the same thing: *)

Module Bar3 := Bar <+ HeadTail.

(** Another example of functor: starting from a first module
    satisfying interface Foo, we could build another one for which
    the [length] function is working in constant time.
    For that we store somewhere this size, and update it after
    all operations. That's a typical example of time vs. space tradeoff.
*)

Module FastLength (M:Foo) <: Foo.
 Definition t A := (M.t A * nat)%type.
 Definition empty A := (M.empty A, 0).
 Definition cons A x (l:t A) :=
  let (l,n) := l in
  (M.cons A x l, S n).
 Definition decons A (l:t A) :=
   let (l,n) := l in
   match M.decons A l with
   | None => None
   | Some (x,l) => Some (x,(l,pred n))
   end.
 Definition length A (l:t A) := snd l.
End FastLength.

(** A last example of functor: using the Coq standard library
    for building efficient finite sets. *)

Require Import Arith MSets MSetRBT.

(** The interface of finite sets: *)
Print MSetInterface.S.

(** A functor building such a structure of finite sets: *)
Print MSetRBT.Make.

(** What we need for instantiating this functor: *)
Print Orders.OrderedType.

(** Except for a few logical predicates and a few proofs, this interface
    mainly asks for a type [t] and a ternary comparison function named
    [compare]... *)
Print comparison.

(** Moreover the [Nat] module provided by the library [Arith]
    already contains all that (just like for [N] or [Z] modules
    for efficient binary numbers). Let's check this inclusion
    (also called module subtyping) : *)

Module Nat' <: Orders.OrderedType := Nat.

(** So now we can build a module of finite sets of numbers. *)
Pierre Letouzey's avatar
Pierre Letouzey committed
146
Module NatSet := MSetRBT.Make(Nat).
Pierre Letouzey's avatar
Pierre Letouzey committed
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

Print NatSet.

Definition test := NatSet.add 7 (NatSet.add 8 NatSet.empty).

Compute NatSet.mem 7 test.

Compute NatSet.elements test.

(** Note that NatSet.elt is now a alias for nat. *)

Print NatSet.elt.

(** And the type NatSet.t is not abstract as it could (and should)
    be in other languages, once again due to ":" being too restrictive
    in Coq. But looking into the implementation details of this type
    is not recommended (but not a secret either, it's a binary tree
    with some proof of invariants attached to it *)



(** * Part 2 : Records *)

(** This is a particular syntax for inductive types with only
    one constructor. *)

(** Up to now, we could use the type of Coq pairs, possibly nested ... *)

Definition truc := (1,true,pred). (* actually ((1,true),pred) *)

(** ... or define an ad-hoc type via [Inductive], whose constructor(s)
   may have any number of arguments we see fit. *)

Inductive something :=
| Thing : nat -> bool -> (nat -> nat) -> something.

Check (Thing 1 true pred).

(** Another possibility, use a Record : *)

Record myrecord :=
 { position : nat;
   flag : bool;
   next : nat -> nat;
 }.

Print myrecord.
Check Build_myrecord. (** constructor, with a name generated by Coq *)

(** Main interest : each field is named, hopefully with a significant
    name, no need to remember the order of the arguments. *)

(** One may build a record value like this : *)

Definition example_record :=
 {| position := 1; flag := true; next := pred |}.

(** In this case, the order of fields is arbitrary *)

Check {| flag := true; next := pred; position := 1 |}.

(** It is also possible to use the constructor in a usual way.
    Here the Coq-generated name is [Build_myrecord]. *)

Definition example_record' := Build_myrecord 1 true pred.

(** We could also pick our own constructor name when defining the
    record type *)

Record myrecord' := Make_myrecord' { foo : nat; bar : bool}.

(** For accessing a specific field, the syntax of a projection is [r.(...)] *)

Compute example_record.(flag).

(** Coq Records has been extended in a notion called "type classes".
    We won't detail them here, for more on that, see for instance:
    https://softwarefoundations.cis.upenn.edu/qc-current/Typeclasses.html
*)




(** * Part 3 : Extraction *)

(** The Coq extraction is an automated code translator from Coq to
    OCaml or Haskell. It allows to integrate Coq code (ideally,
    a code that we have specified and proved correct in Coq) into
    larger, more realistic programs. For instance, this way we can
    benefit from input/output parts, or any other notions that cannot
    be done directly in Coq. *)

(** The main theoretical guarantee provided by the Coq extraction :

    - If a extracted function is launched in OCaml or Haskell
      on values that could have been expressed in Coq, then the
      computation will produce a result compatible with the result
      we would have had in Coq. The only possible erreurs during
      this computation are exhaustion of machine resources
      (out-of-memory, stack overflow, etc).

    Informally, this means that any property proved on our Coq code
    will continue to be valid on the code obtained by extraction.

    Beware : the previous result only holds if the initial Coq code
    does not depend on incoherent axioms. Otherwise, incoherent axioms
    may lead to extracted code that loops forever, or even crashes !

    Another caveat : the target language may provide values that
    have no Coq counterparts. For instance, in OCaml (or Haskell), it
    is possible to define a cyclic data [let rec mylist = 1 :: mylist].
    If one gives this value as argument to the extracted version of
    [List.length], the computation will never stop, and the extraction
    correctness is not to blaim. Simply, [mylist] is clearly not
    a "value that could have been expressed in Coq".
*)


(** Extraction in practice. On the programming fragment of Coq, the
    one we have almost exlusively considered up to now, the extraction
    is mainly preforming syntactic adjustments. But:

    - If the Coq code contains proof parts, the extraction removes them,
      since they are sorts of assertions, and do not influence the
      computation results. We say that they have no computational
      content.

    - All types are also erased from extracted values, since them have
      no computational content either (you cannot "match" on a type).
      Moreover the target languages separate strictly between the
      worlds of types and the world of values (no pairs such as
      [(int,int)] in OCaml, for instance).

    - Types are normally translated into types in the target language,
      but this is not always possible since Coq types are way richer.
      In case a Coq type has not counterpart in the target language,
      we overcome this limitation by type approximations and
      use of "unsage" primitives of the target language ([Obj.magic]
      in OCaml, [unsafeCoerce] in Haskell).
*)

(** Example *)

Fixpoint fact n :=
  match n with
  | 0 => 1
  | S n => (S n) * fact n
  end.

Compute fact 8.

Require Extraction.

(** Simpliest extraction : just one definition at a time.
    No recursive dependency analysis. *)

Extraction fact.

(** Here we obtain:

let rec fact = function
| O -> S O
| S n0 -> mul (S n0) (fact n0)
*)

(** Or in Haskell: *)

Extraction Language Haskell.
Extraction fact.

Extraction Language OCaml.

(** More interesting : extracting fact and all its dependencies
    (including type definition). This way we get a standalone
    code fragment in OCaml (resp. Haskell). *)

Recursive Extraction fact.

(** We obtain:

type nat =
| O
| S of nat

(** val add : nat -> nat -> nat **)

let rec add n m =
  match n with
  | O -> m
  | S p -> S (add p m)

(** val mul : nat -> nat -> nat **)

let rec mul n m =
  match n with
  | O -> O
  | S p -> add m (mul p m)

(** val fact : nat -> nat **)

let rec fact = function
| O -> S O
| S n0 -> mul (S n0) (fact n0)

*)

(** The code produced by [Recursive Extraction] could normally be
    used unmodified in an OCaml file or sent directly to an OCaml
    "toplevel". Or we could let Coq write this extracted code to
    a file for us: *)

Extraction "fact.ml" fact.

(** This file can then be either loaded in a toplevel, via the
    command [#use "fact.ml";;], or be integrated in a larger program
    and be compiled and run. *)

(** Example of OCaml session after this extraction:

#use "fact.ml";;
(* No nice notation for numbers here *)
fact (S (S (S (S (S (S (S O)))))));;
(* One may write conversion functions between int and (extracted) nat ... *)
let rec n2i = function O -> 0 | S n -> 1+n2i n;;
let rec i2n = function 0 -> O | n -> S (i2n (n-1));;
(* ... then "wrap" the extracted function to obtain a int->int function *)
let ocaml_fact n = n2i (fact (i2n n));;
let _ = ocaml_fact 8;; (* 40320 *)
let _ = ocaml_fact 9;; (* stack overflow *)
*)


(** Why a "stack overflow" above ? An inefficient computation in Coq
    will not become efficient by miracle after extraction...
    For serious computation with big numbers, rather use Coq type [N]
*)

Require Import NArith.

Check N.peano_rect.

Definition Nfact n : N :=
  (N.peano_rect _ 1 (fun n p => (N.succ n) * p) n)%N.

Compute Nfact 8.

Extraction "nfact.ml" Nfact.

(** Example of OCaml session after this extraction :

#use "nfact.ml";;
(* Conversion functions between positive and int, then between n and int *)
let rec p2i = function XH -> 1 | XO p -> 2* (p2i p) | XI p -> 2*(p2i p)+1;;
let n2i = function N0 -> 0 | Npos p -> p2i p;;

let rec i2p i =
  if i <= 1 then XH
  else if i mod 2 = 0 then XO (i2p (i/2))
  else XI (i2p (i/2));;

let i2n = function 0 -> N0 | n -> Npos (i2p n);;

let _ = n2i (nfact (i2n 10));; (* 3628800 *)
let _ = n2i (nfact (i2n 20));; (* 2432902008176640000 *)
let _ = n2i (nfact (i2n 30));; (* 458793068007522304 *)
*)

(** Note that the result for [!30] is smaller than the one for [!20],
    which should not be the case. In fact, the OCaml type [int] is
    bounded : usually [max_int = 2^62-1].
    The extracted code is fine, the result of [nfact (i2n 30)] is
    indeed correct, but the conversion [n2i] toward [int] produces a
    result which is accurate only up to some "modulo". Various solutions
    exists to leverage this issue, for instance use some OCaml library
    of arbritrary precision numbers (old [bignum] library, or the recent
    [zarith] one). Or use the type [Integer] in Haskell. *)


(** Example of an extraction involving types that cannot be expressed
    in OCaml : an excerpt of the session of dependent types. *)

Fixpoint narity n :=
 match n with
 | 0 => nat
 | S n => nat -> narity n
 end.

Compute narity 5.

Fixpoint narity_S_sum n : narity (S n) :=
 match n with
 | 0 => fun a => a
 | S n => fun a b => narity_S_sum n (a+b)
 end.

Definition narity_sum n : narity n :=
 match n with
 | 0 => 0
 | S n => narity_S_sum n
 end.

Compute narity_sum 4 5 1 2 3 : nat. (* 5 + 1 + 2 + 3 = 11 *)

Recursive Extraction narity_sum. (* Some [Obj.magic] ... *)

(** Another example : consider again the type of Coq vectors and
    extract it. This way, we obtain an OCaml type [vect] which is
    very close to regular lists, with just an extra number in it
    in constructor [Vcons], remnant of the size annotation.
    This last remnant of a dependent type may be removed via the
    use of an experimental command named [Extraction Implicit].
    And [Vcast] is extracted into an identity function. *)