Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 388:19687f3304c9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 25 Jul 2020 12:54:28 +0900 |
| parents | 8b0715e28b33 |
| children | cb183674facf |
| files | LEMC.agda OD.agda Ordinals.agda filter.agda generic-filter.agda partfunc.agda |
| diffstat | 6 files changed, 70 insertions(+), 128 deletions(-) [+] |
line wrap: on
line diff
--- a/LEMC.agda Sat Jul 25 09:09:00 2020 +0900 +++ b/LEMC.agda Sat Jul 25 12:54:28 2020 +0900 @@ -126,6 +126,7 @@ -- -- 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 @@ -157,7 +158,7 @@ min2 : Minimal u min2 = prev (proj1 y1prop) u (proj2 y1prop) Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u - Min2 x u u∋x = (ε-induction {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) + Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (od→ord x ) cx {x} nx = choice-func x nx minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD
--- a/OD.agda Sat Jul 25 09:09:00 2020 +0900 +++ b/OD.agda Sat Jul 25 12:54:28 2020 +0900 @@ -167,6 +167,9 @@ odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso +odefo→o< : {X y : Ordinal } → odef (ord→od X) y → y o< X +odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) diso diso ( c<→o< (subst (λ k → odef (ord→od X) k ) (sym diso ) lt )) + -- avoiding lv != Zero error orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y orefl refl = refl @@ -319,15 +322,15 @@ ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy --- level trick (what'a shame) --- ε-induction1 : { ψ : HOD → Set (suc n)} --- → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) --- → (x : HOD ) → ψ x --- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where --- induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) --- induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) --- ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) --- ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy +-- level trick (what'a shame) for LEM / minimal +ε-induction1 : { ψ : HOD → Set (suc n)} + → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) + → (x : HOD ) → ψ x +ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where + induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) + induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) + ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) + ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
--- a/Ordinals.agda Sat Jul 25 09:09:00 2020 +0900 +++ b/Ordinals.agda Sat Jul 25 12:54:28 2020 +0900 @@ -24,6 +24,9 @@ TransFinite : { ψ : ord → Set n } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x + TransFinite1 : { ψ : ord → Set (suc n) } + → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : ord) → ψ x record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field @@ -62,6 +65,7 @@ osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) + TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O) x<nx = IsNext.x<nx (Ordinals.isNext O) osuc<nx = IsNext.osuc<nx (Ordinals.isNext O)
--- a/filter.agda Sat Jul 25 09:09:00 2020 +0900 +++ b/filter.agda Sat Jul 25 12:54:28 2020 +0900 @@ -20,6 +20,7 @@ open ODAxiom odAxiom import ODC +open ODC O open _∧_ open _∨_
--- a/generic-filter.agda Sat Jul 25 09:09:00 2020 +0900 +++ b/generic-filter.agda Sat Jul 25 12:54:28 2020 +0900 @@ -60,11 +60,6 @@ extend : {x : Nat} → (fr : dom f (lift x) ) → dom g (lift x ) feq : {x : Nat} → {fr : dom f (lift x) } → pmap f (lift x) fr ≡ pmap g (lift x) (extend fr) -record Gf (f : Nat → Two) (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where - field - gn : Nat - f<n : (f ↑ gn) f⊆ p - record FiniteF (p : PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where field f-max : Nat @@ -84,60 +79,9 @@ -- ; dense-p = λ {p} d → {!!} -- } -open Gf open _f⊆_ open import Data.Nat.Properties -GF : (Nat → Two ) → F-Filter (PFunc (Lift n Nat) (Lift n Two)) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_ -GF f = record { - filter = λ p → Gf f p - ; f⊆P = lift OneObj - ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } - ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } - } where - f1 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q - f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q (extend (f<n fp ) x<g) ; feq = λ {x} {fr} → lemma {x} {fr} } where - lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → pmap (f ↑ gn fp) (lift x) fr ≡ pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) - lemma {x} {fr} = begin - pmap (f ↑ gn fp) (lift x) fr - ≡⟨ feq (f<n fp ) ⟩ - pmap p (lift x) (extend (f<n fp) fr) - ≡⟨ feq p⊆q ⟩ - pmap q (lift x) (extend p⊆q (extend (f<n fp) fr)) - ∎ where open ≡-Reasoning - f2 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) - f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where - fmin : PFunc (Lift n Nat) (Lift n Two) - fmin = f ↑ (min (gn fp) (gn fq)) - lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p (lift x)) (gr : dom q (lift x)) → pmap p (lift x) fr ≡ pmap q (lift x) gr - lemma1 {x} x<g fr gr = begin - pmap p (lift x) fr - ≡⟨ meq p ⟩ - pmap p (lift x) (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))) - ≡⟨ sym (feq (f<n fp)) ⟩ - pmap (f ↑ (min (gn fp) (gn fq))) (lift x) x<g - ≡⟨ feq (f<n fq) ⟩ - pmap q (lift x) (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))) - ≡⟨ meq q ⟩ - pmap q (lift x) gr - ∎ where open ≡-Reasoning - lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) (lift x) - lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ; - proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }} - f∩→⊆ : (p q : PFunc (Lift n Nat) (Lift n Two) ) → (p f∩ q ) f⊆ q - f∩→⊆ p q = record { - extend = λ {x} pq → proj1 (proj2 pq) - ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) - } - lemma3 : {x : Nat} → ( fr : Lift n (x ≤ min (gn fp) (gn fq))) → pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr ≡ pmap (p f∩ q) (lift x) (lemma2 fr) - lemma3 {x} fr = - pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr - ≡⟨ feq (f<n fq) ⟩ - pmap q (lift x) (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) )) - ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩ - pmap (p f∩ q) (lift x) (lemma2 fr) - ∎ where open ≡-Reasoning - ODSuc : (y : HOD) → infinite ∋ y → HOD ODSuc y lt = Union (y , (y , y)) @@ -200,35 +144,6 @@ ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) -record Gfo (x : Ordinal) : Set n where - field - gfunc : Ordinal - gmax : Ordinal - gcond : (odef ω→2 gfunc) ∧ (odef infinite gmax) - gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) ) ⊆ ord→od x - pcond : odef HODω2 x - -open Gfo - -HODGf : HOD -HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} } - -G : (Nat → Two) → Filter HODω2 -G f = record { - filter = HODGf - ; f⊆PL = {!!} - ; filter1 = {!!} - ; filter2 = {!!} - } where - filter0 : HOD - filter0 = {!!} - f⊆PL1 : filter0 ⊆ Power HODω2 - f⊆PL1 = {!!} - filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q - filter11 = {!!} - filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) - filter12 = {!!} - -- the set of finite partial functions from ω to 2 Hω2f : Set (suc n) @@ -244,26 +159,62 @@ 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 + field + phod : HOD + ptl→ : Nat → Ordinal + ptl→∈P : (i : Nat) → odef phod (ptl→ i) + ptl← : (x : Ordinal) → odef phod x → Nat + ptl-iso→ : { x : Ordinal } → (lt : odef phod x ) → ptl→ (ptl← x lt ) ≡ x + ptl-iso← : { x : Nat } → ptl← (ptl→ x ) (ptl→∈P x) ≡ x + open CountableOrdinal +open CountableHOD -PGOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Set n -PGOD i C p q = ¬ ( odef (ord→od (ctl→ C i)) q ∧ ( (x : Ordinal ) → odef (ord→od p) x → odef (ord→od q) x )) +PGHOD : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD +PGHOD P i C p = record { od = record { def = λ x → odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) } + ; odmax = ctl→ C i ; <odmax = λ {y} lt → odefo→o< (proj1 lt)} + +next-p : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal +next-p P i C p with ODC.decp O ( PGHOD P i C p =h= od∅ ) +next-p P i C p | yes y = p +next-p P i C p | no not = od→ord (ODC.minimal O (PGHOD P i C p ) not) -PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD -PGHOD i C p = record { od = record { def = λ x → PGOD i C {!!} {!!} } ; odmax = {!!} ; <odmax = {!!} } +data PD (P : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) → Set n where + pd0 : PD P C o∅ 0 + pdsuc : {p : Ordinal } {i : Nat} → PD P C p i → PD P C (next-p P i C p) (Suc i) + +record PDN (P : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where + field + px∈ω : odef (phod P) x + pdod : PD P C x (ptl← P x px∈ω) + +open PDN -ord-compare : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Ordinal -ord-compare i C p q with ODC.p∨¬p O ( (q : Ordinal ) → PGOD i C p q ) -ord-compare i C p q | case1 y = p -ord-compare i C p q | case2 n = od→ord (ODC.minimal O (PGHOD i C p ) (∅< (subst₂ (λ j k → odef j {!!} ) refl {!!} n)) ) +PDHOD : (P : CountableHOD ) → (C : CountableOrdinal) → HOD +PDHOD P C = record { od = record { def = λ x → PDN P C x } + ; odmax = odmax (phod P) ; <odmax = λ {y} lt → <odmax (phod P) (px∈ω lt) } where + +-- +-- p 0 ≡ ∅ +-- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q +--- else p n -data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) → Set (suc n) where - pd0 : PD P C o∅ 0 - -- pdq : {q pnx : Ordinal } {n : Nat} → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) +Gω2r : (x : Ordinal) → (lt : infinite ∋ ord→od x ) → Hω2 (ω→nat (ord→od x) lt ) x +Gω2r x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) → Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} {!!} (ord→od x)) where + ψ : HOD → Set n + ψ y = (lt : odef infinite (od→ord y) ) → Hω2 (ω→nat y lt ) (od→ord y ) + ind : {x : HOD} → ({y : HOD} → OD.def (od x) (od→ord y) → + (lt : infinite-d (od→ord y)) → Hω2 (ω→nat y lt) (od→ord y)) → + (lt : infinite-d (od→ord x)) → Hω2 (ω→nat x lt) (od→ord x) + ind {x} prev lt with ω→nat x lt + ... | Zero = subst (λ k → Hω2 Zero k) ? hφ + ... | Suc t = {!!} -P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P +P-GenericFilter : {P : CountableHOD } → (C : CountableOrdinal) → GenericFilter (phod P) P-GenericFilter {P} C = record { - genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } + genf = record { filter = PDHOD P C ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} } ; generic = λ D → {!!} }
--- a/partfunc.agda Sat Jul 25 09:09:00 2020 +0900 +++ b/partfunc.agda Sat Jul 25 12:54:28 2020 +0900 @@ -209,25 +209,7 @@ lemma2 (just i1 ∷ p) = lemma2 p lemma2 (nothing ∷ p) = lemma2 p -record 3Gf (f : Nat → Two) (p : List (Maybe Two)) : Set where - field - 3gn : Nat - 3f<n : p 3⊆ (f 3↑ 3gn) - -open 3Gf - -min = Data.Nat._⊓_ +-- min = Data.Nat._⊓_ -- m≤m⊔n = Data.Nat._⊔_ -open import Data.Nat.Properties +-- open import Data.Nat.Properties -3GF : {n : Level } → (Nat → Two ) → F-Filter (List (Maybe Two)) (λ x → One) _3⊆_ _3∩_ -3GF {n} f = record { - filter = λ p → 3Gf f p - ; f⊆P = OneObj - ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q - ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq } - } where - lemma1 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q - lemma1 p q fp p⊆q = record { 3gn = 3gn fp ; 3f<n = {!!} } - lemma2 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq)) - lemma2 p q fp fq = ?