Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 281:81d639ee9bfd
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 May 2020 22:03:17 +0900 |
parents | a2991ce14ced |
children | 6630dab08784 |
comparison
equal
deleted
inserted
replaced
280:a2991ce14ced | 281:81d639ee9bfd |
---|---|
82 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) | 82 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) |
83 ¬¬X∋x nn = not record { | 83 ¬¬X∋x nn = not record { |
84 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) | 84 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) |
85 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) | 85 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) |
86 } | 86 } |
87 record Minimal (x : OD) : Set (suc n) where | 87 record Minimal (x : OD) (ne : ¬ (x == od∅ ) ) : Set (suc n) where |
88 field | 88 field |
89 min : OD | 89 min : OD |
90 x∋min : ¬ (x == od∅ ) → x ∋ min | 90 x∋min : x ∋ min |
91 min-empty : ¬ (x == od∅ ) → (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) | 91 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) |
92 open Minimal | 92 open Minimal |
93 induction : {x : OD} → ({y : OD} → x ∋ y → Minimal y) → Minimal x | 93 open _∧_ |
94 induction {x} prev = record { | 94 induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) → (ne : ¬ (x == od∅ )) → Minimal x ne |
95 min = {!!} | 95 induction {x} prev ne = c2 |
96 ; x∋min = {!!} | 96 where |
97 ; min-empty = {!!} | 97 ch : choiced x |
98 } where | 98 ch = choice-func x ne |
99 c1 : OD | 99 c1 : OD |
100 c1 = a-choice (choice-func x {!!} ) | 100 c1 = a-choice ch |
101 c2 : OD | 101 c2 : Minimal x ne |
102 c2 with p∨¬p ( (y : OD ) → def c1 (od→ord y) ∧ (def x (od→ord y))) | 102 c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord y))) ) |
103 c2 | case1 _ = c1 | 103 c2 | case1 Yes = record { |
104 c2 | case2 No = {!!} -- minimal ( record { def = λ y → def c1 y ∧ def x y } ) {!!} | 104 min = c1 |
105 Min1 : (x : OD) → Minimal x | 105 ; x∋min = is-in ch |
106 Min1 x = (ε-induction {λ y → Minimal y } induction x ) | 106 ; min-empty = Yes |
107 } | |
108 c2 | case2 No = c3 where | |
109 y1 : OD | |
110 y1 = record { def = λ y → ( def c1 y ∧ def x y) } | |
111 noty1 : ¬ (y1 == od∅ ) | |
112 noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) ) | |
113 ch1 : choiced y1 | |
114 ch1 = choice-func y1 noty1 | |
115 c3 : Minimal x ne | |
116 c3 with is-o∅ (od→ord (a-choice ch1)) | |
117 ... | yes eq = record { | |
118 min = od∅ | |
119 ; x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) | |
120 ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) ) | |
121 } | |
122 ... | no n = record { | |
123 min = min min3 | |
124 ; x∋min = ? | |
125 ; min-empty = {!!} | |
126 } where | |
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 ch1not : ¬ (a-choice ch1 == od∅) | |
136 ch1not ch1=0 = n (lemma ch1=0) | |
137 min3 : Minimal (a-choice ch1) ch1not | |
138 min3 = ( prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))) | |
139 | |
140 | |
141 Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne | |
142 Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) | |
107 minimal : (x : OD ) → ¬ (x == od∅ ) → OD | 143 minimal : (x : OD ) → ¬ (x == od∅ ) → OD |
108 minimal x not = min (Min1 x) | 144 minimal x not = min (Min1 x not ) |
109 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) | 145 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) |
110 x∋minimal x ne = x∋min (Min1 x) ne | 146 x∋minimal x ne = x∋min (Min1 x ne) |
111 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) | 147 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) |
112 minimal-1 x ne y = min-empty (Min1 x) ne y | 148 minimal-1 x ne y = min-empty (Min1 x ne ) y |
113 | 149 |
114 | 150 |
115 | 151 |
116 | 152 |