POPL Tutorial/Sequent vs Natural Deduction: Solution

This is Literate Twelf Code: here Status: %% OK %% Output: here.

This is the solution to this exercise.

Translation: Natural Deduction to Sequent Calculus

nd-to-seq : true A -> conc A -> type.
%mode nd-to-seq +X1 -X2.

-top      : nd-to-seq topI topR.

-andI     : nd-to-seq (andI (DtrueA : true A) (DtrueB : true B)) %% true (and A B)
                (andR DconcA DconcB)
             <- nd-to-seq DtrueA (DconcA : conc A)
             <- nd-to-seq DtrueB (DconcB : conc B).

-andE1    : nd-to-seq (andE1 (DtrueAB : true (and A B))) %% true A
                (cut (andL ([dA : hyp A] [_] (init dA))) DconcAB)
             <- nd-to-seq DtrueAB (DconcAB : conc (and A B)).

-andE2    : nd-to-seq (andE2 (DtrueAB : true (and A B))) %% true B
                (cut (andL ([_] [dB : hyp B] (init dB))) DconcAB)
             <- nd-to-seq DtrueAB (DconcAB : conc (and A B)).

-impI     : nd-to-seq (impI ([dA : true A] Dimp dA : true B)) %% true (imp A B)
                (impR [hA : hyp A] (DconcB hA))
             <- ({dA : true A}
                    {hA : hyp A}
                    {dtrans : nd-to-seq dA (init hA)}
                    nd-to-seq (Dimp dA) (DconcB hA : conc B)).

-impE     : nd-to-seq (impE (DtrueA : true A) (DtrueAB : true (imp A B))) %% true B
                (cut (impL ([hB : hyp B] init hB) DconcA) DconcAB)
             <- nd-to-seq DtrueA (DconcA : conc A)
             <- nd-to-seq DtrueAB (DconcAB : conc (imp A B)).

%block truetohyp : some {A : prop} block 
            {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

hyp-to-true : hyp A -> true A -> type.
%mode hyp-to-true +X1 -X2.

%block hyptotrue : some {A : prop}
           block {HA : hyp A} {DA : true A} {Dtrans : hyp-to-true HA DA}.
%worlds (hyptotrue) (hyp-to-true _ _).
%total {} (hyp-to-true _ _).


seq-to-nd : conc A -> true A -> type.
%mode seq-to-nd +X1 -X2.

-init   : seq-to-nd (init (DhypA : hyp A)) DtrueA
           <- hyp-to-true DhypA (DtrueA : true A).

-top    : seq-to-nd (topR : conc top) topI.

-andR   : seq-to-nd 
              (andR
                  (DconcA : conc A)
                  (DconcB : conc B) : conc (and A B))
              (andI
                  DtrueA
                  DtrueB)
           <- seq-to-nd DconcA (DtrueA : true A)
           <- seq-to-nd DconcB (DtrueB : true B).

-andL   : seq-to-nd 
              (andL 
                  ([hA : hyp A] [hB : hyp B] DconcC hA hB : conc C)
                  (Hab : hyp (and A B))
                : conc C)
              (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)
                      (DtrueC dA dB : true C))
           <- hyp-to-true Hab (DtrueAB : true (and A B)).

-impR   : seq-to-nd
              (impR
                  ([hA] DconcB hA : conc B) : conc (imp A B))
              (impI ([dA] DtrueB dA))
           <- ({hA} {dA : true A} {dtrans : hyp-to-true hA dA}
                  seq-to-nd (DconcB hA)
                  (DtrueB dA : true B)).

-impL   : seq-to-nd
              (impL
                  ([hB : hyp B] DconcC hB : conc C)
                  (DconcA : conc A)
                  (Hab : hyp (imp A B)))
              (DtrueC (impE DtrueA DtrueAB))
           <- ({hB} {dB : true B} {dtrans : hyp-to-true hB dB}
                  seq-to-nd (DconcC hB)
                  (DtrueC dB : true C))
           <- seq-to-nd DconcA (DtrueA : true A)
           <- hyp-to-true Hab (DtrueAB : true (imp A B)).

-cut    : seq-to-nd
              (cut
                  ([hA : hyp A] DconcB hA : conc B)
                  (DconcA : conc A))
              (DtrueB DtrueA)
           <- ({hA} {dA : true A} {dtrans : hyp-to-true hA dA}
                  seq-to-nd (DconcB hA)
                  (DtrueB dA : true B))
           <- seq-to-nd DconcA
              (DtrueA : true A).

%worlds (hyptotrue) (seq-to-nd _ _).
%total D (seq-to-nd D _).