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

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

82% false
18% true
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

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

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

%% 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

#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))]))