Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 66:92a11dc6425c
regularity done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 30 May 2019 01:55:59 +0900 |
| parents | 164ad5a703d8 |
| children | 94c796aee319 |
| files | ordinal-definable.agda |
| diffstat | 1 files changed, 25 insertions(+), 52 deletions(-) [+] |
line wrap: on
line diff
--- a/ordinal-definable.agda Thu May 30 01:02:47 2019 +0900 +++ b/ordinal-definable.agda Thu May 30 01:55:59 2019 +0900 @@ -221,16 +221,6 @@ tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b)) tri-c< {n} x y | tri> ¬a ¬b c = tri> ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst (o<→c< c) oiso diso) -¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n} -¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where - lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} - lemma ox = TransFinite {suc n} {λ ox → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} } {!!} {!!} {!!} ox - --- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n )) - --- ==∅→≡ : {n : Level} → { x : OD {suc n} } → ( x == od∅ {suc n} ) → x ≡ od∅ {suc n} --- ==∅→≡ {n} {x} eq = cong ( λ k → record { def = k } ) (trans {!!} ∅-base-def ) where - c<> : {n : Level } { x y : OD {suc n}} → x c< y → y c< x → ⊥ c<> {n} {x} {y} x<y y<x with tri-c< x y c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x @@ -277,8 +267,25 @@ lemma : ¬ od→ord x ≡ o∅ lemma eq = not ( ∅7 eq ) -∅10 : {n : Level} → {ox : Ordinal {n}} → {x : OD{n}} → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅)) → o∅ o< ox -∅10 {n} {ox} {x} refl not = subst (λ k → o∅ o< k) diso (∅9 not) +∅10 : {n : Level} → {ox : Ordinal {n}} → (not : ¬ (ord→od ox == od∅)) → o∅ o< ox +∅10 {n} {ox} not = subst (λ k → o∅ o< k) diso (∅9 not) + +¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n} +¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where + lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} + lemma ox ne with is-o∅ ox + lemma ox ne | yes refl with ne ( ord→== lemma1 ) where + lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅ + lemma1 = cong ( λ k → od→ord k ) o∅→od∅ + lemma o∅ ne | yes refl | () + lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p)) + + +-- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n )) + +-- ==∅→≡ : {n : Level} → { x : OD {suc n} } → ( x == od∅ {suc n} ) → x ≡ od∅ {suc n} +-- ==∅→≡ {n} {x} eq = cong ( λ k → record { def = k } ) (trans {!!} ∅-base-def ) where + open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) @@ -355,46 +362,12 @@ } ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq - minord : (x : OD {suc n} ) → ¬ (x == od∅ ) → Minimumo (od→ord x) - minord x not = ominimal (od→ord x) (∅9 not) minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} - minimul x not = ord→od ( mino (minord x not)) - omin→cmin : {x : OD {suc n}} → {not : ¬ x == od∅ } → mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) - omin→cmin {x} {not} m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl - minimul<x : (x : OD {suc n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not - minimul<x x not = omin→cmin {x} {not} (min<x (minord x not)) - omin∅→min∅ : (ox : Ordinal {suc n}) → {not : ¬ ( ord→od ox == od∅)} - → mino (ominimal ox (∅10 refl not)) ≡ o∅ → mino (ominimal (od→ord (ord→od ox)) (∅9 not)) ≡ o∅ - omin∅→min∅ ox {not} eq with ominimal ox (∅10 refl not) - omin∅→min∅ record { lv = Zero ; ord = (Φ .0) } eq | record { mino = mino ; min<x = case1 () } - omin∅→min∅ record { lv = Zero ; ord = (Φ .0) } eq | record { mino = mino ; min<x = case2 () } - omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } refl | record { mino = .o∅ ; min<x = case1 () } - omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 (Φ .0)) } {not} refl | record { mino = record { lv = .0 ; ord = .(Φ 0) } ; min<x = case2 Φ< } = {!!} where - lemma : mino (ominimal (od→ord (ord→od (record { lv = Zero ; ord = OSuc Zero (Φ Zero) }))) (∅5 (λ eq → not (∅7 eq)))) ≡ o∅ - lemma = {!!} - omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 (OSuc .0 ord₁)) } {_} refl | record { mino = record { lv = .0 ; ord = .(Φ 0) } ; min<x = case2 Φ< } = {!!} - omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!} - omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } eq | record { mino = mino ; min<x = case2 () } - omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!} - omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } refl | record { mino = .o∅ ; min<x = case2 () } - omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!} - omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } refl | record { mino = .o∅ ; min<x = case2 () } + minimul x not = od∅ regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - regularity x not = regularity-ord (od→ord x) {x} (sym oiso ) not where - regularity-ord : (ox : Ordinal ) → {x : OD} → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅)) - → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - regularity-ord ox {x} refl not with ominimal ox (∅10 refl not) | minimul x not | is-o∅ (mino (minord x not)) | is-o∅ ox - regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case1 () } | r | t | s - regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case2 () } | r | t | s - regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = min ; min<x = case1 () } | r | t | s - regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Suc lv₁ ; ord = ord } ; min<x = case2 () } | r | t | s - regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< } | r | yes p | s - = record { proj1 = {!!} ; proj2 = record { eq→ = {!!} ; eq← = λ () } } - regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< } | r | no ¬p | yes p = {!!} - regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< } | r | no ¬p | no ¬p₁ = {!!} - regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Zero ; ord = OSuc .0 ord₂ } ; min<x = case2 (s< lt) } | r | t | s = {!!} - regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case1 lt } | r | t | s = {!!} - regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case2 () } | r | t | s - regularity-ord record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } refl not | record { mino = min ; min<x = min<x } | r | t | s = {!!} - regularity-ord record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } refl not | record { mino = min ; min<x = min<x } | r | t | s = {!!} + proj1 (regularity x not ) = ¬∅=→∅∈ not + proj2 (regularity x not ) = record { eq→ = reg ; eq← = λ () } where + reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y + reg {y} t with proj1 t + ... | x∈∅ = x∈∅