% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.

% =================================================================
% Program. ascending sorting
:- pred insertionsort(list(int),list(int)).
:- mode insertionsort(in,out).

insertionsort([],[]).
insertionsort([X|Xs],S) :- ord_ins(X,TS,S),
         insertionsort(Xs,TS).

:- pred ord_ins(int,list(int),list(int)).   
:- mode ord_ins(in,in,out).

ord_ins(A,[],[A]).
ord_ins(A,[B|Xs],[A,B|Xs]) :- constr( A=<B ).
ord_ins(A,[B|Xs],[B|AXs]) :- constr( A>B ), 
     ord_ins(A,Xs,AXs).
% =================================================================
% catamorphisms
:- pred listMax(list(int),bool,int).
:- mode listMax(in,out,out).
:- cata listMax/3-1.

listMax([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listMax([H|T],IsDef,MaxHT) :-
         constr( IsDef & (MaxHT = ite(IsDefT, ite(H>MaxT,H,MaxT), H )) ),
         listMax(T,IsDefT,MaxT).

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

lastElem([],IsDef,Last) :- constr( ((~IsDef) & (Last=0)) ).
lastElem([H|T],IsDef,Last) :-
         constr( IsDef & (Last=ite(IsDefT,LastT,H)) ),
         lastElem(T,IsDefT,LastT).

% =================================================================
% Verification.
% Property:
:- pred ff1.
ff1 :-      % listMax of unsorted equal lastElem of ascending, insertionsorted list 
   constr( ~(( (IsDefLMax =  IsDefSMax) & 
               (IsDefLMax =  IsDefSLast)) & 
               (IsDefLMax => ((MaxL=LastS) & (MaxL=MaxS))) )),
   listMax(L,IsDefLMax,MaxL), listMax(S,IsDefSMax,MaxS), 
   lastElem(S,IsDefSLast,LastS),
   insertionsort(L,S).

:- pred ff2.
ff2 :-      
    constr(~( (((IsDefMaxLA = IsDefLastLA) &
                 IsDefMaxLB)  & IsDefLastLB) &  
               ((IsDefMaxLA & (MaxXLA=MaxLA)) => ( (MaxLA=MaxLB) & (LastLA=LastLB) ))                     
              )),
    listMax(LA,IsDefMaxLA,MaxLA), listMax(LB,IsDefMaxLB,MaxLB),
    constr( MaxXLA = ite(X>MaxLA,X,MaxLA) ),
    lastElem(LA,IsDefLastLA,LastLA), lastElem(LB,IsDefLastLB,LastLB),
    ord_ins(X,LA,LB).

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