Commits

Paweł Wieczorek committed 7bdb437

*

Comments (0)

Files changed (21)

 # $Id$
-COQ_MAKEFILE= coq_makefile
+COQ_MAKEFILE= coq_makefile -I .
 GEN_MAKEFILE= Makefile.Coq
 SOURCES= `find . -name \*.v`
 WRAPED_MAKE= ${MAKE} -f ${GEN_MAKEFILE}
+Section PcLangDefinition.
+
+Require Import String.
+
+Require Import Sets.Ensembles.
+Require Import List.
+
+Inductive pcProp :=
+| pcVar : string -> pcProp
+| pcImpl : pcProp -> pcProp -> pcProp
+| pcNeg : pcProp -> pcProp
+| pcTrue : pcProp
+| pcFalse : pcProp
+.
+
+Notation "[ x ]" := (pcVar x) : pc_scope.
+(*
+Notation "[T]" := (pcTrue) : pc_scope.
+Notation "[F]" := (pcFalse) : pc_scope.
+*)
+
+Definition PcPropSet := Ensemble pcProp.
+
+Definition pcProp_dec : forall p1 p2 : pcProp, {p1 = p2} + {p1 <> p2}.
+intros p1 p2.
+decide equality p1 p2.
+apply string_dec.
+Qed.
+
+End PcLangDefinition.
+
+Notation "a --> b" := (pcImpl a b) (at level 85) : pc_scope.
+Notation "! a" := (pcNeg a) (at level 90) : pc_scope.
+
+Open Scope pc_scope.
Empty file added.
+Set Implicit Arguments.
+Require Import Lang.
+Require Import List.
+Require Import Sets.Ensembles.
+Implicit Arguments In.
+Implicit Arguments Union.
+Implicit Arguments Add.
+
+
+Section ProofDef.
+
+
+Inductive pcConseq : Type :=
+ (* pcPrfAx q  : formula q jest w zalozeniach/aksjomatach *)
+| pcPrfAx : pcProp -> pcConseq
+ (* pcPrfDefu p q : formula q jest wynikiem r.odrywania z (p->q) i q *)
+| pcPrfDedu : pcProp -> pcProp -> pcConseq
+.
+
+Definition pcProof := list pcConseq.
+
+Fixpoint pcConseqProp (p:pcConseq) :=
+match p with
+| pcPrfAx p => p
+| pcPrfDedu _ q => q
+end.
+
+Fixpoint pcProofProps (p:pcProof) : PcPropSet :=
+match p with
+| nil => Empty_set _
+| rule :: ps => Add (pcProofProps ps) (pcConseqProp rule)
+end.
+
+Fixpoint pcProofAxs (p:pcProof) : PcPropSet :=
+match p with
+| nil => Empty_set _
+| (pcPrfAx p) :: ps => Add (pcProofAxs ps) p
+| _ :: ps => pcProofAxs ps
+end.
+
+Fixpoint PcInfSeq T (proof:pcProof) : Prop :=
+match proof with
+| (pcPrfAx p :: proof) => In T p /\ PcInfSeq T proof
+| (pcPrfDedu p q :: proof) => 
+    let U := Union  T (pcProofProps proof)
+    in In U (p --> q) /\ In U p /\ PcInfSeq T proof
+| nil => True
+end.
+
+Definition PcPrf T (p:pcProp) (proof:pcProof) : Prop := 
+match proof with
+| (q::_)  => (pcConseqProp q) = p /\ PcInfSeq T proof
+| _ => False
+end.
+
+Definition PcPrv T (p:pcProp) : Prop := exists proof, PcPrf T p proof.
+
+Definition PcCns T : PcPropSet := PcPrv T.
+
+
+End ProofDef.
+
+Notation "T , a" := (Add T a) (at level 90) : pc_scope.
+Notation "T |- p" := (PcPrv T p) (at level 95) : pc_scope.
+
+Section Theory.
+
+Definition PcInconsistent T := exists p, (T |- p) /\ (T |- !p).
+Definition PcConsistent T := ~ PcInconsistent T.
+
+End Theory.
+
+Open Scope pc_scope.
+
+
+Require Import Sets.Ensembles.
+Require Import Lang.
+Require Import Proof.
+Require Import List.
+Require Import Program.Syntax.
+Require Import Set_calculus.
+Require Import Finite_ensembles.
+Require Import Sets.Finite_sets.
+(*
+ * Rozne pomocnicze
+ *)
+
+Section ProofHelpers.
+
+
+
+End ProofHelpers.
+
+(*
+ * Podstawowe techniczne oczywizmy
+ *)
+Section ProofLemmas.
+
+Lemma pcProof_not_empty T p proof :
+      PcPrf T p proof -> exists x xs, proof = x::xs /\ pcConseqProp x = p.
+Proof.
+intros T p proof PrfT_p_prf.
+destruct proof as [ | proof_end proof_rest].
+ (* gdy proof jest nil *)
+ simpl in PrfT_p_prf. contradiction.
+ (* gdy nie *)
+ exists proof_end. exists proof_rest. split. auto.
+ destruct PrfT_p_prf as [ A _ ]. assumption.
+Qed.
+
+Lemma pcInfSeqAxs_subset: forall T proof,
+   PcInfSeq T proof -> Included _ (pcProofAxs proof) T.
+Proof.
+ intros T proof IST.
+ set (S := pcProofAxs proof).
+ induction proof.
+  compute. intros. contradiction.
+ destruct a.
+  simpl in S.
+  unfold "," in S.
+  simpl in IST.
+  destruct IST as [p_inT proof_infseq].
+  
+   intros x inS.
+   destruct inS.
+   apply IHproof. assumption. assumption.
+   compute in H.
+   destruct H. assumption.
+   apply IHproof. 
+   
+  simpl in IST.
+  destruct IST. destruct H0.
+  assumption.
+Qed.
+
+Lemma pcInfSeqAxs_finite: forall T proof,
+   PcInfSeq T proof -> Finite _ (pcProofAxs proof).
+Proof.
+ intros T proof IST.
+ set (S := pcProofAxs proof).
+ induction proof.
+  compute. intros. apply Empty_is_finite.
+ destruct a.
+  simpl in S.
+  unfold "," in S.
+  simpl in IST.
+  destruct IST as [p_inT proof_infseq].
+  apply union_finite. apply pcProp_dec. 
+   apply IHproof. assumption.
+   apply singleton_is_finite.
+  
+  simpl in IST.
+  destruct IST. destruct H0.
+  apply IHproof. 
+  assumption.
+Qed.
+
+Lemma pcProofAxs_subset: forall T p proof,
+  PcPrf T p proof -> Included _ (pcProofAxs proof ) T.
+Proof.
+ intros T p proof PrfT.
+ induction proof.
+  contradiction.
+  destruct PrfT.
+  apply pcInfSeqAxs_subset. assumption.
+Qed.
+
+Lemma pcProofAxs_finite: forall T p proof,
+  PcPrf T p proof -> Finite _ (pcProofAxs proof ).
+Proof.
+ intros T p proof PrfT.
+ induction proof.
+  contradiction.
+  destruct PrfT.
+  apply pcInfSeqAxs_finite with T. assumption.
+Qed.
+ 
+End ProofLemmas.
+
+
+(*
+ * 
+ *)
+
+Theorem PcInfSeq_superset: forall T S proof, Included _ T S -> PcInfSeq T proof -> PcInfSeq S proof.
+Proof.
+intros T S proof TsubsetS IST_proof.
+induction proof.
+simpl. auto.
+destruct a.
+
+ simpl in IST_proof.
+ simpl. destruct IST_proof as [pInT IST_subproof].
+ split. apply TsubsetS. assumption. apply IHproof.
+ assumption.
+
+ simpl in IST_proof.
+ assert (Included _ (Union T (pcProofProps proof)) (Union S (pcProofProps proof))) as H.
+ apply union_subl. assumption.
+
+ simpl. destruct IST_proof as [in1 in2]. destruct in2 as [in2 in3].
+ split.
+  apply H. assumption.
+  split. apply H. assumption.
+  apply IHproof. assumption.
+Qed.
+
+
+Theorem T_in_CnsT: forall T, Included _ T (PcCns T).
+Proof.
+intros. intros x inT.
+set (prfx := [pcPrfAx x]).
+unfold Ensembles.In. unfold PcCns.
+exists prfx.
+simpl. split. auto. auto.
+Qed.
+
+Theorem PcProof_superset: forall T S p, Included _ T S -> (T |- p) -> (S |- p).
+Proof.
+intros T S p TisSubsetS PrvT_p.
+destruct PrvT_p as [prf PrfT_p].
+exists prf.
+induction prf. contradiction.
+ destruct PrfT_p as [prf_end prfinfseq].
+ split. assumption.
+ apply PcInfSeq_superset with T. assumption. assumption.
+Qed.
+
+
+Theorem PcProof_superset1: forall T a p, (T |- p) -> (T, a |- p).
+Proof.
+intros.
+apply PcProof_superset with T.
+ intros x inT. apply Union_introl. assumption.
+ assumption.
+Qed.
+
+
+Lemma PcInfSeq_need_finite_axs: forall T proof,
+     PcInfSeq T proof -> exists S, Included _ S T /\ Finite _ S /\ PcInfSeq S proof.
+Proof.
+intros T proof infSeq.
+set (S := pcProofAxs proof).
+exists S.
+assert (Included pcProp S T) as Hinc.
+apply pcInfSeqAxs_subset. assumption.
+split.
+ assumption.
+ split. apply pcInfSeqAxs_finite with T. assumption.
+ induction proof.
+ auto.
+ destruct a.
+ simpl. simpl in infSeq. destruct infSeq as [inT H]. split. 
+ simpl in S. apply elem_sub_unionr. apply In_singleton.
+ apply PcInfSeq_superset with (pcProofAxs proof).
+ apply elem_sub_unionl.
+ apply IHproof. assumption.
+ apply pcInfSeqAxs_subset. assumption.
+
+ simpl. simpl in infSeq. destruct infSeq as [in1 in2].
+ destruct in2 as [in2 in3].
+ split. 
+ apply PcInfSeq_superset.
+ apply elem_sub_unionl.
+ apply IHproof. assumption.
+ apply pcInfSeqAxs_subset. assumption.
+ 
+Qed.
+
+Lemma PcInfSeq_need_finite_axs: forall T p,
+    (T |- p) -> exists S, Included _ S T /\ Finite _ S /\ (S |- p).
+Proof.
+intros T p PrvTp.
+induction PrvTp as [proof PrfTp].
+set (S := pcProofAxs proof).
+exists S.
+assert (Included pcProp S T) as Hinc.
+apply pcProofAxs_subset with p. assumption.
+split.
+ assumption.
+ split.
+ apply pcProofAxs_finite with T p. assumption.
+ induction proof.
+ contradiction.
+ 
+Qed.
+*)
+
+
+Theorem PcConsistent_subset: forall T S,
+ PcConsistent T -> Included _ S T -> PcConsistent S.
+Proof.
+intros.
+intro.
+absurd (PcInconsistent T).
+ assumption.
+ destruct H1.
+ destruct H1.
+ exists x.
+ split.
+ apply PcProof_superset with S. assumption. assumption.
+ apply PcProof_superset with S. assumption. assumption.
+
+Qed.
+
+Theorem PcCompactness: forall T,
+ PcConsistent T <-> (forall S, Included _ S T -> Finite _ S -> PcConsistent S).
+Proof.
+intros.
+split.
+intros.
+apply PcConsistent_subset with T. assumption. assumption.
+
+intros.
+intro IncT.
+destruct IncT as [p incProof]. destruct incProof as [Tp Tnp].
+destruct PcProof_need_finite_axs with T p as [A HA]. assumption.
+ destruct HA as [AsubsetT HA]. destruct HA as [Afinite Ap].
+destruct PcProof_need_finite_axs with T (!p) as [B HB]. assumption.
+ destruct HB as [BsubsetT HB]. destruct HB as [Bfinite Bnp].
+set (C := Union A B).
+assert (PcInconsistent C) as incC.
+exists p. split.
+apply PcProof_superset with A.
+apply elem_sub_unionl. assumption.
+apply PcProof_superset with B.
+apply elem_sub_unionr. assumption.
+absurd (PcInconsistent C).
+apply H. apply union_preserves_subset. assumption. assumption.
+apply union_finite. apply pcProp_dec. assumption. assumption.
+ assumption.
+Qed. 
Empty file added.

