Require Export Base.

Definition var := nat.

Inductive form: Type :=
  | Var: var → form
  | Fal: form
  | Imp: form → form → form
  | And: form → form → form
  | Or: form → form → form.

Definition Not s := Imp s Fal.
Definition Equi s t : form := And (Imp s t) (Imp t s).

Instance form_eq_dec : ∀ s t: form, dec (s = t).

Section EntailmentRelationProperties.

  Variable F: Type.
  Variable E: list F → F → Prop.

  (*** Generic Structural Properties ***)
  Definition Monotonicity : Prop :=
    ∀ A A' s, A <<= A' → E A s → E A' s.

  Definition Reflexivity : Prop :=
    ∀ A s, s el A → E A s.

  Definition Cut : Prop :=
    ∀ A s t, E A s → E (s::A) t → E A t.

  Definition Consistency : Prop :=
    ∃ s:F, ¬E nil s.

End EntailmentRelationProperties.

Definition context := list form.

(*** Logical Properties ***)

Definition CharFal (E: context → form → Prop) : Prop :=
  ∀ A, E A Fal ↔ ∀ s, E A s.

Definition CharImp (E: context → form → Prop) : Prop :=
  ∀ A s t, E A (Imp s t) ↔ E (s::A) t.

Definition CharAnd (E: context → form → Prop) : Prop :=
  ∀ A s t, E A (And s t) ↔ ∀ u, E (s::t::A) u → E A u.

Definition CharOr (E: context → form → Prop) : Prop :=
  ∀ A s t, E A (Or s t) ↔ ∀ u, E (s::A) u → E (t::A) u → E A u.

Fixpoint subst (sigma: var → form) (s: form) : form :=
  match s with
  | Var x ⇒ sigma x
  | Fal ⇒ Fal
  | Imp s t ⇒ Imp (subst sigma s) (subst sigma t)
  | And s t ⇒ And (subst sigma s) (subst sigma t)
  | Or s t ⇒ Or (subst sigma s) (subst sigma t)
  end.

Definition Substitution (E: context → form → Prop) :=
  ∀ A s sigma, E A s → E (map (subst sigma) A) (subst sigma s).

Definition EntailRelAllProps (E: context → form → Prop) :=
  Reflexivity E ∧ Monotonicity E ∧ Cut E ∧ Consistency E
  ∧ CharImp E ∧ CharFal E ∧ CharAnd E ∧ CharOr E
  ∧ Substitution E.

