%%% Judgmental S5
%%% Author: Frank Pfenning
%%% 
%%% Following:
%%% A Symmetric Modal Lambda Calculus for Distributed Computing
%%% Tom Murphy, Karl Crary, Robert Harper, and Frank Pfenning
%%% Draft from Jan 2004

world : type.				%name world W o.
prop : type.				%name prop A.

%%% Natural deduction

@ : prop -> world -> type.		%name @ N.
%infix none 1 @.

% Implication
=> : prop -> prop -> prop.
%infix right 8 =>.
=>I : (A @ W -> B @ W) -> (A => B @ W).
=>E : (A => B @ W) -> A @ W -> B @ W.

% Necessity
! : prop -> prop.
%prefix 9 !.
!I : ({o:world} A @ o) -> ! A @ W.
!E : ! A @ W -> A @ W.
!G : ! A @ W' -> ! A @ W.

% Possibility
? : prop -> prop.
%prefix 9 ?.
?I : A @ W -> ? A @ W.
?E : ? A @ W -> ({o:world} A @ o -> C @ W) -> C @ W.
?G : ? A @ W' -> ? A @ W.

%%% Sequent calculus (SS5)

hyp : prop -> world -> type.		%name hyp H h.
conc : prop -> world -> type.		%name conc D.

% Judgmental rules
init : hyp A W -> conc A W.

% Implication
=>R : (hyp A W -> conc B W)
       -> conc (A => B) W.
=>L : conc A W
       -> (hyp B W -> conc C U)
       -> (hyp (A => B) W -> conc C U).

% Necessity
!R : ({o:world} conc A o)
      -> conc (! A) W.
