Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 285:313140ae5e3d
clean up
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 10 May 2020 09:25:13 +0900 |
parents | a8f9c8a27e8d |
children | 5de8905a5a2b |
comparison
equal
deleted
inserted
replaced
284:a8f9c8a27e8d | 285:313140ae5e3d |
---|---|
88 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) | 88 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) |
89 ¬¬X∋x nn = not record { | 89 ¬¬X∋x nn = not record { |
90 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) | 90 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) |
91 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) | 91 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) |
92 } | 92 } |
93 record Minimal (x : OD) (ne : ¬ (x == od∅ ) ) : Set (suc n) where | 93 record Minimal (x : OD) : Set (suc n) where |
94 field | 94 field |
95 min : OD | 95 min : OD |
96 x∋min : x ∋ min | 96 x∋min : x ∋ min |
97 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) | 97 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) |
98 open Minimal | 98 open Minimal |
99 open _∧_ | 99 open _∧_ |
100 -- | 100 -- |
101 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only | 101 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only |
102 -- | 102 -- |
103 induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x)) | 103 induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u ) |
104 → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) | 104 → (u : OD ) → (u∋x : u ∋ x) → Minimal u |
105 induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y)) | 105 induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y)) |
106 ... | case1 P = | 106 ... | case1 P = |
107 record { min = x | 107 record { min = x |
108 ; x∋min = u∋x | 108 ; x∋min = u∋x |
109 ; min-empty = P | 109 ; min-empty = P |
110 } | 110 } |
111 ... | case2 NP = | 111 ... | case2 NP = min2 where |
112 record { min = min min2 | |
113 ; x∋min = x∋min min2 | |
114 ; min-empty = min-empty min2 | |
115 | |
116 } where | |
117 p : OD | 112 p : OD |
118 p = record { def = λ y1 → def x y1 ∧ def u y1 } | 113 p = record { def = λ y1 → def x y1 ∧ def u y1 } |
119 np : ¬ (p == od∅) | 114 np : ¬ (p == od∅) |
120 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) | 115 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) |
121 y1choice : choiced p | 116 y1choice : choiced p |
122 y1choice = choice-func p np | 117 y1choice = choice-func p np |
123 y1 : OD | 118 y1 : OD |
124 y1 = a-choice y1choice | 119 y1 = a-choice y1choice |
125 y1prop : (x ∋ y1) ∧ (u ∋ y1) | 120 y1prop : (x ∋ y1) ∧ (u ∋ y1) |
126 y1prop = is-in y1choice | 121 y1prop = is-in y1choice |
127 min2 : Minimal u (∅< (proj2 y1prop)) | 122 min2 : Minimal u |
128 min2 = prev (proj1 y1prop) u (proj2 y1prop) | 123 min2 = prev (proj1 y1prop) u (proj2 y1prop) |
129 Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) | 124 Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u |
130 Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x) } induction x u u∋x ) | 125 Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) |
131 cx : {x : OD} → ¬ (x == od∅ ) → choiced x | 126 cx : {x : OD} → ¬ (x == od∅ ) → choiced x |
132 cx {x} nx = choice-func x nx | 127 cx {x} nx = choice-func x nx |
133 minimal : (x : OD ) → ¬ (x == od∅ ) → OD | 128 minimal : (x : OD ) → ¬ (x == od∅ ) → OD |
134 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) | 129 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) |
135 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) | 130 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) |