Convert a natural deduction proof into to sequent calculus proof

Executable Specification

[View nd-to-seq.mod]

%% Natural deduction

nd (imp A B) :- nd A => nd B.
nd B :- nd (imp A B), nd A.


%% Sequent calculus

conc A :- hyp A.                                     % init
conc B :- hyp A => conc B, conc A.                   % cut

conc (imp A B) :- hyp A => conc B.                   % impR
conc C :- hyp (imp A B), conc A, hyp B => conc C.    % impL

Reasoning

[View nd-to-seq.thm] [Show All Proofs] [Hide All Proofs]

Click on a command or tactic to see a detailed view of its use.

%% Convert a natural deduction proof into to sequent calculus proof
%%
%% We consider a logic with just impliciation

Define convert nil nil.
Define convert (nd G :: L) (hyp G :: K) := convert L K.

Theorem convert_member : forall L K H,
  convert L K -> member (nd H) L -> member (hyp H) K. [Show Proof][Hide Proof]
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to H4 H3. search.

Theorem nd_to_seq_ext : forall L K G,
  {L |- nd G} -> convert L K -> {K |- conc G}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  apply convert_member to H2 H3. search.
  apply IH to H3 _. search.
  apply IH to H3 H2. apply IH to H4 H2. search.

Theorem nd_to_seq : forall G, {nd G} -> {conc G}. [Show Proof][Hide Proof]
intros. apply nd_to_seq_ext to H1 _. search.