%{ This page gives a Twelf encoding of a focused [[sequent calculus]], and proves the [[cut elimination]] theorem for that focused sequent calculus. }%

%{ == Formulas == }% 

o+ : type. %name o+ A+. % Positive propositions
o- : type. %name o- A-. % Negative propositions
a+ : type. %name a+ X+. % Positive atoms
a- : type. %name a- X-. % Negative atoms


%{ ==== Suspended formulas ==== }%

s+ : type. %name s+ S+. % Suspended positive formulas
s+a : a- -> s+. % Right-biased/negative atoms 
s+p : o+ -> s+. % Right-focile/positive propositions

s- : type. %name s- S-. % Suspended negative formulas
s-a : a+ -> s-. % Left-biased/positive atoms
s-p : o- -> s-. % Left-focile/negative propositions


%{ ==== Inclusions and atomic propositions ==== }%

up   : s+ -> o-. % Embedded negative suspension
down : s- -> o+. % Embedded positive suspension
%abbrev ap-  : a- -> o- = [x] up (s+a x). 
%abbrev ap+  : a+ -> o+ = [x] down (s-a x). 



%{ === Connectives === }%

-o : o+ -> o- -> o-. % implication (lolli)
%infix right 3 -o.

v : o+ -> o+ -> o+.  % or (oplus)
%infix right 4 v.
zero : o+.           % the unit of or

@ : o+ -> o+ -> o+.  % positive and (tensor)
%infix right 6 @.
& : o- -> o- -> o-.  % negative and (amp)
%infix right 5 &.
one : o+.            % the unit of tensor
true : o-.           % the unit of amp





%{ == Focused sequent calculus == }%

%{ === Ordered contexts === }%

ps : type. 
%name ps PS.

# : ps. 
, : o+ -> ps -> ps. %infix right 1 ,.



%{ === Judgments === }%

inv  : ps -> o- -> type.  % Right-active inversion 
inv' : ps -> s+ -> type.  % Left-active inversion

rfoc : o+ -> type.        % Right focus
lfoc : o- -> s+ -> type.  % Left focus

rsusp : s- -> type.  
lsusp : s+ -> s+ -> type.

hyp  : s- -> type.        % Inactive hypothesis
%abbrev conc   : s+ -> type = [c] inv' # c. % Neutral sequent

%block at+ : block {x: a+}.
%block at- : block {x: a-}.
%block focus : some {A : s-} block {h : hyp A}.



%{ === Structural rules === }%

