Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 224:afc864169325
recover ε-induction
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 10 Aug 2019 12:31:25 +0900 |
| parents | 59771eb07df0 |
| children | e06b76e5b682 |
line wrap: on
line diff
--- a/ordinal.agda Fri Aug 09 17:57:58 2019 +0900 +++ b/ordinal.agda Sat Aug 10 12:31:25 2019 +0900 @@ -29,12 +29,6 @@ _o<_ : {n : Level} ( x y : Ordinal ) → Set n _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) -o<-dom : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal -o<-dom {n} {x} _ = x - -o<-cod : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal -o<-cod {n} {_} {y} _ = y - s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x s<refl {n} {lv} {Φ lv} = Φ< s<refl {n} {lv} {OSuc lv x} = s< s<refl @@ -66,12 +60,6 @@ lv x ≡ lv y → ord x ≅ ord y → x ≡ y ordinal-cong refl refl = refl -ordinal-lv : {n : Level} {x y : Ordinal {n}} → x ≡ y → lv x ≡ lv y -ordinal-lv refl = refl - -ordinal-d : {n : Level} {x y : Ordinal {n}} → x ≡ y → ord x ≅ ord y -ordinal-d refl = refl - ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t @@ -81,9 +69,6 @@ trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ trio>≡ refl = ≡→¬d< -triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly ) -triO {n} {lx} {ly} x y = <-cmp lx ly - triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) @@ -100,22 +85,6 @@ <-osuc {n} {record { lv = lx ; ord = Φ .lx }} = case2 Φ< <-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl ) -osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x ) -osuc-lveq {n} = refl - -osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox -osucc {n} {ox} {oy} (case1 x) = case1 x -osucc {n} {ox} {oy} (case2 x) with d<→lv x -... | refl = case2 (s< x) - -case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥ -case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2 -... | refl = nat-≡< refl lt1 - -case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥ -case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2 -... | refl = nat-≡< refl lt1 - o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥ o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt @@ -156,20 +125,6 @@ osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case2 x₁) = nat-≡< (sym (d<→lv x₁)) x₂ osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 y<x = o<> (case2 x<y) y<x -maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx -maxαd x y with triOrdd x y -maxαd x y | tri< a ¬b ¬c = y -maxαd x y | tri≈ ¬a b ¬c = x -maxαd x y | tri> ¬a ¬b c = x - -minαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx -minαd x y with triOrdd x y -minαd x y | tri< a ¬b ¬c = x -minαd x y | tri≈ ¬a b ¬c = y -minαd x y | tri> ¬a ¬b c = x - -_o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n) -a o≤ b = (a ≡ b) ∨ ( a o< b ) ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ ) @@ -208,99 +163,9 @@ lemma1 (case1 x) = ¬a x lemma1 (case2 x) = ≡→¬d< x -xo<ab : {n : Level} {oa ob : Ordinal {suc n}} → ( {ox : Ordinal {suc n}} → ox o< oa → ox o< ob ) → oa o< osuc ob -xo<ab {n} {oa} {ob} a→b with trio< oa ob -xo<ab {n} {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc -xo<ab {n} {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc -xo<ab {n} {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) - -maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal -maxα x y with trio< x y -maxα x y | tri< a ¬b ¬c = y -maxα x y | tri> ¬a ¬b c = x -maxα x y | tri≈ ¬a refl ¬c = x - -minα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal -minα {n} x y with trio< {n} x y -minα x y | tri< a ¬b ¬c = x -minα x y | tri> ¬a ¬b c = y -minα x y | tri≈ ¬a refl ¬c = x - -min1 : {n : Level} → {x y z : Ordinal {suc n} } → z o< x → z o< y → z o< minα x y -min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y -min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x -min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x -min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y - --- --- max ( osuc x , osuc y ) --- - -omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n} -omax {n} x y with trio< x y -omax {n} x y | tri< a ¬b ¬c = osuc y -omax {n} x y | tri> ¬a ¬b c = osuc x -omax {n} x y | tri≈ ¬a refl ¬c = osuc x - -omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y -omax< {n} x y lt with trio< x y -omax< {n} x y lt | tri< a ¬b ¬c = refl -omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) -omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) - -omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y -omax≡ {n} x y eq with trio< x y -omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) -omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl -omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) - -omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y -omax-x {n} x y with trio< x y -omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc -omax-x {n} x y | tri> ¬a ¬b c = <-osuc -omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc - -omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y -omax-y {n} x y with trio< x y -omax-y {n} x y | tri< a ¬b ¬c = <-osuc -omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc -omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc - -omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x -omxx {n} x with trio< x x -omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) -omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) -omxx {n} x | tri≈ ¬a refl ¬c = refl - -omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x) -omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) open _∧_ -osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) -proj1 (osuc2 {n} x y) (case1 lt) = case1 lt -proj1 (osuc2 {n} x y) (case2 (s< lt)) = case2 lt -proj2 (osuc2 {n} x y) (case1 lt) = case1 lt -proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt -... | refl = case2 (s< lt) - -OrdTrans : {n : Level} → Transitive {suc n} _o≤_ -OrdTrans (case1 refl) (case1 refl) = case1 refl -OrdTrans (case1 refl) (case2 lt2) = case2 lt2 -OrdTrans (case2 lt1) (case1 refl) = case2 lt1 -OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) - -OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n) -OrdPreorder {n} = record { Carrier = Ordinal - ; _≈_ = _≡_ - ; _∼_ = _o≤_ - ; isPreorder = record { - isEquivalence = record { refl = refl ; sym = sym ; trans = trans } - ; reflexive = case1 - ; trans = OrdTrans - } - } - TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) @@ -355,9 +220,9 @@ → ¬ p TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) -open import Ordinals +open import Ordinals -C-Ordinal : {n : Level } → Ordinals {suc n} +C-Ordinal : {n : Level} → Ordinals {suc n} C-Ordinal {n} = record { ord = Ordinal {suc n} ; o∅ = o∅ @@ -384,3 +249,142 @@ caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → ψ (record { lv = lx ; ord = OSuc lx x₁ }) caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev + +module C-Ordinal-with-choice {n : Level} where + + import OD + -- open inOrdinal C-Ordinal + open OD (C-Ordinal {n}) + open OD.OD + + -- + -- another form of regularity + -- + ε-induction : {m : Level} { ψ : OD → Set m} + → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) + → (x : OD ) → ψ x + ε-induction {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where + ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } + → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) ) + ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x = + ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where + lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox } + lemma z lt with osuc-≡< y<x + lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso + lemma z lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 + ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) = + ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where + -- + -- if lv of z if less than x Ok + -- else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma + -- + -- lx Suc lx (1) lz(a) <lx by case1 + -- ly(1) ly(2) (2) lz(b) <lx by case1 + -- lz(a) lz(b) lz(c) lz(c) <lx by case2 ( ly==lz==lx) + -- + lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥ + lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2 + lemma1 : {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly + lemma1 {ly} {oy} = let open ≡-Reasoning in begin + lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) + ≡⟨ cong ( λ k → lv k ) diso ⟩ + lv (record { lv = ly ; ord = oy }) + ≡⟨⟩ + ly + ∎ + lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z + lemma z lt with c<→o< {z} {ord→od (record { lv = ly ; ord = oy })} lt + lemma z lt | case1 lz<ly with <-cmp lx ly + lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen + lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- ly(1) + subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) )) + lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- lz(a) + subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c)))) + lemma z lt | case2 lz=ly with <-cmp lx ly + lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen + lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- lz(b) + ... | eq = subst (λ k → ψ k ) oiso + (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) + lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c) + ... | eq = subst (λ k → ψ k ) oiso ( ε-induction-ord lx (dz oz=lx) {lv (od→ord z)} {ord (od→ord z)} (case2 (dz<dz oz=lx) )) where + oz=lx : lv (od→ord z) ≡ lx + oz=lx = let open ≡-Reasoning in begin + lv (od→ord z) + ≡⟨ eq ⟩ + lv (od→ord (ord→od (ordinal ly oy))) + ≡⟨ cong ( λ k → lv k ) diso ⟩ + lv (ordinal ly oy) + ≡⟨ sym lx=ly ⟩ + lx + ∎ + dz : lv (od→ord z) ≡ lx → OrdinalD lx + dz refl = OSuc lx (ord (od→ord z)) + dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x + dz<dz refl = s<refl + + --- + --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice + --- + record choiced ( X : OD) : Set (suc (suc n)) where + field + a-choice : OD + is-in : X ∋ a-choice + + choice-func' : (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X + choice-func' X p∨¬p not = have_to_find where + ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n)) + ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X + lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox + lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where + ∋-p' : (A x : OD ) → Dec ( A ∋ x ) + ∋-p' A x with p∨¬p ( A ∋ x ) + ∋-p' A x | case1 t = yes t + ∋-p' A x | case2 t = no t + ∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) } + → ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B + ∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x) + ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t + ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where + lemma : ¬ ((x : Ordinal {suc n}) → A x) → B + lemma not with p∨¬p B + lemma not | case1 b = b + lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) + caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) + caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) )) + caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } ) + caseΦ lx prev | no ¬p = lemma where + lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X) + lemma1 x with trio< x (ordinal lx (Φ lx)) + lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where + lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx) + lemma2 (case1 lt) = case1 lt + lemma1 x | tri< a ¬b ¬c | case2 found = case2 found + lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df ) + lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt )) + lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c )) + lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X + lemma = ∀-imply-or lemma1 + caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) ) + caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } ) + caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p }) + caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where + lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥ + lemma y lt with trio< y (ordinal lx x ) + lemma y lt | tri< a ¬b ¬c = not_found y a + lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p + lemma y lt | tri> ¬a ¬b c with osuc-≡< lt + lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl ) + lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 ) + caseOSuc lx x (case2 found) | no ¬p = case2 found + caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) → + ψ (record { lv = lx ; ord = OSuc lx x }) + caseOSuc1 lx x lt = caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl)) + have_to_find : choiced X + have_to_find with lemma-ord (od→ord X ) + have_to_find | t = dont-or t ¬¬X∋x where + ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥) + ¬¬X∋x nn = not record { + eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) + ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) + } +