Members/kono/Proof/ZF-in-agda: ordinal-definable.agda comparison

comparison ordinal-definable.agda @ 57:419688a279e0

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 28 May 2019 11:31:43 +0900
parents	aad8cdce8845
children	323b561210b5

comparison

equal deleted inserted replaced

-:aad8cdce8845
+:419688a279e0
 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { mino = record { lv = (Suc lv) ; ord = ord } ; min<x = case2 s<refl}
 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ())
 ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lx ; ord = Φ (Suc lx) } ; min<x = case2 ℵΦ<  }
 ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case2 ())
-∅5 : {n : Level} →  ( x : Ordinal {n} )  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
+∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
-∅5 {n} record { lv = Zero ; ord = (Φ .0) } not = ⊥-elim (not refl)
+∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl)
-∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ<
+∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
-∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n)
+∅5 {n} {record { lv = (Suc lv) ; ord = ord }} not = case1 (s≤s z≤n)
 ∅8 : {n : Level} →  ( x : Ordinal {n} )  → ¬  x o< o∅ {n}
 ∅8 {n} x (case1 ())
 ∅8 {n} x (case2 ())
 eq→ = λ d →  lemma ( eq→  eq (def-subst d (sym oiso) refl )) ;
 eq← = λ d →  lemma ( eq←  eq (def-subst d (sym oiso) refl ))  }
 where
 lemma : {x : OD {n} } {z : Ordinal {n}} → def (ord→od (od→ord x)) z → def x z
 lemma {x} {z} d = def-subst d oiso refl
+=-iso : {n : Level } {x y : OD {suc n} } → (x == y) ≡ (ord→od (od→ord x) == y)
+=-iso {_} {_} {y} = cong ( λ k → k == y ) (sym oiso)
 ord→== : {n : Level} →  { x y : OD {n} } → od→ord x ≡  od→ord y →  x == y
 ord→== {n} {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
 lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
 lemma ox ox  refl = eq-refl
 ∅2 : {n : Level} →  { x : OD {n} } → o∅ {n} o<  od→ord x → ¬ ( x  == od∅ {n} )
 ∅2 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal (od→ord x ) lt
 ... | min with eq→ ( def-subst (o<→c< (Minimumo.min<x min)) oiso refl )
 ... | ()
+∅0 : {n : Level} →  { x : Ordinal {n} } → o∅ {n} o< x → ¬ ( ord→od x  == od∅ {n} )
+∅0 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal x lt
+... | min with eq→ (o<→c< (Minimumo.min<x min))
+... | ()
 is-od∅ : {n : Level} →  ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} )
 is-od∅ {n} x with trio< {n} (od→ord x) (o∅ {suc n})
 is-od∅ {n} x | tri≈ ¬a b ¬c = yes ( ∅7 (orefl b) )
 is-od∅ {n} x | tri< (case1 ()) ¬b ¬c
 is-∋ {n} x y with tri-c< x y
 is-∋ {n} x y | tri< a ¬b ¬c = no ¬c
 is-∋ {n} x y | tri≈ ¬a b ¬c = no ¬c
 is-∋ {n} x y | tri> ¬a ¬b c = yes c
+is-o∅ : {n : Level} →  ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} )
+is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl
+is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
+is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
 open _∧_
-∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x
+∅9 : {n : Level} → {x : OD {n} } → ¬ x == od∅ → o∅ o< od→ord x
-∅9 x not = ∅5 ( od→ord x) lemma where
+∅9 {_} {x} not = ∅5  lemma where
 lemma : ¬ od→ord x ≡ o∅
 lemma eq = not ( ∅7  eq )
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record {
 selection {ψ} {X} {y} = record {
 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
 ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
 }
 minord : (x : OD {suc n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x)
-minord x not = ominimal (od→ord x) (∅9 x not)
+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))
 minimul<x : (x : OD {suc n} ) →  (not :  ¬ x == od∅ ) → x ∋ minimul x not
 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 :  (x : OD) (not : ¬ (x == od∅)) →
+regularity-ord :  (x : Ordinal ) (not :  o∅ o< x ) →
-(x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+(ord→od x ∋ minimul (ord→od x) (∅0 not)) ∧ (Select (minimul (ord→od x) (∅0 not)) (λ x₁ → (minimul (ord→od x) (∅0 not) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅)
-proj1 ( regularity x non ) =  minimul<x x non
+proj1 ( regularity-ord x non ) =  minimul<x (ord→od x) (∅0 non)
-proj2 ( regularity x non ) = reg1 where
+proj2 ( regularity-ord x non ) = reg1 where
-reg2 : {y : Ordinal} → ( def (minimul x non) y ∧ (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥
+reg2 : {y : Ordinal} → ( def (minimul (ord→od x) (∅0 non)) y ∧ (minimul (ord→od x) (∅0 non) ∋ 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-∋ x ( ord→od y)
+... | 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 x non) (ord→od y)
+reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) (∅0 non)) (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}} → Minimumo (od→ord x) → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
+reg0 : {y : Ordinal {suc n}} → Minimumo x → def (Select (minimul (ord→od x) (∅0 non)) (λ z → (minimul (ord→od x) (∅0 non) ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y
-reg0 {y} m t with trio< y (mino (minord x non))
+reg0 {y} m t with trio< y (mino (minord (ord→od x) (∅0 non)))
-reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} ( record {
+reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} t
-proj1 = (def-subst {suc n} {minimul x  non} (o<→c< a) refl diso )
-; proj2 = record { proj1 = proj1 (proj2 t )
-; proj2 = proj2 (proj2 t )
-}} )
 ... | ()
-reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord x non) ) refl
+reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) (∅0 non)) ) refl
-(def-subst {suc n} {ord→od y} {mino (minord x  non)} (proj1 t) refl (sym diso))
+(def-subst {suc n} {ord→od y} {mino (minord (ord→od x)  (∅0 non))} (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} m t | tri> ¬a ¬b c with o<> y (mino (minord x non)) (lemma (proj1 t)) c where
+reg0 {y} m t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) (∅0 non))) (lemma {!!}) c where
-lemma : def (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 eq)))))) y → y o< mino (minord x non)
+lemma : def (ord→od (mino (ominimal x (∅5 (λ eq → (∅0 non) (∅7 {!!})))))) y → y o< mino (minord (ord→od x) (∅0 non))
-lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord x non))}
+lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) (∅0 non)))}
-(def-subst {suc n}  {ord→od (mino (minord x non))} {y} d refl (sym diso))
+(def-subst {suc n}  {ord→od (mino (minord (ord→od x) (∅0 non)))} {y} {!!} refl (sym diso))
 lemma d | clt = o<-subst clt ord-iso ord-iso
 ... | ()
-reg1 :  Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
+reg1 :  Select (minimul (ord→od x) (∅0 non)) (λ x₁ → (minimul (ord→od x) (∅0 non) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
-reg1 = record { eq→ =  reg0 (minord x non) ; eq← = λ () }
+reg1 = record { eq→ =  reg0 (ominimal x non) ; eq← = λ () } where
+∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
+∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  where
+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 with regularity-ord ( od→ord x ) ( ∅9 not )
+... | t = ?

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

comparison ordinal-definable.agda @ 57:419688a279e0