Util/Ensemble_facts.v

+Require Import Sets.Ensembles.
+
+
+(*
+ * (A + B) + C = 
+ *)
+Theorem U {T:Type}: forall T A B C: 

Util/Ensemble_facts.v.d

+Util/Ensemble_facts.vo Util/Ensemble_facts.glob: Util/Ensemble_facts.v

Util/Finite_ensembles

+
+Require Import Sets.Finite_sets.
+Require Import Logic.Decidable.
+Require Import Sets.Ensembles.
+Require Import Set_calculus.
+
+Section S1.
+
+Variable U:Type.
+Variable A B C D: Ensemble U.
+Check eq.
+Variable decU: forall a b:U, decidable(eq a b).
+
+Lemma singleton_decidable (a:U) (x:U) : decidable (In _ (Singleton _ a) x).
+Proof.
+ intros a x.
+ destruct decU with a x.
+ left. compute. rewrite H. apply In_singleton.
+ right. intro. inversion H0. contradiction.
+Qed.
+
+
+Lemma finite_set_is_decidable: Finite _ A -> forall a, decidable (In _ A a).
+Proof.
+intros FA.
+induction FA.
+intros. right. intro. contradiction.
+intros.
+ destruct IHFA with a.
+ left. apply Union_introl. assumption.
+ destruct decU with a x.
+ left. apply Union_intror. rewrite H1. apply In_singleton.
+ right. intro. destruct H2. contradiction. inversion H2. symmetry in H3.
+ contradiction.
+Qed.
+
+
+End S1.
+
+Section S2.
+
+Variable U:Type.
+Variable A B C D: Ensemble U.
+Check eq.
+Variable decU: forall a b:U, decidable(eq a b).
+
+
+Lemma union_finite:
+ Finite _ A -> Finite _ B -> Finite _ (Union _ A B).
+Proof.
+ intros FA FB.
+ induction FA.
+ rewrite union_emptyl.
+ assumption.
+ unfold Add.
+ rewrite union_AB_C_eq_AC_B.
+ destruct finite_set_is_decidable with U B x.
+ apply decU. assumption.
+ replace (Union U (Union U A B) (Singleton U x))
+  with (Add _ (Union _ A B) x).
+ rewrite set_add_same.
+ apply IHFA. apply Union_intror. assumption.
+ auto.
+
+ assert (~(In U (Union _ A B) x)).
+ intro. destruct H1. contradiction. contradiction.
+ apply Union_is_finite. assumption. assumption.
+Qed.
+
+End S2.
+

