Require Export PropiL.

Inductive ndc : context → form → Prop :=
  | ndcA A s: s el A → ndc A s
  | ndcC A s: ndc (Not s :: A) Fal → ndc A s
  | ndcII A s t: ndc (s::A) t → ndc A (Imp s t)
  | ndcIE A s t: ndc A (Imp s t) → ndc A s → ndc A t
  | ndcAI A s t: ndc A s → ndc A t → ndc A (And s t)
  | ndcAE A s t u: ndc A (And s t) → ndc (s::t::A) u → ndc A u
  | ndcOIL A s t: ndc A s → ndc A (Or s t)
  | ndcOIR A s t: ndc A t → ndc A (Or s t)
  | ndcOE A s t u: ndc A (Or s t) → ndc (s::A) u → ndc (t::A) u → ndc A u.

Hint Constructors ndc.

Lemma ndc_refl: Reflexivity ndc.

Lemma ndc_mono: Monotonicity ndc.

Lemma ndcW1 A s t: ndc A s → ndc (t::A) s.

Lemma ndcW A B s: ndc A s → A <<= B → ndc B s.

Lemma ndcE A s: ndc A Fal → ndc A s.

Lemma ndc_cut: Cut ndc.

(* Lemma ndc_cons: Consistency nd. --- based on bent/genc *)

Lemma ndc_imp: CharImp ndc.

Lemma ndc_fal: CharFal ndc.

Lemma ndc_and: CharAnd ndc.

Lemma ndc_or: CharOr ndc.

Lemma ndc_subst: Substitution ndc.

Lemma nd_ndc A s: nd A s → ndc A s.

Lemma ndDN A s: nd A s → nd A (Not (Not s)).

Lemma Glivenko A s: ndc A s → nd A (Not (Not s)).

Corollary Glivenko_refute A: nd A Fal ↔ ndc A Fal.

Lemma ndc_refute A s: ndc A s ↔ ndc (Not s :: A) Fal.

Corollary nd_embeds_ndc A s: ndc A s ↔ nd (Not s :: A) Fal.

Definition assn := var → bool.

Fixpoint satis (f : assn) (s : form) : Prop :=
  match s with
    | Var x ⇒ if f x then True else False
    | Fal ⇒ False
    | Imp s1 s2 ⇒ satis f s1 → satis f s2
    | And s1 s2 ⇒ satis f s1 ∧ satis f s2
    | Or s1 s2 ⇒ satis f s1 ∨ satis f s2
  end.

Instance satis_dec : ∀ f s, dec (satis f s).

Fixpoint eval alpha s : bool :=
  match s with
    | Var x ⇒ alpha x
    | Fal ⇒ false
    | Imp s t ⇒ if eval alpha s then eval alpha t else true
    | And s t ⇒ if eval alpha s then eval alpha t else false
    | Or s t ⇒ if eval alpha s then true else eval alpha t
  end.

Lemma satis_eval alpha s :
  satis alpha s ↔ eval alpha s = true.

Lemma satis_pos_imp alpha s t :
  satis alpha (Imp s t) ↔ ¬ satis alpha s ∨ satis alpha t.

Lemma satis_neg_imp alpha s t :
  ¬ satis alpha (Imp s t) ↔ satis alpha s ∧ ¬ satis alpha t.

Lemma satis_pos_and alpha s t :
  satis alpha (And s t) ↔ satis alpha s ∧ satis alpha t.

Lemma satis_neg_and alpha s t :
  ¬ satis alpha (And s t) ↔ ¬ satis alpha s ∨ ¬ satis alpha t.

Lemma satis_pos_or alpha s t :
  satis alpha (Or s t) ↔ satis alpha s ∨ satis alpha t.

Lemma satis_neg_or alpha s t :
  ¬ satis alpha (Or s t) ↔ ¬ satis alpha s ∧ ¬ satis alpha t.

Definition valid s : Prop :=
  ∀ alpha, satis alpha s.

Lemma valid_unsat s :
  valid s ↔ ¬ ∃ alpha, satis alpha (Not s).

Definition bent A s : Prop :=
  ∀ alpha, (∀ t, t el A → satis alpha t) → satis alpha s.

Lemma ndc_bent A s: ndc A s → bent A s.

Lemma ndc_cons: Consistency ndc.

Lemma ndc_EntailRelation: EntailRelAllProps ndc.

Implicit Types x y z : var.
Implicit Types s t : form.
Implicit Types alpha beta : assn.
Implicit Types A B : context.
Implicit Types m n k : nat.
Implicit Types S T : sform.
Implicit Types C D : clause.

