Commits

Paweł Wieczorek committed c739825

Comments (0)

Files changed (3)

metalogic/Fol/Lang.v

 Require Import metalogic.Util.Tactics.
 Require Import Arith.Wf_nat.
 Require Import Arith.Max.
+Require Import Arith.Peano_dec.
 Require Import Program.Equality.
 
 Reserved Notation "T ,, a"  (at level 75, right associativity).
 | folTcons n t ts => folTermFV t ++ folTermListFV _ ts
 end.
 
+Fixpoint folTermC t :=
+match t with
+| folVar y => nil
+| folApp f ts => if eq_nat_dec (folFuncAr L f) 0
+      then t::nil
+      else nil
+end
+with folTermListC n (ts:folTermList n) :=
+match ts with
+| folTnil => nil
+| folTcons n t ts => folTermC t ++ folTermListC _ ts
+end.
+
 
 Definition folTerm_closed t := folTermFV t = nil.
 Definition folTermList_closed n ts := folTermListFV n ts = nil.
 Definition folTerm_noFV t x := ~ List.In x (folTermFV t).
 Definition folTermList_noFV n t x := ~ List.In x (folTermListFV n t).
 
+Definition folTerm_noC t c := ~ List.In c (folTermC t).
+
 Lemma folTerm_0eq: forall ts : folTermList 0 , ts = folTnil.
 Proof.
 intros.
 end
 .
 
+Fixpoint folPropC p :=
+match p with
+| folTrue => nil
+| folAtom r ts => folTermListC _ ts
+| folImpl p q => folPropC p ++ folPropC q
+| folNeg p => folPropC p
+| folForall x p => folPropC p
+| folExists x p => folPropC p
+end
+.
+
 Fixpoint folPropBV p : list string :=
 match p with
 | folTrue => nil
 
 Definition folProp_closed p := folPropFV p = nil.
 Definition folProp_noFV p x := ~ List.In x (folPropFV p).
+Definition folProp_C p c := List.In c (folPropC p).
+Definition folProp_noC p c := ~ List.In c (folPropC p).
 Definition folPropSet_closed (T:FolPropSet) := forall p, folProp_closed p.
+Definition folConstantS c := folFuncAr L c = 0.
+
+Definition folConstant t := match t with
+ | folVar _ => False
+ | folApp f xs => folConstantS f
+end.
+
+Definition FolPropSetC T : Ensemble (folTerm) := fun c => exists p, In T p /\ folProp_C p c.
+Definition FolPropSet_noC T c := ~ In (FolPropSetC T) c.
 
 Inductive FolSubstCorr x s : folProp -> Prop := 
 | folSubstCorr_const: forall p, folTerm_closed s -> FolSubstCorr x s p

metalogic/Fol/Proof_facts4.v

 admit.
 Qed.
 
-    
+(**------------------------------------------------------------------------
+ * Lemat o stalej: Jezeli stala c nie wystepuje w aksjomatach teorii T
+ * to T |- f[x ~> c] pociaga za soba T |- Ax.f
+ *)
+
+Lemma folDeriv_constant L T (p:folProp L) x c: 
+      FolPropSet_noC L T c
+   -> folDeriv T (p <[ x ~> c ]>)
+   -> folDeriv T ([[A x]] p).
+Proof.
+admit.
+Qed.

metalogic/Fol/TheoremModelExistence.v

 Require Import metalogic.Util.Defs.
 Require Import metalogic.Util.Laws.
 Require Import Program.Equality.
+Require Import Arith.Div2.
 Require Import Arith.
 Require Import List.
 Require Import String.
  **************************************************************************
  **************************************************************************
  * Rozszerzanie do teorii swiadkowo zupelnej (opisowo konstruktywnej).
- *
+ *)
 
 
+(**************************************************************************
+ * Sygnatura.
+ *)
+
 Module Type WitnessExtensionDef. 
 
-Include Type AscendingSetsChainDef.
+Include Type AscendingSetsChainDefP.
 
-Parameter L : FolLang.
-
-Definition LextFuncs := sum (folFuncs L) (nat).
-
-Parameter EnumSig: nat -> { p : folProp L | folPropFV L p = cons "x"%string nil }.
+Definition LextFuncs L := sum (folFuncs L) (nat).
 
 End WitnessExtensionDef.
 
