1%% Cut admissibility for sequent calculus
2%%
3%% An object level sequent A_1, ..., A_n |- C is encoded as
4%% {hyp A_1, ..., hyp A_n |- conc C}. We use the ctx meta-level
5%% predicate to describe the structure of contexts for the conc
6%% predicate. In this case, the important point is that the context
7%% contains only hypotheses (hyp A) and not conclusions (conc A).
8%%
9%% This is based on a similar development for Twelf
10
11Specification "cut".
12
13Define ctx : olist -> prop by
14  ctx nil ;
15  ctx (hyp A :: L) := ctx L.
16
17Theorem ctx_lemma :
18  forall E L, ctx L ->  member E L -> exists A, E = hyp A.
19induction on 1. intros. case H1.
20  case H2.
21  case H2. search. apply IH to H3 H4. search.
22
23%% We can independently prove inversion lemmas for 'bot', 'and', 'imp',
24%% and 'all'.
25%%
26%% For 'or' and 'ex' the inversion lemmas depend on the cut admissibility
27%% result and thus we prove those inversions during the cut proof.
28
29Theorem bot_inv : forall L C,
30  ctx L -> {L |- conc bot} -> {L |- conc C}.
31induction on 2. intros. case H2.
32  search.
33  search.
34  apply IH to _ H4 with C = C. search.
35  apply IH to _ H4 with C = C. apply IH to _ H5 with C = C. search.
36  apply IH to _ H5 with C = C. search.
37  apply IH to _ H4 with C = C. search.
38  apply IH to _ H4 with C = C. search.
39  apply ctx_lemma to H1 H4. case H3.
40
41Theorem and_left_inv : forall L C1 C2,
42  ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}.
43induction on 2. intros. case H2.
44  search.
45  search.
46  search.
47  apply IH to _ H4. search.
48  apply IH to _ H4. apply IH to _ H5. search.
49  apply IH to _ H5. search.
50  apply IH to _ H4. search.
51  apply IH to _ H4. search.
52  apply ctx_lemma to H1 H4. case H3.
53
54Theorem and_right_inv : forall L C1 C2,
55  ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}.
56induction on 2. intros. case H2.
57  search.
58  search.
59  search.
60  apply IH to _ H4. search.
61  apply IH to _ H4. apply IH to _ H5. search.
62  apply IH to _ H5. search.
63  apply IH to _ H4. search.
64  apply IH to _ H4. search.
65  apply ctx_lemma to H1 H4. case H3.
66
67Theorem imp_inv : forall L C1 C2,
68  ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}.
69induction on 2. intros. case H2.
70  search.
71  search.
72  apply IH to _ H4. search.
73  apply IH to _ H4. apply IH to _ H5. search.
74  search.
75  apply IH to _ H5. search.
76  apply IH to _ H4. search.
77  apply IH to _ H4. search.
78  apply ctx_lemma to H1 H4. case H3.
79
80Theorem all_inv : forall L C,
81  ctx L -> {L |- conc (all C)} -> nabla x, {L |- conc (C x)}.
82induction on 2. intros. case H2.
83  search.
84  search.
85  apply IH to _ H4. search.
86  apply IH to _ H4. apply IH to _ H5. search.
87  apply IH to _ H5. search.
88  search.
89  apply IH to _ H4. search.
90  apply IH to _ H4. search.
91  apply ctx_lemma to H1 H4. case H3.
92
93Theorem cut_admissibility : forall L K C,
94  {form K} -> ctx L ->
95    {L |- conc K} -> {L, hyp K |- conc C} -> {L |- conc C}.
96
97% The proof is by nested induction on
98%  1) The size of the cut formula K
99%  2) The height of {L, hyp K |- conc C}
100
101induction on 1. induction on 4. intros. case H4.
102  % Case analysis on {L, hyp K |- conc C}
103
104  % conc C in context - impossible
105  % apply ctx_lemma to _ H5.
106
107  % init rule
108  case H5. case H7.
109    case H6. search.
110    apply ctx_lemma to H2 H8. case H6. search.
111
112  % topR - C = top
113  search.
114
115  % botL
116  case H5. case H7.
117    % essential case - K = bot
118    case H6. apply bot_inv to H2 H3 with C = C. search.
119    % commutative case
120    apply ctx_lemma to H2 H8. case H6. search.
121
122  % andR - C = and A B
123  apply IH1 to H1 _ H3 H5. apply IH1 to H1 _ H3 H6.
124    search.
125
126  % andL
127  apply IH1 to H1 _ H3 H6. case H5. case H9.
128    case H8.
129    % essential case - K = and A B
130    apply and_left_inv to _ H3. apply and_right_inv to _ H3. case H1.
131      apply IH to H12 _ H10 H7. apply IH to H13 _ H11 H14. search.
132
133    % commutative case
134    apply ctx_lemma to H2 H10. case H8.
135    search.
136
137  % orR_1 - C = or A B
138  apply IH1 to H1 H2 H3 H5. search.
139
140  % orR_2 - C = or A B
141  apply IH1 to H1 H2 H3 H5. search.
142
143  % orL
144  apply IH1 to H1 _ H3 H6. apply IH1 to H1 _ H3 H7. case H5. case H11.
145    case H10.
146    % essential case - K = or A B
147    % A nested inversion lemma for 'or'
148    assert (forall L D, ctx L -> {L |- conc (or A B)} ->
149                          {L, hyp A |- conc D} -> {L, hyp B |- conc D} ->
150                          {L |- conc D}).
151      induction on 2. intros. case H13.
152        search.
153        search.
154        apply IH2 to _ H17 H14 H15. search.
155        case H1. apply IH to H17 H12 H16 H14. search.
156        case H1. apply IH to H18 H12 H16 H15. search.
157        apply IH2 to _ H17 H14 H15. apply IH2 to _ H18 H14 H15. search.
158        apply IH2 to _ H18 H14 H15. search.
159        apply IH2 to _ H17 H14 H15. search.
160        apply IH2 to _ H17 H14 H15. search.
161        apply ctx_lemma to H12 H17. case H16.
162
163    apply H12 to H2 H3 H8 H9. search.
164
165    % commutative case
166    apply ctx_lemma to H2 H12. case H10.
167    search.
168
169  % impR - C = imp A B.
170  apply IH1 to H1 _ H3 H5. search.
171
172  % impL
173  apply IH1 to H1 _ H3 H6. apply IH1 to H1 _ H3 H7. case H5. case H11.
174    case H10.
175    % essential case - K = imp A B
176    apply imp_inv to _ H3. case H1.
177      apply IH to H13 _ H8 H12. apply IH to H14 _ H15 H9. search.
178
179    % commutative case
180    apply ctx_lemma to H2 H12. case H10.
181    search.
182
183  % allR - C = all A
184  apply IH1 to H1 _ H3 H5. search.
185
186  % allL
187  apply IH1 to H1 _ H3 H6. case H5. case H9.
188    case H8.
189    % essential case - K = all A
190    apply all_inv to _ H3. case H1.
191      inst H10 with n1 = T. inst H11 with n1 = T.
192        apply IH to H13 _ H12 H7. search.
193
194    % commutative case
195    apply ctx_lemma to H2 H10. case H8.
196    search.
197
198  % exR - C = ex A
199  apply IH1 to H1 H2 H3 H5. search.
200
201  % exL
202  apply IH1 to H1 _ H3 H6. case H5. case H9. case H8.
203    % essential case - K = ex A
204    % A nested inversion lemma for 'ex'
205    assert (forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
206                                   {L, hyp (A x) |- conc D} ->
207                                   {L |- conc D}).
208      induction on 2. intros. case H11.
209        search.
210        search.
211        apply IH2 to _ H14 H12. search.
212        apply IH2 to _ H14 H12. apply IH2 to _ H15 H12. search.
213        apply IH2 to _ H15 H12. search.
214        apply IH2 to _ H14 H12. search.
215        case H1. inst H14 with n1 = T. inst H12 with n1 = T.
216          apply IH to H15 H10 H13 H16. search.
217        assert {L1, hyp (A n2) |- conc D}.
218          apply IH2 to _ H14 H15. search.
219        apply ctx_lemma to H10 H14. case H13.
220
221    apply H10 to H2 H3 H7. search.
222
223    % commutative case
224    apply ctx_lemma to H2 H10. case H8.
225    search.
226
227  case H6.
228    case H5.
229    apply ctx_lemma to H2 H7. case H5.
230