Require Export PropL.


Inductive sform : Type :=
| Pos : formsform
| Neg : formsform.

Definition clause := list sform.

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

Instance eq_sform_dec S T :
 dec (S = T :> sform).

Definition positive (S : sform) : Prop :=
  match S with +sTrue | -sFalse end.

Fixpoint pos (C : clause) : clause :=
  match C with
    | nilnil
    | + s :: C'+ s :: pos C'
    | - s :: C'pos C'

Lemma pos_iff S C :
  S pos C S C positive S.

Lemma pos_mono C D :
  C Dpos C pos D.

Lemma pos_idempotent C :
  pos (pos C) = pos C.

Lemma pos_incl C :
  pos C C.

Lemma pos_incl_pos A B :
  pos A Bpos A pos B.

Models and satisfaction

We consider finite Kripke models whose states are clauses. There is a transition from A to B iff all positive formulas in A are in B. A state is labelled with a variable x if it contains the signed formula +x. We will show that nd is sound and complete for this class of models.

Definition state := clause.
Definition model := list state.

Section Model.
  Variable M : model.
  Implicit Types A B C : state.

  Definition before (A B : state) : Prop :=
    A M B M pos A B.

  Lemma before_refl A :
    A Mbefore A A.

  Lemma before_tran A B C :
    before A Bbefore B Cbefore A C.

  Lemma before_in s A B :
    before A B+s A+s B.

  Fixpoint satis (A : state) (s : form) : Prop :=
    match s with
      | Var x+Var x A
      | Imp s t B, before A Bsatis B ssatis B t
      | FalFalse

  Lemma satis_not A s :
    A Msatis A (Not s) → ¬ satis A s.

  Lemma satis_mono A B s :
    before A Bsatis A ssatis B s.

  Fixpoint satis' (A : state) (C : clause) : Prop :=
    match C with
      | nilTrue
      | +s :: C'satis A s satis' A C'
      | -s :: C'¬ satis A s satis' A C'

  Lemma satis_iff A C :
    satis' A C S, S C
                     match S with
                       | +ssatis A s
                       | -s¬ satis A s

  Lemma satis_in A C S :
    satis' A CS Cmatch S with
                          | +ssatis A s
                          | -s¬ satis A s

  Lemma satis_weak C D A :
    C Dsatis' A Dsatis' A C.

  Global Instance before_forall_dec A p :
    ( B, dec (p B)) → dec ( B, before A Bp B).

  Global Instance satis_dec A s :
    dec (satis A s).

End Model.

Semantic entailment and soundness

Definition sem (A : context) (s : form) : Prop :=
   M B, B M → ( t, t Asatis M B t) → satis M B s.

Lemma nd_sem A s :
  nd A ssem A s.


Definition sat (C : clause) : Prop :=
   M A, A M satis' M A C.

Lemma sat_weak C D :
  C Dsat Dsat C.

Lemma sem_unsat A s :
  sem A s¬ sat (-s :: map Pos A).

Lemma sem_iff_unsat A s :
 sem A s ¬ sat (-s :: map Pos A).


A demo is a model satisfying certain consistency properties. We will show that every state A of a demo satifies every positive formula in A and dissatifies every negative formula in A.

Definition demo' (M : model) (A : clause) (S : sform) : Prop :=
  match S with
    | - Var x¬ +Var x A
    | + Imp s t-s A +t A
    | - Imp s t B, before M A B +s B -t B
    | + FalFalse
    | _True

Definition demo (M : model) : Prop :=
   A, A M S, S Ademo' M A S.

Definition sign (b : bool) :=
  if b then Pos else Neg.

Lemma demo_satis M A b s :
  demo MA Msign b s A
  if b then satis M A s else ¬ satis M A s.

Lemma demo_satis' M A :
  demo MA Msatis' M A A.

Intuitionistic ND cannot prove double negation

Definition DN x := Imp (Not (Not (Var x))) (Var x).

Section ND_not_DN.
  Variable x : var.
  Let A := [-DN x; + Not (Not (Var x)); - Not (Var x); -Var x].
  Let B := [+ Not (Not (Var x)); - Not (Var x); +Var x; -Fal].
  Let M := [A; B].
  Let D : demo M.

  Lemma not_nd_DN : ¬ nd nil (DN x).

End ND_not_DN.


Inductive tab : clauseProp :=
| tabF C : tab (+Fal :: C)
| tabC (x : var) C : tab (-Var x :: +Var x :: C)
| tabIP s t C : tab (-s :: C) → tab (+ t :: C) → tab (+Imp s t :: C)
| tabIN s t C : tab (+s :: -t :: pos C) → tab (-Imp s t :: C)
| tabW C C' : C' Ctab C'tab C.

Definition uns (S : sform) : form :=
  match S with +ss | -sNot s end.

Definition ndr (C : clause) : Prop :=
  nd (map uns (pos C)) Fal s, -s C nd (map uns (pos C)) s.

Lemma tab_ndr C :
  tab Cndr C.

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

Lemma pos_map_Pos A :
  pos (map Pos A) = map Pos A.

Lemma tab_nd A s :
  tab (-s :: map Pos A) → nd A s.

Main results assuming main lemma

Section MainResults.
  Variable main : C, {sat C} + {tab C}.

  Lemma nd_plus_not_sem A s :
    {nd A s} + {¬ sem A s}.

  Lemma nd_dec A s :
    dec (nd A s).

  Lemma nd_iff_sem A s :
    nd A s sem A s.

End MainResults.