Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison LEMC.agda @ 285:313140ae5e3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 10 May 2020 09:25:13 +0900
parents a8f9c8a27e8d
children 5de8905a5a2b
comparison
equal deleted inserted replaced
284:a8f9c8a27e8d 285:313140ae5e3d
88 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) 88 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
89 ¬¬X∋x nn = not record { 89 ¬¬X∋x nn = not record {
90 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) 90 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
91 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) 91 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
92 } 92 }
93 record Minimal (x : OD) (ne : ¬ (x == od∅ ) ) : Set (suc n) where 93 record Minimal (x : OD) : Set (suc n) where
94 field 94 field
95 min : OD 95 min : OD
96 x∋min : x ∋ min 96 x∋min : x ∋ min
97 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y) 97 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
98 open Minimal 98 open Minimal
99 open _∧_ 99 open _∧_
100 -- 100 --
101 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only 101 -- from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
102 -- 102 --
103 induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x)) 103 induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u )
104 → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) 104 → (u : OD ) → (u∋x : u ∋ x) → Minimal u
105 induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y)) 105 induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y))
106 ... | case1 P = 106 ... | case1 P =
107 record { min = x 107 record { min = x
108 ; x∋min = u∋x 108 ; x∋min = u∋x
109 ; min-empty = P 109 ; min-empty = P
110 } 110 }
111 ... | case2 NP = 111 ... | case2 NP = min2 where
112 record { min = min min2
113 ; x∋min = x∋min min2
114 ; min-empty = min-empty min2
115
116 } where
117 p : OD 112 p : OD
118 p = record { def = λ y1 → def x y1 ∧ def u y1 } 113 p = record { def = λ y1 → def x y1 ∧ def u y1 }
119 np : ¬ (p == od∅) 114 np : ¬ (p == od∅)
120 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) 115 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ )
121 y1choice : choiced p 116 y1choice : choiced p
122 y1choice = choice-func p np 117 y1choice = choice-func p np
123 y1 : OD 118 y1 : OD
124 y1 = a-choice y1choice 119 y1 = a-choice y1choice
125 y1prop : (x ∋ y1) ∧ (u ∋ y1) 120 y1prop : (x ∋ y1) ∧ (u ∋ y1)
126 y1prop = is-in y1choice 121 y1prop = is-in y1choice
127 min2 : Minimal u (∅< (proj2 y1prop)) 122 min2 : Minimal u
128 min2 = prev (proj1 y1prop) u (proj2 y1prop) 123 min2 = prev (proj1 y1prop) u (proj2 y1prop)
129 Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u (∅< u∋x) 124 Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u
130 Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u (∅< u∋x) } induction x u u∋x ) 125 Min2 x u u∋x = (ε-induction {λ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x )
131 cx : {x : OD} → ¬ (x == od∅ ) → choiced x 126 cx : {x : OD} → ¬ (x == od∅ ) → choiced x
132 cx {x} nx = choice-func x nx 127 cx {x} nx = choice-func x nx
133 minimal : (x : OD ) → ¬ (x == od∅ ) → OD 128 minimal : (x : OD ) → ¬ (x == od∅ ) → OD
134 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) 129 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not)))
135 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) ) 130 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )