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

changeset 447:364d738f871d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Mar 2022 14:44:24 +0900
parents eb4049abad70
children 81691a6b352b
files src/ODC.agda src/ODUtil.agda src/generic-filter.agda
diffstat 3 files changed, 24 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODC.agda	Sun Mar 13 08:05:15 2022 +0900
+++ b/src/ODC.agda	Sun Mar 13 14:44:24 2022 +0900
@@ -95,6 +95,11 @@
    t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
    t1 = power→ A t PA∋t
 
+power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
+power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01  where
+   p01 :  {z : HOD} → (x ∩ y) ∋ z → A ∋ z
+   p01 {z} xyz = double-neg-eilm (  power→ A x ax (proj1 xyz ))
+
 OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
 OrdP  x y with trio< x (& y)
 OrdP  x y | tri< a ¬b ¬c = no ¬c
--- a/src/ODUtil.agda	Sun Mar 13 08:05:15 2022 +0900
+++ b/src/ODUtil.agda	Sun Mar 13 14:44:24 2022 +0900
@@ -72,7 +72,6 @@
     ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫
    } 
 
-
 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
 ω<next-o∅ {y} lt = <odmax infinite lt
 
--- a/src/generic-filter.agda	Sun Mar 13 08:05:15 2022 +0900
+++ b/src/generic-filter.agda	Sun Mar 13 14:44:24 2022 +0900
@@ -85,17 +85,11 @@
 ---
 --   p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
 --  
-next-p :  (p : Ordinal) → (f : HOD → HOD) → Ordinal
-next-p p f with is-o∅  ( & (f (* p)))  
-next-p p f | yes y = p
-next-p p f | no not = & (ODC.minimal O (f (* p) ) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
-
----
---  search on p(n)
---
 find-p :  (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : Ordinal) → Ordinal
 find-p P C Zero x = x
-find-p P C (Suc i) x = find-p P C i ( next-p x (λ p → PGHOD i P C (& p) ))
+find-p P C (Suc i) x with is-o∅ ( & ( PGHOD i P C (find-p P C i x)) )
+... | yes y  = find-p P C i x
+... | no not  = & (ODC.minimal O ( PGHOD i P C (find-p P C i x)) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
 
 ---
 -- G = { r ∈ Power P | ∃ n → p(n) ⊆ q }
@@ -136,13 +130,19 @@
 open _⊆_
 
 p-monotonic1 :  (P p : HOD ) (C : CountableModel P ) → {n : Nat} → (* (find-p P C n (& p))) ⊆ (* (find-p P C (Suc n) (& p)))
-p-monotonic1 = {!!}
+p-monotonic1 P p C {n} with is-o∅ (& (PGHOD n P C (find-p P C n (& p))))
+... | yes y =   refl-⊆
+... | no not = record { incl = λ {x} lt → proj2 (proj2 fmin∈PGHOD) (& x) lt  } where
+    fmin : HOD
+    fmin = ODC.minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
+    fmin∈PGHOD : PGHOD n P C (find-p P C n (& p)) ∋ fmin
+    fmin∈PGHOD = ODC.x∋minimal O (PGHOD n P C (find-p P C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
 
 p-monotonic :  (P p : HOD ) (C : CountableModel P ) → {n m : Nat} → n ≤ m → (* (find-p P C n (& p))) ⊆ (* (find-p P C m (& p)))
 p-monotonic P p C {Zero} {Zero} n≤m = refl-⊆
 p-monotonic P p C {Zero} {Suc m} z≤n = trans-⊆ (p-monotonic P p C {Zero} {m} z≤n ) (p-monotonic1 P p C {m} )  
 p-monotonic P p C {Suc n} {Suc m} (s≤s n≤m) with <-cmp n m
-... | tri< a ¬b ¬c = trans-⊆ (p-monotonic P p C {Suc n} {m}  {!!} ) (p-monotonic1 P p C {m} )  
+... | tri< a ¬b ¬c = trans-⊆ (p-monotonic P p C {Suc n} {m} a) (p-monotonic1 P p C {m} )  
 ... | tri≈ ¬a refl ¬c = refl-⊆
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
 
@@ -153,29 +153,22 @@
    } where
         PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  PGHOD i P C 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 P C 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 (Suc i) x y Px Py with is-o∅  ( & (PGHOD i P C (& (* 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 P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
-            fmin∈PGHOD : PGHOD i P C (& (* x)) ∋ fmin
-            fmin∈PGHOD = ODC.x∋minimal O (PGHOD i P C (& (* x))) (λ eq → not (=od∅→≡o∅ eq))
-            pg-01 : Power P ∋ fmin 
-            pg-01 = incl (PGHOD∈PL i x ) (subst (λ k → PGHOD i P C k ∋ fmin ) &iso  fmin∈PGHOD )
         f⊆PL :  PDHOD P p0 C ⊆ Power P
         f⊆PL = record { incl = λ {x} lt →  x∈PP lt  }
         f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q
         f1 {p} {q}  q⊆P PD∋p p⊆q =  record { gr = gr PD∋p ;  pn<gr = f04 ; x∈PP = power←  _ _ (incl q⊆P) } where
-           f03 : {x : Ordinal} → odef p x → odef q x
-           f03 {x} lt = subst (λ k → def (od q) k) &iso (incl p⊆q (subst (λ k → def (od p) k) (sym &iso) lt) )
            f04 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
            f04 y lt1 = subst₂ (λ j k → odef j k ) (sym *iso) &iso (incl p⊆q (subst₂ (λ j k → odef k j ) (sym &iso) *iso ( pn<gr PD∋p y  lt1 )))
                -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
         f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q)
-        f2 {p} {q} PD∋p PD∋q = {!!}
+        f2 {p} {q} PD∋p PD∋q with <-cmp (gr PD∋p) (gr PD∋q)
+        ... | tri< a ¬b ¬c = record { gr = gr PD∋p ;  pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
+            f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
+            f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y ?) ⟫
+        ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ;  pn<gr =  λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt);  x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
+            f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
+            f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ 
+        ... | tri> ¬a ¬b c = record { gr = gr PD∋q ;  pn<gr = {!!} ; x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }