%% Soundness and completeness for a focused logic Specification "focus". %% All logics have the same structure for contexts Define ctx : olist -> prop by ctx nil ; ctx (hyp B :: L) := {form B} /\ ctx L. Theorem ctx_member : forall E L, ctx L -> member E L -> exists B, E = hyp B /\ {form B}. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H4 H5. search. Theorem hyp_form : forall L B, ctx L -> {L |- hyp B} -> {form B}. intros. case H2. apply ctx_member to H1 H4. case H3. search. Theorem hyp_imp_form : forall L B1 B2, ctx L -> {L |- hyp (imp B1 B2)} -> {form B1} /\ {form B2}. intros. apply hyp_form to H1 H2. case H3. search. %% The focused system is sound % This requires mutual induction Theorem sound : (forall L A B, ctx L -> {form B} -> {L |- focus B A} -> {L, hyp B |- conc (atom A)}) /\ (forall L B, ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}). induction on 3 3. split. % focus -> conc intros. case H3. search. case H2. apply IH1 to H1 H6 H4. apply IH to _ H7 H5. search. apply ctx_member to H1 H5. case H4. % unfocus -> conc intros. case H3. case H2. apply IH1 to _ H6 H4. search. apply hyp_form to H1 H4. apply IH to H1 H6 H5. cut H7 with H4. search. apply ctx_member to H1 H5. case H4. Theorem soundness : forall L B, ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}. apply sound. search. %% The full logic can be restricted to initial cuts Theorem init_form : forall L B, {form B} -> member (hyp B) L -> {L |- conc-i B}. induction on 1. intros. case H1. search. apply IH to H3 _ with L = hyp B1 :: L. apply IH to H4 _ with L = hyp C :: L. search. Theorem restrict_init : forall L B, ctx L -> {form B} -> {L |- conc B} -> {L |- conc-i B}. induction on 3. intros. case H3. case H4. apply ctx_member to H1 H6. apply init_form to H7 H6. case H5. search. case H2. apply IH to _ H6 H4. search. apply hyp_imp_form to H1 H4. apply IH to H1 H7 H5. apply IH to _ H2 H6. search. apply ctx_member to H1 H5. case H4. %% The focused logic is complete Theorem lemma : forall B2, (forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} -> {L |- unfocus B1} -> {L, hyp B2 |- unfocus C} -> {L |- unfocus C}) /\ (forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} -> {L |- unfocus B1} -> {L, hyp B2 |- focus B A} -> {L |- focus B A}). intros. induction on 5 5. split. % {L, hyp B2 |- unfocus C} -> {L |- unfocus C} intros. case H5. case H3. apply IH to _ _ H8 _ H6. search. case H6. case H9. case H8. search. apply ctx_member to H1 H10. case H8. apply IH1 to H1 H2 H11 H4 H7. search. case H7. case H6. apply ctx_member to H1 H8. case H6. % {L, hyp B2 |- focus B A} -> {L |- focus B A} intros. case H5. search. case H3. apply hyp_imp_form to H1 H2. apply IH to _ _ H8 _ H6. apply IH1 to _ _ H9 _ H7. search. case H7. case H6. apply ctx_member to H1 H8. case H6. Theorem conc-i_complete : forall L B, ctx L -> {form B} -> {L |- conc-i B} -> {L |- unfocus B}. induction on 3. intros. case H3. search. case H2. apply IH to _ H6 H4. search. apply hyp_imp_form to H1 H4. apply IH to H1 H7 H5. apply IH to _ H2 H6. apply lemma with B2 = C. apply H11 to H1 H4 H2 H9 H10. search. apply ctx_member to H1 H5. case H4. Theorem completeness : forall L B, ctx L -> {form B} -> {L |- conc B} -> {L |- unfocus B}. intros. apply restrict_init to H1 H2 H3. apply conc-i_complete to H1 H2 H4. search.