Commits

Paweł Wieczorek  committed 0eac99d

* porządki w drzewie katalogów

  • Participants
  • Parent commits 4aa3f50

Comments (0)

Files changed (40)

File Pc/Lang.v

-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.

File Pc/Pc.v

Empty file removed.

File Pc/Proof.v

-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 := (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.
-
-
-Section ProofInd.
-
-(*
- * W <- Wiedza, |- <- jako siekierka dowodzenia w Coqu
- * P: proof -> Prop
- * Q: infseq -> Prop, r:rule
- *
- * W |-  forall r is, Q(is) -> Q(r:is)
- * -----------------------------------------------------------------
- * W |-  forall proof. P(proof)
- 
-
-Hypothesis T: PcPropSet.
-Hypothesis P: pcProof -> Prop.
-Hypothesis Q: forall proof, PcInfSeq T proof -> Prop.
-Hypothesis HQis: forall proof r is, Q proof is -> Q (r::is).
-
-Fixpoint proof_ind (proof:pcProof) : P proof := 
-match proof return (P proof) with
-| [] => False.
-|
-end.
-*)
-End ProofInd.
-
-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.
-
-

File Pc/Proof_facts.v

-
-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.
-Require Import Sets.Ensembles.
-(*
- * 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.
-  assumption. split.
-  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. 
- assumption. split.
- assumption.
- apply IHproof. assumption.
- apply pcInfSeqAxs_subset. assumption.
- 
-Qed.
-
-Lemma PcProof_need_finite_axs: forall T p,
-    (T |- p) -> exists S, Included _ S T /\ Finite _ S /\ (S |- p).
-Proof.
-intros T p PrvTp.
-destruct PrvTp as [proof PrfTp].
-induction proof.
- contradiction.
- destruct PrfTp as [proof_of_p H].
- destruct PcInfSeq_need_finite_axs with T (a::proof) as [S Inf].
- assumption.
- exists S.
- destruct Inf as [incl finite]. destruct finite as [finite infseq].
- split.
- assumption.
- split. assumption. exists (a::proof). split. assumption.
- assumption.
-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. 
-
-
-Theorem PcDeduction: forall T p q,
-  (T |- p --> q)   <->  (T, p |- q).
-Proof.
-intros. split.
-intros.
-destruct H as [proof PrfT].
-set (proof' := (pcPrfDedu p q)::(pcPrfAx p)::proof).
-exists proof'. simpl. split. auto. split.
-Focus 2. split.
-apply Union_intror. apply In_singleton.
-split.
-apply Union_intror. apply In_singleton.
-apply PcInfSeq_superset with T. apply elem_sub_unionl.
-destruct PrfT.
-
-intros. 
-Qed.

File Pc/Theory.v

Empty file removed.

File Util/Ensemble_facts.v

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

File Util/Ensemble_facts.v.d

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

File 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.
-

File 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.
-

File 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.
-

File Util/Laws.v

-Section Principles.
-
-End Principles.

File Util/Laws.v.d

-Util/Laws.vo Util/Laws.glob: Util/Laws.v

File 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.
-

File Util/List_facts.v.d

-Util/List_facts.vo Util/List_facts.glob: Util/List_facts.v

File Util/Seq.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.

File Util/Seq.v.d

-Util/Seq.vo Util/Seq.glob: Util/Seq.v

File 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.

File Util/Set_calculus.v.d

-Util/Set_calculus.vo Util/Set_calculus.glob: Util/Set_calculus.v

File Util/Theory.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.

File Util/Theory.v.d

-Util/Theory.vo Util/Theory.glob: Util/Theory.v ./Pc/Lang.vo ./Pc/Proof.vo ./Pc/Proof_facts.vo

File metalogic/Pc/Lang.v

+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.

File metalogic/Pc/Pc.v

Empty file added.

File metalogic/Pc/Proof.v

+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 := (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.
+
+
+Section ProofInd.
+
+(*
+ * W <- Wiedza, |- <- jako siekierka dowodzenia w Coqu
+ * P: proof -> Prop
+ * Q: infseq -> Prop, r:rule
+ *
+ * W |-  forall r is, Q(is) -> Q(r:is)
+ * -----------------------------------------------------------------
+ * W |-  forall proof. P(proof)
+ 
+
+Hypothesis T: PcPropSet.
+Hypothesis P: pcProof -> Prop.
+Hypothesis Q: forall proof, PcInfSeq T proof -> Prop.
+Hypothesis HQis: forall proof r is, Q proof is -> Q (r::is).
+
+Fixpoint proof_ind (proof:pcProof) : P proof := 
+match proof return (P proof) with
+| [] => False.
+|
+end.
+*)
+End ProofInd.
+
+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.
+
+

File metalogic/Pc/Proof_facts.v

+
+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.
+Require Import Sets.Ensembles.
+(*
+ * 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.
+  assumption. split.
+  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. 
+ assumption. split.
+ assumption.
+ apply IHproof. assumption.
+ apply pcInfSeqAxs_subset. assumption.
+ 
+Qed.
+
+Lemma PcProof_need_finite_axs: forall T p,
+    (T |- p) -> exists S, Included _ S T /\ Finite _ S /\ (S |- p).
+Proof.
+intros T p PrvTp.
+destruct PrvTp as [proof PrfTp].
+induction proof.
+ contradiction.
+ destruct PrfTp as [proof_of_p H].
+ destruct PcInfSeq_need_finite_axs with T (a::proof) as [S Inf].
+ assumption.
+ exists S.
+ destruct Inf as [incl finite]. destruct finite as [finite infseq].
+ split.
+ assumption.
+ split. assumption. exists (a::proof). split. assumption.
+ assumption.
+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. 
+
+
+Theorem PcDeduction: forall T p q,
+  (T |- p --> q)   <->  (T, p |- q).
+Proof.
+intros. split.
+intros.
+destruct H as [proof PrfT].
+set (proof' := (pcPrfDedu p q)::(pcPrfAx p)::proof).
+exists proof'. simpl. split. auto. split.
+Focus 2. split.
+apply Union_intror. apply In_singleton.
+split.
+apply Union_intror. apply In_singleton.
+apply PcInfSeq_superset with T. apply elem_sub_unionl.
+destruct PrfT.
+
+intros. 
+Qed.

File metalogic/Pc/Theory.v

Empty file added.

File metalogic/Util/Ensemble_facts.v

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

File metalogic/Util/Ensemble_facts.v.d

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

File metalogic/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.
+

File metalogic/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.
+

File metalogic/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.
+

File metalogic/Util/Laws.v

+Section Principles.
+
+End Principles.

File metalogic/Util/Laws.v.d

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

File metalogic/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.
+

File metalogic/Util/List_facts.v.d

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

File metalogic/Util/Seq.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.

File metalogic/Util/Seq.v.d

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

File metalogic/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.

File metalogic/Util/Set_calculus.v.d

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

File metalogic/Util/Theory.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.

File metalogic/Util/Theory.v.d

+Util/Theory.vo Util/Theory.glob: Util/Theory.v ./Pc/Lang.vo ./Pc/Proof.vo ./Pc/Proof_facts.vo