-(**------------------------------------------------------------------------
+(**************************************************************************
+ * Rozszerzanie jezyka i teorii tak aby byly opisowo konstruktywne.
  *)
 
 Module WitnessExtensionChain (M:WitnessExtensionDef) <: AscendingSetsChainDef.
 Import M.
 Export M.
 
-Let folFuncEqDec': forall f1 f2 : LextFuncs, {f1=f2} + {f1<>f2}.
+(**------------------------------------------------------------------------
+ * Konstrukcja nowego jezyka.
+ *)
+
+Let lang_func_eq_dec L : forall f1 f2 : LextFuncs L, {f1=f2} + {f1<>f2}.
 Proof.
 intros.
 destruct f1; destruct f2; try (right;discriminate).
 deceq (eq_nat_dec).
 Defined.
 
-Let folFuncAr' (f:LextFuncs) :=
+Let lang_func_ar L (f:LextFuncs L) :=
 match f with
 | inl f => folFuncAr L f
 | inr n => 0
 end.
 
-Definition L' : FolLang := folLang
-   (LextFuncs)
-   (folFuncEqDec')
-   (folFuncAr')
+Let lang_c L : {c : LextFuncs L | lang_func_ar L c = 0}.
+Proof.
+intros.
+exists (inr 0).
+auto.
+Qed.
+
+Let lang_func_num L n := 
+if eq_nat_dec (2*(div2 n)) n
+then inl (folFuncNum L (div2 n))
+else inr (div2 n).
+
+Let lang_func_num_corr L : forall f : LextFuncs L, exists n : nat, lang_func_num L n = f.
+Proof.
+admit.
+Qed.
+
+Definition LW L := folLang
+   (LextFuncs L)
+   (lang_func_eq_dec L)
+   (lang_func_ar L)
    (folRels L)
    (folRelAr L)
    (folRelEqDec L)
+   (lang_c L)
+   (lang_func_num L)
+   (lang_func_num_corr L)
+   (folRelNum L)
+   (folRelCnt L)
 .
 
-Let funcMap f : LextFuncs := inl f.
-Let relMap r: folRels L := r.
+(**------------------------------------------------------------------------
+ * Wskazanie rozszerzenia.
+ *)
 
-Let Far : forall f, folFuncAr L f = folFuncAr L' (inl f).
+Let funcMap L f : LextFuncs L := inl f.
+Let relMap L r: folRels L := r.
+
+Let Far L : forall f, folFuncAr L f = folFuncAr (LW L) (inl f).
 intros.
 simpl. auto.
 Qed.
 
-Let Rar : forall r, folRelAr L r = folRelAr L' r.
+Let Rar L : forall r, folRelAr L r = folRelAr (LW L) r.
 intros.
 simpl. auto.
 Qed.
 
-Let mapP := folLangMapP L L' funcMap relMap Far Rar.
+Let LEXT L := folLangExt L (LW L)
+     (funcMap L)
+     (relMap L)
+     (Far L)
+     (Rar L)
+.
+
+Let mapP L := folPropMap (LEXT L).
 
 Let Enum n:= projT1 (EnumSig n).
 Let Enum' n := mapP (Enum n).
 apply folTermClosed_intro with (folTermClosed_unpack L (folSomeClosedTerm L)).
 destruct folSomeClosedTerm.
 simpl. auto.
-Defined.
+Qed.
 
 (**************************************************************************
  * Nadawanie interpretacji symbolom funkcyjnym i relacja.
 unfold folTermClosed_unpack.
 destruct x.
 auto.
-Defined.
+Qed.
+
 
 (*
 Fixpoint folCollectTermArgs n : nAryB n (folTermList L n) Muniv :=
 destruct ts as [ts Hts].
 simpl.
 auto.
-Defined.
+Qed.
 
 Let Mrel: forall r : folRels L, Defs.nAryP (folRelAr L r) Muniv :=
 fun r => folCollectApp Prop (folRelAr L r) 
 (**************************************************************************
  * TWIERDZENIE O ISTNIENIU MODELU.
  * Teoria T ma model gdy jest niesprzeczna.
+ *
+ * (Opis wszystkich tych twierdzen FolModelExistence* naraz)
+ *
+ * 1. Skoro jest T niesprzeczna to mozemy ja rozszerzyc i jej jezyk L.
+ *    Nazwijmy rozszerzona teorie jako T', a rozszerzony jezyk jako L'.
+ * 2. Wiemy ze T' dalej jest niesprzeczna, wiec mozemy uzupelnij ja do
+ *    teorii zupelnej, nazwijmy ja T*, ktora dalej jest niesprzeczna.
+ * 3. T* jest swiadkowo zupelna (opisowo konstruktywna) i zupelna,
+ *    zatem ma model M. Model M jest struktura nad sygnatura jezyka L'.
+ * 4. Obcinajac M do sygnatur L otrzymujemy model dla wejsciowej teorii T.
  *)
 
 Theorem FolModelExistence : forall L (T:FolPropSet L),
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.