module reverse.
% reverse with an accumulator.
% The "implementation" rv is hidden.
rev1 L K :-
pi rv\
(
(pi M\ rv nil M M),
(pi X\ pi M\ pi N\ pi R\ rv (X::M) R N :- rv M (X::R) N)
) =>
rv L nil K.
% reverse with hypothetical judgments.
%
rev2 L K :-
pi rv\
(
rv nil K,
pi X\ pi P\ pi Q\ rv (X :: P) Q :- rv P (X :: Q)
)
=> rv L nil.
% Reasoning about reverse:
% We show that reverse is symmetric.
% Suppose that rev L K is provable. Then
%
% pi rv\ ((pi X\ pi P\ pi Q\ rv (X :: P) Q :- rv P (X :: Q))
% => rv nil K => rv L nil)
%
% is also provable. Now, instantiate rv with
% x\y\ not (rv y x). Then we have
%
% ((pi X\ pi P\ pi Q\ not rv (X :: P) Q :- not rv P (X :: Q))
% => (not rv nil K => not rv L nil))
%
% Now since this formula is provable in intuitionistic logic, it
% is also provable in classical logic. Hence, by the contrapositive
% law, we have, in classical logic,
%
% ((pi X\ pi P\ pi Q\ rv P (X :: Q) :- rv (X :: P) Q)
% => (rv L nil => rv nil K))
%
% Since this is just definite formulas, it follows that the formula
% is also provable intuitionistically. We can now universally
% generalize on rv to get to
%
% pi rv\((pi X\ pi P\ pi Q\ rv P (X :: Q) :- rv (X :: P) Q)
% => (rv L nil => rv nil K))
%
% which means that rev K L is provable.