% Meta interpreter for Prolog

prove(true) :- !.
prove( (A,B) ) :- !,
        prove(A), % prove first conjunct
        prove(B). % prove second conjunct
prove(L) :-
        clause(L,B), % find appropriate clause for L
        prove(B).

:- dynamic app/3.
app([],Ys,Ys).
app([X|Xs],Ys,[X|Zs]) :- app(Xs,Ys,Zs).

% Extend the interpreter: return the length of a proof
lprove(true,0) :- !.
lprove( (A,B), L) :- !,
        lprove(A,LA), % prove first conjunct
        lprove(B,LB), % prove second conjunct
        L is LA+LB.
lprove(H,L) :-
        clause(H,B), % find appropriate clause for L
        lprove(B,LB),
        L is LB+1.