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

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.

# Finitary Semantics

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 X2X1 <<= 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 Xx el X) K.

Fixpoint evalTK (s: form) : list state :=
match s with
| Var xinterpTK x
| Fal[]
| And s1 s2inter (evalTK s1) (evalTK s2)
| Or s1 s2union (evalTK s1) (evalTK s2)
| Imp s1 s2FImp (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
| FalFalse
| Imp s1 s2s1 el B s2 el A
| And s1 s2s1 el A s2 el A
| Or s1 s2s1 el A s2 el A
| Var x¬ Var x el B
end)
( s, s el B
match s with
| And s1 s2s1 el B s2 el B
| Or s1 s2s1 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)).

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 xx :: 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 xinterp FKM x
| Fal[]
| And s1 s2inter (eq_decX:=@eq_decW FKM) (evalFK s1) (evalFK s2)
| Or s1 s2union (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 xx 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 | -ss 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
| +FalTrue
| +Imp s tsup D (-s::C) sup D (+t :: C)
| -Imp s tsup D (+s::-t::pos C)
| +And s tsup D (+s::+t::C)
| -And s tsup D (-s::C) sup D (-t::C)
| +Or s tsup D (+s::C) sup D (+t::C)
| -Or s tsup 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.