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

changeset 440:d1c9f5ae5d0a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
give up this generic filter definition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 01 Mar 2022 14:31:31 +0900
parents fdcbf23ba2f9
children 6b26db38367f eb4049abad70
files src/LEMC.agda src/generic-filter.agda
diffstat 2 files changed, 29 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/LEMC.agda	Sat Feb 26 17:44:30 2022 +0900
+++ b/src/LEMC.agda	Tue Mar 01 14:31:31 2022 +0900
@@ -131,7 +131,6 @@
          --
          --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
          --
-         -- FIXME : don't use HOD make this level n, so we can remove ε-induction1 
          record Minimal (x : HOD)  : Set (suc n) where
            field
                min : HOD
--- a/src/generic-filter.agda	Sat Feb 26 17:44:30 2022 +0900
+++ b/src/generic-filter.agda	Tue Mar 01 14:31:31 2022 +0900
@@ -79,7 +79,8 @@
 
 ---
 --   p(n+1) = if (f n) != ∅ then (f n) otherwise p(n)
---
+--       is not working well
+--       skipped a(n) may cantains extra elements in possible r
 next-p :  (p : Ordinal) → (f : HOD → HOD) → Ordinal
 next-p p f with is-o∅  ( & (f (* p)))  
 next-p p f | yes y = p
@@ -139,16 +140,24 @@
      next : HOD
      is-small :  next ⊆ p ∧ ( ¬ ( next =h= p ))
 
-⊆-reduction : { ψ : (x : HOD) → Set (suc n) }
-    → (p : HOD) → ψ p
-    → (next : (x : HOD) → ψ x → ⊆-reduce x ) 
-    → (ind  : (x : HOD) → (m : ψ x) → ψ ( ⊆-reduce.next (next x m )) )
-    → ψ od∅
-⊆-reduction {ψ} p ψp next ind = TransFinite {λ x → {!!} } {!!} o∅
+record ⊆-reduce-∅ (next : HOD → HOD) : Set (suc n) where
+   field
+     p : HOD
+     is-∅ :  & (next p) ≡ o∅
 
+⊆-reduction : (next : (x : HOD) → ⊆-reduce x ) → (x : HOD) → ¬ ( x ∈ ( ⊆-reduce.next (next x )))
+⊆-reduction  next x = subst (λ k → ¬ (x ∈ ⊆-reduce.next (next k))) *iso (r02 x) where
+    r01 : (x₁ : Ordinal) → ((y : Ordinal) → y o< x₁ → ¬ odef (⊆-reduce.next (next (* y))) y) →
+            ¬ odef (⊆-reduce.next (next (* x₁))) x₁
+    r01 = {!!}
+    r02 : (x : HOD) → ¬ (x ∈ ⊆-reduce.next (next (* (& x))))
+    r02 x = TransFinite0 {λ x → ¬ ( odef ( ⊆-reduce.next (next (* x))) x) } r01 (& x) 
 
-P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P
-P-GenericFilter P p0 C = record {
+next-x≡∅ : (next : HOD → HOD)  → ( (x : HOD) → ¬ ( x ∈ next x) ) →  ⊆-reduce-∅ next
+next-x≡∅ = {!!}
+ 
+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 → {!!}
    } where
@@ -168,26 +177,26 @@
             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 → power← P x (λ {y} y<x →
-             find-p-⊆P (gr lt) {!!} (& y) {!!} (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
+             find-p-⊆P (gr lt) _ (& y) Pp0 (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
         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 = {!!} ;  pn<gr = {!!} ; x∈PP = {!!} }  where
            --  reduction : {ψ : (x : HOD) → x =h= od∅ → P x} → 
            --  q ∈ a(∃ n) ⊆ P → ( p n ⊆ q →  PDHOD P p0 C ∋ q )
            --                 ∨ (¬ (p n ⊆ q) → induction on (p n - q) 
-           PDNp :  {!!} -- PD⊆⊆N P C (& p)
-           PDNp = PD∋p
+           -- PDNp :  {!!} -- PD⊆⊆N P C (& p)
+           -- PDNp = PD∋p
            f02 : {x : Ordinal} → odef q x → odef P x
            f02 {x} lt = subst (λ k → def (od P) k) &iso (incl q⊆P (subst (λ k → def (od q) k) (sym &iso) lt) )
            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) )
            next1 : Ordinal
            next1 = {!!} -- find-p P C (gr PD) (next-p x (λ p₁ → PGHOD (gr PD) P C (& p₁))) 
-           f05 : next1 o< ctl-M C
-           f05 = {!!}
-           f06 : odef (Power P) (& q)
-           f06 = {!!}
-           f07 :  (y : Ordinal) → odef (* (& q)) y → odef (* {!!} ) y
-           f07 = {!!}
+           -- f05 : next1 o< ctl-M C
+           -- f05 = {!!}
+           -- f06 : odef (Power P) (& q)
+           -- f06 = {!!}
+           -- f07 :  (y : Ordinal) → odef (* (& q)) y → odef (* {!!} ) y
+           -- f07 = {!!}
         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 = {!!}
 
@@ -206,7 +215,7 @@
 
 lemma725 : (P p : HOD ) (C : CountableModel P) 
     →  * (ctl-M C) ∋ Power P
-    →  Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p C )))
+    →  Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p {!!} C )))
 lemma725 = {!!}
 
 open import PFOD O
@@ -220,7 +229,7 @@
 lemma725-1 = {!!}
 
 lemma726 :  (C : CountableModel HODω2) 
-    →  Union ( Replace HODω2 (λ p → filter ( genf ( P-GenericFilter HODω2 p C )))) =h= ω→2
+    →  Union ( Replace HODω2 (λ p → filter ( genf ( P-GenericFilter HODω2 p {!!} C )))) =h= ω→2
 lemma726 = {!!}
 
 --