Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 283:2d77b6d12a22
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 10 May 2020 00:18:59 +0900 |
parents | 6630dab08784 |
children | a8f9c8a27e8d |
comparison
equal
deleted
inserted
replaced
282:6630dab08784 | 283:2d77b6d12a22 |
---|---|
95 induction {x} prev ne = c2 | 95 induction {x} prev ne = c2 |
96 where | 96 where |
97 ch : choiced x | 97 ch : choiced x |
98 ch = choice-func x ne | 98 ch = choice-func x ne |
99 c1 : OD | 99 c1 : OD |
100 c1 = a-choice ch | 100 c1 = a-choice ch -- x ∋ c1 |
101 c2 : Minimal x ne | 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 Yes = record { | 103 c2 | case1 Yes = record { |
104 min = c1 | 104 min = c1 |
105 ; x∋min = is-in ch | 105 ; x∋min = is-in ch |
108 c2 | case2 No = c3 where | 108 c2 | case2 No = c3 where |
109 y1 : OD | 109 y1 : OD |
110 y1 = record { def = λ y → ( def c1 y ∧ def x y) } | 110 y1 = record { def = λ y → ( def c1 y ∧ def x y) } |
111 noty1 : ¬ (y1 == od∅ ) | 111 noty1 : ¬ (y1 == od∅ ) |
112 noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) ) | 112 noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) ) |
113 ch1 : choiced y1 | 113 ch1 : choiced y1 -- a-choice ch1 ∈ c1 , a-choice ch1 ∈ x |
114 ch1 = choice-func y1 noty1 | 114 ch1 = choice-func y1 noty1 |
115 c3 : Minimal x ne | 115 c3 : Minimal x ne |
116 c3 with is-o∅ (od→ord (a-choice ch1)) | 116 c3 with is-o∅ (od→ord (a-choice ch1)) |
117 ... | yes eq = record { | 117 ... | yes eq = record { |
118 min = od∅ | 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∅) ) | 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) ) | 120 ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) ) |
121 } | 121 } |
122 ... | no n = record { | 122 ... | no n = record { |
123 min = min min3 | 123 min = min min3 |
124 ; x∋min = {!!} | 124 ; x∋min = x∋min3 (x∋min min3) |
125 ; min-empty = min3-empty -- λ y p → min3-empty min3 y p -- p : (min min3 ∋ y) ∧ (x ∋ y) | 125 ; min-empty = min3-empty -- λ y p → min3-empty min3 y p -- p : (min min3 ∋ y) ∧ (x ∋ y) |
126 } where | 126 } where |
127 lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ | 127 lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ |
128 lemma eq = begin | 128 lemma eq = begin |
129 od→ord (a-choice ch1) | 129 od→ord (a-choice ch1) |
130 ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩ | 130 ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩ |
131 od→ord od∅ | 131 od→ord od∅ |
132 ≡⟨ ord-od∅ ⟩ | 132 ≡⟨ ord-od∅ ⟩ |
133 o∅ | 133 o∅ |
134 ∎ where open ≡-Reasoning | 134 ∎ where open ≡-Reasoning |
135 -- Minimal (a-choice ch1) ch1not | |
136 -- min ∈ a-choice ch1 , min ∩ a-choice ch1 ≡ ∅ | |
135 ch1not : ¬ (a-choice ch1 == od∅) | 137 ch1not : ¬ (a-choice ch1 == od∅) |
136 ch1not ch1=0 = n (lemma ch1=0) | 138 ch1not ch1=0 = n (lemma ch1=0) |
137 min3 : Minimal (a-choice ch1) ch1not | 139 min3 : Minimal (a-choice ch1) ch1not |
138 min3 = ( prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))) | 140 min3 = prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0)) |
139 x∋min3 : a-choice ch1 ∋ min min3 | 141 x∋min3 : a-choice ch1 ∋ min min3 → x ∋ min min3 |
140 x∋min3 = x∋min min3 | 142 x∋min3 lt = {!!} |
141 min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y)) | 143 min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y)) |
142 min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = {!!} } -- (min min3 ∋ y) ∧ (a-choice ch1 ∋ y) | 144 min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = ? } -- (min min3 ∋ y) ∧ (a-choice ch1 ∋ y) |
143 -- p : (min min3 ∋ y) ∧ (x ∋ y) | 145 -- p : (min min3 ∋ y) ∧ (x ∋ y) |
144 | 146 |
145 | 147 |
146 Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne | 148 Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne |
147 Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) | 149 Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) |