Fixpoint satis' alpha C : Prop :=
  match C with
    | nil ⇒ True
    | T::C' ⇒ satis alpha (uns T) ∧ satis' alpha C'
  end.

Definition sat C := ∃ alpha, satis' alpha C.

Lemma satis_iff alpha C :
  satis' alpha C ↔ ∀ S, S el C → satis alpha (uns S).

Lemma satis_in alpha C S :
  satis' alpha C → S el C → satis alpha (uns S).

Lemma satis_weak alpha C C' :
  C <<= C' → satis' alpha C' → satis' alpha C.

Lemma sat_weak C C' :
  C <<= C' → sat C' → sat C.

Definition cent C D : Prop :=
  ∀ alpha, satis' alpha C → satis' alpha D.

Lemma cent_weak C D D' :
  D <<= D' → cent C D' → cent C D.

Lemma cent_sat C D :
  cent C D → sat C → sat D.

Definition svar S : Prop :=
  match S with
    | +Var _ | -Var _ ⇒ True
    | _ ⇒ False
  end.

Definition solved C : Prop :=
  (∀ S, S el C → svar S) ∧ ∀ x, +Var x el C → ¬ -Var x el C.

Definition phi C x := if decision (+Var x el C) then true else false.

Lemma solved_phi C :
  solved C → satis' (phi C) C.

Lemma solved_sat C: solved C → sat C.

Lemma solved_sat' C: solved C → { alpha | satis' alpha C }.

Lemma solved_nil :
  solved nil.

Lemma solved_pos_var x C :
  solved C → ¬ -Var x el C → solved (+Var x :: C).

Lemma solved_neg_var x C :
  solved C → ¬ +Var x el C → solved (-Var x :: C).

Lemma cent_solved_sat C D :
  cent C D → solved C → sat D.

Record ref_pred (rho : clause → Prop) :=
  { ref_Fal: ∀ C, +Fal el C → rho C;
    ref_weak: ∀ C C', C <<= C' → rho C → rho C';
    ref_clash: ∀ x C, +Var x el C → -Var x el C → rho C;
    ref_pos_imp: ∀ s t C, rho (-s::C) → rho (+t::C) → rho (+Imp s t::C);
    ref_neg_imp: ∀ s t C, rho (+s::-t::C) → rho (-Imp s t::C);
    ref_pos_and: ∀ s t C, rho (+s::+t::C) → rho (+And s t::C);
    ref_neg_and: ∀ s t C, rho (-s::C) → rho (-t::C) → rho (-And s t::C);
    ref_pos_or: ∀ s t C, rho (+s::C) → rho (+t::C) → rho (+Or s t::C);
    ref_neg_or: ∀ s t C, rho (-s::-t::C) → rho (-Or s t::C);
    ref_sound: ∀ C, rho C → ¬ sat C }.

Lemma ref_unsat :
  ref_pred (fun C ⇒ ¬ sat C).

Lemma ref_ndc :
  ref_pred (fun C ⇒ ndc (map uns C) Fal).

Inductive rec C : clause → Type :=
  | recNil : rec C nil
  | recPF D : rec C (+Fal :: D)
  | recNF D : rec C D → rec C (-Fal ::D)
  | recPV D x : -Var x el C → rec C (+Var x :: D)
  | recPV' D x : ¬ -Var x el C → rec (+Var x :: C) D → rec C (+Var x :: D)
  | recNV D x : +Var x el C → rec C (-Var x :: D)
  | recNV' D x : ¬ +Var x el C → rec (-Var x :: C) D → rec C (-Var x :: D)
  | recPI D s t : rec C (-s :: D) → rec C (+t :: D) → rec C (+Imp s t :: D)
  | recNI D s t : rec C (+s :: -t :: D) → rec C (-Imp s t :: D)
  | recPA D s t : rec C (+s :: +t :: D) → rec C (+And s t :: D)
  | recNA D s t : rec C (-s :: D) → rec C (-t :: D) → rec C (-And s t :: D)
  | recPO D s t : rec C (+s :: D) → rec C (+t :: D) → rec C (+Or s t :: D)
  | recNO D s t : rec C (-s :: -t :: D) → rec C (-Or s t :: D).

Definition provider C D : rec C D.

