# Commits

committed fcc85c6

* Pc: Twierdzenie o zwartości.

# File Pc/Proof.v Modified

• Ignore whitespace
• Hide word diff
` match proof with`
` | (pcPrfAx p :: proof) => In T p /\ PcInfSeq T proof`
` | (pcPrfDedu p q :: proof) => `
`-    let U := Union  T (pcProofProps proof)`
`+    let U := (pcProofProps proof)`
`     in In U (p --> q) /\ In U p /\ PcInfSeq T proof`
` | nil => True`
` end.`
` 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.`
` `
` End Theory.`
` `
`+`
`+`
`+`
` Open Scope pc_scope.`
` `
` `

# File Pc/Proof_facts.v Modified

• Ignore whitespace
• Hide word diff
` `
`  simpl. destruct IST_proof as [in1 in2]. destruct in2 as [in2 in3].`
`  split.`
`-  apply H. assumption.`
`-  split. apply H. assumption.`
`+  assumption. split.`
`+  assumption.`
`   apply IHproof. assumption.`
` Qed.`
` `
`  simpl. simpl in infSeq. destruct infSeq as [in1 in2].`
`  destruct in2 as [in2 in3].`
`  split. `
`- apply PcInfSeq_superset.`
`- apply elem_sub_unionl.`
`+ assumption. split.`
`+ assumption.`
`  apply IHproof. assumption.`
`  apply pcInfSeqAxs_subset. assumption.`
`  `
` Qed.`
` `
`-Lemma PcInfSeq_need_finite_axs: forall T p,`
`+Lemma PcProof_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.`
`+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.`
`- apply pcProofAxs_finite with T p. assumption.`
`- induction proof.`
`- contradiction.`
`- `
`+ assumption.`
`+ split. assumption. exists (a::proof). split. assumption.`
`+ assumption.`
` Qed.`
`-*)`
` `
` `
` Theorem PcConsistent_subset: forall T S,`