Library PropiLFmodel
Require Export PropiLmodel.
Lemma filter_idempotent
X (p: X → Prop) {p_dec: ∀ x, dec (p x)} (A: list X):
filter p (filter p A) = filter p A.
Section ListOperation.
Variable X: Type.
Context {eq_decX: eq_dec X}.
Implicit Type A B: list X.
(* List union and intersection *)
Fixpoint union A B :=
match A with
| [] ⇒ B
| x :: A' ⇒ if decision (x el B) then union A' B
else x :: union A' B
end.
Fixpoint inter A B :=
match A with
| [] ⇒ []
| x :: A' ⇒ if decision (x el B) then x :: inter A' B
else inter A' B
end.
Lemma union_sound A B (x:X):
x el union A B ↔ x el A ∨ x el B.
Lemma inter_sound A B (x: X):
x el inter A B ↔ x el A ∧ x el B.
Fixpoint Binter (C: list (list X)): list X :=
match C with
| [] ⇒ []
| A :: C' ⇒ inter A (Binter C')
end.
Lemma Binter_sound (C: list (list X)) (x: X):
x el Binter C → (∀ A, A el C → x el A).
Fixpoint Bunion (C: list (list X)): list X :=
match C with
| [] ⇒ []
| A :: C' ⇒ union A (Bunion C')
end.
Lemma Bunion_sound (C: list (list X)) (x: X):
x el Bunion C ↔ ∃ A, A el C ∧ x el A.
Lemma union_sub A B C: A <<= C ∧ B <<= C ↔ union A B <<= C.
Lemma inter_sub A B C: A <<= C → B <<= C → inter A B <<= C.
Lemma power_once A x: x el A → [x] el power A.
End ListOperation.
Section UpwardClosure.
Variable X: Type.
Variable U: list X.
Variable R: X → X → Prop.
Context {eq_decX: eq_dec X}.
Context {R_dec: ∀ x y, dec (R x y)}.
Implicit Type x y: X.
Implicit Type C: list X.
Lemma filter_idempotent
X (p: X → Prop) {p_dec: ∀ x, dec (p x)} (A: list X):
filter p (filter p A) = filter p A.
Section ListOperation.
Variable X: Type.
Context {eq_decX: eq_dec X}.
Implicit Type A B: list X.
(* List union and intersection *)
Fixpoint union A B :=
match A with
| [] ⇒ B
| x :: A' ⇒ if decision (x el B) then union A' B
else x :: union A' B
end.
Fixpoint inter A B :=
match A with
| [] ⇒ []
| x :: A' ⇒ if decision (x el B) then x :: inter A' B
else inter A' B
end.
Lemma union_sound A B (x:X):
x el union A B ↔ x el A ∨ x el B.
Lemma inter_sound A B (x: X):
x el inter A B ↔ x el A ∧ x el B.
Fixpoint Binter (C: list (list X)): list X :=
match C with
| [] ⇒ []
| A :: C' ⇒ inter A (Binter C')
end.
Lemma Binter_sound (C: list (list X)) (x: X):
x el Binter C → (∀ A, A el C → x el A).
Fixpoint Bunion (C: list (list X)): list X :=
match C with
| [] ⇒ []
| A :: C' ⇒ union A (Bunion C')
end.
Lemma Bunion_sound (C: list (list X)) (x: X):
x el Bunion C ↔ ∃ A, A el C ∧ x el A.
Lemma union_sub A B C: A <<= C ∧ B <<= C ↔ union A B <<= C.
Lemma inter_sub A B C: A <<= C → B <<= C → inter A B <<= C.
Lemma power_once A x: x el A → [x] el power A.
End ListOperation.
Section UpwardClosure.
Variable X: Type.
Variable U: list X.
Variable R: X → X → Prop.
Context {eq_decX: eq_dec X}.
Context {R_dec: ∀ x y, dec (R x y)}.
Implicit Type x y: X.
Implicit Type C: list X.
Upward-closed sets
Definition stepUC x C y : Prop := R x y.
Definition UCS x: list X :=
FCI.C (step := stepUC x) U.
Lemma UCS_closure x y:
y el U → stepUC x (UCS x) y → y el (UCS x).
Lemma UCS_ind x (p: X → Prop):
(∀ C y, inclp C p → y el U → stepUC x C y → p y)
→ inclp (UCS x) p.
Lemma UCS_in x y:
y el UCS x ↔ y el U ∧ R x y.
Lemma UCS_sub x: UCS x <<= U.
End UpwardClosure.
Definition UCS x: list X :=
FCI.C (step := stepUC x) U.
Lemma UCS_closure x y:
y el U → stepUC x (UCS x) y → y el (UCS x).
Lemma UCS_ind x (p: X → Prop):
(∀ C y, inclp C p → y el U → stepUC x C y → p y)
→ inclp (UCS x) p.
Lemma UCS_in x y:
y el UCS x ↔ y el U ∧ R x y.
Lemma UCS_sub x: UCS x <<= U.
End UpwardClosure.
Definition upset (X: Type) (R: X → X → Prop) (A: list X) (K: list X):=
A <<= K ∧ ∀ x, x el A → ∀ y, y el K → R x y → y el A.
Definition state := list var.
Definition base := list state.
Section TruthValues.
Variable K: base.
Variable Kdupfree: dupfree K.
Definition truthVal (X: list state) := upset (fun X1 X2 ⇒ X1 <<= X2) X K.
Lemma truthVal_union X Y:
truthVal X → truthVal Y → truthVal (union X Y).
Lemma truthVal_inter X Y:
truthVal X → truthVal Y → truthVal (inter X Y).
Lemma truthVal_Bunion F:
(∀ X, X el F → truthVal X) → truthVal (Bunion F).
Lemma truthVal_Binter F:
(∀ X, X el F → truthVal X) → truthVal (Binter F).
Implication
Section Implication.
Definition stepImp (X Y: list state) (U: list (list state)) (Z: list state)
: Prop := inter Z X <<= Y.
Definition TK: list (list state) := filter truthVal (power K).
Definition FImpList X Y: list (list state) :=
FCI.C (step := stepImp X Y) TK.
Lemma FImpList_closure X Y Z:
Z el TK → stepImp X Y (FImpList X Y) Z → Z el FImpList X Y.
Lemma FImpList_ind X Y (p: list state → Prop):
(∀ C Z, inclp C p → Z el TK → stepImp X Y C Z → p Z)
→ inclp (FImpList X Y) p.
Lemma FImpList_in X Y Z:
Z el FImpList X Y ↔ Z el TK ∧ inter Z X <<= Y.
Definition FImp X Y := Bunion (FImpList X Y).
Lemma truthVal_FImp X Y: truthVal (FImp X Y).
Lemma FImp_Heyting Z X Y: Z el TK →
Z <<= FImp X Y ↔ inter Z X <<= Y.
Lemma FImp_greatest X Y Z:
Z el TK → inter Z X <<= Y → Z <<= FImp X Y.
Lemma FImp_in1 X Y A:
A el FImp X Y → A el X → A el Y.
Lemma FImp_in2 X Y A:
truthVal X → truthVal Y → A el X → A el Y → A el FImp X Y.
Lemma FImp_in3 X Y A:
truthVal Y → A el Y → A el FImp X Y.
Lemma FImp_in4 X Y A:
(∃ Z, Z el TK ∧ A el Z ∧ inter Z X <<= Y) → A el FImp X Y.
End Implication.
Definition interpTK (x: var) : list state := filter (fun X ⇒ x el X) K.
Fixpoint evalTK (s: form) : list state :=
match s with
| Var x ⇒ interpTK x
| Fal ⇒ []
| And s1 s2 ⇒ inter (evalTK s1) (evalTK s2)
| Or s1 s2 ⇒ union (evalTK s1) (evalTK s2)
| Imp s1 s2 ⇒ FImp (evalTK s1) (evalTK s2)
end.
Fixpoint evalTK' (A: context) : list state :=
match A with
| [] ⇒ K
| s :: A' ⇒ inter (evalTK' A') (evalTK s)
end.
Lemma truthVal_evalTK s: truthVal (evalTK s).
Lemma truthVal_evalTK' A: truthVal (evalTK' A).
Lemma rep_evalTK s: evalTK s === rep (evalTK s) K.
Lemma rep_evalTK' A: evalTK' A === rep (evalTK' A) K.
Lemma nd_soundTK A s: nd A s → evalTK' A <<= evalTK s.
End TruthValues.
Section CounterModels.
Let K1: base := [[]].
Example K_Fal: ¬ nd [] Fal.
Example K_var x: ¬ nd [] (Var x).
Example K_orxy: ¬ nd [] (Or (Var 0) (Var 1)).
Let K2: base := [[0]].
Example K_neg: ¬ nd [] (Not (Var 0)).
Let K3: base := [[]; [0]].
Example K_XM: ¬ nd [] (Or (Var 0) (Not (Var 0))).
Example K_DN: ¬ nd [] (Imp (Not (Not (Var 0))) (Var 0)).
Let K4: base := [[]; [0]; [0;1]].
Example K_Peirce: ¬ nd [] (Imp (Imp (Imp (Var 0) (Var 1)) (Var 0)) (Var 0)).
End CounterModels.
Section Demo.
Definition Hintikka (A B: context): Prop :=
(∀ s, s el A →
match s with
| Fal ⇒ False
| Imp s1 s2 ⇒ s1 el B ∨ s2 el A
| And s1 s2 ⇒ s1 el A ∧ s2 el A
| Or s1 s2 ⇒ s1 el A ∨ s2 el A
| Var x ⇒ ¬ Var x el B
end) ∧
(∀ s, s el B →
match s with
| And s1 s2 ⇒ s1 el B ∨ s2 el B
| Or s1 s2 ⇒ s1 el B ∧ s2 el B
| _ ⇒ True
end).
Lemma Hintikka_equi (C D C' D': context):
Hintikka C D → C' === C → D' === D → Hintikka C' D'.
Instance Hintikka_dec C D: dec (Hintikka C D).
Definition PContext: Type := context × context.
Definition Demo (D: list PContext): Prop :=
∀ A B, (A, B) el D →
Hintikka A B ∧
(∀ s t, Imp s t el B →
∃ C', C' el D ∧ let (A', B') := C' in
A <<= A' ∧ s el A' ∧ t el B').
Definition dsub (D D': list PContext): Prop :=
∀ A B, (A, B) el D → ∃ C', C' el D' ∧
let (A', B'):= C' in A === A' ∧ B === B'.
Definition dequi D D' : Prop := dsub D D' ∧ dsub D' D.
Lemma Demo_equi D D': Demo D → dequi D D' → Demo D'.
End Demo.
Instance prod_eq_dec X Y:
eq_dec X → eq_dec Y → eq_dec (prod X Y).
Section RelationToList.
Variable X: Type.
Variable R: X → X → Prop.
Variable S: list X.
Context {eq_decX: eq_dec X}.
Context {R_dec: ∀ x y, dec (R x y)}.
Let SS := list_prod S S.
Definition stepRList (C: list (X × X)) (p: X × X): Prop :=
let (x,y) := p in x el S ∧ y el S ∧ R x y.
Instance stepRList_dec C p: dec (stepRList C p).
Definition RList : list (X × X) := FCI.C (step:= stepRList) SS.
Lemma RList_closure p:
p el SS → stepRList RList p → p el RList.
Lemma RList_ind (P: X × X → Prop):
(∀ C p, inclp C P → p el SS → stepRList C p → P p)
→ inclp RList P.
Lemma RList_in p: p el RList ↔ let (x,y) := p in x el S ∧ y el S ∧ R x y.
End RelationToList.
Section FiniteClosure.
Variable F: Type.
Context {eq_decF: eq_dec F}.
Variable FS: list F.
Variable FE: list (F × F).
Implicit Type x y z: F.
Definition stepImp (X Y: list state) (U: list (list state)) (Z: list state)
: Prop := inter Z X <<= Y.
Definition TK: list (list state) := filter truthVal (power K).
Definition FImpList X Y: list (list state) :=
FCI.C (step := stepImp X Y) TK.
Lemma FImpList_closure X Y Z:
Z el TK → stepImp X Y (FImpList X Y) Z → Z el FImpList X Y.
Lemma FImpList_ind X Y (p: list state → Prop):
(∀ C Z, inclp C p → Z el TK → stepImp X Y C Z → p Z)
→ inclp (FImpList X Y) p.
Lemma FImpList_in X Y Z:
Z el FImpList X Y ↔ Z el TK ∧ inter Z X <<= Y.
Definition FImp X Y := Bunion (FImpList X Y).
Lemma truthVal_FImp X Y: truthVal (FImp X Y).
Lemma FImp_Heyting Z X Y: Z el TK →
Z <<= FImp X Y ↔ inter Z X <<= Y.
Lemma FImp_greatest X Y Z:
Z el TK → inter Z X <<= Y → Z <<= FImp X Y.
Lemma FImp_in1 X Y A:
A el FImp X Y → A el X → A el Y.
Lemma FImp_in2 X Y A:
truthVal X → truthVal Y → A el X → A el Y → A el FImp X Y.
Lemma FImp_in3 X Y A:
truthVal Y → A el Y → A el FImp X Y.
Lemma FImp_in4 X Y A:
(∃ Z, Z el TK ∧ A el Z ∧ inter Z X <<= Y) → A el FImp X Y.
End Implication.
Definition interpTK (x: var) : list state := filter (fun X ⇒ x el X) K.
Fixpoint evalTK (s: form) : list state :=
match s with
| Var x ⇒ interpTK x
| Fal ⇒ []
| And s1 s2 ⇒ inter (evalTK s1) (evalTK s2)
| Or s1 s2 ⇒ union (evalTK s1) (evalTK s2)
| Imp s1 s2 ⇒ FImp (evalTK s1) (evalTK s2)
end.
Fixpoint evalTK' (A: context) : list state :=
match A with
| [] ⇒ K
| s :: A' ⇒ inter (evalTK' A') (evalTK s)
end.
Lemma truthVal_evalTK s: truthVal (evalTK s).
Lemma truthVal_evalTK' A: truthVal (evalTK' A).
Lemma rep_evalTK s: evalTK s === rep (evalTK s) K.
Lemma rep_evalTK' A: evalTK' A === rep (evalTK' A) K.
Lemma nd_soundTK A s: nd A s → evalTK' A <<= evalTK s.
End TruthValues.
Section CounterModels.
Let K1: base := [[]].
Example K_Fal: ¬ nd [] Fal.
Example K_var x: ¬ nd [] (Var x).
Example K_orxy: ¬ nd [] (Or (Var 0) (Var 1)).
Let K2: base := [[0]].
Example K_neg: ¬ nd [] (Not (Var 0)).
Let K3: base := [[]; [0]].
Example K_XM: ¬ nd [] (Or (Var 0) (Not (Var 0))).
Example K_DN: ¬ nd [] (Imp (Not (Not (Var 0))) (Var 0)).
Let K4: base := [[]; [0]; [0;1]].
Example K_Peirce: ¬ nd [] (Imp (Imp (Imp (Var 0) (Var 1)) (Var 0)) (Var 0)).
End CounterModels.
Section Demo.
Definition Hintikka (A B: context): Prop :=
(∀ s, s el A →
match s with
| Fal ⇒ False
| Imp s1 s2 ⇒ s1 el B ∨ s2 el A
| And s1 s2 ⇒ s1 el A ∧ s2 el A
| Or s1 s2 ⇒ s1 el A ∨ s2 el A
| Var x ⇒ ¬ Var x el B
end) ∧
(∀ s, s el B →
match s with
| And s1 s2 ⇒ s1 el B ∨ s2 el B
| Or s1 s2 ⇒ s1 el B ∧ s2 el B
| _ ⇒ True
end).
Lemma Hintikka_equi (C D C' D': context):
Hintikka C D → C' === C → D' === D → Hintikka C' D'.
Instance Hintikka_dec C D: dec (Hintikka C D).
Definition PContext: Type := context × context.
Definition Demo (D: list PContext): Prop :=
∀ A B, (A, B) el D →
Hintikka A B ∧
(∀ s t, Imp s t el B →
∃ C', C' el D ∧ let (A', B') := C' in
A <<= A' ∧ s el A' ∧ t el B').
Definition dsub (D D': list PContext): Prop :=
∀ A B, (A, B) el D → ∃ C', C' el D' ∧
let (A', B'):= C' in A === A' ∧ B === B'.
Definition dequi D D' : Prop := dsub D D' ∧ dsub D' D.
Lemma Demo_equi D D': Demo D → dequi D D' → Demo D'.
End Demo.
Instance prod_eq_dec X Y:
eq_dec X → eq_dec Y → eq_dec (prod X Y).
Section RelationToList.
Variable X: Type.
Variable R: X → X → Prop.
Variable S: list X.
Context {eq_decX: eq_dec X}.
Context {R_dec: ∀ x y, dec (R x y)}.
Let SS := list_prod S S.
Definition stepRList (C: list (X × X)) (p: X × X): Prop :=
let (x,y) := p in x el S ∧ y el S ∧ R x y.
Instance stepRList_dec C p: dec (stepRList C p).
Definition RList : list (X × X) := FCI.C (step:= stepRList) SS.
Lemma RList_closure p:
p el SS → stepRList RList p → p el RList.
Lemma RList_ind (P: X × X → Prop):
(∀ C p, inclp C P → p el SS → stepRList C p → P p)
→ inclp RList P.
Lemma RList_in p: p el RList ↔ let (x,y) := p in x el S ∧ y el S ∧ R x y.
End RelationToList.
Section FiniteClosure.
Variable F: Type.
Context {eq_decF: eq_dec F}.
Variable FS: list F.
Variable FE: list (F × F).
Implicit Type x y z: F.
Reflexive-transitive closure
Definition stepRTC (C: list (F × F)) (p: F × F) : Prop :=
p el FE ∨
let (x, y) := p in
y = x ∨
(∃ z, z el FS ∧ (x,z) el C ∧ (z,y) el C).
Instance stepRTC_dec C p:
dec (stepRTC C p).
Definition RTC: list (F × F) :=
FCI.C (step := stepRTC) (list_prod FS FS).
Lemma RTC_closure p:
p el list_prod FS FS → stepRTC RTC p → p el RTC.
Lemma RTC_ind (P: (F×F) → Prop):
(∀ C p, inclp C P → p el list_prod FS FS → stepRTC C p → P p)
→ inclp RTC P.
Lemma RTC_reflexive x: x el FS → (x,x) el RTC.
Lemma RTC_transitive x y z:
x el FS → y el FS → z el FS
→ (x,y) el RTC → (y,z) el RTC → (x,z) el RTC.
Lemma RTC_in x y: (x,y) el RTC → x el FS ∧ y el FS.
Lemma RTC_iff x y:
(x,y) el RTC ↔ x el FS ∧ y el FS ∧
((x,y) el FE ∨ y = x ∨
(∃ z, z el FS ∧ (x,z) el RTC ∧ (z,y) el RTC)).
p el FE ∨
let (x, y) := p in
y = x ∨
(∃ z, z el FS ∧ (x,z) el C ∧ (z,y) el C).
Instance stepRTC_dec C p:
dec (stepRTC C p).
Definition RTC: list (F × F) :=
FCI.C (step := stepRTC) (list_prod FS FS).
Lemma RTC_closure p:
p el list_prod FS FS → stepRTC RTC p → p el RTC.
Lemma RTC_ind (P: (F×F) → Prop):
(∀ C p, inclp C P → p el list_prod FS FS → stepRTC C p → P p)
→ inclp RTC P.
Lemma RTC_reflexive x: x el FS → (x,x) el RTC.
Lemma RTC_transitive x y z:
x el FS → y el FS → z el FS
→ (x,y) el RTC → (y,z) el RTC → (x,z) el RTC.
Lemma RTC_in x y: (x,y) el RTC → x el FS ∧ y el FS.
Lemma RTC_iff x y:
(x,y) el RTC ↔ x el FS ∧ y el FS ∧
((x,y) el FE ∨ y = x ∨
(∃ z, z el FS ∧ (x,z) el RTC ∧ (z,y) el RTC)).
Compute UCS from RTC
Definition ucsPred x (p: F × F) := let (x',_) := p in x' = x.
Lemma dec_ucsPred x : ∀ p, dec (ucsPred x p).
Let UCSFilter x FERTC : list (F × F)
:= filter (ucsPred x) (p_dec:=dec_ucsPred x) FERTC.
Definition UCSE x FERTC:=
map (fun (p: F × F) ⇒ let (_,y) := p in y) (UCSFilter x FERTC).
Lemma UCSE_sound x y: (x,y) el RTC ↔ y el UCSE x RTC.
(* By stepFKImp we assume FE is FERTC, i.e. FE satisfies RTC *)
Definition stepFKImp (A B C: list F) x : Prop :=
∀ y, y el inter (UCSE x FE) A → y el B.
Definition FKImp A B: list F :=
FCI.C (step := stepFKImp A B) FS.
Lemma FKImp_closure A B x:
x el FS → stepFKImp A B (FKImp A B) x → x el FKImp A B.
Lemma FKImp_ind A B (p: F → Prop):
(∀ C x, inclp C p → x el FS → stepFKImp A B C x → p x)
→ inclp (FKImp A B) p.
Lemma FKImp_in x A B:
x el FKImp A B
↔ x el FS ∧ ∀ y, y el inter (UCSE x FE) A → y el B.
End FiniteClosure.
Section DemoKBase.
Fixpoint CVars (A: context): list var :=
match A with
| [] ⇒ []
| s :: A' ⇒ match s with
| Var x ⇒ x :: CVars A'
| _ ⇒ CVars A'
end
end.
Lemma CVars_correct A x: (Var x) el A ↔ x el CVars A.
Definition baseVars (D: list (context × context)): list var :=
undup (Bunion
(map (fun (C: context × context) ⇒ let (A,_):= C in CVars A) D)).
Lemma baseVars_incl (D: list (context × context)) C:
C el D → let (A,_):= C in CVars A <<= baseVars D.
Lemma baseVars_in D A B:
(A, B) el D → rep (CVars A) (baseVars D) === CVars A.
Definition baseKD (D: list (context × context)): list state :=
undup
(map (fun (C: context × context) ⇒
let (A,B) := C in rep (CVars A) (baseVars D)) D).
Lemma baseKD_in D: ∀ A B,
(A, B) el D → rep (CVars A) (baseVars D) el baseKD D.
Lemma baseKD_sound D (FA: list var):
FA el baseKD D → ∃ C, C el D ∧ let (A, B) := C in CVars A === FA.
Lemma baseKD_complete D A B:
(A, B) el D → rep (CVars A) (baseVars D) el baseKD D
∧ CVars A === rep (CVars A) (baseVars D).
Definition satisD D A s: Prop :=
rep (CVars A) (baseVars D) el (evalTK (baseKD D) s).
End DemoKBase.
Section PContextRelation.
Definition RC (C C': PContext): Prop
:= let (A,_) := C in let (A', _) := C' in A <<= A'.
Instance RC_dec: ∀ C C', dec (RC C C').
Definition RCList (D: list PContext) := (RList (R:=RC) D).
Let pRC (x: var) (C: PContext) := let (A,_):= C in Var x el A.
Let pRC_dec x: ∀ C, dec (pRC x C).
Definition RCinterp (D: list PContext) x
: list (context × context) := filter (p_dec:= pRC_dec x) (pRC x) D.
Lemma RTC_RCList (D: list PContext) (C1 C2: PContext):
(C1, C2) el @RTC _ _ D (RCList D) ↔ C1 el D ∧ C2 el D ∧ RC C1 C2.
End PContextRelation.
Record FiniteKripkeModel : Type :=
mkFiniteKripkeModel {
WF: Type;
WS: list WF;
WE: list (WF × WF);
eq_decW: eq_dec WF;
WER := RTC WS WE;
interp: var → list WF;
persist: ∀ x a b, a el WS → b el WS
→ a el interp x → (a,b) el WER → b el interp x
}.
Section FiniteKripke.
Variable FKM: FiniteKripkeModel.
Implicit Type x y z: WF FKM.
Fixpoint evalFK s: list (WF FKM) :=
match s with
| Var x ⇒ interp FKM x
| Fal ⇒ []
| And s1 s2 ⇒ inter (eq_decX:=@eq_decW FKM) (evalFK s1) (evalFK s2)
| Or s1 s2 ⇒ union (eq_decX:=@eq_decW FKM) (evalFK s1) (evalFK s2)
| Imp s1 s2 ⇒
FKImp (eq_decF:=@eq_decW FKM) (WS FKM) (WER FKM) (evalFK s1) (evalFK s2)
end.
Definition satisFK x s := x el evalFK s.
Definition satisFK' x A := ∀ s, s el A → satisFK x s.
Lemma evalFK_mono x y s:
x el WS FKM → y el WS FKM → satisFK x s → (x,y) el WER FKM → satisFK y s.
Lemma evalFK_OrAR x B:
(∀ s, s el B → ¬satisFK x s) → ¬satisFK x (OrAR B).
Lemma nd_soundFK A s:
nd A s → ∀ x, x el WS FKM → satisFK' x A → satisFK x s.
Let W: Type := {x | x el WS FKM}.
Let pW := fun x ⇒ x el WS FKM.
Implicit Type u v w: W.
Let WR u v: Prop :=
let (x, Ex) := u in let (y, Ey) := v in (x,y) el WER FKM.
Let WRref: reflexive _ WR.
Let WRtra: transitive _ WR.
Let interp (x: var) (w: W): Prop :=
let (y, _) := w in y el (@interp FKM) x.
Definition FK2K : KripkeModel.
End FiniteKripke.
Section SubClause.
Definition trip (S: sform) : form := match S with | +s | -s ⇒ s end.
Instance positive_dec: ∀ S, dec (positive S).
Instance negative_dec: ∀ S, dec (negative S).
Definition C2PC (C: clause) : PContext :=
(map trip (filter positive C), map trip (filter negative C)).
Lemma postrip_in s C:
+s el C ↔ s el map trip (filter positive C).
Lemma negtrip_in s C:
-s el C ↔ s el map trip (filter negative C).
Definition subPC (C C': PContext): Prop :=
let (A,B) := C in let (A',B') := C' in A <<= A' ∧ B <<= B'.
Lemma subC (C C': clause):
C <<= C' ↔ subPC (C2PC C) (C2PC C').
Definition PC2C (A B: context): clause :=
map (fun (s: form) ⇒ +s) A ++ map (fun (s: form) ⇒ -s) B.
Lemma PC2C_pos A B s:
s el A ↔ +s el PC2C A B.
Lemma PC2C_neg A B s:
s el B ↔ -s el PC2C A B.
Lemma PC2C_pushneg A B s: PC2C A (s :: B) <<= -s :: PC2C A B.
Lemma PC2C_pushpos A B s: PC2C (s :: A) B <<= +s :: PC2C A B.
Definition pos (C: clause) : clause := filter positive C.
Lemma negtrip_empty C: map trip (filter negative (pos C)) = [].
(* D supports C if some C' el D and tab C', since tab C' -> tab C by tabW *)
Definition sup (D: list clause) (C: clause) : Prop :=
∃ C', C' el D ∧ C' <<= C.
Definition stepTab' (D: list clause) (S: sform) (C: clause): Prop :=
match S with
| +Var x ⇒ -Var x el C
| +Fal ⇒ True
| +Imp s t ⇒ sup D (-s::C) ∧ sup D (+t :: C)
| -Imp s t ⇒ sup D (+s::-t::pos C)
| +And s t ⇒ sup D (+s::+t::C)
| -And s t ⇒ sup D (-s::C) ∧ sup D (-t::C)
| +Or s t ⇒ sup D (+s::C) ∧ sup D (+t::C)
| -Or s t ⇒ sup D (-s::-t::C)
| _ ⇒ False
end.
Definition stepTab (D: list clause) (C: clause) : Prop :=
∃ S, S el C ∧ stepTab' D S C.
Instance stepTab_dec D C: dec (stepTab D C).
Lemma stepTab_mono D D' C:
D <<= D' → stepTab D C → stepTab D' C.
End SubClause.
Section TableauxDecidability.
Variable U: clause.
Variable sscU: ss_closed U.
Definition lfpTab :=
FCI.C (step_dec:=stepTab_dec) (step:=stepTab) (power U).
Lemma lfpTab_closure (C: clause):
C el power U → stepTab lfpTab C → C el lfpTab.
Lemma lfpTab_ind (p: clause → Prop):
(∀ D C, inclp D p → C el power U → stepTab D C → p C)
→ inclp lfpTab p.
Lemma lfp_tab (C: clause):
C el lfpTab → let (A, B) := (C2PC C) in tab A B.
Lemma tab_lfp A B:
PC2C A B <<= U → tab A B → rep (PC2C A B) U el lfpTab.
Lemma tab_dec' A B:
PC2C A B <<= U → dec (tab A B).
End TableauxDecidability.
Section TableauxConsistency.
Theorem tab_dec A B: dec (tab A B).
Definition cons (C: PContext) :=
let (A,B) := C in ¬tab A B.
Instance cons_dec: ∀ C, dec (cons C).
Lemma consW: ∀ C C', cons C → subPC C' C → cons C'.
End TableauxConsistency.
Lemma dec_ucsPred x : ∀ p, dec (ucsPred x p).
Let UCSFilter x FERTC : list (F × F)
:= filter (ucsPred x) (p_dec:=dec_ucsPred x) FERTC.
Definition UCSE x FERTC:=
map (fun (p: F × F) ⇒ let (_,y) := p in y) (UCSFilter x FERTC).
Lemma UCSE_sound x y: (x,y) el RTC ↔ y el UCSE x RTC.
(* By stepFKImp we assume FE is FERTC, i.e. FE satisfies RTC *)
Definition stepFKImp (A B C: list F) x : Prop :=
∀ y, y el inter (UCSE x FE) A → y el B.
Definition FKImp A B: list F :=
FCI.C (step := stepFKImp A B) FS.
Lemma FKImp_closure A B x:
x el FS → stepFKImp A B (FKImp A B) x → x el FKImp A B.
Lemma FKImp_ind A B (p: F → Prop):
(∀ C x, inclp C p → x el FS → stepFKImp A B C x → p x)
→ inclp (FKImp A B) p.
Lemma FKImp_in x A B:
x el FKImp A B
↔ x el FS ∧ ∀ y, y el inter (UCSE x FE) A → y el B.
End FiniteClosure.
Section DemoKBase.
Fixpoint CVars (A: context): list var :=
match A with
| [] ⇒ []
| s :: A' ⇒ match s with
| Var x ⇒ x :: CVars A'
| _ ⇒ CVars A'
end
end.
Lemma CVars_correct A x: (Var x) el A ↔ x el CVars A.
Definition baseVars (D: list (context × context)): list var :=
undup (Bunion
(map (fun (C: context × context) ⇒ let (A,_):= C in CVars A) D)).
Lemma baseVars_incl (D: list (context × context)) C:
C el D → let (A,_):= C in CVars A <<= baseVars D.
Lemma baseVars_in D A B:
(A, B) el D → rep (CVars A) (baseVars D) === CVars A.
Definition baseKD (D: list (context × context)): list state :=
undup
(map (fun (C: context × context) ⇒
let (A,B) := C in rep (CVars A) (baseVars D)) D).
Lemma baseKD_in D: ∀ A B,
(A, B) el D → rep (CVars A) (baseVars D) el baseKD D.
Lemma baseKD_sound D (FA: list var):
FA el baseKD D → ∃ C, C el D ∧ let (A, B) := C in CVars A === FA.
Lemma baseKD_complete D A B:
(A, B) el D → rep (CVars A) (baseVars D) el baseKD D
∧ CVars A === rep (CVars A) (baseVars D).
Definition satisD D A s: Prop :=
rep (CVars A) (baseVars D) el (evalTK (baseKD D) s).
End DemoKBase.
Section PContextRelation.
Definition RC (C C': PContext): Prop
:= let (A,_) := C in let (A', _) := C' in A <<= A'.
Instance RC_dec: ∀ C C', dec (RC C C').
Definition RCList (D: list PContext) := (RList (R:=RC) D).
Let pRC (x: var) (C: PContext) := let (A,_):= C in Var x el A.
Let pRC_dec x: ∀ C, dec (pRC x C).
Definition RCinterp (D: list PContext) x
: list (context × context) := filter (p_dec:= pRC_dec x) (pRC x) D.
Lemma RTC_RCList (D: list PContext) (C1 C2: PContext):
(C1, C2) el @RTC _ _ D (RCList D) ↔ C1 el D ∧ C2 el D ∧ RC C1 C2.
End PContextRelation.
Record FiniteKripkeModel : Type :=
mkFiniteKripkeModel {
WF: Type;
WS: list WF;
WE: list (WF × WF);
eq_decW: eq_dec WF;
WER := RTC WS WE;
interp: var → list WF;
persist: ∀ x a b, a el WS → b el WS
→ a el interp x → (a,b) el WER → b el interp x
}.
Section FiniteKripke.
Variable FKM: FiniteKripkeModel.
Implicit Type x y z: WF FKM.
Fixpoint evalFK s: list (WF FKM) :=
match s with
| Var x ⇒ interp FKM x
| Fal ⇒ []
| And s1 s2 ⇒ inter (eq_decX:=@eq_decW FKM) (evalFK s1) (evalFK s2)
| Or s1 s2 ⇒ union (eq_decX:=@eq_decW FKM) (evalFK s1) (evalFK s2)
| Imp s1 s2 ⇒
FKImp (eq_decF:=@eq_decW FKM) (WS FKM) (WER FKM) (evalFK s1) (evalFK s2)
end.
Definition satisFK x s := x el evalFK s.
Definition satisFK' x A := ∀ s, s el A → satisFK x s.
Lemma evalFK_mono x y s:
x el WS FKM → y el WS FKM → satisFK x s → (x,y) el WER FKM → satisFK y s.
Lemma evalFK_OrAR x B:
(∀ s, s el B → ¬satisFK x s) → ¬satisFK x (OrAR B).
Lemma nd_soundFK A s:
nd A s → ∀ x, x el WS FKM → satisFK' x A → satisFK x s.
Let W: Type := {x | x el WS FKM}.
Let pW := fun x ⇒ x el WS FKM.
Implicit Type u v w: W.
Let WR u v: Prop :=
let (x, Ex) := u in let (y, Ey) := v in (x,y) el WER FKM.
Let WRref: reflexive _ WR.
Let WRtra: transitive _ WR.
Let interp (x: var) (w: W): Prop :=
let (y, _) := w in y el (@interp FKM) x.
Definition FK2K : KripkeModel.
End FiniteKripke.
Section SubClause.
Definition trip (S: sform) : form := match S with | +s | -s ⇒ s end.
Instance positive_dec: ∀ S, dec (positive S).
Instance negative_dec: ∀ S, dec (negative S).
Definition C2PC (C: clause) : PContext :=
(map trip (filter positive C), map trip (filter negative C)).
Lemma postrip_in s C:
+s el C ↔ s el map trip (filter positive C).
Lemma negtrip_in s C:
-s el C ↔ s el map trip (filter negative C).
Definition subPC (C C': PContext): Prop :=
let (A,B) := C in let (A',B') := C' in A <<= A' ∧ B <<= B'.
Lemma subC (C C': clause):
C <<= C' ↔ subPC (C2PC C) (C2PC C').
Definition PC2C (A B: context): clause :=
map (fun (s: form) ⇒ +s) A ++ map (fun (s: form) ⇒ -s) B.
Lemma PC2C_pos A B s:
s el A ↔ +s el PC2C A B.
Lemma PC2C_neg A B s:
s el B ↔ -s el PC2C A B.
Lemma PC2C_pushneg A B s: PC2C A (s :: B) <<= -s :: PC2C A B.
Lemma PC2C_pushpos A B s: PC2C (s :: A) B <<= +s :: PC2C A B.
Definition pos (C: clause) : clause := filter positive C.
Lemma negtrip_empty C: map trip (filter negative (pos C)) = [].
(* D supports C if some C' el D and tab C', since tab C' -> tab C by tabW *)
Definition sup (D: list clause) (C: clause) : Prop :=
∃ C', C' el D ∧ C' <<= C.
Definition stepTab' (D: list clause) (S: sform) (C: clause): Prop :=
match S with
| +Var x ⇒ -Var x el C
| +Fal ⇒ True
| +Imp s t ⇒ sup D (-s::C) ∧ sup D (+t :: C)
| -Imp s t ⇒ sup D (+s::-t::pos C)
| +And s t ⇒ sup D (+s::+t::C)
| -And s t ⇒ sup D (-s::C) ∧ sup D (-t::C)
| +Or s t ⇒ sup D (+s::C) ∧ sup D (+t::C)
| -Or s t ⇒ sup D (-s::-t::C)
| _ ⇒ False
end.
Definition stepTab (D: list clause) (C: clause) : Prop :=
∃ S, S el C ∧ stepTab' D S C.
Instance stepTab_dec D C: dec (stepTab D C).
Lemma stepTab_mono D D' C:
D <<= D' → stepTab D C → stepTab D' C.
End SubClause.
Section TableauxDecidability.
Variable U: clause.
Variable sscU: ss_closed U.
Definition lfpTab :=
FCI.C (step_dec:=stepTab_dec) (step:=stepTab) (power U).
Lemma lfpTab_closure (C: clause):
C el power U → stepTab lfpTab C → C el lfpTab.
Lemma lfpTab_ind (p: clause → Prop):
(∀ D C, inclp D p → C el power U → stepTab D C → p C)
→ inclp lfpTab p.
Lemma lfp_tab (C: clause):
C el lfpTab → let (A, B) := (C2PC C) in tab A B.
Lemma tab_lfp A B:
PC2C A B <<= U → tab A B → rep (PC2C A B) U el lfpTab.
Lemma tab_dec' A B:
PC2C A B <<= U → dec (tab A B).
End TableauxDecidability.
Section TableauxConsistency.
Theorem tab_dec A B: dec (tab A B).
Definition cons (C: PContext) :=
let (A,B) := C in ¬tab A B.
Instance cons_dec: ∀ C, dec (cons C).
Lemma consW: ∀ C C', cons C → subPC C' C → cons C'.
End TableauxConsistency.