% =================================================================
:- pred constr(bool).    
:- mode constr(in).
:- ignore constr/1.
% ===========================================================
% Program
:- pred rev(list(int),list(int)).
:- mode rev(in,out).
rev([],[]).
rev([H|T],R) :-
  rev(T,S),
  snoc(S,H,R).

:- pred snoc(list(int),int,list(int)).
:- mode snoc(in,in,out).  
snoc([],X,[X]).
snoc([X|Xs],Y,[X|Zs]) :-
  snoc(Xs,Y,Zs). 
% ==========================================================

% Catamorphism       % Definition of a total function
:- pred listMin(list(int),bool,int).   
:- mode listMin(in,out,out).
:- cata listMin/3-1.

listMin([],IsDef,A) :- constr( (~IsDef) & (A=0) ). % 0 can be any int.
listMin([H|T],IsDef,Min) :-  
         constr( IsDef & ( Min = ite(IsDefT, ite(H<MinT,H,MinT), H ))  ),   
         listMin(T,IsDefT,MinT).  
% ==========================================================

% Contract on rev:
:- spec rev(L,R) ==>
   listMin(L,IsDefL,N1), listMin(R,IsDefR,N2) =>
    			  constr( ( (IsDefL=IsDefR) & (N1=N2) ) ).

% Contract on snoc:
:- spec snoc(A,B,C) ==>
          listMin(A,IsDefA,N1), listMin(C,IsDefC,N2) =>
          constr( IsDefC & (N2=ite(IsDefA, ite(B<N1,B,N1), B) )). 
% ==========================================================
% Property
:- pred ff1.
ff1 :-
  constr( ~( (IsDefL=IsDefR) & (N1=N2) ) ), 
  listMin(L,IsDefL,N1),
	rev(L,R),
  listMin(R,IsDefR,N2).

:- pred ff2.
ff2 :-
      constr(~( IsDefC & (N2=ite(IsDefA, ite(B<N1,B,N1), B) ))),
      listMin(A,IsDefA,N1), listMin(C,IsDefC,N2),
      snoc(A,B,C).
% ==========================================================

% NON-CATA predicates: constr rev snoc