%% Cut elimination for sequent calculus
%%
%% 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

Define ctx nil.
Define ctx (hyp A :: L) := ctx L.

Theorem ctx_lemma :
  forall A L, ctx L -> member (conc A) L -> false.
induction on 1. intros. case H1.
  case H2.
  case H2. apply IH to H3 H4.


%% 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}.
induction on 2. intros. case H2.
  apply ctx_lemma to H1 H3.
  search.
  search.
  apply IH to _ H4 with C = C. search.
  apply IH to _ H4 with C = C. apply IH to _ H5 with C = C. search.
  apply IH to _ H5 with C = C. search.
  apply IH to _ H4 with C = C. search.
  apply IH to _ H4 with C = C. search.

Theorem and_left_inv : forall L C1 C2,
  ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}.
induction on 2. intros. case H2.
  apply ctx_lemma to H1 H3.
  search.
  search.
  search.
  apply IH to _ H4. search.
  apply IH to _ H4. apply IH to _ H5. search.
  apply IH to _ H5. search.
  apply IH to _ H4. search.
  apply IH to _ H4. search.

Theorem and_right_inv : forall L C1 C2,
  ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}.
induction on 2. intros. case H2.
  apply ctx_lemma to H1 H3.
  search.
  search.
  search.
  apply IH to _ H4. search.
  apply IH to _ H4. apply IH to _ H5. search.
  apply IH to _ H5. search.
  apply IH to _ H4. search.
  apply IH to _ H4. search.

Theorem imp_inv : forall L C1 C2,
  ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}.
induction on 2. intros. case H2.
  apply ctx_lemma to H1 H3.
  search.
  search.
  apply IH to _ H4. search.
  apply IH to _ H4. apply IH to _ H5. search.
  search.
  apply IH to _ H5. search.
  apply IH to _ H4. search.
  apply IH to _ H4. search.

Theorem all_inv : forall L C,
  ctx L -> {L |- conc (all C)} -> nabla x, {L |- conc (C x)}.
induction on 2. intros. case H2.
  apply ctx_lemma to H1 H3.
  search.
  search.
  apply IH to _ H4. search.
  apply IH to _ H4. apply IH to _ H5. search.
  apply IH to _ H5. search.
  search.
  apply IH to _ H4. search.
  apply IH to _ H4. search.


Theorem cut_admissibility : forall L K C,
  {prop 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 H6.
    search. % K = C
    search. % K <> C

  % topR - C = top
  search.

  % botL
  case H5. case H6.
    % essential case - K = bot
    apply bot_inv to H2 H3 with C = C. search.

    % commutative case
    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 H8.
    % essential case - K = and A B
    apply and_left_inv to _ H3. apply and_right_inv to _ H3. case H1.
      apply IH to H11 _ H9 H7. apply IH to H12 _ H10 H13. search.

    % commutative case
    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 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 H12.
        apply ctx_lemma to H11 H15.
        search.
        search.
        apply IH2 to _ H16 H13 H14. search.
        case H1. apply IH to H16 H11 H15 H13. search.
        case H1. apply IH to H17 H11 H15 H14. search.
        apply IH2 to _ H16 H13 H14. apply IH2 to _ H17 H13 H14. search.
        apply IH2 to _ H17 H13 H14. search.
        apply IH2 to _ H16 H13 H14. search.
        apply IH2 to _ H16 H13 H14. search.

    apply H11 to H2 H3 H8 H9. search.

    % commutative case
    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 H10.
    % essential case - K = imp A B
    apply imp_inv to _ H3. case H1.
      apply IH to H12 _ H8 H11. apply IH to H13 _ H14 H9. search.

    % commutative case
    search.

  % allR - C = all A
  apply IH1 to H1 _ H3 H5. search.

  % allL
  apply IH1 to H1 _ H3 H6. case H5. case H8.
    % essential case - K = all A
    apply all_inv to _ H3. case H1.
      inst H9 with n1 = T. inst H10 with n1 = T.
        apply IH to H12 _ H11 H7. search.

    % commutative case
    search.

  % exR - C = ex A
  apply IH1 to H1 H2 H3 H5. search.

  % exL
  apply IH1 to H1 _ H3 H6. case H5. 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 H10.
        apply ctx_lemma to H9 H12.
        search.
        search.
        apply IH2 to _ H13 H11. search.
        apply IH2 to _ H13 H11. apply IH2 to _ H14 H11. search.
        apply IH2 to _ H14 H11. search.
        apply IH2 to _ H13 H11. search.
        case H1. inst H13 with n1 = T. inst H11 with n1 = T.
          apply IH to H14 H9 H12 H15. search.
        assert {L1, hyp (A n2) |- conc D}.
          apply IH2 to _ H13 H14. search.

    apply H9 to H2 H3 H7. search.

    % commutative case
    search.