# HG changeset patch # User Shinji KONO # Date 1589029397 -32400 # Node ID 81d639ee9bfd049bdbadf4674487c4ee01ee2d9f # Parent a2991ce14ced1bec71dff01e8053396a4e6e7423 ... diff -r a2991ce14ced -r 81d639ee9bfd LEMC.agda --- a/LEMC.agda Sat May 09 17:35:56 2020 +0900 +++ b/LEMC.agda Sat May 09 22:03:17 2020 +0900 @@ -84,32 +84,68 @@ eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) } - record Minimal (x : OD) : Set (suc n) where + record Minimal (x : OD) (ne : ¬ (x == od∅ ) ) : Set (suc n) where field min : OD - x∋min : ¬ (x == od∅ ) → x ∋ min - min-empty : ¬ (x == od∅ ) → (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) + x∋min : x ∋ min + min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) open Minimal - induction : {x : OD} → ({y : OD} → x ∋ y → Minimal y) → Minimal x - induction {x} prev = record { - min = {!!} - ; x∋min = {!!} - ; min-empty = {!!} - } where + open _∧_ + induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) → (ne : ¬ (x == od∅ )) → Minimal x ne + induction {x} prev ne = c2 + where + ch : choiced x + ch = choice-func x ne c1 : OD - c1 = a-choice (choice-func x {!!} ) - c2 : OD - c2 with p∨¬p ( (y : OD ) → def c1 (od→ord y) ∧ (def x (od→ord y))) - c2 | case1 _ = c1 - c2 | case2 No = {!!} -- minimal ( record { def = λ y → def c1 y ∧ def x y } ) {!!} - Min1 : (x : OD) → Minimal x - Min1 x = (ε-induction {λ y → Minimal y } induction x ) + c1 = a-choice ch + c2 : Minimal x ne + c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord y))) ) + c2 | case1 Yes = record { + min = c1 + ; x∋min = is-in ch + ; min-empty = Yes + } + c2 | case2 No = c3 where + y1 : OD + y1 = record { def = λ y → ( def c1 y ∧ def x y) } + noty1 : ¬ (y1 == od∅ ) + noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) ) + ch1 : choiced y1 + ch1 = choice-func y1 noty1 + c3 : Minimal x ne + c3 with is-o∅ (od→ord (a-choice ch1)) + ... | yes eq = record { + min = od∅ + ; x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) ) + ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) ) + } + ... | no n = record { + min = min min3 + ; x∋min = ? + ; min-empty = {!!} + } where + lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅ + lemma eq = begin + od→ord (a-choice ch1) + ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩ + od→ord od∅ + ≡⟨ ord-od∅ ⟩ + o∅ + ∎ where open ≡-Reasoning + ch1not : ¬ (a-choice ch1 == od∅) + ch1not ch1=0 = n (lemma ch1=0) + min3 : Minimal (a-choice ch1) ch1not + min3 = ( prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))) + + + Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne + Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne ) minimal : (x : OD ) → ¬ (x == od∅ ) → OD - minimal x not = min (Min1 x) + minimal x not = min (Min1 x not ) x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) - x∋minimal x ne = x∋min (Min1 x) ne + x∋minimal x ne = x∋min (Min1 x ne) minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) - minimal-1 x ne y = min-empty (Min1 x) ne y + minimal-1 x ne y = min-empty (Min1 x ne ) y