Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1048:a8d6ac036d88
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 07 Dec 2022 20:56:57 +0900 |
| parents | aebab71cc386 |
| children | e6b9de04d0ca |
| files | src/OrdUtil.agda src/zorn.agda |
| diffstat | 2 files changed, 41 insertions(+), 46 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OrdUtil.agda Wed Dec 07 11:06:36 2022 +0900 +++ b/src/OrdUtil.agda Wed Dec 07 20:56:57 2022 +0900 @@ -40,7 +40,6 @@ o≤> {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y o≤> {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x - open _∧_ ¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) ) @@ -224,6 +223,12 @@ ... | case1 eq = case2 eq ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) +x<y∨y≤x : (x sp1 : Ordinal ) → ( x o< sp1 ) ∨ ( sp1 o≤ x ) +x<y∨y≤x x sp1 with trio< x sp1 +... | tri< a ¬b ¬c = case1 a +... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b)) +... | tri> ¬a ¬b c = case2 (o<→≤ c) + OrdTrans : Transitive _o≤_ OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
--- a/src/zorn.agda Wed Dec 07 11:06:36 2022 +0900 +++ b/src/zorn.agda Wed Dec 07 20:56:57 2022 +0900 @@ -459,6 +459,22 @@ z52 : supf (supf b) ≡ supf b z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ + x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x + x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x + ... | case2 le = le + ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where + z46 : odef (UnionCF A f ay supf x) (f (supf x)) + z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf z47 )) ⟫ where + z47 : supf (supf x) ≡ supf x + z47 = supf-idem x≤z sx≤z + z45 : f (supf x) ≤ supf x + z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46 + + supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b + supf-mono< {a} {b} b≤z sa<sb with order {a} {b} b≤z sa<sb (init asupf refl) + ... | case2 lt = lt + ... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb ) + -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b) -- the condition of cfcs is satisfied, this is obvious @@ -1135,53 +1151,27 @@ fc1 = subst (λ k → FClosure A f k w ) (sym su=u) (proj1 fc) sa<x : supf0 px o< b sa<x = subst (λ k → supf0 px o< k ) x=b ( proj2 fc) - zc36 : sp1 ≡ x -- this cannot heppen because px o< supf0 px ( px o≤ spuf0 px o< supf1 x ≡ x → ⊥ ) + zc36 : sp1 ≡ x -- this cannot heppen because zc36 with osuc-≡< zc31 ... | case1 eq = trans eq (sym x=b) - ... | case2 sp1<b with osuc-≡< ( zc-b<x _ (subst (λ k → sp1 o< k ) ? sp1<b)) - ... | case1 sp1=px = ⊥-elim ( <<-irr ? z42 ) where - z40 : odef pchainpx (f (supf1 sp1)) - z40 = case2 ⟪ fsuc _ (init ? ?) , ? ⟫ - z41 : f (supf1 sp1) ≤ sp1 - z41 = MinSUP.x≤sup sup1 z40 - z44 : sp1 ≤ supf1 sp1 - z44 = ? - z43 : px o≤ supf0 px - z43 with zc43 (supf0 px) px - ... | case2 le = le - ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf0 px) (ZChain.asupf zc)))) where - z46 : odef (UnionCF A f ay supf1 px) (f (supf1 px)) - z46 = ⟪ proj2 ( mf (supf1 px) ?) , ch-is-sup (supf0 px) spx<px z48 (fsuc _ (init ? z47 )) ⟫ where - z47 : supf1 (supf0 px) ≡ supf1 px - z47 = subst₂ (λ j k → j ≡ k ) (sym (sf1=sf0 ?)) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) ) - z48 : supf1 (supf0 px) ≡ supf0 px - z48 = subst (λ k → k ≡ supf0 px ) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) ) - z45 : f (supf0 px) ≤ supf0 px - z45 = subst (λ k → f k ≤ k ) ? ( IsMinSUP.x≤sup (is-minsup ? ) z46 ) - z42 : (supf1 sp1) << f (supf1 sp1) - z42 = proj1 ( mf< (supf1 sp1) ? ) - ... | case2 sp1<px = ⊥-elim ( o≤> z39 z44 ) where - z39 : supf1 px o≤ supf1 x -- supf0 px o≤ px - z39 = supf1-mono (o<→≤ px<x) - z43 : px o≤ supf0 px - z43 with zc43 (supf0 px) px - ... | case2 le = le - ... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf0 px) (ZChain.asupf zc)))) where - z46 : odef (UnionCF A f ay supf1 px) (f (supf1 px)) - z46 = ⟪ proj2 ( mf (supf1 px) ?) , ch-is-sup (supf0 px) spx<px z48 (fsuc _ (init ? z47 )) ⟫ where - z47 : supf1 (supf0 px) ≡ supf1 px - z47 = subst₂ (λ j k → j ≡ k ) (sym (sf1=sf0 ?)) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) ) - z48 : supf1 (supf0 px) ≡ supf0 px - z48 = subst (λ k → k ≡ supf0 px ) (sym (sf1=sf0 ?)) ( ZChain.supf-idem zc o≤-refl (o<→≤ spx<px) ) - z45 : f (supf0 px) ≤ supf0 px - z45 = subst (λ k → f k ≤ k ) ? ( IsMinSUP.x≤sup (is-minsup ? ) z46 ) - z44 : supf1 x o< supf1 px - z44 = osucprev ( begin - osuc (supf1 x) ≡⟨ cong osuc (sf1=sp1 px<x) ⟩ - osuc sp1 ≤⟨ osucc sp1<px ⟩ - px ≤⟨ z43 ⟩ - supf0 px ≡⟨ sym (sf1=sf0 o≤-refl ) ⟩ - supf1 px ∎ ) where open o≤-Reasoning O + ... | case2 sp1<b = ⊥-elim ? where + -- sp1 o< x → ⊥ + -- supf0 px o≤ sp1 o< x → supf0 px o≤ px + -- px o≤ supf0 px → px ≡ spuf0 px o≤ spuf1 x o< x + sp1<x : sp1 o< x + sp1<x = subst (λ k → sp1 o< k ) ? sp1<b + zc38 : supf0 px o≤ px + zc38 = begin + supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ + supf1 px ≤⟨ supf1-mono ? ⟩ + supf1 x ≡⟨ sf1=sp1 ? ⟩ + sp1 ≤⟨ zc-b<x _ sp1<x ⟩ + px ∎ where open o≤-Reasoning O + zc37 : supf0 px ≡ px + zc37 with trio< (supf0 px) px + ... | tri< a ¬b ¬c = ⊥-elim ( o≤> (ZChain.x≤supfx zc o≤-refl zc38) a ) + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> zc38 c ) ... | no lim with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )