%% 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.