deactr  : (inv' PS A+) -> inv PS (up A+).
deactl  : (hyp A- -> inv' PS C) -> (inv' (down A- , PS) C).

%{ ==== Focusing ==== }%

focus-r : rfoc A -> conc (s+p A).

focus-l : lfoc A C -> (hyp (s-p A) -> conc C). 

%{ ==== Bluring ==== }%

blur-r  : rsusp S- -> rfoc (down S-). 
play-atom+ : hyp (s-a X) -> rsusp (s-a X).
play-prop- : inv # A -> rsusp (s-p A).

blur-l  : lsusp S+ C -> lfoc (up S+) C.
play-atom- : lsusp (s+a X) (s+a X).
play-prop+ : inv' (A+ , #) C -> lsusp (s+p A+) C.



%{ === Positive connectives === }%

@l : inv' (A , B , PS) C -> inv' (A @ B , PS) C.
@r : rfoc A -> rfoc B -> rfoc (A @ B).

-or: inv (A , PS) B -> inv PS (A -o B).
-ol : rfoc A -> lfoc B C -> lfoc (A -o B) C.



%{ === Negative connectives === }%

vl : inv' (A , PS) C -> inv' (B , PS) C -> inv' (A v B , PS) C.
vr1 : rfoc A -> rfoc (A v B).
vr2 : rfoc B -> rfoc (A v B).

&l1 : lfoc A C -> lfoc (A & B) C.
&l2 : lfoc B C -> lfoc (A & B) C.
&r : inv PS A -> inv PS B -> inv PS (A & B). 



%{ == Cut admissibility == }%

%{ Top-level cuts are where the cut formula is the only thing that requires
inversion in either sequent, but the cut formula is not in focus
in the other sequent. }%

top-level- : {A-: s-} rsusp A- -> (hyp A- -> conc G) -> conc G -> type.
top-level+ : {A+: s+} conc A+  -> lsusp A+ G         -> conc G -> type.
%mode top-level+ +A +D +E -F.
%mode top-level- +A +D +E -F.

%{ The principal cuts are the "important but easy" cases where the cut formula
is being focused upon (on one hand) and inverted upon (on the other hand). }%

principal+  : {A+}  rfoc A+   -> inv' (A+ , PS) C     -> inv' PS C -> type.
principal-  : {A-}  inv PS A- -> lfoc A- C            -> inv' PS C -> type.
%mode principal+  +A +D1 +D2 -D.
%mode principal-  +A +D1 +D2 -D.

%{ The left commutative cuts happen when the cut formula is exposed
in an invertible position in one sequent, but the other sequent has secondary
inversions to do. 

The positive left-commutative cuts work the first sequent, and the
negative left-commutative cuts work on the second sequent. The ultimate
goal is the same: allow a top-level cut to be requested on one
inversion  }%

% left-commutative+ 
%    : {A+} inv' PS (p-f A+) -> inv' (A+ , #) C         -> inv' PS C -> type.
% left-commutative- 
%    : {A-} inv # A-         -> (hyp-f A- -> inv' PS C) -> inv' PS C -> type.
% left-commutative-focus+
%    : {A+} lfoc B (p-f A+)  -> inv' (A+ , #) C         -> lfoc B C  -> type. 
% left-commutative-focus- 
%    : {A-} inv # A-         -> (hyp-f A- -> lfoc B C)  -> lfoc B C  -> type.
% mode left-commutative+ +A +D +E -F.
% mode left-commutative- +A +D +E -F.
% mode left-commutative-focus+ +A +D +E -F.
% mode left-commutative-focus- +A +D +E -F.

left-commutative-focus+
   : {A+} lfoc B A+ -> lsusp A+ G -> lfoc B G -> type.
%mode left-commutative-focus+ +A +D +E -F.

left-commutative-inv+ 
   : {A+} inv' PS A+ -> lsusp A+ G -> inv' PS G -> type.
%mode left-commutative-inv+ +A +D +E -F.


left-commutative-focus-
   : {A-} rsusp A- -> (hyp A- -> lfoc B C) -> lfoc B C -> type.
%mode left-commutative-focus- +A +D +E -F.

right-commutative-focus- 
   : {A-} rsusp A- -> (hyp A- -> rfoc G) -> rfoc G -> type.
%mode right-commutative-focus- +A +D +E -F.

right-commutative-inv- 
   : {A-} rsusp A- -> (hyp A- -> inv PS G) -> inv PS G -> type.
%mode right-commutative-inv- +A +D +E -F.

left-commutative-inv- 
   : {A-} rsusp A- -> (hyp A- -> inv' PS G) -> inv' PS G -> type.
%mode left-commutative-inv- +A +D +E -F.


%{ === Positive cut formula === }%

/ : top-level+ (s+a X-) D play-atom- (D: conc (s+a X-)).
/ : top-level+ (s+p A+) (focus-r D) (play-prop+ E) F
     <- principal+ A+ D E (F: conc G).

/ : top-level+ A+ (focus-l D DH) E (focus-l F DH)
     <- left-commutative-focus+ A+ D E (F: lfoc B G).

%{ ==== Principal cut ==== }%

/ : principal+ (A @ B) (@r D1 D2) (@l E) F''
     <- principal+ A D1 E  (F': inv' (B , PS) C)
     <- principal+ B D2 F' (F'': inv' PS C).
/ : principal+ (A v B) (vr1 D) (vl EA EB) F
     <- principal+ A D EA F.
/ : principal+ (A v B) (vr2 D) (vl EA EB) F
     <- principal+ B D EB F.

/ : principal+ (down S-) (blur-r D) (deactl E) F
     <- left-commutative-inv- S- D E F.

%{ ==== Left commutative focus ==== }%

/ : left-commutative-focus+ A+ (&l1 DB) E (&l1 FB)
     <- left-commutative-focus+ A+ DB E FB.
/ : left-commutative-focus+ A+ (&l2 DC) E (&l2 FC)
     <- left-commutative-focus+ A+ DC E FC.
/ : left-commutative-focus+ A+ (-ol DB DC) E (-ol DB FC)
     <- left-commutative-focus+ A+ DC E (FC: lfoc C G).

/ : left-commutative-focus+ (s+a X-) (blur-l play-atom-) E (blur-l E).
/ : left-commutative-focus+ A+
     (blur-l (play-prop+ D)) E (blur-l (play-prop+ F))
     <- left-commutative-inv+ A+ D E F. 

%{ ==== Left commutative inversion ==== }%

/ : left-commutative-inv+ A+ (@l D) E (@l F)
     <- left-commutative-inv+ A+ D E (F: inv' (B , C , PS) G).
/ : left-commutative-inv+ A+ (vl DB DC) E (vl FB FC)
     <- left-commutative-inv+ A+ DB E (FB: inv' (B , PS) G)
     <- left-commutative-inv+ A+ DC E (FC: inv' (C , PS) G).

/ : left-commutative-inv+ A+ (deactl ([x: hyp B] D x)) E (deactl ([x] F x))
     <- {x: hyp B} left-commutative-inv+ A+ (D x) E (F x). 
/ : left-commutative-inv+ A+ (D: conc A+) E (F: conc G)
     <- top-level+ A+ D E F. % CALL UP TO TOP LEVEL, NOTHING GETS SMALLER



%{ === Negative cut formula === }%

/ : top-level- (s-a X+) (play-atom+ DH) ([h: hyp (s-a X+)] E h) (E DH).
/ : top-level- (s-p A-) (play-prop- D) ([h] focus-l (E h) h) F
     <- left-commutative-focus- (s-p A-) (play-prop- D) E E'
     <- principal- A- D E' (F: conc G).

/ : top-level- A- D ([h] focus-r (E h)) (focus-r F)
     <- right-commutative-focus- A- D E F.
/ : top-level- A- D ([h] focus-l (E h) EH) (focus-l F EH)
     <- left-commutative-focus- A- D E (F: lfoc B G).

%{ ==== Principal cut ==== }%

/ : principal- (A & B) (&r DA DB) (&l1 EA) F
     <- principal- A DA EA F.
/ : principal- (A & B) (&r DA DB) (&l2 EB) F
     <- principal- B DB EB F.
/ : principal- (A -o B) (-or D) (-ol EA EB) F
     <- principal- B D EB F1
     <- principal+ A EA F1 F. % CROSS CALL (Principal cut)

/ : principal- (up S+) (deactr D) (blur-l E) F
     <- left-commutative-inv+ S+ D E F. % CROSS-CALL (Commutative cuts)

%{ ==== Left commutative focus ==== }%

/ : left-commutative-focus- A- D ([h] &l1 (EB h)) (&l1 FB)
     <- left-commutative-focus- A- D EB (FB: lfoc B G).
/ : left-commutative-focus- A- D ([h] &l2 (EC h)) (&l2 FC)
     <- left-commutative-focus- A- D EC (FC: lfoc C G).
/ : left-commutative-focus- A- D ([h] -ol (EB h) (EC h)) (-ol FB FC)
     <- right-commutative-focus- A- D EB (FB: rfoc B)
     <- left-commutative-focus- A- D EC (FC: lfoc C G).

/ : left-commutative-focus- A- D ([h] blur-l play-atom-) (blur-l play-atom-).
/ : left-commutative-focus- A- 
     D ([h] blur-l (play-prop+ (E h))) (blur-l (play-prop+ F)) 
     <- left-commutative-inv- A- D E F.

%{ ==== Right commutative focus ==== }%

/ : right-commutative-focus- A- D ([h] @r (EB h) (EC h)) (@r FB FC)
     <- right-commutative-focus- A- D EB (FB: rfoc B)
     <- right-commutative-focus- A- D EC (FC: rfoc C).
/ : right-commutative-focus- A- D ([h] vr1 (EB h)) (vr1 FB)
     <- right-commutative-focus- A- D EB FB.
/ : right-commutative-focus- A- D ([h] vr2 (EC h)) (vr2 FC)
     <- right-commutative-focus- A- D EC FC.

/ : right-commutative-focus- (s-a X+)  D ([h] blur-r (play-atom+ h)) (blur-r D).
/ : right-commutative-focus- A- 
     D ([h] blur-r (play-atom+ H)) (blur-r (play-atom+ H)).
/ : right-commutative-focus- A- 
     D ([h] blur-r (play-prop- (E h))) (blur-r (play-prop- F))
     <- right-commutative-inv- A- D E F.

%{ ==== Right commutative inversion ==== }%

/ : right-commutative-inv- A- D ([h] &r (EB h) (EC h)) (&r FB FC)
     <- right-commutative-inv- A- D EB (FB: inv PC B)
     <- right-commutative-inv- A- D EC (FC: inv PC C).
/ : right-commutative-inv- A- D ([h] -or (E h)) (-or F)
     <- right-commutative-inv- A- D E (F: inv (B , PC) C).

/ : right-commutative-inv- A- D ([h] deactr (E h)) (deactr F)
     <- left-commutative-inv- A- D E F.

%{ ==== Left commutative inversion, negative cut formula ==== }%

/ : left-commutative-inv- A- D ([h] @l (E h)) (@l F)
     <- left-commutative-inv- A- D E F.
/ : left-commutative-inv- A- D ([h] vl (EB h) (EC h)) (vl FB FC)
     <- left-commutative-inv- A- D EB FB
     <- left-commutative-inv- A- D EC FC.

/ : left-commutative-inv- A- D ([h] deactl ([x] E h x)) (deactl ([x] F x))
     <- {x: hyp B} left-commutative-inv- A- D ([h] E h x) (F x).
/ : left-commutative-inv- A- D ([h] (E h: conc G)) F
     <- top-level- A- D E F. % CALL UP TO TOP LEVEL, NOTHING GETS SMALLER

%worlds (at+ | at- | focus)
  (top-level+ _ _ _ _)
  (top-level- _ _ _ _)
  (principal+ _ _ _ _)
  (left-commutative-focus+ _ _ _ _)
  (left-commutative-inv+ _ _ _ _)
  (principal- _ _ _ _)
  (left-commutative-focus- _ _ _ _)
  (right-commutative-focus- _ _ _ _)
  (right-commutative-inv- _ _ _ _)
  (left-commutative-inv- _ _ _ _).
%total {(A1 A2 A3 A4 A5 A6 A7 A8 A9 A10)
          [(D1 D2 D3 D4 D5 D6 D7 D8 D9 D10)
           (E1 E2 E3 E4 E5 E6 E7 E8 E9 E10)]}
  (top-level+ A1 D1 E1 F1)
  (top-level- A2 D2 E2 F2)
  (principal+ A3 D3 E3 F3)
  (left-commutative-focus+ A4 D4 E4 F4)
  (left-commutative-inv+ A5 D5 E5 F5)
  (principal- A6 D6 E6 F6)
  (left-commutative-focus- A7 D7 E7 F7)  
  (right-commutative-focus- A8 D8 E8 F8)
  (right-commutative-inv- A9 D9 E9 F9)
  (left-commutative-inv- A10 D10 E10 F10).

%{ == Examples == }%

%solve _ : {A}{B}{C} inv'  
            (ap+ A @ (ap+ B v ap+ C) , #)
            (s+p ((ap+ A @ ap+ B) v (ap+ A @ ap+ C))).
%solve _ : {A}{B} inv'
            (ap+ A @ ap+ B , #) 
            (s+p (ap+ A @ ap+ B @ ap+ B @ ap+ A)).