Util/Finite_ensembles.

+
+Require Import Sets.Finite_sets.
+Require Import Logic.Decidable.
+Require Import Sets.Ensembles.
+Require Import Set_calculus.
+
+Section S1.
+
+Variable U:Type.
+Variable A B C D: Ensemble U.
+Check eq.
+Variable decU: forall a b:U, decidable(eq a b).
+
+Lemma singleton_decidable (a:U) (x:U) : decidable (In _ (Singleton _ a) x).
+Proof.
+ intros a x.
+ destruct decU with a x.
+ left. compute. rewrite H. apply In_singleton.
+ right. intro. inversion H0. contradiction.
+Qed.
+
+
+Lemma finite_set_is_decidable: Finite _ A -> forall a, decidable (In _ A a).
+Proof.
+intros FA.
+induction FA.
+intros. right. intro. contradiction.
+intros.
+ destruct IHFA with a.
+ left. apply Union_introl. assumption.
+ destruct decU with a x.
+ left. apply Union_intror. rewrite H1. apply In_singleton.
+ right. intro. destruct H2. contradiction. inversion H2. symmetry in H3.
+ contradiction.
+Qed.
+
+
+End S1.
+
+Section S2.
+
+Variable U:Type.
+Variable A B C D: Ensemble U.
+Check eq.
+Variable decU: forall a b:U, decidable(eq a b).
+
+
+Lemma union_finite:
+ Finite _ A -> Finite _ B -> Finite _ (Union _ A B).
+Proof.
+ intros FA FB.
+ induction FA.
+ rewrite union_emptyl.
+ assumption.
+ unfold Add.
+ rewrite union_AB_C_eq_AC_B.
+ destruct finite_set_is_decidable with U B x.
+ apply decU. assumption.
+ replace (Union U (Union U A B) (Singleton U x))
+  with (Add _ (Union _ A B) x).
+ rewrite set_add_same.
+ apply IHFA. apply Union_intror. assumption.
+ auto.
+
+ assert (~(In U (Union _ A B) x)).
+ intro. destruct H1. contradiction. contradiction.
+ apply Union_is_finite. assumption. assumption.
+Qed.
+
+End S2.
+

