-- Curry
import Test.Prop
import Nat
double :: Nat -> Nat
double x = add x x
even :: Nat -> Bool
even Z = True
even (S Z) = False
even (S (S n)) = even n
evenDouble :: Nat -> Prop
evenDouble x = always (even (double x))
(* Coq *)
Fixpoint add (b : nat) (c : nat) : nat :=
match b with
| O => c
| S d => S (add d c)
end.
Definition double (b : nat) : nat := add b b.
Fixpoint even (b : nat) : bool :=
match b with
| O => true
| S c => match c with
| O => false
| S d => even d
end
end.
Theorem evenDouble :
(forall (b : nat) ,
(even (double b)) =
true).
Proof.
Qed.
- Explicit type arguments for polymorphic functions
-- Curry
import Test.Prop
data List a = Nil | Cons a (List a)
map :: (a -> b) -> List a -> List b
map _ Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)
mapId xs = always (map id xs == xs)
(* Coq *)
Inductive List (A : Type) : Type :=
| Nil : List A
| Cons : A -> (List A) -> (List A).
Definition id (A : Type) (b : A) : A := b.
Fixpoint map (A B : Type) (b : A -> B) (c : List A) : List B :=
match c with
| Nil _ => Nil B
| Cons _ d e => Cons B (b d) (map A B b e)
end.
Theorem mapId :
(forall (A : Type) (b : List A) ,
(map A A (id A) b) =
b).
Proof.
Qed.
- Polymorphic comparison operators are problematic
-- Curry
import Test.Prop
data BTree a = Leaf a | Node (BTree a) (BTree a)
height :: BTree a -> Int
height (Leaf x) = 1
height (Node t1 t2) = 1 + max (height t1) (height t2)
aBTree = Node (Leaf 1) (Node (Leaf 2) (Node (Node (Leaf 3) (Leaf 4)) (Leaf 5)))
prop = always (height aBTree == 5)
(* Coq *)
Inductive BTree (A : Type) : Type :=
| Leaf : A -> (BTree A)
| Node : (BTree A) -> (BTree A) -> (BTree A).
(* doesn't work *)
Definition max (A : Type) (b : A) (c : A) : A := match >= b c with
| true => b
| false => c
end.
Definition aBTree : BTree (Int) := Node (Leaf 1) (Node (Leaf 2) (Node (Node (Leaf 3) (Leaf 4)) (Leaf 5))).
Fixpoint height (A : Type) (b : BTree A) : Int :=
match b with
| Leaf _ c => 1
| Node _ d e => + 1 (max (Int) (height A d) (height A e))
end.
Theorem prop :
(forall ,
(height (Int) (aBTree)) =
5).
Proof.
Qed.