!L : (hyp A W' -> conc C U)
      -> (hyp (! A) W -> conc C U).

% Possibility
?R : conc A W'
      -> conc (? A) W.
?L : ({o:world} hyp A o -> conc C U)
      -> (hyp (? A) W -> conc C U).

%%% Admissibility of Cut

cut : {A:prop} conc A W -> (hyp A W -> conc C U) -> conc C U -> type.
%mode cut +A +D +E -F.

% Initial cuts
ci_l : cut A (init H) ([h] E h) (E H).
ci_r : cut A D ([h] init h) D.

% Principal cuts
c_=> : cut (A1 => A2) (=>R ([h1] D2 h1)) ([h] =>L (E1 h) ([h2] E2 h h2) h) F
	<- cut (A1 => A2) (=>R ([h1] D2 h1)) ([h] E1 h) E1'
	<- ({h2:hyp A2 W} cut (A1 => A2) (=>R ([h1] D2 h1)) ([h] E2 h h2) (E2' h2))
	<- cut A1 E1' ([h1] D2 h1) F1
	<- cut A2 F1 ([h2] E2' h2) F.
c_! : cut (! A1) (!R ([o] D1 o)) ([h] !L ([h1] E1 h h1) h) F
       <- ({h1:hyp A1 W'} cut (! A1) (!R ([o] D1 o)) ([h] E1 h h1) (E1' h1))
       <- cut A1 (D1 W') ([h1] E1' h1) F.
c_? : cut (? A1) (?R D1) ([h] ?L ([o][h1] E1 h o h1) h) F
       <- ({o:world} {h1:hyp A1 o} cut (? A1) (?R D1) ([h] E1 h o h1) (E1' o h1))
       <- cut A1 D1 ([h1] E1' W' h1) F.

% Right commuting cuts
cr_init : cut A D ([h] init H) (init H).
cr_=>R : cut A D ([h] =>R ([h1] E1 h h1)) (=>R ([h1] F1 h1))
	  <- ({h1:hyp C1 U} cut A D ([h] E1 h h1) (F1 h1)).
cr_=>L : cut A D ([h] =>L (E1 h) ([h2] E2 h h2) H) (=>L F1 ([h2] F2 h2) H)
	  <- cut A D ([h] E1 h) F1
	  <- ({h2:hyp B2 U'} cut A D ([h] E2 h h2) (F2 h2)).
cr_!R : cut A D ([h] !R ([o] E1 h o)) (!R ([o] F1 o))
	 <- ({o:world} cut A D ([h] E1 h o) (F1 o)).
cr_!L : cut A D ([h] !L ([h1] E1 h h1) H) (!L ([h1] F1 h1) H)
	 <- ({h1:hyp B1 U'} cut A D ([h] E1 h h1) (F1 h1)).
cr_?R : cut A D ([h] ?R (E1 h)) (?R F1)
	 <- cut A D ([h] E1 h) F1.
cr_?L : cut A D ([h] ?L ([o][h1] E1 o h1 h) H) (?L ([o] [h1] F1 o h1) H)
	 <- ({o:world} {h1:hyp B1 o} cut A D ([h] E1 o h1 h) (F1 o h1)).

% Left commuting cuts
cl_=>L : cut A (=>L D1 ([h2] D2 h2) H) ([h] E h) (=>L D1 ([h2] F2 h2) H)
	  <- ({h2:hyp B2 U'} cut A (D2 h2) ([h] E h) (F2 h2)).
cl_!L : cut A (!L ([h1] D1 h1) H) ([h] E h) (!L ([h1] F1 h1) H)
	 <- ({h1:hyp B1 U'} cut A (D1 h1) ([h] E h) (F1 h1)).
cl_?L : cut A (?L ([o][h1] D1 o h1) H) ([h] E h) (?L ([o][h1] F1 o h1) H)
	 <- ({o:world} {h1:hyp B1 o} cut A (D1 o h1) ([h] E h) (F1 o h1)).

%block lo : block {o:world}.
%block lh : some {A:prop} {W:world} block {h:hyp A W}.
%worlds (lo | lh) (cut A D E F).
%total {A [D E]} (cut A D E F).

%%% Translation ND to SEQ

ndseq : A @ W -> conc A W -> type.	%name ndseq R r.
%mode ndseq +N -D.

% Implication
ns_=>I : ndseq (=>I ([u1] N2 u1)) (=>R ([h1] D2 h1))
	  <- ({u1:A1 @ W} {h1:hyp A1 W}
		ndseq u1 (init h1) -> ndseq (N2 u1) (D2 h1)).
ns_=>E : ndseq (=>E N2 N1) D
	  <- ndseq N2 D'
	  <- ndseq N1 D1
	  <- cut (A1 => A2) D' ([h] =>L D1 ([h2] init h2) h) D.

% Necessity
ns_!I : ndseq (!I ([o] N1 o)) (!R ([o] D1 o))
	 <- ({o:world} ndseq (N1 o) (D1 o)).
ns_!E : ndseq (!E N1) D
	 <- ndseq N1 D'
         <- cut (! A1) D' ([h] !L ([h1] init h1) h) D.
ns_!G : ndseq (!G N1) D
	 <- ndseq N1 D'
         <- cut (! A1) D' ([h] !R ([o] !L ([ho] init ho) h)) D.

% Possibility
ns_?I : ndseq (?I N1) (?R D1)
	 <- ndseq N1 D1.
ns_?E : ndseq (?E N1 ([o][u1] N2 o u1)) D
	 <- ndseq N1 D1'
	 <- ({o:world} {u1:A1 @ o} {h1:hyp A1 o} 
	       ndseq u1 (init h1) -> ndseq (N2 o u1) (D2 o h1))
	 <- cut (? A1) D1' ([h] ?L ([o][h1] D2 o h1) h) D.
ns_?G : ndseq (?G N1) D
	 <- ndseq N1 D'
	 <- cut (? A1) D' ([h] ?L ([o] [h1] ?R (init h1)) h) D.

%block luhs : some {A:prop} {W:world}
	       block {u:A @ W} {h:hyp A W} {r:ndseq u (init h)}.
%worlds (lo | luhs) (ndseq N D).
%total N (ndseq N D).

%%% Translation SEQ to ND

seqnd : conc A W -> A @ W -> type.	%name seqnd S.
hypnd : hyp A W -> A @ W -> type.	%name hypnd T t.
%mode seqnd +D -N.
%mode hypnd +H -N.

% Init
sn_init : seqnd (init H) D
	   <- hypnd H D.

% Implication
sn_=>R : seqnd (=>R ([h1] D2 h1)) (=>I ([u1] N2 u1))
	  <- ({h1:hyp A1 W} {u1:A1 @ W}
		hypnd h1 u1 -> seqnd (D2 h1) (N2 u1)).

sn_=>L : seqnd (=>L D1 ([h2] D2 h2) H) (N2 (=>E N N1))
	  <- seqnd D1 N1
	  <- ({h2:hyp A2 W} {u2:A2 @ W}
		hypnd h2 u2 -> seqnd (D2 h2) (N2 u2))
	  <- hypnd H N.

% Necessity
sn_!R : seqnd (!R ([o] D1 o)) (!I ([o] N1 o))
	 <- ({o:world} seqnd (D1 o) (N1 o)).
sn_!L : seqnd (!L ([h1] D2 h1) H) (N2 (!E (!G N)))
	 <- ({h1:hyp A1 W'} {u1:A1 @ W'}
	       hypnd h1 u1 -> seqnd (D2 h1) (N2 u1))
	 <- hypnd H N.

% Possibility
sn_?R : seqnd (?R D1) (?G (?I N1))
	 <- seqnd D1 N1.
sn_?L : seqnd (?L ([o][h1] D2 o h1) H) (?E (?G N) ([o] [u1] N2 o u1))
	 <- ({o:world} {h1:hyp A1 o} {u1:A1 @ o}
	       hypnd h1 u1 -> seqnd (D2 o h1) (N2 o u1))
	 <- hypnd H N.

%block lhut : some {A:prop} {W:world}
	       block {h:hyp A W} {u:A @ W} {t:hypnd h u}.
%worlds (lo | lhut) (seqnd D N) (hypnd H N').
%total (D H) (seqnd D N) (hypnd H N').

%%% Normal deductions
norm : A @ W -> type.			%name norm M.
elim : A @ W -> type.			%name elim E e.
%mode norm +N.
%mode elim +N.

% Coercion
n_elim : norm N <- elim N.

% Implication
n_=>I : norm (=>I ([u1] N2 u1))
	 <- ({u1:A1 @ W} elim u1 -> norm (N2 u1)).
n_=>E : elim (=>E N2 N1)
	 <- elim N2
	 <- norm N1.

% Necessity
n_!I : norm (!I ([o] N1 o))
	 <- ({o:world} norm (N1 o)).
% !E by itself is redundant, but could be admitted
%{
n_!E : elim (!E N1)
	 <- elim N1.
}%
n_!E!G : elim (!E (!G N1))
	 <- elim N1.

% Possibility
% ?I and ?E by themselves are redundant, but could be admitted
%{
n_?I : norm (?I N1)
	<- norm N1.
n_?E : norm (?E N ([o][u1] N2 o u1))
	<- elim N
	<- ({o:world} {u1:A1 @ o} elim u1 -> norm (N2 o u1)).
}%
n_?G?I : norm (?G (?I N1))
	  <- norm N1.
n_?E?G : norm (?E (?G N) ([o] [u1] N2 o u1))
	  <- elim N
	  <- ({o:world} {u1:A1 @ o} elim u1 -> norm (N2 o u1)).

%%% Translation of cut-free sequent derivations
%%% yields normal deductions

tnorm : seqnd D N -> norm N -> type.
telim : hypnd H N -> elim N -> type.
%mode tnorm +S -M.
%mode telim +T -E.

tn_init : tnorm (sn_init T) (n_elim E)
	   <- telim T E.
tn_=>R : tnorm (sn_=>R ([h1][u1][t1] S2 h1 u1 t1)) (n_=>I ([u1][e1] M2 u1 e1))
	  <- ({h1:hyp A1 W} {u1:A1 @ W} {t1:hypnd h1 u1} {e1:elim u1}
		telim t1 e1 -> tnorm (S2 h1 u1 t1) (M2 u1 e1)).
tn_=>L : tnorm (sn_=>L T ([h2][u2][e2] S2 h2 u2 e2) S1)
	  (M2 _ (n_=>E M1 E))
	  <- tnorm S1 M1
	  <- ({h2:hyp A2 W} {u2:A2 @ W} {t2:hypnd h2 u2} {e2:elim u2}
		telim t2 e2 -> tnorm (S2 h2 u2 t2) (M2 u2 e2))
	  <- telim T E.
tn_!R : tnorm (sn_!R ([o] S1 o)) (n_!I ([o] M1 o))
	 <- ({o:world} tnorm (S1 o) (M1 o)).
tn_!L : tnorm (sn_!L T ([h1][u1][t1] S2 h1 u1 t1))
	 (M2 _ (n_!E!G E))
	 <- ({h1:hyp A1 W'} {u1:A1 @ W'} {t1:hypnd h1 u1} {e1:elim u1}
	       telim t1 e1 -> tnorm (S2 h1 u1 t1) (M2 u1 e1))
	 <- telim T E.
tn_?R : tnorm (sn_?R S1) (n_?G?I M1)
	 <- tnorm S1 M1.
tn_?L : tnorm (sn_?L T ([o][h1][u1][t1] S2 o h1 u1 t1))
	 (n_?E?G ([o][u1][e1] M2 o u1 e1) E)
	 <- ({o:world} {h1:hyp A1 o} {u1:A1 @ o} {t1:hypnd h1 u1} {e1:elim u1}
	       telim t1 e1 -> tnorm (S2 o h1 u1 t1) (M2 o u1 e1))
	 <- telim T E.

%block lhute : some {A:prop} {W:world}
		block {h:hyp A W} {u:A @ W} {t:hypnd h u} {e:elim u}
		      {te:telim t e}.
%worlds (lo | lhute) (tnorm S M) (telim T E).
%total (S T) (tnorm S M) (telim T E).

%%% Global normalization corollary
%%% formulated here only for closed terms
%%% all lemmas work for open terms

normalize : A @ W -> A @ W -> type.
%mode normalize +N -N'.

nn0 : normalize N N'
       <- ndseq N D
       <- seqnd D N'.

%worlds () (normalize N N').
%total [] (normalize N N').

normalization : normalize N N' -> norm N' -> type.
%mode normalization +NN -M.

nz0 : normalization (nn0 S R) M
       <- tnorm S M.
%worlds () (normalization NN M).
%total [] (normalization N N').