Util/Finite_ensembles.v

+
+Require Import Sets.Finite_sets.
+Require Import Logic.Decidable.
+Require Import Sets.Ensembles.
+Require Import Set_calculus.
+
+Section S1.
+
+Variable U:Type.
+Variable A B C D: Ensemble U.
+Check eq.
+Variable decU: forall a b:U, {a=b} + {a<>b}.
+
+Lemma singleton_decidable (a:U) (x:U) : decidable (In _ (Singleton _ a) x).
+Proof.
+ intros a x.
+ destruct decU with a x.
+ left. compute. rewrite e. apply In_singleton.
+ right. intro. inversion H. contradiction.
+
+Qed.
+
+
+Lemma finite_set_is_decidable: Finite _ A -> forall a, decidable (In _ A a).
+Proof.
+intros FA.
+induction FA.
+intros. right. intro. contradiction.
+intros.
+ destruct IHFA with a.
+ left. apply Union_introl. assumption.
+ destruct decU with a x.
+ left. apply Union_intror. rewrite e. apply In_singleton.
+ right. intro. destruct H1. contradiction. inversion H1. symmetry in H2.
+ contradiction.
+Qed.
+
+
+End S1.
+
+Section S2.
+
+Variable U:Type.
+Variable A B C D: Ensemble U.
+Check eq.
+Variable decU: forall a b:U, {a=b} + {a<>b}.
+
+Lemma union_finite:
+ Finite _ A -> Finite _ B -> Finite _ (Union _ A B).
+Proof.
+ intros FA FB.
+ induction FA.
+ rewrite union_emptyl.
+ assumption.
+ unfold Add.
+ rewrite union_AB_C_eq_AC_B.
+ destruct finite_set_is_decidable with U B x.
+ apply decU. assumption.
+ replace (Union U (Union U A B) (Singleton U x))
+  with (Add _ (Union _ A B) x).
+ rewrite set_add_same.
+ apply IHFA. apply Union_intror. assumption.
+ auto.
+
+ assert (~(In U (Union _ A B) x)).
+ intro. destruct H1. contradiction. contradiction.
+ apply Union_is_finite. assumption. assumption.
+Qed.
+
+End S2.
+
+Section Principles.
+
+End Principles.
+Util/Laws.vo Util/Laws.glob: Util/Laws.v

