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

changeset 693:a3b7f1e0ca60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
same problem again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 Jul 2022 11:49:11 +0900
parents 38103b4e6780
children 196eff771492
files src/Ordinals.agda src/ordinal.agda src/zorn.agda
diffstat 3 files changed, 42 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/src/Ordinals.agda	Mon Jul 11 05:50:49 2022 +0900
+++ b/src/Ordinals.agda	Mon Jul 11 11:49:11 2022 +0900
@@ -26,7 +26,7 @@
      <-osuc   : { x : ord  } → x o< osuc x
      osuc-≡<  : { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      Oprev-p  : ( x : ord  ) → Dec ( Oprev ord osuc x )
-     o<-irr   : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1
+     o<-irr   : { x y : ord } → ( lt lt1 : x o< y ) → lt ≡ lt1
      TransFinite : { ψ : ord  → Set (suc n) }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
--- a/src/ordinal.agda	Mon Jul 11 05:50:49 2022 +0900
+++ b/src/ordinal.agda	Mon Jul 11 11:49:11 2022 +0900
@@ -200,12 +200,12 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
-OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ )
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
-OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
-OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl
-OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
+OrdIrr : {n : Level } {x y : Ordinal {suc n} } (lt lt1 : x o< y) → lt ≡ lt1
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case1 x₁) = cong case1 (NP.<-irrelevant _ _ )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case2 x₁) = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case2 x) (case1 x₁) = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
+OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} (case2 Φ<) (case2 Φ<) = refl
+OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} (case2 (s< x)) (case2 (s< x₁)) = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
       lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
       lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl
       lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y )
--- a/src/zorn.agda	Mon Jul 11 05:50:49 2022 +0900
+++ b/src/zorn.agda	Mon Jul 11 11:49:11 2022 +0900
@@ -278,7 +278,7 @@
       psup :  Ordinal → Ordinal 
       p≤z : (x : Ordinal ) →   odef A (psup x)
       chainf : (x : Ordinal) → HOD
-      is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x) w → Chain A f mf ay chainf (psup x) w 
+      is-chain : {x w : Ordinal} → odef (chainf x) w → Chain A f mf ay chainf (psup x) w 
 
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  
           (zc0 : (x : Ordinal) →  ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where
@@ -307,9 +307,9 @@
 --
 -- data Chain is total
 
-chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {x y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD)
+chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD)
    {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {x} {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
+chain-total A f mf {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
      ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
@@ -483,7 +483,7 @@
           pchain  = chainf sc px 
 
           no-ext :  ZChain1 A f mf ay x
-          no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 }  where
+          no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = ? }  where
             psup1 : Ordinal → Ordinal
             psup1 z with o≤? z x
             ... | yes _ = ZChain1.psup sc z
@@ -517,15 +517,40 @@
           UZ : HOD
           UZ = UnionCF A x pchainf
           chainf0 : (z : Ordinal ) → HOD
-          chainf0 z with o≤? x z
-          ... | yes _  = UZ
-          ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z
+          chainf0 z with trio< z x
+          ... | tri< a ¬b ¬c = ZChain1.chainf (pzc z a) z
+          ... | tri≈ ¬a b ¬c = UZ
+          ... | tri> ¬a ¬b c = UZ
+          Chain-ext : {s a : Ordinal}  → (ca : odef UZ a)
+             → Chain A f mf ay ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca)))) s a → Chain A f mf ay chainf0 s a 
+          Chain-ext {s} {a} ca (ch-init a x) = ch-init a x
+          Chain-ext {s} {a} ca (ch-is-sup is-sup fc) = ch-is-sup sc5 fc where
+              sc7 : odef ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca))) s ) a
+              sc7 = ChainP.csupz is-sup
+              sc8  : (z<x : s o< x ) → chainf0 s ≡ ( ZChain1.chainf (pzc _ z<x )) s
+              sc8  z<x with  trio< s x
+              ... | tri≈ ¬a b ¬c = ?
+              ... | tri> ¬a ¬b c = ?
+              ... | tri< a ¬b ¬c with o<-irr a z<x 
+              ... | refl = refl 
+              sc6 : odef (chainf0 s) a
+              sc6 with trio< s x 
+              ... | tri≈ ¬a b ¬c = ?
+              ... | tri> ¬a ¬b c = ?
+              ... | tri< a' ¬b ¬c with o<-irr a' ? -- (UChain.u<x (proj2 ca))
+              ... | eq = ? -- ChainP.csupz is-sup 
+              sc5 : ChainP A f mf ay chainf0 s a
+              sc5 = record {
+                  asup = ChainP.asup is-sup
+                ; fcy<sup = ChainP.fcy<sup is-sup
+                ; csupz = sc6
+                ; order = ? }
           total-UZ : IsTotalOrderSet UZ
           total-UZ {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay chainf0 {!!} {!!}
-                   -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _  (UChain.chain∋z (proj2 ca))) 
-                   -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _  (UChain.chain∋z (proj2 cb)))
+               uz01 = chain-total A f mf ay chainf0  
+                   (Chain-ext ca (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) (UChain.chain∋z (proj2 ca)))) 
+                   (Chain-ext cb (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) (UChain.chain∋z (proj2 cb)))) 
           usup : SUP A UZ
           usup = supP UZ (λ lt → proj1 lt) total-UZ 
           spu = & (SUP.sup usup)