Soundness and completeness for a focused logic

Executable Specification

[View focus.mod]

% Formulas
form (atom A).
form (imp B C) :- form B, form C.

% The full logic
conc B :- hyp B.
conc (imp B C) :- hyp B => conc C.
conc D :- hyp (imp B C), conc B, hyp C => conc D.

% The focused logic (two phases: focused and unfocused)
focus (atom A) A.
focus (imp B C) A :- unfocus B, hyp C => focus C A.

unfocus (imp B C) :- hyp B => unfocus C.
unfocus (atom A) :- hyp B, focus B A.

% The full logic restricted to initial cuts
conc-i (atom A) :- hyp (atom A).
conc-i (imp B C) :- hyp B => conc-i C.
conc-i D :- hyp (imp B C), conc-i B, hyp C => conc-i D.

Reasoning

[View focus.thm] [Show All Proofs] [Hide All Proofs]

Click on a command or tactic to see a detailed view of its use.

%% Soundness and completeness for a focused logic

%% All logics have the same structure for contexts

Define ctx nil.
Define 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}. [Show Proof][Hide Proof]
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}. [Show Proof][Hide Proof]
intros. case H2. apply ctx_member to H1 H3. search.

Theorem hyp_imp_form : forall L B1 B2,
  ctx L -> {L |- hyp (imp B1 B2)} -> {form B1} /\ {form B2}. [Show Proof][Hide Proof]
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}). [Show Proof][Hide Proof]
induction on 3 3. split.

  % focus -> conc
  intros. case H3.
    apply ctx_member to H1 H4.
    search.
    case H2. apply IH1 to H1 H6 H4. apply IH to _ H7 H5. search.

  % unfocus -> conc
  intros. case H3.
    apply ctx_member to H1 H4.
    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.

Theorem soundness : forall L B,
  ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}. [Show Proof][Hide Proof]
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}. [Show Proof][Hide Proof]
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}. [Show Proof][Hide Proof]
induction on 3. intros. case H3.
  apply ctx_member to H1 H4.
  case H4. apply ctx_member to H1 H5.
  apply init_form to H6 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.


%% 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}). [Show Proof][Hide Proof]
intros. induction on 5 5. split.

  % {L, hyp B2 |- unfocus C} -> {L |- unfocus C}
  intros. case H5.
    case H6. apply ctx_member to H1 H7.
    case H3. apply IH to _ _ H8 _ H6. search.
    case H6. case H8.
      search.
      apply ctx_member to H1 H9.
        apply IH1 to H1 H2 H10 H4 H7. search.

  % {L, hyp B2 |- focus B A} -> {L |- focus B A}
  intros. case H5.
    case H6. apply ctx_member to H1 H7.
    search.
    case H3. apply hyp_imp_form to H1 H2.
      apply IH to _ _ H8 _ H6. apply IH1 to _ _ H9 _ H7. search.

Theorem conc-i_complete : forall L B,
  ctx L -> {form B} -> {L |- conc-i B} -> {L |- unfocus B}. [Show Proof][Hide Proof]
induction on 3. intros. case H3.
  apply ctx_member to H1 H4.
  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.

Theorem completeness : forall L B,
  ctx L -> {form B} -> {L |- conc B} -> {L |- unfocus B}. [Show Proof][Hide Proof]
intros. apply restrict_init to H1 H2 H3.
  apply conc-i_complete to H1 H2 H4. search.