Soundness and completeness for a focused logic

Executable Specification

[View focus.sig] [View focus.mod]
sig focus.

kind    i, form      type.

type    atom         i -> form.
type    imp          form -> form -> form.

type    form         form -> o.
type    hyp, conc    form -> o.
type    focus        form -> i -> o.
type    unfocus      form -> o.
type    conc-i       form -> o.

module focus.

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

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

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

Theorem hyp_form : forall L B,
  ctx L -> {L |- hyp B} -> {form B}.

Theorem hyp_imp_form : forall L B1 B2,
  ctx L -> {L |- hyp (imp B1 B2)} -> {form B1} /\ {form B2}.


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


Theorem soundness : forall L B,
  ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}.


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

Theorem restrict_init : forall L B,
  ctx L -> {form B} -> {L |- conc B} -> {L |- conc-i B}.

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

Theorem conc-i_complete : forall L B,
  ctx L -> {form B} -> {L |- conc-i B} -> {L |- unfocus B}.

Theorem completeness : forall L B,
  ctx L -> {form B} -> {L |- conc B} -> {L |- unfocus B}.