Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 60:6a1f67a4cc6e
dead end
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 May 2019 12:06:43 +0900 |
| parents | d13d1351a1fa |
| children | f2cb756084e0 |
| files | ordinal-definable.agda |
| diffstat | 1 files changed, 38 insertions(+), 41 deletions(-) [+] |
line wrap: on
line diff
--- a/ordinal-definable.agda Wed May 29 05:46:05 2019 +0900 +++ b/ordinal-definable.agda Wed May 29 12:06:43 2019 +0900 @@ -70,6 +70,9 @@ sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n}) +congf : {n : Level} {x y : OD {n}} → { f g : OD {n} → OD {n} } → x ≡ y → f ≡ g → f x ≡ g y +congf refl refl = refl + o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) @@ -233,6 +236,10 @@ ∅0 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal x lt ... | min with eq→ (o<→c< (Minimumo.min<x min)) ... | () + +∅< : {n : Level} → { x y : OD {n} } → def x (od→ord y ) → ¬ ( x == od∅ {n} ) +∅< {n} {x} {y} d eq with eq→ eq d +∅< {n} {x} {y} d eq | lift () is-od∅ : {n : Level} → ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} ) @@ -260,6 +267,9 @@ 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) + open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} @@ -333,6 +343,8 @@ proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } } + ∅-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} @@ -341,46 +353,31 @@ minimul<x x not = lemma0 (min<x (minord x not)) where lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) lemma0 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 - regularity-ord : (x : Ordinal ) (not : ¬ (ord→od x == od∅)) → - (ord→od x ∋ minimul (ord→od x) not) ∧ (Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅) - proj1 ( regularity-ord x not ) = minimul<x (ord→od x) not - proj2 ( regularity-ord x not ) = reg1 where - reg2 : {y : Ordinal} → ( def (minimul (ord→od x) not) y ∧ (minimul (ord→od x) not ∋ ord→od y) ∧ ((ord→od x) ∋ ord→od y) ) → ⊥ - reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t) - ... | p1 | p2 | p3 with is-∋ (ord→od x) ( ord→od y) - reg2 {y} t | p1 | p2 | p3 | no ¬p = ⊥-elim (¬p p3 ) -- ¬ x ∋ ord→od y empty x case - reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) not) (ord→od y) - reg2 {y} t | p1 | p2 | p3 | yes p | no ¬p = ⊥-elim (¬p p2 ) -- minimum contains nothing q.e.d. - reg2 {y} t | p1 | p2 | p3 | yes p | yes p₁ = {!!} - reg0 : {y : Ordinal {suc n}} → def (Select (minimul (ord→od x) not) (λ z → (minimul (ord→od x) not ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y - reg0 {y} t with trio< y (mino (minord (ord→od x) not)) - reg0 {y} t | tri< a ¬b ¬c with reg2 {y} t - ... | () - reg0 {y} t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) not) ) refl - (def-subst {suc n} {ord→od y} {mino (minord (ord→od x) not)} (proj1 t) refl (sym diso)) - where - lemma : ( ox oy : Ordinal {suc n} ) → ox ≡ oy → ord→od ox c< ord→od oy → Lift (suc n) ⊥ - lemma ox oy refl lt = lift ( o≡→¬c< {suc n} {ord→od oy} {ord→od oy} refl lt ) - reg0 {y} t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) not)) (lemma {!!}) c where - lemma : def (ord→od (mino (minord (ord→od x) not))) y → y o< mino (minord (ord→od x) not) - lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) not))} - (def-subst {suc n} {ord→od (mino (minord (ord→od x) not))} {y} {!!} refl (sym diso)) - lemma d | clt = o<-subst clt ord-iso ord-iso - ... | () - reg1 : Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅ - reg1 = record { eq→ = reg0 ; eq← = λ () } where - ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) - ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 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 = - subst₂ ( λ x min → (x ∋ min) ∧ (Select min (λ x₁ → (min ∋ x₁) ∧ (x ∋ x₁)) == od∅) ) - oiso lemma ( regularity-ord (od→ord x) (subst (λ k → ¬ (k == od∅) ) (sym oiso) not )) where - lemma : minimul (ord→od (od→ord x)) (subst (λ k → ¬ (k == od∅)) (sym oiso) not) ≡ minimul x not - lemma = cong₂ (λ x not → minimul x not ) oiso {!!} - - - - - - + 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 = record { proj1 = minimul<x x not ; proj2 = record {eq→ = reg0 ; eq← = λ () } } where + noto : o∅ o< (od→ord (ord→od ox)) + noto = lemma {ox} {od→ord (ord→od ox)} diso (∅10 refl not) where + lemma : { ox oy : Ordinal {suc n}} → oy ≡ ox → o∅ o< ox → o∅ o< oy + lemma refl lt = lt + Min : Minimumo ox + Min = ominimal ox (∅10 refl not) + Mino : Minimumo (od→ord (ord→od ox )) + Mino = ominimal (od→ord (ord→od ox )) noto + m=mo : ox ≡ od→ord (ord→od ox ) → mino Mino ≡ mino Min + m=mo eq with ox + ... | xx = ? + reg0 : {y : Ordinal {suc n}} → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) y → def od∅ y + reg0 {y} t with trio< y ( mino Mino ) + reg0 {y} t | tri< a ¬b ¬c = {!!} + reg0 {y} t | tri≈ ¬a refl ¬c with o≡→¬c< {suc n} {ord→od (mino Mino)} refl lemma where + lemma : ord→od y c< ord→od (mino Mino) + lemma = subst (λ k → k c< ord→od (mino Mino) ) oiso {!!} -- (proj1 t) + reg0 {y} t | tri≈ ¬a b ¬c | () + reg0 {y} t | tri> ¬a ¬b c with o<> y (mino Mino) lemma c where + lemma : y o< mino Mino + lemma = {!!} + reg0 {y} t | tri> ¬a ¬b c | ()