Util/List_facts.v

+Require Import List.
+
+
+Lemma list_eq: forall T (x:T) y (xs:list T) ys, x::xs = y::ys -> x = y /\ xs = ys.
+Proof.
+intros.
+inversion H.
+auto.
+Qed.
+

Util/List_facts.v.d

+Util/List_facts.vo Util/List_facts.glob: Util/List_facts.v
+
+Section Seq.
+
+Inductive ProofSeq : Type :=
+| Seq_intro: nat -> (nat -> pcProp) -> ProofSeq
+.
+
+(*
+Definition nth n (xs:Seq default) :=
+match xs with Seq_intro N f =>
+match (N-n) with
+| 0 => default
+| _ => f n
+end end.
+
+Definition append (xs:Seq default) (ys:Seq default) := 
+match (xs,ys) with
+ (Seq_intro xN xF, Seq_intro yN yF) =>
+  let f n := match (xN - n)  with
+      | 0 => yF (n - xN)
+      | _ => xF n
+      end in Seq_intro default (xN + yN) f
+end.
+
+Definition last (xs:Seq default) :=
+match xs with
+ (Seq_intro N F) => F (N-1)
+end.
+
+Definition head (xs:Seq default) :=
+match xs with
+ (Seq_intro N F) => F 0
+end.
+
+Definition tail (xs:Seq default) :=
+match xs with
+ (Seq_intro N F) => Seq_intro default (N-1) (fun n => F (n+1))
+end.
+*)
+
+End Seq.
+Util/Seq.vo Util/Seq.glob: Util/Seq.v

