Library PropiLFmodel2

Require Export PropiLFmodel.

Lemma sigma_forall_list X A (p : X Prop) (p_dec : x, dec (p x)) :
  {x | x el A ¬ p x} + { x, x el A p x}.

Section MaximalExtension.

  Variable X: Type.
  Context {eq_decX: eq_dec X}.
  Variable p: list X Prop.
  Context {p_dec: A, dec (p A)}.
  Variable U: list X.

  Definition qmax (M: list X): Prop :=
    M <<= U p M x, x el U p (x::M) x el M.

  Lemma qmax_or A :
    A <<= U p A {x | x el U p (x::A) ¬ x el A} + {qmax A}.

  Lemma qmax_exists A :
    A <<= U p A {M | A <<= M qmax M}.

  Variable p_mono: A A', p A A' <<= A p A'.

  Definition maxext C :=
    C <<= U p C C', C' <<= U p C' C <<= C' C' <<= C.

  Lemma qmax_maxext C: qmax C maxext C.

  Lemma maxext_nomore C (D: maxext C) s: s el U ¬s el C ¬ p (s :: C).

  Lemma extension A:
    A <<= U p A {M| M el power U A <<= M qmax M}.

  Lemma maxExtension A:
    A <<= U p A {M| M el power U A <<= M maxext M}.

End MaximalExtension.

Section DemoFiniteKripke.

  Definition D2FKM (D: list PContext) : FiniteKripkeModel.
  Defined.

  Definition satisDFK (D: list PContext) (C: PContext) (s: form): Prop
    := C el @evalFK (D2FKM D) s.

  Theorem DemoSat D (E: Demo D): A B, (A,B) el D s,
    (s el A satisDFK D (A,B) s) (s el B ¬ satisDFK D (A,B) s).

  Lemma DemoSatisAll (D: list PContext) s (A B A' B': context):
    CVars A === CVars A' satisD D A s satisD D A' s.

End DemoFiniteKripke.