Definition DNF Cs: list clause :=
  (fix F {C D: clause} (r: rec C D): list clause :=
    match r with
    | @recNil _ ⇒ [C]
    | @recPF _ _ ⇒ []
    | @recNF _ _ R ⇒ F R
    | @recPV _ _ _ _ ⇒ []
    | @recPV' _ _ _ _ R ⇒ F R
    | @recNV _ _ _ _ ⇒ []
    | @recNV' _ _ _ _ R ⇒ F R
    | @recPI _ _ _ _ R1 R2 ⇒ (F R1) ++ (F R2)
    | @recNI _ _ _ _ R ⇒ F R
    | @recPA _ _ _ _ R ⇒ F R
    | @recNA _ _ _ _ R1 R2 ⇒ (F R1) ++ (F R2)
    | @recPO _ _ _ _ R1 R2 ⇒ (F R1) ++ (F R2)
    | @recNO _ _ _ _ R ⇒ F R
    end
  ) [] Cs (provider [] Cs).

(* Compute DNF + Imp (Var 0) (Imp (Var 1) (Var 0)). *)

Section RL.
  Variable rho : clause → Prop.
  Variable Rho : ref_pred rho.

  Definition decider C D :
    rec C D → solved C →
    {E | solved E ∧ cent E (D ++ C)} + {rho (D ++ C)}.

  Lemma solved_ref C :
    {D| solved D ∧ cent D C} + {rho C}.

  Lemma refutation C :
    {sat C} + {rho C}.

  Lemma ref_iff_unsat C :
    rho C ↔ ¬ sat C.

  Lemma ref_dec C :
    dec (rho C).

End RL.

Lemma satis_pos f A :
  satis' f (map Pos A) ↔ ∀ s, s el A → satis f s.

Theorem ndc_dec_bent A s :
  dec (ndc A s).

(* Recursive Extraction ndc_dec_bent. *)

Lemma bent_iff_unsat A s :
  bent A s ↔ ¬ sat (-s :: map Pos A).

Theorem ndc_iff_sem A s:
  ndc A s ↔ bent A s.

Inductive gk3c: context → context → Prop :=
  | gk3cC A B x: Var x el A → Var x el B → gk3c A B
  | gk3cF A B: Fal el A → gk3c A B
  | gk3cIL A B s t: Imp s t el A → gk3c A (s::B) → gk3c (t::A) B → gk3c A B
  | gk3cIR A B s t: Imp s t el B → gk3c (s::A) (t::B) → gk3c A B
  | gk3cAL A B s t: And s t el A → gk3c (s::t::A) B → gk3c A B
  | gk3cAR A B s t: And s t el B → gk3c A (s::B) → gk3c A (t::B) → gk3c A B
  | gk3cOL A B s t: Or s t el A → gk3c (s::A) B → gk3c (t::A) B → gk3c A B
  | gk3cOR A B s t: Or s t el B → gk3c A (s::t::B) → gk3c A B.

Hint Constructors gk3c.

Lemma gk3cA A B s: s el A → s el B → gk3c A B.

Hint Resolve gk3cA.

Lemma gk3cLW A B: gk3c A B → ∀ A', A <<= A' → gk3c A' B.

Lemma gk3cRW A B: gk3c A B → ∀ B', B <<= B' → gk3c A B'.

Lemma gk3cW A B A' B': gk3c A B → A <<= A' → B <<= B' → gk3c A' B'.

Lemma gk3cLC A B s: gk3c (s::s::A) B → gk3c (s::A) B.

Lemma gk3cRC A B s: gk3c A (s::s::B) → gk3c A (s::B).

(*
  Troelstra & Schwichtenberg proved weakening, inversion lemmas,
  and contraction with maximum depth n of derivation trees.
  Here we have not formalized that.
*)

(* Contradiction Rules *)
Lemma gk3cFL A B s: gk3c A (s::B) → gk3c (Not s::A) B.

Lemma gk3cFR A B s: gk3c (s::A) B → gk3c A (Not s::B).

Lemma gk3cDNR A B s: gk3c A (s::B) → gk3c A (Not (Not s)::B).

Lemma gk3cDNL A B s: gk3c (s::A) B → gk3c (Not (Not s)::A) B.

Lemma gk3c_emptyR A: ¬ gk3c A [Fal] → ¬ gk3c A [].

Lemma gk3cTF' A B: A === [Imp Fal Fal] → B === [Fal] → ¬ gk3c A B.

Lemma gk3cTF: ¬gk3c [Imp Fal Fal] [Fal].

Lemma gk3c_NF': ¬ gk3c [] [Fal].

Lemma gk3c_NF1 B: B === [Fal] → ¬ gk3c [] B.

Lemma gk3c_NF: ¬ gk3c [] [Fal].

Lemma gk3c_con: ¬ gk3c [] [].

Lemma gk3c_NV' B x: B === [Var x] → ¬ gk3c [] B.

Lemma gk3c_NV x: ¬ gk3c [] [Var x].

(* From GK3c to Nc *)