Util/Set_calculus.v

+Require Import Sets.Ensembles.
+Require Import Sets.Finite_sets.
+Require Import Setoid.
+Require Import Logic.Decidable.
+(*
+ * Podstawowe rownosci z "rachunku zbiorow". Albo jestem slepy albo rzeczywiscie
+ * w stdlib'ie Coq'a tego nie ma.
+ *)
+
+Section Ensemble_Calculus.
+
+Variable U : Type.
+Variable A B C D: Ensemble U.
+
+(*
+ * Union
+ * union_symm: A + B = B + A
+ * union_conn: A + (B + C) = (A + B) + C
+ * union_sub: A < C /\  B < D -> A + B < C + D
+ * union_empty: A + 0 = A.
+ * subset_trans: A < B -> B < C -> A < C
+ * union_preserve_subset: A < C -> B < C -> A + B < C
+ *)
+
+
+Check Union.
+Lemma union_symm: Union _ A B = Union _ B A.
+Proof.
+apply Extensionality_Ensembles.
+split.
+
+compute. intros.
+   inversion H.
+        apply Union_intror. assumption.
+        apply Union_introl. assumption.
+
+compute. intros. 
+   inversion H.
+        apply Union_intror. assumption.
+        apply Union_introl. assumption.
+Qed.
+
+Lemma union_conn: Union _ A (Union _ B C) = Union _ (Union _ A B) C.
+Proof.
+apply Extensionality_Ensembles.
+split.
+
+compute. intros x A_BC.
+ destruct A_BC as [x inA | x inBC].
+     apply Union_introl. apply Union_introl. assumption.
+     destruct inBC.
+       apply Union_introl. apply Union_intror. assumption.
+       apply Union_intror. assumption.
+
+compute. intros x AB_C.
+ destruct AB_C as [x inAB | x inC ].
+     destruct inAB.
+       apply Union_introl. assumption.
+       apply Union_intror. apply Union_introl. assumption.
+     apply Union_intror. apply Union_intror. assumption.
+Qed.
+
+
+Lemma union_sub:
+ Included _ A C -> Included _ B D -> Included _ (Union _ A B) (Union _ C D).
+Proof.
+intros AsubC BsubD.
+intros x inAB.
+destruct inAB.
+ apply Union_introl. apply AsubC. assumption.
+ apply Union_intror. apply BsubD. assumption.
+Qed.
+
+Lemma union_emptyl:
+ Union _ (Empty_set _) A = A.
+Proof.
+apply Extensionality_Ensembles.
+split.
+ intros x inU.
+ destruct inU.
+ contradiction.
+ assumption.
+
+ intros x inU.
+ apply Union_intror. assumption.
+Qed.
+
+Theorem set_equal: A = B -> Included _ A B /\ Included _ B A.
+Proof.
+intros.
+split.
+rewrite H. intros b inb. assumption.
+rewrite H. intros b inb. assumption.
+Qed.
+
+
+Lemma set_add_same (x:U) : In _ A x -> Add _ A x = A.
+Proof.
+intros.
+apply Extensionality_Ensembles.
+split. intros y inY. destruct inY.
+ assumption. inversion H0. rewrite <- H1.
+ assumption.
+ intros y inY. apply Union_introl. assumption.
+Qed.
+
+Lemma subset_trans: Included _ A B -> Included _ B C -> Included _ A C.
+Proof.
+intros.
+compute. intros. apply H0. apply H. assumption.
+Qed.
+
+Lemma union_preserves_subset:
+ Included _ A C -> Included _ B C -> Included _ (Union _ A B) C.
+Proof.
+intros. intros x inX. destruct inX.
+apply H. assumption.
+apply H0. assumption.
+Qed.
+
+End Ensemble_Calculus.
+
+
+
+Section C2.
+
+Variable U : Type.
+Variable A B C : Ensemble U.
+
+
+(*
+ * union_AB_C_eq_AC_B: (A + B) + C = (A + C) + B
+ * union_subl: A < C -> A + B < C + B
+ * union_add: ( A + {x} ) + B = (A + B) + {x}
+ * elem_sub_union: A < A + B
+ *) 
+
+Lemma union_AB_C_eq_AC_B: Union _ (Union _ A B) C = Union _ (Union _ A C) B.
+Proof.
+replace (Union U A B) with (Union U B A).
+rewrite <- union_conn.
+rewrite union_symm.
+auto. apply union_symm.
+Qed.
+
+
+Lemma union_subl:
+ Included _ A C -> Included _ (Union _ A B) (Union _ C B).
+Proof.
+ intros.
+ apply union_sub. 
+ assumption. intros x inB. assumption.
+Qed.
+
+Lemma union_emptyr:
+ Union _ A (Empty_set _) = A.
+Proof.
+rewrite <- union_symm. apply union_emptyl.
+Qed.
+
+Lemma union_eq_empty:
+ (Union _ A B = Empty_set _) -> A = Empty_set _ /\ B = Empty_set _.
+Proof.
+intros.
+destruct set_equal with U (Union U A B) (Empty_set U). assumption.
+compute in H0. compute in H1.
+split.
+ apply Extensionality_Ensembles.
+ split.
+ intros x inX.  apply H0. apply Union_introl. assumption.
+ intros x inX. contradiction.
+ apply Extensionality_Ensembles.
+ split.
+ intros x inX. apply H0. apply Union_intror. assumption.
+ intros x inX. contradiction.
+Qed.
+
+Lemma singleton_is_finite (x:U): Finite U (Singleton U x).
+Proof.
+intros.
+rewrite <- union_emptyl.
+apply Union_is_finite. apply Empty_is_finite.
+intro H. contradiction.
+Qed.
+
+Lemma elem_sub_unionl: Included _ A (Union _ A B).
+Proof.
+compute. intros x inX. apply Union_introl. assumption.
+Qed.
+
+Lemma elem_sub_unionr: Included _ B (Union _ A B).
+Proof.
+compute. intros x inX. apply Union_intror. assumption.
+Qed.
+
+End C2.
+
+
+Section C3.
+
+Variable U : Type.
+Variable A B C : Ensemble U.
+
+
+End C3.

