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

changeset 448:81691a6b352b

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 19:03:33 +0900
parents 364d738f871d
children be685f338fdc
files src/OD.agda src/generic-filter.agda src/nat.agda
diffstat 3 files changed, 33 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/OD.agda	Sun Mar 13 14:44:24 2022 +0900
+++ b/src/OD.agda	Sun Mar 13 19:03:33 2022 +0900
@@ -206,6 +206,9 @@
 =od∅→≡o∅  : {x : HOD} → od x == od od∅ → & x ≡ o∅ 
 =od∅→≡o∅ {x} eq = trans (cong (λ k → & k ) (==→o≡ {x} {od∅} eq)) ord-od∅
 
+≡od∅→=od∅  : {x : HOD} → x ≡ od∅ → od x == od od∅
+≡od∅→=od∅ {x} eq = ≡o∅→=od∅ (subst (λ k → & x  ≡ k ) ord-od∅ ( cong & eq ) )
+
 ∅0 : record { def = λ x →  Lift n ⊥ } == od od∅  
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} lt = lift (¬x<0 lt)
--- a/src/generic-filter.agda	Sun Mar 13 14:44:24 2022 +0900
+++ b/src/generic-filter.agda	Sun Mar 13 19:03:33 2022 +0900
@@ -149,7 +149,7 @@
 P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel P) → GenericFilter P
 P-GenericFilter P p0 Pp0 C = record {
       genf = record { filter = PDHOD P p0 C ; f⊆PL =  f⊆PL ; filter1 = f1 ; filter2 = f2 }
-    ; generic = λ D → {!!}
+    ; generic = fdense
    } where
         PGHOD∈PL :  (i : Nat) → (x : Ordinal) →  PGHOD i P C x ⊆ Power P
         PGHOD∈PL i x = record { incl = λ {x} p → proj1 p }
@@ -164,11 +164,34 @@
         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 ?) ⟫
+            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 (f5 lt)) ⟫ where
+               f5 : odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y
+               f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋p} {gr PD∋q} (<to≤ a))
+                   (subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) (sym &iso) lt) )
+--    subst (λ k → odef k y) *iso (pn<gr PD∋q y (subst (λ k → odef _ k ) &iso (incl (p-monotonic _ _ C a ) (subst (λ k → odef _ k) &iso lt) ))) ⟫
         ... | 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)   } 
+        ... | tri> ¬a ¬b c = record { gr = gr PD∋q ;  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∋q) (& p0))) y → odef (p ∩ q) y
+            f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y (f5 lt)) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ where
+               f5 : odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (* (find-p P C (gr PD∋p) (& p0))) y
+               f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋q} {gr PD∋p} (<to≤ c))
+                   (subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) (sym &iso) lt) )
+        fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
+        fdense D eq0  = ⊥-elim (  ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where
+           open Dense
+           fd : HOD
+           fd = dense-f D p0
+           PP∋D : dense D ⊆ Power P
+           PP∋D = d⊆P D
+           fd02 : dense D ∋ dense-f D p0 
+           fd02 = dense-d D (ODC.power→⊆ O _ _ Pp0 )
+           fd03 : PDHOD P p0 C  ∋ dense-f D p0 
+           fd03 = f1 {p0} {dense-f D p0} {!!} {!!} ( dense-p D {!!} )
+           fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
+           fd01 = ⟪ fd02 , fd03 ⟫ 
+
 
 
 
--- a/src/nat.agda	Sun Mar 13 14:44:24 2022 +0900
+++ b/src/nat.agda	Sun Mar 13 19:03:33 2022 +0900
@@ -26,6 +26,10 @@
 a<sa {Zero} = s≤s z≤n
 a<sa {Suc la} = s≤s a<sa 
 
+<to≤ : {x y  : Nat } → x < y → x ≤ y 
+<to≤ {Zero} {Suc y} (s≤s z≤n) = z≤n
+<to≤ {Suc x} {Suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)
+
 =→¬< : {x : Nat  } → ¬ ( x < x )
 =→¬< {Zero} ()
 =→¬< {Suc x} (s≤s lt) = =→¬< lt