Montrer que la formule suivante est valide / prouvable : (A → (B → C)) ↔ (A ∧ B → C) Remarque: → est associatif à droite, on aurait pu écrire: (A → B → C) $↔(A ∧ B → C)
La curry cation consiste à transformer une fonction qui prend plusieurs arguments en une fonction qui prend un seul argument et qui retourne une fonction qui prend en arguments les arguments restants.
| Pourquoi utiliser la curry cation ? | Afi n de pouvoir réaliser des applications partielles plus facilement. |
|---|
Remarque: cette opération porte le nom de Haskell Curry (1900-1982).
En Caml Au lieu d'écrire:
# let f(x,y) = x + y;; val f : int * int -> int = <fun>
On écrit:
# let f x = fun y -> x + y;; val f : int -> int -> int = <fun>
ou bien
# let f x y = x + y;; val f : int -> int -> int = <fun>
En Coq On utilise la curry cation quand on écrit des fonctions ou des théorèmes.
On écrira plutôt:
Lemma toto: forall p q : R, p > 0 -> q > 0 -> p*q > 0.
que:
Lemma toto: forall p q : R, p > 0 /\ q > 0 -> p*q > 0.
Comment faire “curry” et “uncurry”?
let curry f (A*B->C) = function x -> function y -> f(x,y) let uncurry f(A->B->C) = function(x,y)-> f x y
Lien avec les preuves :
Lemma curry_prop : forall A B C : Type, (A*B -> C) -> A -> B -> C. Proof. intros A B C f x y apply f. split. apply x. apply y. Defined.
Print curry_prop.
curry_prop =
fun (A B C:Type) (f:A*B->C) (x:A)(y:B)=>f(x,y) :
forall A B C:Type,
(A * B -> C) -> A -> B -> C