Fixpoint neg (B: context): context :=
  match B with
   | [] ⇒ []
   | s :: B' ⇒ Not s :: neg B'
  end.

Lemma neg_in B s: s el B → Not s el neg B.

Lemma neg_incl B B': B <<= B' → neg B <<= neg B'.

Lemma gk3c_ndcG A B:
  gk3c A B → ndc (A ++ neg B) Fal.

Lemma gk3c_ndc A s:
  gk3c A [s] → ndc A s.

Definition gk3cCut: Prop :=
  ∀ A B A' B' s, gk3c A (s::B) → gk3c (s::A') B' → gk3c (A++A') (B++B').

Section gk3c_Cut.
  Implicit Type Cut: gk3cCut.

  (* Explosion Rule or Falsity Characterization *)
  Lemma gk3cCutE Cut A B: gk3c A [Fal] → gk3c A B.

  Lemma gk3cFL_invCut Cut A B s:
    gk3c (Not s::A) B → gk3c A (s::B).

  Lemma gk3cFR_invCut Cut A B s:
    gk3c A (Not s::B) → gk3c (s::A) B.

  Lemma gk3cDNR_invCut Cut A B s:
    gk3c A (Not (Not s)::B) → gk3c A (s::B).

  Lemma gk3cDNL_invCut Cut A B s:
    gk3c (Not (Not s)::A) B → gk3c (s::A) B.

  Example gk3c_Peirce_Cut Cut s t: gk3c [] [(Imp (Imp (Imp s t) s) s)].

  (* Equivalence with natural deduction, assuming Cut *)
  Lemma ndc_gk3cCut Cut A s:
    ndc A s → gk3c A [s].

  Theorem gk3cCut_iff_ndc Cut A s:
    gk3c A [s] ↔ ndc A s.

End gk3c_Cut.

Proposition gk3c_GCut_Var A B x:
  gk3c A B →
  ∀ A' B' : context, gk3c A' B' →
    gk3c (A ++ rem A' (Var x)) (rem B (Var x) ++ B').

Proposition gk3c_GCut_Fal A B:
  gk3c A B →
  ∀ A' B' : context, gk3c A' B' →
    gk3c (A ++ rem A' Fal) (rem B Fal ++ B').

Lemma gk3c_GCut A B A' B' s:
  gk3c A B → gk3c A' B' → gk3c (A ++ rem A' s) (rem B s ++ B').

Theorem gk3c_Cut: gk3cCut.

Lemma gk3cE A B: gk3c A [Fal] → gk3c A B.

Lemma gk3cFL_inv A B s:
  gk3c (Not s::A) B → gk3c A (s::B).

Lemma gk3cFR_inv A B s:
  gk3c A (Not s::B) → gk3c (s::A) B.

Lemma gk3cFL_iff A B s:
   gk3c (Not s::A) B ↔ gk3c A (s::B).

Lemma gk3cFR_iff A B s:
  gk3c A (Not s::B) ↔ gk3c (s::A) B.

Lemma gk3cDNR_inv A B s:
  gk3c A (Not (Not s)::B) → gk3c A (s::B).

Lemma gk3cDNL_inv A B s:
  gk3c (Not (Not s)::A) B → gk3c (s::A) B.

Lemma gk3cDNR_iff A B s:
  gk3c A (Not (Not s)::B) ↔ gk3c A (s::B).

Lemma gk3cDNL_iff A B s:
  gk3c (Not (Not s)::A) B ↔ gk3c (s::A) B.

(* Equivalence with natural deduction, cut-free *)
Lemma ndc_gk3c A s:
  ndc A s → gk3c A [s].

Theorem gk3c_iff_ndc A s:
  gk3c A [s] ↔ ndc A s.

(* Implication free formulas are equivalently derivable *)
Definition ImpFreeA A := ∀ s, s el A → ImpFree s.

Lemma gk3c_tab_ImpFreeG B:
  ImpFreeA B → gk3c [] B → tab [] B.

Lemma nd_ndc_ImpFree s:
  ImpFree s → (ndc [] s ↔ nd [] s).

Section ssL_nd_ndc.
  Lemma gk3c_tab_NegImpFreeG B:
    (¬ ∃ S, match S with | -(Imp _ _) ⇒ True | _ ⇒ False end ∧
                 S el ssL (map Neg B))
    → gk3c [] B → tab [] B.

  Lemma gk3c_tab_NegImpFree s:
    (¬ ∃ S, match S with | -(Imp _ _) ⇒ True | _ ⇒ False end ∧
                 S el ssL [-s])
    → gk3c [] [s] → tab [] [s].

  Lemma nd_ndc_NegImpFree s:
    (¬ ∃ S, match S with | -(Imp _ _) ⇒ True | _ ⇒ False end ∧
                 S el ssL [-s])
    → (ndc [] s ↔ nd [] s).

End ssL_nd_ndc.

Definition goalc := prod context context.

Instance goalc_eq_dec (gamma delta: goalc) :
  dec (gamma = delta).

Section Decidability_GK3c.
  Variable A0 B0 : context.
  Definition Uc := scl (A0 ++ B0).
  Definition Uc_sfc : sf_closed Uc := @scl_closed _.
  Definition Gammac := list_prod (power Uc) (power Uc).

  Definition stepc (Delta : list goalc) (gamma : goalc) : Prop :=
    let (A,B) := gamma in
    (∃ u, u el A ∧ (u el B ∨
       match u with
        | Fal ⇒ True
        | Imp s t ⇒ (A, rep (s::B) Uc) el Delta ∧ (rep (t::A) Uc, B) el Delta
        | And s t ⇒ (rep (s::t::A) Uc, B) el Delta
        | Or s t ⇒ (rep (s::A) Uc, B) el Delta ∧ (rep (t::A) Uc, B) el Delta
        | _ ⇒ False
       end))
    ∨
    (∃ u, u el B ∧
       match u with
        | Imp s t ⇒ (rep (s::A) Uc, rep (t::B) Uc) el Delta
        | And s t ⇒ (A, rep (s::B) Uc) el Delta ∧ (A, rep (t::B) Uc) el Delta
        | Or s t ⇒ (A, rep (s::t::B) Uc) el Delta
        | _ ⇒ False
       end).

  Instance stepc_dec Delta gamma :
    dec (stepc Delta gamma).

  Definition Lambdac : list goalc :=
    FCI.C (step := stepc) Gammac.

  Lemma lambdac_closure gamma :
    gamma el Gammac → stepc Lambdac gamma → gamma el Lambdac.

  Lemma lambdac_ind (p : goalc → Prop) :
    (∀ Delta gamma, inclp Delta p →
      gamma el Gammac → stepc Delta gamma → p gamma)
    → inclp Lambdac p.

  Lemma gk3c_lambdac A B :
    A <<= Uc → B <<= Uc → gk3c A B → (rep A Uc, rep B Uc) el Lambdac.

  Lemma lambdac_gk3c A B :
    (A,B) el Lambdac → gk3c A B.

  Theorem gk3c_dec: dec (gk3c A0 B0).

End Decidability_GK3c.

Theorem ndc_dec_gk3c A s: dec (ndc A s).

Lemma gk3c_bentG A B:
  gk3c A B → bent (A ++ neg B) Fal.

Lemma gk3c_bent A s :
  gk3c A [s] → bent A s.

Lemma ref_gk3c:
  ref_pred (fun C ⇒ gk3c (map uns C) []).

Lemma gk3c_refute A B:
  gk3c A B ↔ gk3c (A ++ neg B) [].

Lemma uns_neg B :
  map uns (map Neg B) = neg B.

Lemma gk3c_dec_ref A B: dec (gk3c A B).

Lemma gk3c_iff_sem A s :
  gk3c A [s] ↔ bent A s.

Inductive hilc (A : context): form → Prop :=
  | hilcK s t: hilc A (FK s t)
  | hilcS s t u: hilc A (FS s t u)
  | hilcAL s t: hilc A (Imp (And s t) s)
  | hilcAR s t: hilc A (Imp (And s t) t)
  | hilcAI s t: hilc A (Imp s (Imp t (And s t)))
  | hilcOL s t: hilc A (Imp s (Or s t))
  | hilcOR s t: hilc A (Imp t (Or s t))
  | hilcOE s t u: hilc A (Imp (Imp s u) (Imp (Imp t u) (Imp (Or s t) u)))
  | hilcDN s: hilc A (Imp (Not (Not s)) s)
  | hilcA s: s el A → hilc A s
  | hilcMP s t: hilc A (Imp s t) → hilc A s → hilc A t.

Lemma hilc_ndc A s :
  hilc A s → ndc A s.

Lemma hilcAK A s t:
  hilc A s → hilc A (Imp t s).

Lemma hilcAS A s t u :
  hilc A (Imp s (Imp t u)) → hilc A (Imp s t) → hilc A (Imp s u).

Lemma hilcI A s: hilc A (Imp s s).

Lemma hilcD w A v :
  hilc (w::A) v → hilc A (Imp w v).

Lemma ndc_hilc A s :
  ndc A s → hilc A s.

Theorem hilc_iff_ndc A s:
  hilc A s ↔ ndc A s.