%%% Intuitionistic propositional calculus
%%% Positive fragment with implies, and, true.
%%% Operational meaning of derivations as programs.
%%% Author: Frank Pfenning, Carsten Schuermann

% Type of propositions.
o : type.
%name o A.

% Syntax: implication, plus a few constants.
=> : o -> o -> o.			%infix right 10 =>.

% Provability.
|- : o -> type.                         %prefix 9 |-.
					%name |- P.

% Axioms.
K : |- A => B => A.
S : |- (A => B => C) => (A => B) => A => C.

% Inference Rule.
MP : |- A => B -> |- A -> |- B. 

% Operational semantics

% Basic reductions
==>   : |- A -> |- A -> type.		%infix right 9 ==>.
stepK : MP (MP K X) Y ==> X. 
stepS : MP (MP (MP S X) Y) Z ==> MP (MP X Z) (MP Y Z).

% Congruence rules

congMPL : MP P1 P2 ==> MP P1 P2 
	   <- P1 ==> P1'.
congMPR : MP P1 P2 ==> MP P1 P2' 
	   <- P2 ==> P2'.

==>* : |- A -> |- A -> type.		%infix right 9 ==>*.
refl : P ==>* P.
step : P1 ==> P2 
	-> P2 ==>* P3
	-> P1 ==>* P3.	    

% Examples:

p1 = (MP (MP K S) S).

p2 = MP (MP S K) K.

p3 = MP (MP (MP S K) K) (MP (MP S K) K).

p4 = MP (MP (MP S K) K) (MP (MP K S) S).

%query 1 1  p1 ==> P.
%query 0 0  p2 ==> P.
%query 1 2  p3 ==> P.
%query 3 3  p3 ==>* P.
%query 4 4  p4 ==>* P.