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)

currification

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.

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