% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program. 
% Delete all multiple copies on lists leaving one copy only.
:- pred list_deletecopies(list(int),list(int)).
:- mode list_deletecopies(in,out).

list_deletecopies([],[]).
list_deletecopies([X],[]). %error: [] ---> [X]
list_deletecopies([X,X|T], ResT) :- cons(X,T,XT), list_deletecopies(XT,ResT).
list_deletecopies([X,Y|T], [X|ResT]) :- constr(~(X=Y)), cons(Y,T,YT),
      list_deletecopies(YT,ResT1), deleteall(X,ResT1,ResT).

% all elements X are deleted from a list, producing a new list.
:- pred deleteall(int,list(int),list(int)).
:- mode deleteall(in,in,out).

deleteall(X,[],[]).
deleteall(X,[X|T],Res) :- deleteall(X,T,Res).
deleteall(X,[H|T],[H|ResT]) :- constr(~(X=H)), deleteall(X,T,ResT).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).

% =================================================================
% catamorphism
:- pred listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ),
         listmin(T,IsDefT,MinT).
  
% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :- 
     constr( ~((IsDefLMin = IsDefSMin) & 
     ((IsDefLMin & IsDefSMin) => (MinL=MinS)) )), 
     listmin(L,IsDefLMin,MinL),  
     listmin(S,IsDefSMin,MinS),
     list_deletecopies(L,S).

:- spec deleteall(X,L,L1) ==> listmin(L,LB,LM), listmin(L1,L1B,L1M) => constr(true).

:- spec cons(H,T,HT) ==> listmin(T,TB,TM), listmin(HT,HTB,HTM) => constr(true).

% =================================================================
:- query ff1/0.
% =================================================================