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 )