voila

#lang racket

;; http://matt.might.net/articles/higher-order-list-operations/

;; Rewrite abstract mapping and folding using matching.
(define (abs-map kons nil f lst)
  (match lst
    ['()            nil]
    [(cons hd tl) 
     (kons (f hd) (abs-map kons nil f tl))]))

voila

%% For any integer X and any list of integers L,
%% if I delete X from L, then L should not contain X
prop_delete1() ->
  ?FORALL({X,L},                                  %% variables 
          {integer(), list(integer())},           %% generators
          not lists:member(X, delete_all(X, L))). %% property

voila

%% A delete_all() implementation
delete_all(X, L) ->
  delete_all(X, L, []).

delete_all(_, [], Acc) ->
  lists:reverse(Acc);
delete_all(X, [X|Rest], Acc) ->
  lists:reverse(Acc) ++ Rest;
delete_all(X, [Y|Rest], Acc) ->
  delete_all(X, Rest, [Y|Acc]).

voila

16> proper:quickcheck(listdel:prop_delete1()).
....................................................................................................
OK: Passed 100 test(s).
true

voila

%% same property but we want to see how often X belongs to L
prop_delete2() ->
  ?FORALL({X,L},                              
          {integer(), list(integer())}, 
          collect(lists:member(X, L),   %% does X belongs to L ?
          not lists:member(X, delete_all(X, L)))).

voila

17> proper:quickcheck(listdel:prop_delete2()).
....................................................................................................
OK: Passed 100 test(s).

82% false
18% true
true

voila

%% Pick X from L's elements
prop_delete3() -> 
  ?FORALL(L, 
          list(integer()), 
          ?IMPLIES(L /= [],                %% rejects empty lists
                   ?FORALL(X, elements(L), %% X always belongs to L
                           not lists:member(X,delete_all(X,L))))). 

voila

27> proper:quickcheck(listdel:prop_delete3()).
..x.x.....x...............!
Failed: After 24 test(s).
[13,13,59,10,11,24,-3,0,4]
13

Shrinking ...(3 time(s))
[13,13]
13
false

voila

delete_all(_, [], Acc) ->
  lists:reverse(Acc);
delete_all(X, [X|Rest], Acc) ->
  delete_all(X, Rest, Acc);
delete_all(X, [Y|Rest], Acc) ->
  delete_all(X, Rest, [Y|Acc]).

voila

4> proper:quickcheck(listdel:prop_delete3()).
.xx..xxx........................x.....x............x...........................x.........x..........x....x......
OK: Passed 100 test(s).
true

5> proper:quickcheck(listdel:prop_delete3(), 1000).
xxx..xx...x.xxxx..xxx.xx...x..xxxx.........x.x.........x...x..........x......x.......x....x...xx...x........x......x......x....x.......x.................x....x......x...........x.......x.....x.x..........x........x.x.................x..x.......................x..........x............x.......x......................................x.......................................x.......x.........x..x...................x..................................................................................x........x.....x..........................................................................x..x.......x..................................x......................x........x..................x...x.........x.x.....................................x.x...........................................x