Cut admissibility for sequent calculus

Executable Specification

[View cut.sig] [View cut.mod]
sig cut.

kind   i, formula         type.

type   top, bot           formula.
type   p                  i -> formula.
type   and, or, imp       formula -> formula -> formula.
type   all, ex            (i -> formula) -> formula.

type   form, hyp, conc    formula -> o.

module cut.

% The actual structure of formulas does not matter, but
% we use this predicate as a target for induction.
form top.
form bot.
form (p X).                             % an arbitrary unary predicate P
form (and A B) :- form A, form B.
form (or A B) :- form A, form B.
form (imp A B) :- form A, form B.
form (all A) :- pi x\ form (A x).
form (ex A) :- pi x\ form (A x).


conc A :- hyp A.                                             % init
conc top.                                                    % topR
conc C :- hyp bot.                                           % botL

conc (and A B) :- conc A, conc B.                            % andR
conc C :- hyp (and A B), hyp A => hyp B => conc C.           % andL

conc (or A B) :- conc A.                                     % orR_1
conc (or A B) :- conc B.                                     % orR_2
conc C :- hyp (or A B), hyp A => conc C, hyp B => conc C.    % orL

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

conc (all A) :- pi x\ conc (A x).                            % allR
conc C :- hyp (all A), hyp (A T) => conc C.                  % allL

conc (ex A) :- conc (A T).                                   % exR
conc C :- hyp (ex A), pi x\ hyp (A x) => conc C.             % exL

Reasoning

[View cut.thm]

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

%%
%% An object level sequent A_1, ..., A_n |- C is encoded as
%% {hyp A_1, ..., hyp A_n |- conc C}. We use the ctx meta-level
%% predicate to describe the structure of contexts for the conc
%% predicate. In this case, the important point is that the context
%% contains only hypotheses (hyp A) and not conclusions (conc A).
%%
%% This is based on a similar development for Twelf

Specification "cut".

Define ctx : olist -> prop by
  ctx nil ;
  ctx (hyp A :: L) := ctx L.

Theorem ctx_lemma :
  forall E L, ctx L ->  member E L -> exists A, E = hyp A.

%% We can independently prove inversion lemmas for 'bot', 'and', 'imp',
%% and 'all'.
%%
%% For 'or' and 'ex' the inversion lemmas depend on the cut admissibility
%% result and thus we prove those inversions during the cut proof.

Theorem bot_inv : forall L C,
  ctx L -> {L |- conc bot} -> {L |- conc C}.

Theorem and_left_inv : forall L C1 C2,
  ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}.

Theorem and_right_inv : forall L C1 C2,
  ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}.

Theorem imp_inv : forall L C1 C2,
  ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}.

Theorem all_inv : forall L C,
  ctx L -> {L |- conc (all C)} -> nabla x, {L |- conc (C x)}.

Theorem cut_admissibility : forall L K C,
  {form K} -> ctx L ->
    {L |- conc K} -> {L, hyp K |- conc C} -> {L |- conc C}.
% The proof is by nested induction on % 1) The size of the cut formula K % 2) The height of {L, hyp K |- conc C} induction on 1. induction on 4. intros. case H4. % Case analysis on {L, hyp K |- conc C} % conc C in context - impossible % apply ctx_lemma to _ H5. % init rule case H5. case H7. case H6. search. apply ctx_lemma to H2 H8. case H6. search. % topR - C = top search. % botL case H5. case H7. % essential case - K = bot case H6. apply bot_inv to H2 H3 with C = C. search. % commutative case apply ctx_lemma to H2 H8. case H6. search. % andR - C = and A B apply IH1 to H1 _ H3 H5. apply IH1 to H1 _ H3 H6. search. % andL apply IH1 to H1 _ H3 H6. case H5. case H9. case H8. % essential case - K = and A B apply and_left_inv to _ H3. apply and_right_inv to _ H3. case H1. apply IH to H12 _ H10 H7. apply IH to H13 _ H11 H14. search. % commutative case apply ctx_lemma to H2 H10. case H8. search. % orR_1 - C = or A B apply IH1 to H1 H2 H3 H5. search. % orR_2 - C = or A B apply IH1 to H1 H2 H3 H5. search. % orL apply IH1 to H1 _ H3 H6. apply IH1 to H1 _ H3 H7. case H5. case H11. case H10. % essential case - K = or A B % A nested inversion lemma for 'or' assert (forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}). induction on 2. intros. case H13. search. search. apply IH2 to _ H17 H14 H15. search. case H1. apply IH to H17 H12 H16 H14. search. case H1. apply IH to H18 H12 H16 H15. search. apply IH2 to _ H17 H14 H15. apply IH2 to _ H18 H14 H15. search. apply IH2 to _ H18 H14 H15. search. apply IH2 to _ H17 H14 H15. search. apply IH2 to _ H17 H14 H15. search. apply ctx_lemma to H12 H17. case H16. apply H12 to H2 H3 H8 H9. search. % commutative case apply ctx_lemma to H2 H12. case H10. search. % impR - C = imp A B. apply IH1 to H1 _ H3 H5. search. % impL apply IH1 to H1 _ H3 H6. apply IH1 to H1 _ H3 H7. case H5. case H11. case H10. % essential case - K = imp A B apply imp_inv to _ H3. case H1. apply IH to H13 _ H8 H12. apply IH to H14 _ H15 H9. search. % commutative case apply ctx_lemma to H2 H12. case H10. search. % allR - C = all A apply IH1 to H1 _ H3 H5. search. % allL apply IH1 to H1 _ H3 H6. case H5. case H9. case H8. % essential case - K = all A apply all_inv to _ H3. case H1. inst H10 with n1 = T. inst H11 with n1 = T. apply IH to H13 _ H12 H7. search. % commutative case apply ctx_lemma to H2 H10. case H8. search. % exR - C = ex A apply IH1 to H1 H2 H3 H5. search. % exL apply IH1 to H1 _ H3 H6. case H5. case H9. case H8. % essential case - K = ex A % A nested inversion lemma for 'ex' assert (forall L D, nabla x, ctx L -> {L |- conc (ex A)} -> {L, hyp (A x) |- conc D} -> {L |- conc D}). induction on 2. intros. case H11. search. search. apply IH2 to _ H14 H12. search. apply IH2 to _ H14 H12. apply IH2 to _ H15 H12. search. apply IH2 to _ H15 H12. search. apply IH2 to _ H14 H12. search. case H1. inst H14 with n1 = T. inst H12 with n1 = T. apply IH to H15 H10 H13 H16. search. assert {L1, hyp (A n2) |- conc D}. apply IH2 to _ H14 H15. search. apply ctx_lemma to H10 H14. case H13. apply H10 to H2 H3 H7. search. % commutative case apply ctx_lemma to H2 H10. case H8. search. case H6. case H5. apply ctx_lemma to H2 H7. case H5.