Lemma EntailRelAllProps_ext E E':
  EntailRelAllProps E → (∀ A s, E A s ↔ E' A s) → EntailRelAllProps E'.

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
  | genAL A s t u: (And s t) el A → gen (s::t::A) u → gen A u
  | genAR A s t: gen A s → gen A t → gen A (And s t)
  | genOL A s t u: (Or s t) el A → gen (s::A) u → gen (t::A) u → gen A u
  | genOR1 A s t: gen A s → gen A (Or s t)
  | genOR2 A s t: gen A t → gen A (Or s t).

(* Hints for auto to use rules of gen *)
Hint Constructors gen.

Lemma genA: Reflexivity gen.

Hint Resolve genA.

Lemma gen_mono: Monotonicity gen.

Lemma genW A B s: gen A s → A <<= B → gen B s.

Lemma gen_GCut A s B u:
  gen A s → gen B u → gen (A ++ rem B s) u.
Lemma gen_cut: Cut gen.

Lemma genCW A s t: gen A s → gen [s] t → gen A t.

Lemma gen_NoFal: ¬ gen [] Fal.

Lemma gen_cons: Consistency gen.

Lemma gen_imp: CharImp gen.

Lemma gen_fal: CharFal gen.

Lemma gen_and: CharAnd gen.

Lemma gen_and_both A s t: gen A (And s t) → gen A s ∧ gen A t.

Lemma gen_or: CharOr gen.

Lemma gen_subst: Substitution gen.

Lemma gen_EntailRelation: EntailRelAllProps gen.

Lemma gen_NoVar x:
  ¬ gen [] (Var x).

Lemma gen_NoNVar x:
  ¬ gen [] (Not (Var x)).

Inductive nd : context → form → Prop :=
  | ndA A s: s el A → nd A s
  | ndE A s: nd A Fal → nd A s
  | ndII A s t: nd (s::A) t → nd A (Imp s t)
  | ndIE A s t: nd A (Imp s t) → nd A s → nd A t
  | ndAI A s t: nd A s → nd A t → nd A (And s t)
  | ndAE A s t u: nd A (And s t) → nd (s::t::A) u → nd A u
  | ndOIL A s t: nd A s → nd A (Or s t)
  | ndOIR A s t: nd A t → nd A (Or s t)
  | ndOE A s t u: nd A (Or s t) → nd (s::A) u → nd (t::A) u → nd A u.

(* Hints for auto to use rules of nd *)
Hint Constructors nd.

(* nd satisfies Entailment Relation properties *)
Lemma nd_refl: Reflexivity nd.

Lemma nd_mono: Monotonicity nd.

Lemma ndW A B s: nd A s → A <<= B → nd B s.

Lemma nd_cut: Cut nd.

Lemma ndCW A s t: nd A s → nd [s] t → nd A t.

(* Lemma nd_cons: Consistency nd. --- will be proved using Gentzen *)

Lemma nd_imp: CharImp nd.

Lemma nd_fal: CharFal nd.

Lemma nd_and: CharAnd nd.

Lemma nd_or: CharOr nd.

Lemma nd_subst: Substitution nd.

Lemma gen_nd A s: gen A s → nd A s.

Lemma nd_gen A s: nd A s → gen A s.

Theorem gen_iff_nd A s: gen A s ↔ nd A s.

Lemma nd_NoFal: ¬ nd [] Fal.

Lemma nd_cons: Consistency nd.

Lemma nd_EntailRelation: EntailRelAllProps nd.

(* One-sided ND *)
Fixpoint c2f A s: form :=
  match A with
   | [] ⇒ s
   | s' :: A' ⇒ c2f A' (Imp s' s)
  end.

Lemma nd_onesided A s: nd A s ↔ nd [] (c2f A s).

Definition FK (s t : form) : form :=
  Imp s (Imp t s).

Definition FS (s t u : form) : form :=
  (Imp (Imp s (Imp t u))
       (Imp (Imp s t)
            (Imp s u))).

Inductive hil (A : context): form → Prop :=
  | hilK s t: hil A (FK s t)
  | hilS s t u: hil A (FS s t u)
  | hilAL s t: hil A (Imp (And s t) s)
  | hilAR s t: hil A (Imp (And s t) t)
  | hilAI s t: hil A (Imp s (Imp t (And s t)))
  | hilOL s t: hil A (Imp s (Or s t))
  | hilOR s t: hil A (Imp t (Or s t))
  | hilOE s t u: hil A (Imp (Imp s u) (Imp (Imp t u) (Imp (Or s t) u)))
  | hilE s: hil A (Imp Fal s)
  | hilA s: s el A → hil A s
  | hilMP s t: hil A (Imp s t) → hil A s → hil A t.

Lemma hil_nd A s :
  hil A s → nd A s.

Lemma hilAK A s t:
  hil A s → hil A (Imp t s).

Lemma hilAS A s t u :
  hil A (Imp s (Imp t u)) → hil A (Imp s t) → hil A (Imp s u).

Lemma hilI A s: hil A (Imp s s).

Lemma hilD w A v :
  hil (w::A) v → hil A (Imp w v).

Lemma nd_hil A s :
  nd A s → hil A s.

Theorem hil_iff_nd A s:
  hil A s ↔ nd A s.

