Testit vs Proof

Take.md

Hehkutettu Haskellin QuickCheck

import Prelude hiding (take)

import Test.QuickCheck

take :: Int -> [a] -> [a]
take _ []     = []
take 0 _      = []
take n (x:xs) = x : take (n-1) xs

take_length_prop :: NonNegative Int -> [a] -> Bool
take_length_prop n l = length (take intn l) <= intn
  where intn = fromIntegral n

main :: IO ()
main = quickCheckWith stdArgs { maxSuccess = 1000 } p
  where p = take_length_prop :: NonNegative Int -> [Int] -> Bool

Vähän joutuu kikkailee testin kirjottamisen kanssa.

Ihan huike Coq

Lemma le_0_n : forall n : nat,
  0 <= n.
Proof.
  induction n.
  apply le_n.
  apply le_S. apply IHn. Qed.

Lemma le_n_S : forall n m : nat,
  n <= m -> S n <= S m.
Proof.
  intros n m H.
  induction H.
    apply le_n.
    apply le_S. apply IHle. Qed.

Fixpoint take {X : Type} (n : nat) (l : list X) : list X :=
  match l, n with
  | nil     , _    => nil
  | _       , O    => nil
  | cons h t, S n' => cons h (take n' t)
  end.

Fact take_length_fact : forall (X : Type) (n : nat) (l : list X),
  length (take n l) <= n.
Proof.
  intros X n.
  induction n as [| n'].
    destruct l.
      simpl. apply le_n.
      simpl. apply le_n.
    destruct l.
      simpl. apply le_0_n.
      simpl. apply le_n_S. apply IHn'. Qed.

Perusteista ku lähtee niin verbosea on.