Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison HOD.agda @ 172:8c4d1423d7c4
non terminateing on ε-induction
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Jul 2019 14:59:28 +0900 |
parents | 729b80df8a8a |
children | e6e1bdbda450 |
comparison
equal
deleted
inserted
replaced
171:729b80df8a8a | 172:8c4d1423d7c4 |
---|---|
236 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α | 236 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α |
237 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x | 237 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x |
238 | 238 |
239 -- another form of regularity | 239 -- another form of regularity |
240 -- | 240 -- |
241 -- {-# TERMINATING #-} | 241 {-# TERMINATING #-} |
242 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | 242 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} |
243 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | 243 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) |
244 → (x : OD {suc n} ) → ψ x | 244 → (x : OD {suc n} ) → ψ x |
245 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where | 245 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where |
246 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy) | 246 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } |
247 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case1 ()) | 247 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) |
248 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case2 ()) | 248 ε-induction-ord Zero (Φ 0) (case1 ()) |
249 ε-induction-ord record { lv = lx ; ord = (OSuc lx ox) } {oy} y<x = | 249 ε-induction-ord Zero (Φ 0) (case2 ()) |
250 ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where | 250 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = |
251 lemma : (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox } | 251 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where |
252 lemma : (y : OD) → ord→od record { lv = ly ; ord = oy } ∋ y → od→ord y o< record { lv = lx ; ord = ox } | |
252 lemma y lt with osuc-≡< y<x | 253 lemma y lt with osuc-≡< y<x |
253 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso | 254 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso |
254 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 | 255 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 |
255 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {oy} = | 256 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = |
256 TransFinite {suc n} {suc n ⊔ m} {λ x → x o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od x)} lemma1 lemma2 oy where | 257 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where |
257 lemma1 : (ly : Nat) → | 258 lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ |
258 record { lv = ly ; ord = Φ ly } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → | 259 lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 |
259 ψ (ord→od (record { lv = ly ; ord = Φ ly })) | 260 lemma1 : {n : Level } {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly |
260 lemma1 ly lt = ind {!!} | 261 lemma1 {n} {ly} {oy} = let open ≡-Reasoning in begin |
261 lemma2 : (ly : Nat) (oy : OrdinalD ly) → | 262 lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) |
262 (record { lv = ly ; ord = oy } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od (record { lv = ly ; ord = oy }))) → | 263 ≡⟨ cong ( λ k → lv k ) diso ⟩ |
263 record { lv = ly ; ord = OSuc ly oy } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od (record { lv = ly ; ord = OSuc ly oy })) | 264 lv (record { lv = ly ; ord = oy }) |
264 lemma2 ly oy p lt = ind {!!} | 265 ≡⟨⟩ |
265 | 266 ly |
267 ∎ | |
268 lemma2 : { lx : Nat } → lx < Suc lx | |
269 lemma2 {Zero} = s≤s z≤n | |
270 lemma2 {Suc lx} = s≤s (lemma2 {lx}) | |
271 -- lx Suc lx (1) z(a) <lx by case1 | |
272 -- ly(1) ly(2) (2) z(b) <lx by case1 | |
273 -- z(a) z(b) z(c) z(c) <lx by case2 ( ly==z==x) | |
274 -- | |
275 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z | |
276 lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt | |
277 lemma z lt | case1 lz<ly with <-cmp lx ly | |
278 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
279 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- (1) | |
280 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) | |
281 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- z(a) | |
282 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) | |
283 lemma z lt | case2 lz=ly with <-cmp lx ly | |
284 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | |
285 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) | |
286 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) | |
287 lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) | |
288 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord (Suc lx) (Φ (Suc lx)) {_} {ord (od→ord z)} | |
289 (case1 (subst (λ k → k < Suc lx) (trans (sym lemma1) (sym eq)) lemma2 ))) | |
290 | |
266 | 291 |
267 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 292 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
268 OD→ZF {n} = record { | 293 OD→ZF {n} = record { |
269 ZFSet = OD {suc n} | 294 ZFSet = OD {suc n} |
270 ; _∋_ = _∋_ | 295 ; _∋_ = _∋_ |