% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% ====================================================
% Program.
:- pred member(int,list(int),bool).
:- mode member(in,in,out).
member(X,[],Res) :- constr(~Res).
member(X,[Y|Ys],B) :-
      constr( B=ite(X=Y,true,B1) ) ,
      member(X,Ys,B1).

:- 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.

:- pred ff1.
ff1 :-                              % member
   constr( ~(ite(IsDefMinL, ((X=MinL) => B), ~B))),
   listMin(L,IsDefMinL,MinL),
   member(X,L,B).

%:- pred ff2.
%ff2 :-                              % listMin
%   constr( ~(MinHT =< H) ),
%   cons(H,T,HT),
%   listMin(HT,IsDefMinHT,MinHT).
%
%:- pred ff3.
%ff3 :-                              % cons
%  constr( ~( IsDefMinHT &
%            (MinHT = ite(IsDefMinT,ite(H<MinT,H,MinT),H)) ) ),
%  listMin(T,IsDefMinT,MinT), listMin(HT,IsDefMinHT,MinHT),
%  cons(H,T,HT).

% ====================================================
:- query ff1/0.
%:- query ff2/0.
%:- query ff3/0.
% ====================================================
%  Catamorphic abstraction

:- cata_abs list(int) ==> listMin(T,IsDefMinT,MinT).

% ================================================================