% The actual structure of propositions does not matter, but % we use this predicate as a measure for induction. prop top. prop bot. prop (p X). % an arbitrary unary predicate P prop (and A B) :- prop A, prop B. prop (or A B) :- prop A, prop B. prop (imp A B) :- prop A, prop B. prop (all A) :- pi x\ prop (A x). prop (ex A) :- pi x\ prop (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
Click on a command or tactic to see a detailed view of its use.
%% 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. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] 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)}. [Show Proof][Hide Proof] 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}. [Show Proof][Hide Proof] % 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.