% ====================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program
:- pred append(list(int),list(int),list(int)).
:- mode append(in,in,out).

append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

% =================================================================
% Catamorphisms.
% -------------
% head of a list. For hd(List,B,Res) we have B=false iff List=[]
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Res) :- constr( ((~IsDef) & Res=0)).
hd([H|T],IsDef,Res) :- constr( (IsDef & Res=H) ).

%all_leq(List,N,Res) Res iff all elements of List are =< N
:- pred all_leq(list(int),int,bool).
:- mode all_leq(in,in,out).
:- cata all_leq/3-1.

all_leq([],N,Res) :- constr( Res ).
all_leq([Y|Ys],N,Res) :- constr( Res=ite(Y=<N,ResYs,false) ), all_leq(Ys,N,ResYs).

%all_grt(List,N,Res) Res iff all elements of List are >= N
:- pred all_grt(list(int),int,bool).
:- mode all_grt(in,in,out).
:- cata all_grt/3-1.

all_grt([],N,Res) :- constr( Res ).
all_grt([Y|Ys],N,Res) :- constr( Res=ite(Y>=N,ResYs,false) ), all_grt(Ys,N,ResYs).

% Res=true iff L is weakly-descending-sorted: e.g., 9>=8>=7>=...
:- pred isDSorted(list(int),bool).
:- mode isDSorted(in,out).
:- cata isDSorted/2-1.

isDSorted([],Res) :- constr( Res ).
isDSorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    isDSorted(T,ResT),
    constr(Res = (IsDefT => (H>=HdT & ResT))).

% =================================================================
% ------ Verification of contract on append:

:- pred ff1.
ff1 :-                                            
  constr( ~((B1 & B2) => ((BXs & BYs) = BZs)) ),  
  isDSorted(Xs,BXs), isDSorted(Ys,BYs), isDSorted(Zs,BZs),
  all_grt(Xs,K,B1), all_leq(Ys,K,B2),
  append(Xs,Ys,Zs).
% =================================================================
:- query ff1/0.
% =================================================================