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

comparison src/zorn.agda @ 556:ba889c711524

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 Fri, 29 Apr 2022 17:53:31 +0900
parents 726b6dac5eaa
children f1e899cbe845
comparison
equal deleted inserted replaced
555:726b6dac5eaa 556:ba889c711524
50 ≤-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl 50 ≤-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl
51 ≤-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z 51 ≤-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
52 ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y 52 ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
53 ≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z ) 53 ≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
54 54
55 <-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
56 <-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO (sym a=b) b<a
57 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO refl
58 (IsStrictPartialOrder.trans PO b<a a<b)
55 59
56 open _==_ 60 open _==_
57 open _⊆_ 61 open _⊆_
58 62
59 -- open import Relation.Binary.Properties.Poset as Poset 63 -- open import Relation.Binary.Properties.Poset as Poset
74 -- 78 --
75 79
76 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n) 80 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
77 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧ odef A (f x ) 81 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧ odef A (f x )
78 82
83 immieate-f : (A : HOD) → ( f : Ordinal → Ordinal ) → Set n
84 immieate-f A f = { x y : Ordinal } → odef A x → odef A y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
85
79 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where 86 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
80 init : odef A s → FClosure A f s s 87 init : odef A s → FClosure A f s s
81 fsuc : (x : Ordinal) ( p : FClosure A f s x ) → FClosure A f s (f x) 88 fsuc : (x : Ordinal) ( p : FClosure A f s x ) → FClosure A f s (f x)
82 89
83 A∋fc : {A : HOD} {s y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y 90 A∋fc : {A : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y
84 A∋fc {A} {s} {.s} f mf (init as) = as 91 A∋fc {A} s f mf (init as) = as
85 A∋fc {A} {s} f mf (fsuc y fcy) = proj2 (mf y ( A∋fc {A} {s} f mf fcy ) ) 92 A∋fc {A} s f mf (fsuc y fcy) = proj2 (mf y ( A∋fc {A} s f mf fcy ) )
86 93
87 fcn : {A : HOD} {s x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ 94 s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → * s ≤ * y
88 fcn mf (init as) = zero 95 s≤fc {A} s {.s} f mf (init x) = case1 refl
89 fcn {A} {s} {x} {f} mf (fsuc y p) with mf y (A∋fc f mf p) 96 s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) )
90 ... | ⟪ case1 eq , _ ⟫ = fcn mf p 97 ... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy )
91 ... | ⟪ case2 y<fy , _ ⟫ = suc (fcn mf p ) 98 ... | case2 x<fx with s≤fc {A} s f mf fcy
92 99 ... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx )
93 ncf : {A : HOD} {s : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → ℕ → Ordinal 100 ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx )
94 ncf {A} {s} mf zero = s 101
95 ncf {A} {s} {f} mf (suc x) = f (ncf {A} {s} mf x ) 102 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) (imm : immieate-f A f )
96
97 FC→ : {A : HOD} {s : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → (x : ℕ ) → (fc : FClosure A f s (ncf {A} {s} mf x) ) → fcn mf fc ≡ x
98 FC→ {A} {s} {f} mf zero (init x) = refl
99 FC→ {A} {.(f x)} {f} mf zero (fsuc x fc) = {!!}
100 FC→ {A} {s} {f} mf (suc x) fc = {!!}
101
102 fcn-inject : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) → (mf : ≤-monotonic-f A f)
103 → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn mf fcx ≡ fcn mf fcy → x ≡ y
104 fcn-inject f mf (init x) (init x₁) refl = refl
105 fcn-inject {A} {s} f mf (init sa) (fsuc y fcy) eq with proj1 (mf y (A∋fc f mf fcy ))
106 ... | case1 y=fy = subst (λ k → s ≡ k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=fy )) (fcn-inject f mf (init sa) fcy (trans eq fcn0 )) where
107 fcn0 : fcn mf ( fsuc y fcy ) ≡ fcn mf fcy
108 fcn0 with mf y (A∋fc f mf fcy )
109 ... | ⟪ case1 x , proj4 ⟫ = refl
110 ... | case2 y<fy = {!!}
111 fcn-inject f mf (fsuc x fcx) (init sa) eq = {!!} -- cong f ( fcn-inject f mf fcx fcy ( cong pred eq ))
112 fcn-inject f mf (fsuc x fcx) (fsuc y fcy) eq = {!!} -- cong f ( fcn-inject f mf fcx fcy ( cong pred eq ))
113
114 fcn-cmp : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f)
115 → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x ) 103 → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
116 fcn-cmp {A} {s} {x} {y} f mf cx cy with <-cmp (fcn mf cx) (fcn mf cy) 104 fcn-cmp {A} s {.s} {.s} f mf imm (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )
117 ... | t = {!!} 105 fcn-cmp {A} s f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) )
118 106 ... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy )
119 fcn-mono : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) 107 ... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where
120 → (imm : { x y : Ordinal } → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) ) 108 lt : * s < * (f y)
121 → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn mf fcx Data.Nat.≤ fcn mf fcy → * x ≤ * y 109 lt with s≤fc s f mf cy
122 fcn-mono f mf imm (init _) (init _) z≤n = case1 refl 110 ... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y
123 fcn-mono {A} {s} {x} f mf imm (init sa) (fsuc y fcy) z≤n with proj1 (mf y (A∋fc f mf fcy ) ) 111 ... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y
124 ... | case1 eq = subst (λ k → * s ≤ k ) eq ( fcn-mono f mf imm (init sa) fcy z≤n ) 112 fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc s f mf cx
125 ... | case2 lt = ≤-ftrans (fcn-mono f mf imm (init sa) fcy z≤n) (case2 lt) 113 ... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt)
126 fcn-mono f mf imm (fsuc x fcx) (fsuc y fcy) lt with fcn-mono f mf imm fcx fcy {!!} 114 ... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt) (λ eq → <-irr (case1 eq) s<x ) s<x
127 ... | case1 x=y = case1 (subst₂ (λ j k → * (f j) ≡ * (f k)) &iso &iso ( cong (λ k → * (f (& k ))) x=y ) ) 115 fcn-cmp {A} s f mf imm (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
128 ... | case2 x<y with <-cmp (fcn mf fcx) (fcn mf fcy) 116 ... | case1 x=fx | case1 y=fy = {!!}
129 ... | tri< a ¬b ¬c = {!!} 117 ... | case1 x=fx | case2 y<fy = {!!}
130 ... | tri≈ ¬a b ¬c = {!!} 118 ... | case2 x<fx | case1 y=fy = {!!}
131 ... | tri> ¬a ¬b c = {!!} 119 ... | case2 x<fx | case2 y<fy = {!!} where
132 -- = case2 {!!} -- * x < * y → * (f x) < * (f y) 120 fc-mono : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → FClosure A f x y ∨ FClosure A f y x
121 fc-mono = ?
122 fc1 : Tri (* (f x) < * (f y)) (* (f x) ≡ * (f y)) (* (f y) < * (f x))
123 fc1 with fcn-cmp s f mf imm cx cy
124 ... | tri< a ¬b ¬c = {!!}
125 ... | tri≈ ¬a b ¬c = {!!}
126 ... | tri> ¬a ¬b c = {!!}
133 127
134 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where 128 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x) ( f : Ordinal → Ordinal ) : Set n where
135 field 129 field
136 y : Ordinal 130 y : Ordinal
137 ay : odef B y 131 ay : odef B y
167 → Maximal A 161 → Maximal A
168 Zorn-lemma {A} 0<A supP = zorn00 where 162 Zorn-lemma {A} 0<A supP = zorn00 where
169 supO : (C : Ordinal ) → (* C) ⊆ A → IsTotalOrderSet (* C) → Ordinal 163 supO : (C : Ordinal ) → (* C) ⊆ A → IsTotalOrderSet (* C) → Ordinal
170 supO C C⊆A TC = & ( SUP.sup ( supP (* C) C⊆A TC )) 164 supO C C⊆A TC = & ( SUP.sup ( supP (* C) C⊆A TC ))
171 z01 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ 165 z01 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
172 z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO (sym a=b) b<a 166 z01 {a} {b} A∋a A∋b = <-irr
173 z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO refl
174 (IsStrictPartialOrder.trans PO b<a a<b)
175 z07 : {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A 167 z07 : {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
176 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) 168 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
177 s : HOD 169 s : HOD
178 s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 170 s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
179 sa : A ∋ * ( & s ) 171 sa : A ∋ * ( & s )