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