1. Paweł Wieczorek
  2. Metalogic

Commits

Paweł Wieczorek  committed fcc85c6

* Pc: Twierdzenie o zwartości.

  • Participants
  • Parent commits 7bdb437
  • Branches default

Comments (0)

Files changed (2)

File Pc/Proof.v

View file
 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

View file
 
  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,