Inductive tab (C D: list form): Prop :=
 | tabF : Fal el C → tab C D
 | tabC x : Var x el C → Var x el D → tab C D
 | tabIP s t: Imp s t el C → tab C (s::D) → tab (t::C) D → tab C D
 | tabIN s t: Imp s t el D → tab (s :: C) [t] → tab C D
 | tabAP s t: And s t el C → tab (s :: t :: C) D → tab C D
 | tabAN s t: And s t el D → tab C (s :: D) → tab C (t :: D) → tab C D
 | tabOP s t: Or s t el C → tab (s :: C) D → tab (t :: C) D → tab C D
 | tabON s t: Or s t el D → tab C (s :: t :: D) → tab C D.

Lemma tabLW C D: tab C D → ∀ C', C <<= C' → tab C' D.

Lemma tabRW C D: tab C D → ∀ D', D <<= D' → tab C D'.

Lemma tabW C D C' D': tab C D → C <<= C' → D <<= D' → tab C' D'.

Lemma tabCS C D s: s el C → s el D → tab C D.

Fixpoint OrAR (B: list form) : form :=
  match B with
  | [] ⇒ Fal
  | s :: B' ⇒ match B' with
               | [] ⇒ s
               | _ ⇒ Or s (OrAR B')
               end
  end.

Lemma OrAR_mono A B: A <<= B → gen [OrAR A] (OrAR B).
Lemma tab_genG C D:
  tab C D → gen C (OrAR D).

Lemma tab_gen A s:
  tab A [s] → gen A s.

Lemma gen_tab A s:
  gen A s → tab A [s].

Theorem gen_iff_tab A s:
  gen A s ↔ tab A [s].

Lemma OrAR_mono_nd A B: A <<= B → nd [OrAR A] (OrAR B).
Lemma tab_ndG C D:
  tab C D → nd C (OrAR D).

Lemma tab_nd A s:
  tab A [s] → nd A s.

Lemma nd_OrCut A s t:
  nd A (Or s t) → nd (s::A) t → nd A t.

Lemma nd_OrARcut A B s:
  nd A (OrAR (s::B)) → nd (s::A) (OrAR B) → nd A (OrAR B).

Definition sf_closed (A : context) : Prop :=
  ∀ u, u el A → match u with
                       | Imp s t | And s t | Or 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 u s t A :
  (u = Imp s t ∨ u = And s t ∨ u = Or s t) →
  s el A → t el A → sf_closed A → sf_closed (u :: A).

Fixpoint scl' (s : form) : context :=
  s :: match s with
         | Imp u v | And u v | Or 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: goal):
  dec (gamma = delta).

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
       | And s t ⇒ (A, s) el Delta ∧ (A, t) el Delta
       | Or s t ⇒ (A, s) el Delta ∨ (A, t) el Delta
       | _ ⇒ False
    end
    ∨
    ∃ v, v el A ∧
       match v with
         | Fal ⇒ True
         | Imp s t ⇒ (A, s) el Delta ∧ (rep (t::A) U, u) el Delta
         | And s t ⇒ (rep (s::t::A) U, u) el Delta
         | Or s t ⇒ (rep (s::A) U, u) 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) :
    (∀ 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.

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

Fixpoint sizeF s : nat :=
  match s with
    | Imp s1 s2 | And s1 s2 | Or s1 s2 ⇒ 1 + sizeF s1 + sizeF s2
    | _ ⇒ 1
  end.

Fixpoint depth (s: form): nat :=
  match s with
  | Var _ ⇒ 0
  | Fal ⇒ 0
  | Imp s1 s2 | And s1 s2 | Or s1 s2 ⇒
      1 + (if decision (depth s1 ≤ depth s2) then depth s2 else depth s1)
  end.

Inductive sform : Type :=
  | Pos : form → sform
  | Neg : form → sform.

Definition clause := list sform.

Notation "+ s" := (Pos s) (at level 35).
Notation "- s" := (Neg s).

Definition positive (S: sform): Prop :=
  match S with +s ⇒ True | -s ⇒ False end.

Definition negative (S: sform): Prop :=
  match S with +s ⇒ False | -s ⇒ True end.

Instance sform_eq_dec (S T: sform) : dec (S = T).

Definition uns S : form :=
  match S with +s ⇒ s | -s ⇒ Not s end.

Fixpoint size C : nat :=
  match C with
    | nil ⇒ 0
    | +s::C' | -s::C' ⇒ sizeF s + size C'
  end.

Lemma uns_pos A :
  map uns (map Pos A) = A.

Fixpoint FalFree u: Prop :=
  match u with
    | Var _ ⇒ True
    | Fal ⇒ False
    | Imp s t | And s t | Or s t ⇒ FalFree s ∧ FalFree t
  end.

Fixpoint ImpFree u: Prop :=
  match u with
    | Var _ | Fal ⇒ True
    | Imp _ _ ⇒ False
    | And s t | Or s t ⇒ ImpFree s ∧ ImpFree t
  end.

Fixpoint AndFree u: Prop :=
  match u with
    | Var _ | Fal ⇒ True
    | Imp s t ⇒ AndFree s ∧ AndFree t
    | And _ _ ⇒ False
    | Or s t ⇒ AndFree s ∧ AndFree t
  end.

Fixpoint OrFree u: Prop :=
  match u with
    | Var _ | Fal ⇒ True
    | Imp s t | And s t ⇒ OrFree s ∧ OrFree t
    | Or _ _ ⇒ False
  end.

Section ssL.
  Definition ss_closed' (S: sform) (C: clause): Prop :=
      match S with
      | +Imp s t ⇒ -s el C ∧ +t el C
      | -Imp s t ⇒ +s el C ∧ -t el C
      | +And s t ⇒ +s el C ∧ +t el C
      | -And s t ⇒ -s el C ∧ -t el C
      | +Or s t ⇒ +s el C ∧ +t el C
      | -Or s t ⇒ -s el C ∧ -t el C
      | _ ⇒ True
      end.

  Definition ss_closed (C: clause) : Prop :=
    ∀ S, S el C → ss_closed' S C.

  Definition s2b (S: sform): (bool × form) :=
    match S with | + s ⇒ (true, s) | - s ⇒ (false, s) end.

  Definition b2s (sign: bool) (s: form) := if sign then +s else -s.

  Fixpoint ssLb (sg: bool) (s: form): clause :=
    b2s sg s ::
    if sg then
      match s with
      | Imp s1 s2 ⇒ ssLb false s1 ++ ssLb true s2
      | And s1 s2 | Or s1 s2 ⇒ ssLb true s1 ++ ssLb true s2
      | _ ⇒ []
      end
    else
      match s with
      | Imp s1 s2 ⇒ ssLb true s1 ++ ssLb false s2
      | And s1 s2 | Or s1 s2 ⇒ ssLb false s1 ++ ssLb false s2
      | _ ⇒ []
      end.

  Definition ssL' (S: sform): clause := let (sg,s) := s2b S in ssLb sg s.

  Fixpoint ssL (C: clause): clause :=
    match C with
    | [] ⇒ []
    | Sf :: C' ⇒ ssL' Sf ++ ssL C'
    end.

  Lemma ss_closed'_mono S C C':
    ss_closed' S C → C <<= C' → ss_closed' S C'.

  Lemma ss_closed_app C C':
    ss_closed C → ss_closed C' → ss_closed (C ++ C').

  Lemma ssL'_self (S: sform): ss_closed' S (ssL' S).

  Lemma ssL'_in (S: sform): S el (ssL' S).

  Lemma ssL'_correct (S: sform): ss_closed (ssL' S).

  Lemma ssL_correct C: ss_closed (ssL C) ∧ C <<= ssL C.

  Lemma ssL_in C S: S el C → S el ssL C.

  Lemma ssL'_in_ssL S C S': S' el ssL' S → S el C → S' el ssL C.

  Lemma ssL_mono C D: C <<= D → ssL C <<= ssL D.

  Lemma ssL_app C D: ssL (C ++ D) === ssL C ++ ssL D.

  Lemma ssL_idempotent C: ssL C === ssL (ssL C).

  Lemma ssL'_in_ssL2 S C S': S' el ssL' S → S el ssL C → S' el ssL C.

End ssL.