Section CanonicalDemo.

  Variable U: clause.
  Variable sscU: ss_closed U.
  Context {tab_dec: C D, dec (tab C D)}.

  Definition Cons (C: clause) := cons (C2PC C).

  Instance Cons_dec C: dec (Cons C).

  Lemma Cons_mono: C C', Cons C C' <<= C Cons C'.

  Definition clauseCD := filter (qmax Cons U) (power U).
  Definition CD := map C2PC (filter (qmax Cons U) (power U)).

  Lemma CD_demo: Demo CD.

  Lemma demo_extension C:
    C <<= U cons (C2PC C) {C'| C' el CD subPC (C2PC C) C'}.

End CanonicalDemo.

Section TabND.

  Definition satC (D: list PContext) (C: PContext) : Prop :=
    let (A,B) := C in
       s, (s el A C1, C1 el D satisDFK D C1 s)
              (s el B C2, C2 el D ¬ satisDFK D C2 s).

  Lemma tab_nd_sat A s: {D | Demo D satC D ([],[s])} + {nd A s}.

  Lemma kripke_nd A s:
  {K: FiniteKripkeModel | x, x el WS K
                                    satisFK' (FKM:=K) x A
                                    ¬ satisFK (FKM:=K) x s} + {nd A s}.

  Theorem tab_iff_nd A s: tab A [s] nd A s.

  Lemma tab_iff_ndG A B: tab A B nd A (OrAR B).

End TabND.

Lemma filter_equi X (p: X Prop) {p_dec: x, dec (p x)} A B:
  filter p A === filter p B x, p x (x el A x el B).

Lemma in_map_informative
  (X Y: Type) {eq_decY: eq_dec Y} (f: X Y) (A: list X) (y: Y):
    y el map f A {x | f x = y x el A }.

Section MaximalIdentity.

  Variable U: context.

  Definition sfs := map Pos (scl U) ++ map Neg (scl U).

  Let sclU := @scl_closed U.

  Lemma sclPos_in s: s el scl U +s el sfs.

  Lemma sclNeg_in s: s el scl U -s el sfs.

  Lemma ssc_scl: ss_closed sfs.

  Lemma maxCons_XM C (E: maxext Cons sfs C) s:
    s el scl U +s el C -s el C.

  Definition posVar S :=
    match S with
    | +smatch s with | Var _True | _False end
    | -sFalse
    end.

  Instance posVar_dec S: dec (posVar S).

  Definition posVars (C: clause): clause := filter posVar C.

  Lemma maxCons_equi_vars C C':
    maxext Cons sfs C maxext Cons sfs C'
      ( Sx, posVar Sx Sx el C Sx el C')
       x b, (b2s b (Var x)) el C (b2s b (Var x)) el C'.

  Lemma maxCons_equi_Fal C C':
    maxext Cons sfs C maxext Cons sfs C'
       b, (b2s b Fal) el C (b2s b Fal) el C'.

  Definition negImp S :=
    match S with
    | +sFalse
    | -smatch s with | Imp _ _True | _False end
    end.

  Instance negImp_dec S: dec (negImp S).

  Lemma maxCons_incl C C':
    maxext Cons sfs C maxext Cons sfs C'
      ( Sx, posVar Sx Sx el C Sx el C')
      ( Si, negImp Si Si el C Si el C')
       s b, (b2s b s) el C (b2s b s) el C'.

  Theorem maxCons_equi C C':
    maxext Cons sfs C maxext Cons sfs C'
      ( Sx, posVar Sx Sx el C Sx el C')
      ( Si, negImp Si Si el C Si el C') C === C'.

  Definition subPos C C' := pos C <<= C'.

  Lemma pos_in C s: +s el C +s el pos C.

  Lemma maxCons_ParOrd C C':
    maxext Cons sfs C maxext Cons sfs C' subPos C C' subPos C' C
     s b, (b2s b s) el C (b2s b s) el C'.

  Lemma maxCons_PartialOrder C C':
    maxext Cons sfs C maxext Cons sfs C'
    subPos C C' subPos C' C C === C'.

  Lemma qmax_Uequi {X: Type} U1 U2 (p: list XProp) A:
    qmax p U1 A U1 === U2 qmax p U2 A.

  Let SFL := undup sfs.

  Definition pVar_nImp S := posVar S negImp S.

  Instance pVar_nImp_dec S: dec (pVar_nImp S).

  Lemma maxext_samebase C C':
    qmax Cons SFL C qmax Cons SFL C'
    filter pVar_nImp C === filter pVar_nImp C' C === C'.

  Definition compact_CD :=
    map (fun Cfilter pVar_nImp C) (clauseCD SFL).

  Lemma compact_cons C: C el compact_CD C <<= sfs Cons C.

  Definition compactCD_restore:
    {cCD: list clause |
       C, C el cCD C el power SFL qmax Cons SFL C
                              (filter pVar_nImp C) el compact_CD}.

  Lemma compact_sound:
    let (cCD,_):= compactCD_restore in cCD === clauseCD SFL.

  Lemma compact_CD_equi:
    let (cCD,_):= compactCD_restore in dequi (CD sfs) (map C2PC cCD).

  Lemma compact_restore_demo:
    let (cCD,_):= compactCD_restore in Demo (map C2PC cCD).

  Definition compactDemo := map C2PC compact_CD.

End MaximalIdentity.

(*
Section CompactDemo.
  Lemma compactDemo_nd_sat A s:
    {satC (compactDemo (s::A)) (,s)} + {nd A s}.
  Proof.
    destruct (tab_dec A s) as H|H.
    - right. apply tab_nd, H.
    - remember (s::A) as U.
      left. assert (F:=compact_restore_demo U).
      destruct (compactCD_restore U) as cCD E.
      pose (C:= - s :: map Pos A).
      assert (I: cons (C2PC C)).
        { unfold C2PC, C. simpl. intros I. apply H. apply (tabW I);
          try apply incl_shift; intros t J; apply in_map_iff in J as T [J1 J2];
          apply in_filter_iff in J2 as J2 J3;
          apply in_map_iff in J2 as t' [J4 J5]; subst; auto. }
      assert (J: C <<= undup (sfs U)).
        { unfold sfs, C. rewrite undup_id_equi.
          intros S J|J; subst; apply in_app_iff.
          - right. apply in_map_iff. exists s. split; auto.
            simpl. apply in_app_iff. left. destruct s; simpl; auto.
          - left. apply in_map_iff. apply in_map_iff in J as s1 [J1 J2].
            exists s1. simpl. split; auto. apply in_app_iff.
            right. apply (@scl_incl s1); auto. }
      destruct (@demo_extension (undup (sfs U)) C J I) as [A' B'] [H1 [H2 H3]].
      unfold CD in H1. apply in_map_iff in H1 as C' [H1 H4].
      apply in_filter_iff in H4 as H4 H5.
      assert (H6: C' el cCD).
      { apply E. split; auto. split; auto. unfold compact_CD.
        apply in_map_iff. exists C'. split; auto. unfold clauseCD.
        apply in_filter_iff. auto. }
      assert (K: C2PC C' el map C2PC cCD). { apply in_map_iff. exists C'. auto. }
      rewrite H1 in K. assert (K':= DemoSat F K).
      intros s'. split. intros E1. exfalso. apply E1.
      intros E'|E'; try (exfalso; exact E'). symmetry in E'. subst.
      exists (C2PC (filter pVar_nImp (p_dec:= pVar_nImp_dec) C')). split.
      + unfold compactDemo. apply in_map_iff.
        exists (filter pVar_nImp (p_dec:= pVar_nImp_dec) C'). split; auto.
        unfold compact_CD. apply in_map_iff. exists C'. split; auto.
        unfold clauseCD. apply in_filter_iff. auto.
      + intros G. unfold satisDFK in G. destruct (K' s) as _ K1.
        apply K1. clear K' K1. inv H1.
  Qed.
End CompactDemo. *)