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