Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 434:5f22af3562b7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generic filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 18 Feb 2022 11:44:08 +0900
parents e787d37d27a0
children b18ca68d115a
files src/generic-filter.agda src/partfunc.agda
diffstat 2 files changed, 47 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Sat Sep 04 01:43:27 2021 +0900
+++ b/src/generic-filter.agda	Fri Feb 18 11:44:08 2022 +0900
@@ -54,31 +54,22 @@
 import OPair
 open OPair O
 
-record CountableOrdinal : Set (suc (suc n)) where
-   field
-       ctl→ : Nat → Ordinal
-       ctl← : Ordinal → Nat
-       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
-       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
-
-record CountableHOD : Set (suc (suc n)) where
+record CountableModel : Set (suc (suc n)) where
    field
-       mhod : HOD
-       mtl→ : Nat → Ordinal
-       mtl→∈P : (i : Nat) → odef mhod (mtl→ i)
-       mtl← : (x : Ordinal) → odef mhod x → Nat
-       mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x 
-       mtl-iso← : { x : Nat }  → mtl← (mtl→ x ) (mtl→∈P x) ≡ x
-   
-       
-open CountableOrdinal 
-open CountableHOD
+       ctl-M : Ordinal
+       ctl→ : Nat → Ordinal
+       ctl← : (x : Ordinal )→  x o< ctl-M → Nat
+       is-Model : (x : Nat) → ctl→ x o< ctl-M
+       ctl-iso→ : { x : Ordinal } → (lt : x o< ctl-M)  → ctl→ (ctl← x lt ) ≡ x 
+       ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (is-Model x)  ≡ x
+
+open CountableModel 
 
 ----
 --   a(n) ∈ M
 --   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
 --
-PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
+PGHOD :  (i : Nat) → (C : CountableModel) → (P : HOD) → (p : Ordinal) → HOD
 PGHOD i C P p = record { od = record { def = λ x  →
        odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
    ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  
@@ -92,16 +83,16 @@
 next-p p f | no not = & (ODC.minimal O (f (* p) ) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
 
 ---
---  ascendant search on p(n)
+--  search on p(n)
 --
-find-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
+find-p :  (C : CountableModel) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
 find-p C P Zero x = x
 find-p C P (Suc i) x = find-p C P i ( next-p x (λ p → PGHOD i C P (& p) ))
 
 ---
 -- G = { r ∈ Power P | ∃ n → r ⊆ p(n) }
 --
-record PDN  (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where
+record PDN  (C : CountableModel) (P : HOD ) (x : Ordinal) : Set n where
    field
        gr : Nat
        pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
@@ -112,7 +103,7 @@
 ---
 -- G as a HOD
 --
-PDHOD :  (C : CountableOrdinal) → (P : HOD ) → HOD
+PDHOD :  (C : CountableModel) → (P : HOD ) → HOD
 PDHOD C P = record { od = record { def = λ x →  PDN C P x }
     ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  } 
 
@@ -122,7 +113,7 @@
 --  Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
 --
 --  p 0 ≡ ∅
---  p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
+--  p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q  (by axiom of choice) ( q =  * ( ctl→ n ) )
 ---             else p n
 
 P∅ : {P : HOD} → odef (Power P) o∅
@@ -134,18 +125,33 @@
 
 open _⊆_
 
-P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
+P-GenericFilter : (C : CountableModel) → (P : HOD ) → GenericFilter P
 P-GenericFilter C P = record {
-      genf = record { filter = PDHOD C P ; f⊆PL =  f⊆PL ; filter1 = {!!} ; filter2 = {!!} }
+      genf = record { filter = PDHOD C P ; f⊆PL =  f⊆PL ; filter1 = f1 ; filter2 = f2 }
     ; generic = λ D → {!!}
    } where
-        find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y 
-        find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso
+        PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  PGHOD i C P x ⊆ Power P
+        PGHOD∈PL i x = record { incl = λ {x} p → proj1 p }
+        find-p-⊆P :  (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y 
+        find-p-⊆P Zero x y Px Py = subst (λ k → odef P k ) &iso
             ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
-        find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p x (λ p → PGHOD i C P (& p)))   y {!!} {!!}
+        find-p-⊆P (Suc i) x y Px Py with is-o∅  ( & (PGHOD i C P (& (* x))))
+        ... | yes y1 = find-p-⊆P i x y Px Py
+        ... | no not = find-p-⊆P i (& fmin) y pg-01 Py where
+            fmin : HOD
+            fmin = ODC.minimal O (PGHOD i C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
+            fmin∈PGHOD : PGHOD i C P (& (* x)) ∋ fmin
+            fmin∈PGHOD = ODC.x∋minimal O (PGHOD i C P (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
+            pg-01 : Power P ∋ fmin 
+            pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i C P k ∋ fmin ) &iso  fmin∈PGHOD )
         f⊆PL :  PDHOD C P ⊆ Power P
         f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
-             find-p-⊆P C P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
+             find-p-⊆P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
+        f1 : {p q : HOD} → q ⊆ P → PDHOD C P ∋ p → p ⊆ q → PDHOD C P ∋ q
+        f1 {p} {q}  q⊆P PD∋p p⊆q = {!!}
+        f2 : {p q : HOD} → PDHOD C P ∋ p → PDHOD C P ∋ q → PDHOD C P ∋ (p ∩ q)
+        f2 {p} {q} PD∋p PD∋q = {!!}
+
 
 
 open GenericFilter
@@ -153,13 +159,14 @@
 
 record Incompatible  (P : HOD ) : Set (suc (suc n)) where
    field
-      except : HOD → ( HOD ∧ HOD )
-      incompatible : { p : HOD } →  Power P ∋ p  →  Power P ∋ proj1 (except p )  →  Power P ∋ proj2 (except p ) 
-          → ( p ⊆ proj1 (except p)  ) ∧ ( p ⊆ proj2 (except p)  )
-          → ∀ ( r : HOD ) →  Power P ∋ r → ¬ (( proj1 (except p)  ⊆ r ) ∧ ( proj2 (except p)  ⊆ r ))
+      q : {p : HOD } → Power P ∋ p → HOD 
+      r : {p : HOD } → Power P ∋ p → HOD 
+      incompatible : { p : HOD } →  (P∋p : Power P ∋ p)  →  Power P ∋ q P∋p  →  Power P ∋ r P∋p
+          → ( p ⊆ q P∋p)   ∧ ( p ⊆ r P∋p)  
+          → ∀ ( s : HOD ) →  Power P ∋ s → ¬ (( q P∋p  ⊆ s  ) ∧ ( r P∋p  ⊆ s ))
 
-lemma725 : (M : CountableHOD ) (C : CountableOrdinal) (P : HOD ) →  mhod M ∋ Power P
-    →  Incompatible P → ¬ ( mhod M ∋ filter ( genf ( P-GenericFilter C P )))
+lemma725 : (C : CountableModel) (P : HOD ) 
+    →  Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter C P )))
 lemma725 = {!!}
 
 open import PFOD O
@@ -172,7 +179,7 @@
 lemma725-1 :   Incompatible HODω2
 lemma725-1 = {!!}
 
-lemma726 :  (C : CountableOrdinal) (P : HOD ) 
+lemma726 :  (C : CountableModel) (P : HOD ) 
     →  Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2
 lemma726 = {!!}
 
--- a/src/partfunc.agda	Sat Sep 04 01:43:27 2021 +0900
+++ b/src/partfunc.agda	Fri Feb 18 11:44:08 2022 +0900
@@ -2,8 +2,8 @@
 open import Level
 open import Relation.Nullary 
 open import Relation.Binary.PropositionalEquality
-open import Ordinals
-module partfunc {n : Level } (O : Ordinals {n})  where
+-- open import Ordinals
+module partfunc {n : Level } where -- (O : Ordinals {n})  where
 
 open import logic
 open import Relation.Binary 
@@ -13,7 +13,7 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-open import filter O
+-- open import filter O
 
 open _∧_
 open _∨_