ConstructiveSemantics

A little proof of cut eliminiation for the logic FF in an unpublished paper by Reed and Pfenning.

(options removed from twelftag: check=“true”)

% Termination metric
%sort lo %.
%sort hi %.
%term * lo %.
%term s %pi lo %-> hi %.
% Syntax
%sort t+ %.
% "terms" that go in positive atoms
%sort t- %.
%name t- %.
% "terms" that go in negative atoms
%sort p %.
% positive props
%sort o %.
% negative props
%sort i %.
% worlds, frames
% Propositions
%term imp %pi p %-> o %-> o %.
%term top o %.
%term s- %pi t- %-> o %.
%term s+ %pi t+ %-> p %.
%term v %pi o %-> p %.
% Stub terms to make coverage nontrivial
%term t+/ t+ %.
%term t-/ t- %.
% Judgments
%sort j %.
%name j %.
%term /lfoc %pi o %-> t- %-> j %.
%term /rinv %pi o %-> j %.
%term /rfoc %pi p %-> j %.
%sort pf {_ j} %.
%inline lfoc [A] [T] pf (/lfoc A T) %.
%inline rinv [A] pf (/rinv A) %.
%inline rfoc [B] pf (/rfoc B) %.
%sort <= {_ t-} {_ t-} %.
%sort hyp {_ p} %.
% Stub judgment to make coverage nontrivial
%term refl <= T T %.
% Inference Rules
%term s+R %pi (hyp (s+ T)) %-> (rfoc (s+ T)) %.
%term s-L %pi (<= T T0) %-> (lfoc (s- T) T0) %.
%term vR %pi (rinv A) %-> (rfoc (v A)) %.
%term vL %pi (lfoc A T) %-> (hyp (v A)) %-> (rinv (s- T)) %.
%term topR rinv top %.
%term impR %pi (rinv (imp B A)) %<- (%pi (hyp B) %-> (rinv A)) %.
%term impL %pi (lfoc (imp B A) T) %<- (rfoc B) %<- (lfoc A T) %.
% Theorems
%sort trans {_ <= T1 T2} {_ <= T2 T3} {_ <= T1 T3} %.
%sort mono/rinv {_ <= T1 T2} {_ rinv (s- T1)} {_ rinv (s- T2)} %.
%sort mono/lfoc {_ <= T1 T2} {_ lfoc A T1} {_ lfoc A T2} %.
%sort cut/rfoc {B} {_ hi} {_ rfoc B} {_ %pi (hyp B) %-> (pf J)} {_ pf J} %.
%sort cut/rinv {A} {_ hi} {_ rinv A} {_ %pi (hyp (v A)) %-> (pf J)} {_ pf J} %.
%sort cut/pc {A} {_ lo} {_ rinv A} {_ lfoc A T} {_ rinv (s- T)} %.
% mono/rinv proof
%term mono/rinv/ %pi (mono/rinv LE (vL LF H) (vL LF' H)) %<- (mono/lfoc LE LF LF') %.
% mono/lfoc proof
%term mono/lfoc/impL %pi (mono/lfoc LE (impL LF RF) (impL LF' RF)) %<- (mono/lfoc LE LF LF') %.
%term mono/lfoc/s- %pi (mono/lfoc LE (s-L LE') (s-L LE'')) %<- (trans LE' LE LE'') %.
% cut/rfoc proof
%term cut/rfoc/v %pi (cut/rfoc (v A) TM (vR RI) PF1 PF2) %<- (cut/rinv A TM RI PF1 PF2) %.
%term cut/rfoc/s+ cut/rfoc (s+ T) TM (s+R H) PF (PF H) %.
% cut/pc proof
%term cut/pc/imp
  %pi (cut/pc (imp B A) TM (impR RI) (impL LF RF) RI'')
  %<- (cut/rfoc B (s TM) RF RI RI')
  %<- (cut/pc A TM RI' LF RI'') %.
%term cut/pc/s- %pi (cut/pc (s- T) TM IN (s-L LE) OUT) %<- (mono/rinv LE IN OUT) %.
% cut/rinv proof
%term cut/rinv/impL
  %pi (cut/rinv A TM RI ([x] impL (LF x) (RF x)) (impL LF' RF'))
  %<- (cut/rinv A TM RI LF LF')
  %<- (cut/rinv A TM RI RF RF') %.
%term cut/rinv/impR
  %pi (cut/rinv A TM RI ([x] impR ([y] D x y)) (impR Y))
  %<- ({y} cut/rinv A TM RI ([x] D x y) (Y y)) %.
%term cut/rinv/s-L cut/rinv A TM RI ([x] s-L D) (s-L D) %.
%term cut/rinv/vL/hit
  %pi (cut/rinv A (s TM) RI ([x] vL (LF x) x) Y)
  %<- (cut/rinv A (s TM) RI LF Z)
  %<- (cut/pc A TM RI Z Y) %.
%term cut/rinv/vL/miss %pi (cut/rinv A TM RI ([x] vL (LF x) H) (vL LF' H)) %<- (cut/rinv A TM RI LF LF') %.
%term cut/rinv/vR %pi (cut/rinv A TM RI ([x] vR (RI0 x)) (vR RI0')) %<- (cut/rinv A TM RI RI0 RI0') %.
%term cut/rinv/s+R cut/rinv A TM RI ([x] s+R H) (s+R H) %.
%term cut/rinv/topR cut/rinv A TM RI ([x] topR) topR %.
% Checks
%block b [P p] {x hyp P}%.
%mode trans %in %in %out %.
%mode mono/rinv %in %in %out %.
%mode mono/lfoc %in %in %out %.
%mode cut/rfoc %in %in %in %in %out %.
%mode cut/rinv %in %in %in %in %out %.
%mode cut/pc %in %in %in %in %out %.
%worlds (b) (trans _ _ _) (mono/rinv _ _ _) (mono/lfoc _ _ _) %.
%worlds (b) (cut/rfoc _ _ _ _ _) (cut/rinv _ _ _ _ _) (cut/pc _ _ _ _ _) %.
% Assume structure relation is transitive
%total LE1 (trans LE1 LE2 LE3) %.
%total (RI1 LF1) (mono/rinv LE RI1 RI2) (mono/lfoc LE' LF1 LF2) %.
%total {(B A A') (N1 N2 N3) [(RF RI RI') (PFRF1 PFRI1 LF)]} (cut/rfoc B N1 RF PFRF1 PFRF2) (cut/rinv A N2 RI PFRI1 PFRI2) (cut/pc A' N3 RI' LF RI'') %.