%%% 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 =>.
&  : o -> o -> o.			%infix right 11 &.
true : o.

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

% Axioms.
K : |- A => B => A.
S : |- (A => B => C) => (A => B) => A => C.
ONE : |- true.
PAIR : |- A => B => A & B.
LEFT : |- A & B => A.
RIGHT : |- A & B => B.

% 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).
stepL : MP LEFT (MP (MP PAIR X) Y) ==> X.
stepR : MP RIGHT (MP (MP PAIR X) Y) ==> Y.

% 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 (MP (MP S (MP K PAIR))
		  (MP (MP S (MP K RIGHT)) 
		     (MP (MP S K) K))))
	(MP (MP S (MP K LEFT)) (MP (MP S K) K)).

q1 = MP (MP S K) K.

q2 = MP (MP (MP S K) K) (MP (MP S K) K).

%solve r : q2 ==> Q.