Require Export PropL.
Definition assn := var → bool.
Fixpoint satis (f : assn) (s : form) : Prop :=
match s with
| Var x ⇒ f x = true
| Imp s1 s2 ⇒ satis f s1 → satis f s2
| Fal ⇒ False
end.
Instance eq_bool_dec (x y : bool) : dec (x = y).
Instance satis_dec f s : dec (satis f s).
Definition sem (A : context) (s : form) : Prop :=
∀ f, (∀ t, t ∊ A → satis f t) → satis f s.
Lemma ndc_sem A s :
ndc A s → sem A s.
Lemma contra_ndc_sem A s :
¬ sem A s → ¬ ndc A s.
Lemma ndc_consistent : ¬ ndc nil Fal.
Lemma satis_pos_imp f s t :
satis f (Imp s t) ↔ ¬ satis f s ∨ satis f t.
Lemma satis_neg_imp f s t :
¬ satis f (Imp s t) ↔ satis f s ∧ ¬ satis f t.
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 uns (S : sform) : form :=
match S with +s ⇒ s | -s ⇒ Not s end.
Fixpoint satis' (f : assn) (C : clause) : Prop :=
match C with
| nil ⇒ True
| T::C' ⇒ satis f (uns T) ∧ satis' f C'
end.
Definition sat (C : clause) := ∃ f, satis' f C.
Lemma satis_iff f C :
satis' f C ↔ ∀ S, S ∊ C → satis f (uns S).
Lemma satis_in f C S :
satis' f C → S ∊ C → satis f (uns S).
Lemma satis_uns f C :
satis' f C ↔ ∀ s, s ∊ map uns C → satis f s.
Lemma satis_Pos f A :
satis' f (map Pos A) ↔ ∀ s, s ∊ A → satis f s.
Lemma sem_iff_unsat A s :
sem A s ↔ ¬ sat (-s :: map Pos A).
Lemma satis_weak f C C' :
C ⊆ C' → satis' f C' → satis' f C.
Lemma sat_weak C C' :
C ⊆ C' → sat C' → sat C.
Lemma uns_Pos A :
map uns (map Pos A) = A.
Instance sform_eq_dec (S T : sform) : dec (S = T).
Section MainResults.
Variable main : ∀ C, {sat C} + {ndc (map uns C) Fal}.
Lemma ndc_dec A s :
dec (ndc A s).
Lemma ndc_iff_sem A s :
ndc A s ↔ sem A s.
End MainResults.
Inductive sol : clause → Prop :=
| solNil : sol nil
| solPV C x : ¬ -Var x ∊ C → sol C → sol (+Var x :: C)
| solNV C x : ¬ +Var x ∊ C → sol C → sol (-Var x :: C).
Lemma sol_clash C x :
sol C → +Var x ∊ C → -Var x ∊ C → False.
Lemma sol_satis' f C :
sol C →
(∀ x, +Var x ∊ C → f x = true) →
(∀ x, -Var x ∊ C → f x = false) →
satis' f C.
Lemma sol_sat C :
sol C → sat C.
Inductive rec (C : clause) : 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 ∊ C → rec C (+Var x :: D)
| recPV' D x : ¬ -Var x ∊ C → rec (+Var x :: C) D → rec C (+Var x :: D)
| recNV D x : +Var x ∊ C → rec C (-Var x :: D)
| recNV' D x : ¬ +Var x ∊ 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).
Fixpoint sizeF (s : form) : nat :=
match s with
| Imp s1 s2 ⇒ 1 + sizeF s1 + sizeF s2
| _ ⇒ 1
end.
Fixpoint size (C : clause) : nat :=
match C with
| nil ⇒ 0
| +s::C' ⇒ sizeF s + size C'
| -s::C' ⇒ sizeF s + size C'
end.
Lemma size_recursion X (f : X → nat) (t : X → Type) :
(∀ x, (∀ y, f y < f x → t y) → t x) → ∀ x, t x.
Lemma rec_total C D : rec C D.
Section GCTP.
Variable ref : clause → Prop.
Variable ref_Fal : ∀ C, +Fal ∊ C → ref C.
Variable ref_weak : ∀ C C', C ⊆ C' → ref C → ref C'.
Variable ref_clash : ∀ x C, +Var x ∊ C → -Var x ∊ C → ref C.
Variable ref_pos_imp : ∀ s t C, ref (-s::C) → ref (+t::C) → ref (+Imp s t::C).
Variable ref_neg_imp : ∀ s t C, ref (+s::-t::C) → ref (-Imp s t::C).
Lemma rec_sat_ref C D :
rec C D → sol C → {sat (D++C)} + {ref (D++C)}.
Lemma sat_plus_ref C :
{sat C} + {ref C}.
Variable ref_sound : ∀ C, ref C → ¬ sat C.
Lemma ref_iff_unsat C :
ref C ↔ ¬ sat C.
Lemma ref_dec C :
dec (ref C).
End GCTP.