Dictionnaire Coq/OCaml Produit cartésien Listes

OCaml Coq OCaml

Note En OCaml une phrase se termine par un ;; (qui peut être omis
(1, true);; Check (1, true). let l = 1 :: 2 :: [];;
dans certains cas). En Coq, une phrase se termine toujours par un point. (* - : int * bool = (1, true) *) (* (1, true) : nat * bool *) let l’ = [1; 2];;
(* sont 2 définitions équivalentes ayant pour type : int list *)
let fst p = Definition fst (A B:Type) (p:A*B) :=
Typage et calcul, définitions globales et locales let (x, _) = p in x;; let ’(x, _) := p in x.
let snd p = Definition snd (A B:Type) (p:A*B) := fun l -> match l with
OCaml Coq let (_, y) = p in y;; let ’(_, y) := p in y. | [] -> true
| x :: l -> false;;
2 + 2;; Check 2 + 2. (* 2 + 2 : nat *) (* - : ’a list -> bool *)
(* - : int = 4 *) Eval compute in 2 + 2. (*= 4 : nat *)
Note En Coq les n-uplets sont définis comme des couples itérés par
la gauche, ainsi les termes ((1, 2), 3) et (1, 2, 3) sont synonymes Coq
OCaml Coq
et ont pour type (nat * nat) * nat = nat * nat * nat. Require Import List.
let x = expr ;; Definition x := expr . Import ListNotations. (* pour écrire les listes comme en OCaml *)
(* val x : type = expr *) Check x. (* x : type *)
Set Implicit Arguments. (* à spécifier au début du fichier Coq *)
x;; Print x.
Types utilisateur et filtrage
(* - : type = expr *) (* x = expr : type *) Definition l := 1 :: 2 :: [].
Remarques Definition l’ := [1; 2].
let x = expr ’;; Definition x := expr ’. 1. En Coq les constructeurs des types inductifs peuvent être définis (* sont 2 définitions équivalentes ayant pour type : list nat *)
(* val x : type ’ = expr ’ *) (* Error: x already exists. *)
de manière curryfiée (ce qui est le cas dans le code ci-dessous).
Check fun (T:Type) (l:list T) => match l with
2. OCaml tolère l’écriture d’un filtrage non exhaustif (Warning). | [] => true
OCaml Coq
En Coq le filtrage non exhaustif est interdit. | x :: l => false
let x = e1 in e2 let x := e1 in e2 end. (* : ∀ T : Type, list T -> bool *)
3. Dans les scripts Coq ci-dessous, on suppose avoir activé les argu-
let (x, y) = e1 in e2 let ’(x, y) := e1 in e2 ments implicites (début du fichier : Set Implicit Arguments.)
OCaml Coq
Modules
type ’a tree = Inductive tree (A : Type) :=
Fonctions | Leaf of ’a | Leaf (_ : A)
| Node of ’a tree * ’a tree;; | Node (_ : tree A) (_ : tree A). OCaml
OCaml Coq
let a = Definition a :=
type nat = O | S of nat (* ce type somme est prédéfini en Coq *)
fun x -> expr fun x => expr Node(Leaf(1), Leaf(2));; Node (Leaf 1) (Leaf 2).
fun (x : type) -> expr fun x : type => expr (* val a : int tree *) Check a. (* a : tree nat *) module type tPickGt = sig
val pick : nat -> nat
fun x -> fun y -> expr fun x => fun y => expr match a with match a with end
fun x y -> expr fun x y => expr | Leaf x -> e1 | Leaf x => e1 module PickGt : tPickGt = struct
fun (x : t1 ) (y : t2 ) -> expr fun (x : t1 ) (y : t1 ) => expr | Node(a, b) -> e2 | Node a b => e2 let pick n = S n
end
let f = fun x -> expr;; Definition f := fun x => expr. end
let g x y = expr;; Definition g x y := expr. type (’p1 , . . . , ’pℓ ) t = Inductive t (p1 : P1 ) . . . (pℓ : Pℓ ) := module Use (P : tPickGt) = struct
| C1 of (t11 * . . . *t1n1 ) | C1 (p11 : t11 ) . . . (p1n : t1n1 ) let num = P.pick O
1
| ... | ... end
| Ck of (tk1 * . . . *tkn );; | Ck (pk1 : tk1 ) . . . (pkn : tkn ). module M = Use(PickGt);;
k k k
Fonctions d’ordre supérieur, arguments implicites (Coq)
Coq
OCaml Coq
Définition globale de fonctions récursives Module Type tPickGt.
fun f x -> f (f x) fun (T:Type) (f:T -> T) x => f (f x)
(* a pour type *) (* a pour type *) Parameter pick : nat -> nat.
OCaml Coq Axiom pick_gt : ∀ n, pick n > n.
(’a -> ’a) -> ’a -> ’a ∀ (T:Type), (T -> T) -> T -> T
let rec sum a = Fixpoint sum a := End tPickGt.
match a with match a with Module PickGt <: tPickGt.
OCaml Coq
| Leaf n -> n | Leaf n => n Definition pick n := S n.
| Node(a, b) -> sum a + sum b;; | Node a b => sum a + sum b Lemma pick_gt : ∀ n, pick n > n.
Set Implicit Arguments.
let id x = x;; Definition id (T:Type) (x:T) := x. end. Proof. auto. Qed.
(* val id : ’a -> ’a *) About id. (* id : ∀ (T:Type), T -> T End PickGt.
Argument T is implicit *) Module Use (P : tPickGt).
id 2;; (* Ces 3 expressions sont égales : *) Definition num := P.pick O.
(* - : int = 2 *) id 2, @id nat 2, @id _ 2 Rappel En Coq, chaque appel récursif doit se faire sur un sous-terme. Lemma num_gt0 : num > O.
Cela garantit que toute fonction récursive termine. Proof. apply P.pick_gt. Qed.
End Use.
Note Dans le code Coq ci-dessus, Le symbole @ annule l’effet des Module M := Use(PickGt).
arguments implicites (et le symbole _ force l’inférence de type).

Copyright 2017, 2019 Erik Martin-Dorel Dictionnaire Coq/OCaml v1.1 Mis à disposition selon les termes de la Licence CC BY-SA 4.0 International.