Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 284:a8f9c8a27e8d
minimal from LEM
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 10 May 2020 09:19:32 +0900 |
parents | 2d77b6d12a22 |
children | 313140ae5e3d |
comparison
equal
deleted
inserted
replaced
283:2d77b6d12a22 | 284:a8f9c8a27e8d |
---|---|
29 field | 29 field |
30 a-choice : OD | 30 a-choice : OD |
31 is-in : X ∋ a-choice | 31 is-in : X ∋ a-choice |
32 | 32 |
33 open choiced | 33 open choiced |
34 | |
35 double-neg-eilm : {A : Set (suc n)} → ¬ ¬ A → A -- we don't have this in intutionistic logic | |
36 double-neg-eilm {A} notnot with p∨¬p A -- assuming axiom of choice | |
37 ... | case1 p = p | |
38 ... | case2 ¬p = ⊥-elim ( notnot ¬p ) | |
39 | |
34 | 40 |
35 OD→ZFC : ZFC | 41 OD→ZFC : ZFC |
36 OD→ZFC = record { | 42 OD→ZFC = record { |
37 ZFSet = OD | 43 ZFSet = OD |
38 ; _∋_ = _∋_ | 44 ; _∋_ = _∋_ |
89 min : OD | 95 min : OD |
90 x∋min : x ∋ min | 96 x∋min : x ∋ min |
91 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) | 97 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) |
92 open Minimal | 98 open Minimal |
93 open _∧_ | 99 open _∧_ |
94 induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) → (ne : ¬ (x == od∅ )) → Minimal x ne | 100 -- |
95 induction {x} prev ne = c2 | 101 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only |
96 where | 102 -- |
97 ch : choiced x | 103 induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x)) |
98 ch = choice-func x ne | 104 → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) |
99 c1 : OD | 105 induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y)) |
100 c1 = a-choice ch -- x ∋ c1 | 106 ... | case1 P = |
101 c2 : Minimal x ne | 107 record { min = x |
102 c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord y))) ) | 108 ; x∋min = u∋x |
103 c2 | case1 Yes = record { | 109 ; min-empty = P |
104 min = c1 | 110 } |
105 ; x∋min = is-in ch | 111 ... | case2 NP = |
106 ; min-empty = Yes | 112 record { min = min min2 |
107 } | 113 ; x∋min = x∋min min2 |
108 c2 | case2 No = c3 where | 114 ; min-empty = min-empty min2 |
109 y1 : OD | 115 |
110 y1 = record { def = λ y → ( def c1 y ∧ def x y) } | 116 } where |
111 noty1 : ¬ (y1 == od∅ ) | 117 p : OD |
112 noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) ) | 118 p = record { def = λ y1 → def x y1 ∧ def u y1 } |
113 ch1 : choiced y1 -- a-choice ch1 ∈ c1 , a-choice ch1 ∈ x | 119 np : ¬ (p == od∅) |
114 ch1 = choice-func y1 noty1 | 120 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) |
115 c3 : Minimal x ne | 121 y1choice : choiced p |
116 c3 with is-o∅ (od→ord (a-choice ch1)) | 122 y1choice = choice-func p np |
117 ... | yes eq = record { | 123 y1 : OD |
118 min = od∅ | 124 y1 = a-choice y1choice |
119 ; x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) | 125 y1prop : (x ∋ y1) ∧ (u ∋ y1) |
120 ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) ) | 126 y1prop = is-in y1choice |
121 } | 127 min2 : Minimal u (∅< (proj2 y1prop)) |
122 ... | no n = record { | 128 min2 = prev (proj1 y1prop) u (proj2 y1prop) |
123 min = min min3 | 129 Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) |
124 ; x∋min = x∋min3 (x∋min min3) | 130 Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x) } induction x u u∋x ) |
125 ; min-empty = min3-empty -- λ y p → min3-empty min3 y p -- p : (min min3 ∋ y) ∧ (x ∋ y) | 131 cx : {x : OD} → ¬ (x == od∅ ) → choiced x |
126 } where | 132 cx {x} nx = choice-func x nx |
127 lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ | |
128 lemma eq = begin | |
129 od→ord (a-choice ch1) | |
130 ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩ | |
131 od→ord od∅ | |
132 ≡⟨ ord-od∅ ⟩ | |
133 o∅ | |
134 ∎ where open ≡-Reasoning | |
135 -- Minimal (a-choice ch1) ch1not | |
136 -- min ∈ a-choice ch1 , min ∩ a-choice ch1 ≡ ∅ | |
137 ch1not : ¬ (a-choice ch1 == od∅) | |
138 ch1not ch1=0 = n (lemma ch1=0) | |
139 min3 : Minimal (a-choice ch1) ch1not | |
140 min3 = prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0)) | |
141 x∋min3 : a-choice ch1 ∋ min min3 → x ∋ min min3 | |
142 x∋min3 lt = {!!} | |
143 min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y)) | |
144 min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = ? } -- (min min3 ∋ y) ∧ (a-choice ch1 ∋ y) | |
145 -- p : (min min3 ∋ y) ∧ (x ∋ y) | |
146 | |
147 | |
148 Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne | |
149 Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) | |
150 minimal : (x : OD ) → ¬ (x == od∅ ) → OD | 133 minimal : (x : OD ) → ¬ (x == od∅ ) → OD |
151 minimal x not = min (Min1 x not ) | 134 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) |
152 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) | 135 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) |
153 x∋minimal x ne = x∋min (Min1 x ne) | 136 x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) |
154 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) | 137 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) |
155 minimal-1 x ne y = min-empty (Min1 x ne ) y | 138 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y |
156 | 139 |
157 | 140 |
158 | 141 |
159 | 142 |