Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 559:9ba98ecfbe62

fcn-cmp done

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 30 Apr 2022 04:41:06 +0900
parents	fed1c67b9a65
children	d09f9a1d6c2f

comparison

equal deleted inserted replaced

-:fed1c67b9a65
+:9ba98ecfbe62
 ... | case1 eq = fcn s mf p
 ... | case2 y<fy = suc (fcn s mf p )
 fcn-inject : {A : HOD} (s : Ordinal) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx  ≡ fcn s mf cy → * x ≡ * y
-fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) cx cy refl eq where
+fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where
-fc00 :  (i : ℕ ) →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → i ≡ fcn s mf cy → * x ≡ * y
+fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → * x ≡ * y
-fc00 zero (init _) (init x₁) i=x i=y = refl
+fc00 zero zero refl (init _) (init x₁) i=x i=y = refl
-fc00 zero (init sa) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
+fc00 zero zero refl (init sa) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
-... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero (init sa) cy i=x i=y )
+... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero zero refl (init sa) cy i=x i=y )
-fc00 zero (fsuc x cx) (init sa) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
+fc00 zero zero refl (fsuc x cx) (init sa) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
-... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero cx (init sa) i=x i=y )
+... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero zero refl cx (init sa) i=x i=y )
-fc00 zero (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
+fc00 zero zero refl (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
-... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero cx cy  i=x i=y )
+... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero zero refl cx cy  i=x i=y )
-fc00 (suc i) {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
+fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
-... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) cx cy  i=x i=y )
+... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) (suc j) i=j cx cy  i=x j=y )
-... | case1 x=fx | case2 y<fy = {!!}
+... | case1 x=fx | case2 y<fy = subst (λ k → k ≡ * (f y)) x=fx (fc02 x cx i=x) where
-... | case2 x<fx | case1 y=fy = {!!}
+fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) →  suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y)
-... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i cx cy (cong pred i=x) (cong pred i=y)))
+fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) )
+... | case1 eq = trans (sym eq) ( fc02  x1 cx1 i=x1 )
+... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where
+fc04 : * x1 ≡ * y
+fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y)
+... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ k ) y=fy (fc03 y cy j=y) where
+fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) →  suc j ≡ fcn s mf cy1 → * (f x)  ≡ * y1
+fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) )
+... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) eq
+... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where
+fc05 : * x ≡ * y1
+fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1)
+... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=y)))
 fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy  → * x < * y
 fcn-< {A} s {x} {y} {f} mf cx cy x<y = fc01 (fcn s mf cy) cx cy refl x<y where
 fc01 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → fcn s mf cx Data.Nat.< i → * x < * y
 fc03 :  suc i ≡ suc (fcn s mf cy) → i ≡ fcn s mf cy
 fc03 eq = cong pred eq
 fc02 :  * x < * y1
 fc02 =  fc01 i cx cy (fc03 i=y ) a
-fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) (imm : immieate-f A f )
+fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f)
 → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
-fcn-cmp {A} s {.s} {.s} f mf imm (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )
+fcn-cmp {A} s {x} {y} f mf cx cy with <-cmp ( fcn s mf cx ) (fcn s mf cy )
-fcn-cmp {A} s   f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) )
+... | tri< a ¬b ¬c = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where
-... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy )
+fc11 : * x < * y
-... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where
+fc11 = fcn-< {A} s {x} {y} {f} mf cx cy a
-lt : * s < * (f y)
+... | tri≈ ¬a b ¬c = tri≈ (λ lt → <-irr (case1 (sym fc10)) lt) fc10 (λ lt → <-irr (case1 fc10) lt) where
-lt with s≤fc  s f mf cy
+fc10 : * x ≡ * y
-... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y
+fc10 = fcn-inject {A} s {x} {y} {f} mf cx cy b
-... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y
+... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12  where
-fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc  s f mf cx
+fc12 : * y < * x
-... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt)
+fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c
-... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt)  (λ eq → <-irr (case1 eq) s<x  ) s<x
-fcn-cmp {A} s   f mf imm (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
+-- fcn-cmp {A} s {.s} {.s} f mf (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )
-... | case1 x=fx | case1 y=fy = {!!}
+-- fcn-cmp {A} s   f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) )
-... | case1 x=fx | case2 y<fy = {!!}
+-- ... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy )
-... | case2 x<fx | case1 y=fy = {!!}
+-- ... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where
-... | case2 x<fx | case2 y<fy = {!!} where
+--      lt : * s < * (f y)
-fc-mono : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → FClosure A f x y ∨ FClosure A f y x
+--      lt with s≤fc  s f mf cy
-fc-mono = {!!}
+--      ... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y
-fc1 :  Tri (* (f x) < * (f y)) (* (f x) ≡ * (f y)) (* (f y) < * (f x))
+--      ... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y
-fc1 with fcn-cmp s f mf imm cx cy
+-- fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc  s f mf cx
-... | tri< a ¬b ¬c = {!!}
+-- ... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt)
-... | tri≈ ¬a b ¬c = {!!}
+-- ... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt)  (λ eq → <-irr (case1 eq) s<x  ) s<x
-... | tri> ¬a ¬b c = {!!}
+-- fcn-cmp {A} s   f mf imm (fsuc x cx) (fsuc y cy) with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
+-- ... | case1 x=fx | case1 y=fy = {!!}
+-- ... | case1 x=fx | case2 y<fy = {!!}
+-- ... | case2 x<fx | case1 y=fy = {!!}
+-- ... | case2 x<fx | case2 y<fy = {!!} where
+--      fc-mono : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → FClosure A f x y ∨ FClosure A f y x
+--      fc-mono = {!!}
+--      fc1 :  Tri (* (f x) < * (f y)) (* (f x) ≡ * (f y)) (* (f y) < * (f x))
+--      fc1 with fcn-cmp s f mf imm cx cy
+--      ... | tri< a ¬b ¬c = {!!}
+--      ... | tri≈ ¬a b ¬c = {!!}
+--      ... | tri> ¬a ¬b c = {!!}
 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
 field
 y : Ordinal
 ay : odef B y

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

comparison src/zorn.agda @ 559:9ba98ecfbe62