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
| +s ⇒ match s with | Var _ ⇒ True | _ ⇒ False end
| -s ⇒ False
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
| +s ⇒ False
| -s ⇒ match 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 X→Prop) 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 C ⇒ filter 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. *)
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
| +s ⇒ match s with | Var _ ⇒ True | _ ⇒ False end
| -s ⇒ False
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
| +s ⇒ False
| -s ⇒ match 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 X→Prop) 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 C ⇒ filter 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. *)