POPL Tutorial/Sequent vs Natural Deduction: Solution

This is the solution to this exercise. |hidden = true

%% Syntax for Propositions %%
%sort prop %.
%name prop %.
%term top prop %.
%term and %pi prop %-> prop %-> prop %.
%term imp %pi prop %-> prop %-> prop %.
%% Natural Deduction Inference Rules %%
%sort true {_ prop} %.
%term topI true top %.
%term andI %pi (true (and A B)) %<- (true B) %<- (true A) %.
%term andE1 %pi (true A) %<- (true (and A B)) %.
%term andE2 %pi (true B) %<- (true (and A B)) %.
%term impI %pi (true (imp A B)) %<- (%pi (true A) %-> (true B)) %.
%term impE %pi (true B) %<- (true (imp A B)) %<- (true A) %.
%% Sequent Calculus %%
%sort hyp {_ prop} %.
%sort conc {_ prop} %.
%term init %pi (conc A) %<- (hyp A) %.
%term topR conc top %.
%term andL %pi (%pi (hyp (and A B)) %-> (conc C)) %<- (%pi (hyp A) %-> (hyp B) %-> (conc C)) %.
%term andR %pi (conc (and A B)) %<- (conc B) %<- (conc A) %.
%term impL %pi (%pi (hyp (imp A B)) %-> (conc C)) %<- (conc A) %<- (%pi (hyp B) %-> (conc C)) %.
%term impR %pi (conc (imp A B)) %<- (%pi (hyp A) %-> (conc B)) %.
%term cut %pi (conc B) %<- (conc A) %<- (%pi (hyp A) %-> (conc B)) %.
%%  blocks  %%
%block bhyp [A prop] {H hyp A}%.

Translation: Natural Deduction to Sequent Calculus

%sort nd-to-seq {_ true A} {_ conc A} %.
%mode nd-to-seq %in %out %.
%scope nd-to-seq %term top nd-to-seq topI topR %.
%term andI
  %pi (nd-to-seq ((%abs andI) (%the (true A) DtrueA) (%the (true B) DtrueB)) (andR DconcA DconcB))
  %<- (nd-to-seq DtrueA (%the (conc A) DconcA))
  %<- (nd-to-seq DtrueB (%the (conc B) DconcB)) %.
%scope nd-to-seq %term andE1
  %pi (nd-to-seq ((%abs andE1) (%the (true (and A B)) DtrueAB)) (cut (andL ([dA hyp A] [_] init dA)) DconcAB))
  %<- (nd-to-seq DtrueAB (%the (conc (and A B)) DconcAB)) %.
%term andE2
  %pi (nd-to-seq ((%abs andE2) (%the (true (and A B)) DtrueAB)) (cut (andL ([_] [dB hyp B] init dB)) DconcAB))
  %<- (nd-to-seq DtrueAB (%the (conc (and A B)) DconcAB)) %.
%scope nd-to-seq %term impI
  %pi (nd-to-seq ((%abs impI) ([dA true A] %the (true B) (Dimp dA))) (impR ([hA hyp A] DconcB hA)))
  %<- ({dA true A} {hA hyp A} {dtrans nd-to-seq dA (init hA)} nd-to-seq (Dimp dA) (%the (conc B) (DconcB hA))) %.
%term impE
  %pi (nd-to-seq ((%abs impE) (%the (true A) DtrueA) (%the (true (imp A B)) DtrueAB)) (cut (impL ([hB hyp B] init hB) DconcA) DconcAB))
  %<- (nd-to-seq DtrueA (%the (conc A) DconcA))
  %<- (nd-to-seq DtrueAB (%the (conc (imp A B)) DconcAB)) %.
%block truetohyp [A prop] {DA true A} {HA hyp A} {Dtrans nd-to-seq DA (init HA)}%.
%worlds (truetohyp) (nd-to-seq _ _) %.
%total D (nd-to-seq D _) %.

Translation: Sequent Calculus to Natural Deduction

%sort hyp-to-true {_ hyp A} {_ true A} %.
%mode hyp-to-true %in %out %.
%block hyptotrue [A prop] {HA hyp A} {DA true A} {Dtrans hyp-to-true HA DA}%.
%worlds (hyptotrue) (hyp-to-true _ _) %.
%total {} (hyp-to-true _ _) %.
%sort seq-to-nd {_ conc A} {_ true A} %.
%mode seq-to-nd %in %out %.
%scope seq-to-nd %term init
  %pi (seq-to-nd ((%abs init) (%the (hyp A) DhypA)) DtrueA)
  %<- (hyp-to-true DhypA (%the (true A) DtrueA)) %.
%term top seq-to-nd (%the (conc (%abs top)) topR) topI %.
%scope seq-to-nd %term andR
  %pi (seq-to-nd (%the (conc (and A B)) ((%abs andR) (%the (conc A) DconcA) (%the (conc B) DconcB))) (andI DtrueA DtrueB))
  %<- (seq-to-nd DconcA (%the (true A) DtrueA))
  %<- (seq-to-nd DconcB (%the (true B) DtrueB)) %.
%term andL
  %pi (seq-to-nd (%the (conc C) ((%abs andL) ([hA hyp A] [hB hyp B] %the (conc C) (DconcC hA hB)) (%the (hyp (and A B)) Hab))) (DtrueC (andE1 DtrueAB) (andE2 DtrueAB)))
  %<- ({hA} {dA true A} {dtransA hyp-to-true hA dA} {hB} {dB true B} {dtransB hyp-to-true hB dB} seq-to-nd (DconcC hA hB) (%the (true C) (DtrueC dA dB)))
  %<- (hyp-to-true Hab (%the (true (and A B)) DtrueAB)) %.
%scope seq-to-nd %term impR
  %pi (seq-to-nd (%the (conc (imp A B)) ((%abs impR) ([hA] %the (conc B) (DconcB hA)))) (impI ([dA] DtrueB dA)))
  %<- ({hA} {dA true A} {dtrans hyp-to-true hA dA} seq-to-nd (DconcB hA) (%the (true B) (DtrueB dA))) %.
%term impL
  %pi (seq-to-nd ((%abs impL) ([hB hyp B] %the (conc C) (DconcC hB)) (%the (conc A) DconcA) (%the (hyp (imp A B)) Hab)) (DtrueC (impE DtrueA DtrueAB)))
  %<- ({hB} {dB true B} {dtrans hyp-to-true hB dB} seq-to-nd (DconcC hB) (%the (true C) (DtrueC dB)))
  %<- (seq-to-nd DconcA (%the (true A) DtrueA))
  %<- (hyp-to-true Hab (%the (true (imp A B)) DtrueAB)) %.
%scope seq-to-nd %term cut
  %pi (seq-to-nd ((%abs cut) ([hA hyp A] %the (conc B) (DconcB hA)) (%the (conc A) DconcA)) (DtrueB DtrueA))
  %<- ({hA} {dA true A} {dtrans hyp-to-true hA dA} seq-to-nd (DconcB hA) (%the (true B) (DtrueB dA)))
  %<- (seq-to-nd DconcA (%the (true A) DtrueA)) %.
%worlds (hyptotrue) (seq-to-nd _ _) %.
%total D (seq-to-nd D _) %.