Util/Set_calculus.v.d

+Util/Set_calculus.vo Util/Set_calculus.glob: Util/Set_calculus.v
+Require Import Lang.
+Require Import Proof.
+Require Import Proof_facts.
+Require Import Sets.Ensembles.
+Require Import Sets.Finite_sets.
+Section TheoryDefs.
+
+
+Definition PcConsistentTheory T:= exists p, ~ (T |- p).
+Definition PcInconsistentTheory T:= exists p, (T |- p) /\ (T |- !p).
+Definition PcCompleteTheory T:= forall p, (T |- p) \/ (T |- !p).
+
+
+Theorem T0:
+ forall T S, PcConsistentTheory T -> Included _ S T -> PcConsistentTheory S.
+Proof.
+ intros T S consT subset.
+ destruct consT.
+ exists x.
+ intro Sx.
+ absurd (T |- x).
+ assumption.
+ apply PcProof_superset.
+Qed.
+
+Theorem PcCompactness: 
+ forall T S, PcConsistentTheory T <-> (Included _ S T -> Finite _ S -> PcConsistentTheory S).
+Proof.
+intros.
+split.
+ intros.
+
+(*
+Nie wiem czy powinienem byc zainteresowany tym dowodem, bez NNP on nie przejdzie.
+
+Theorem PcInconsistentTheory_corr T:
+  PcInconsistentTheory T <-> ~PcConsistentTheory T.
+Proof.
+ intros T. split.
+ intros inc. unfold PcConsistentTheory.
+*)
+
+End TheoryDefs.
+Util/Theory.vo Util/Theory.glob: Util/Theory.v ./Pc/Lang.vo ./Pc/Proof.vo ./Pc/Proof_facts.vo