Library Gentzen

Require Export PropL.

Inductive gen : context -> form -> Prop :=
| genV A x : Var x el A -> gen A (Var x)
| genF A u : Fal el A -> gen A u
| genIR A s t : gen (s::A) t -> gen A (Imp s t)
| genIL A s t u : Imp s t el A -> gen A s -> gen (t::A) u -> gen A u.

Lemma gen_nd A s :
  gen A s -> nd A s.

Lemma gen_con :
  ~ gen nil Fal.

Lemma gen_DN' A x s :
  A <<= [Var x; Not (Not (Var x))] -> gen A s -> s <> Fal /\ s <> Not (Var x).

Lemma gen_DN x :
  ~ gen [Not (Not (Var x))] (Var x).

Lemma genA A s :
  s el A -> gen A s.

Lemma genW A B s :
  gen A s -> A <<= B -> gen B s.

Lemma genC' A s B u :
  gen A s -> gen B u -> gen (A ++ rem B s) u.

Lemma genC A s u :
  gen A s -> gen (s::A) u -> gen A u.

Lemma nd_gen A s :
  nd A s -> gen A s.

Theorem gen_iff_nd A s :
  gen A s <-> nd A s.

Definition sf_closed (A : context) : Prop :=
  forall u, u el A -> match u with
                 | Imp s t => s el A /\ t el A
                 | _ => True
               end.

Lemma sf_closed_app A B :
  sf_closed A -> sf_closed B -> sf_closed (A ++ B).

Lemma sf_closed_cons s t A :
  s el A -> t el A -> sf_closed A -> sf_closed (Imp s t :: A).

Fixpoint scl' (s : form) : context :=
  s :: match s with
         | Imp u v => scl' u ++ scl' v
         | _ => nil
       end.

Lemma scl'_in s :
  s el scl' s.

Lemma scl'_closed s :
  sf_closed (scl' s).

Fixpoint scl (A : context) : context :=
  match A with
    | nil => nil
    | s :: A' => scl' s ++ scl A'
  end.

Lemma scl_incl' A :
  A <<= scl A.

Lemma scl_incl A B :
  A <<= B -> A <<= scl B.

Lemma scl_closed A :
  sf_closed (scl A).

Definition goal := prod (context) form.

Instance goal_eq_dec gamma delta :
  dec (gamma = delta :> goal).

Section Decidability.
  Variable A0 : context.
  Variable s0 : form.
  Definition U := scl (s0::A0).
  Definition U_sfc : sf_closed U := @scl_closed _.
  Definition Gamma := list_prod (power U) U.

  Definition step (Delta : list goal) (gamma : goal) : Prop :=
    let (A,u) := gamma in
    match u with
       | Var _ => u el A
       | Imp s t => (rep (s::A) U, t) el Delta
       | _ => False
    end
    \/
    exists v, v el A /\
         match v with
           | Fal => True
           | Imp s t => (A, s) el Delta /\ (rep (t::A) U, u) el Delta
           | _ => False
          end.

  Instance step_dec Delta gamma :
    dec (step Delta gamma).

  Definition Lambda : list goal :=
    FCI.C (step := step) Gamma.

  Lemma lambda_closure gamma :
    gamma el Gamma -> step Lambda gamma -> gamma el Lambda.

  Lemma lambda_ind (p : goal -> Prop) :
    (forall Delta gamma, inclp Delta p -> gamma el Gamma -> step Delta gamma -> p gamma) -> inclp Lambda p.

  Lemma gen_lambda A u :
    A <<= U -> u el U -> gen A u -> (rep A U,u) el Lambda.

  Lemma lambda_gen A u :
    (A,u) el Lambda -> gen A u.

  Theorem nd_dec :
    dec (nd A0 s0).

End Decidability.