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.