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

changeset 1473:aca42b19db4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 23 Jun 2024 07:04:50 +0900
parents d0b4be1cab0d
children 893954e484a4
files src/ZProduct.agda src/cardinal.agda
diffstat 2 files changed, 47 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/ZProduct.agda	Sat Jun 22 19:23:56 2024 +0900
+++ b/src/ZProduct.agda	Sun Jun 23 07:04:50 2024 +0900
@@ -427,6 +427,8 @@
        i→  : (x : Ordinal ) → Ordinal
        iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x  )
        inject : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ≡ i→ y → x ≡ y
+       -- 
+       -- no i→-cong : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → x ≡ y → i→ x ≡ i→ y
 
 record HODBijection (A B : HOD ) : Set n where
    field
@@ -436,6 +438,9 @@
        funA  : (x : Ordinal ) → ( lt : odef B  x ) → odef A ( fun← x lt )
        fiso← : (x : Ordinal ) → ( lt : odef A  x ) → fun← ( fun→ x lt ) ( funB x lt ) ≡ x
        fiso→ : (x : Ordinal ) → ( lt : odef B  x ) → fun→ ( fun← x lt ) ( funA x lt ) ≡ x
+       fcong→ : (x y : Ordinal ) → ( ltx : odef A  x ) ( lty : odef A  y )  →  x ≡ y → fun→ x ltx ≡ fun→ y lty
+       fcong← : (x y : Ordinal ) → ( ltx : odef B  x ) ( lty : odef B  y )  →  x ≡ y → fun← x ltx ≡ fun← y lty
+
 
 hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b
 hodbij-refl {a} refl = record {
@@ -445,6 +450,8 @@
      ; funA  = λ x lt → lt
      ; fiso← = λ x lt → refl
      ; fiso→ = λ x lt → refl
+     ; fcong→ = λ x y ltx lty eq → eq
+     ; fcong← = λ x y ltx lty eq → eq
     }
 
 hodbij-sym : { a b : HOD } → HODBijection a b → HODBijection b a
@@ -455,6 +462,8 @@
      ; funA  = funB eq
      ; fiso← = fiso→  eq
      ; fiso→ = fiso←  eq
+     ; fcong→ = fcong← eq 
+     ; fcong← = fcong→ eq
     } where open HODBijection
 
 pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) →
--- a/src/cardinal.agda	Sat Jun 22 19:23:56 2024 +0900
+++ b/src/cardinal.agda	Sun Jun 23 07:04:50 2024 +0900
@@ -116,25 +116,30 @@
 Injection-∙ {a} {b} {c} f g = record { i→ = λ x  → i→ g (i→ f x ) ; iB = λ x ax → iB g (i→ f x ) (iB f x ax) 
            ; inject = λ x y ix iy eq → inject f _ _ ix iy (inject g _ _ (iB f x ix ) (iB f y iy ) eq ) }
 
+WellDefined : {A : HOD} → (f : (x : Ordinal ) → odef A x → Ordinal ) → Set n
+WellDefined {A} f = (x : Ordinal ) → ( lt1 lt2 : odef A  x ) → f x lt1 ≡ f x lt2 
+
 ==-bi : {A B C : HOD } → (ab : HODBijection A B) 
-    → ( (x : Ordinal ) → ( lt1 lt2 : odef A  x ) → fun→ ab x lt1 ≡ fun→ ab x lt2 )
-    → ( (x : Ordinal ) → ( lt1 lt2 : odef B  x ) → fun← ab x lt1 ≡ fun← ab x lt2 )
     → (A =h= C → HODBijection C B) ∧ (B =h= C → HODBijection A C) 
-proj1 (==-bi {A} {B} {C} ab wld→ wld← ) a=c = record {
+proj1 (==-bi {A} {B} {C} ab ) a=c = record {
          fun→  = λ x cx → fun→ ab x (eq← a=c cx)
-       ; fun←  = λ x bx → fun← ab x bx
+       ; fun←  = fun← ab 
        ; funB  = λ x cx → funB ab x (eq← a=c cx)
        ; funA  = λ x cx → eq→ a=c (funA ab x cx)
-       ; fiso→ = λ x bx → trans (wld→ _ _ _) (fiso→ ab x bx)
+       ; fiso→ = λ x bx → trans (fcong→ ab _ _ _ _  refl ) (fiso→ ab x bx )
        ; fiso← = λ x cx → fiso← ab x (eq← a=c cx)
+       ; fcong→ = λ x y cx cy eq → fcong→ ab x y (eq← a=c cx) (eq← a=c cy) eq
+       ; fcong← = fcong← ab 
        } 
-proj2 (==-bi {A} {B} {C} ab wld→ wld←) b=c = record {
+proj2 (==-bi {A} {B} {C} ab ) b=c = record {
          fun→  = λ x cx → fun→ ab x cx
        ; fun←  = λ x bx → fun← ab x (eq← b=c bx)
        ; funB  = λ x cx → eq→  b=c (funB ab x cx)
        ; funA  = λ x cx → funA ab x (eq← b=c cx)
        ; fiso→ = λ x cx → fiso→ ab x (eq← b=c cx)
-       ; fiso← = λ x bx → trans (wld← _ _ _) (fiso← ab x bx)
+       ; fiso← = λ x bx → trans (fcong← ab _ _ _ _  refl ) (fiso← ab x bx )
+       ; fcong→ = fcong→ ab
+       ; fcong← = λ x y cx cy eq → fcong← ab x y (eq← b=c cx) (eq← b=c cy) eq
        }    
 
 --
@@ -142,14 +147,17 @@
 --   A and C may overrap
 --
 bi-∪  : {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D )  
+       → ((A ∩ C) =h= od∅) → ((B ∩ D) =h= od∅)
        → HODBijection (A ∪ C) (B ∪ D)
-bi-∪  {A} {B} {C} {D} ab cd = record { 
+bi-∪  {A} {B} {C} {D} ab cd nac nbd = record { 
          fun→  = fa
        ; fun←  = fb
        ; funB  = fa-isb
        ; funA  = fb-isa
        ; fiso→ = faiso
        ; fiso← = fbiso
+       ; fcong→ = facong
+       ; fcong← = fbcong
        } where
           fa : (x : Ordinal) → odef (A ∪ C) x → Ordinal
           fa x (case1 a) = fun→ ab x a
@@ -169,6 +177,17 @@
           fbiso : (x : Ordinal) (lt : odef (A ∪ C) x) → fb (fa x lt) (fa-isb x lt) ≡ x
           fbiso x (case1 b) = fiso← ab x b
           fbiso x (case2 d) = fiso← cd x d
+          -- without fcong, we don't need nac and nbd
+          facong : (x y : Ordinal) (ltx : odef (A ∪ C) x) (lty : odef (A ∪ C) y) → x ≡ y → fa x ltx ≡ fa y lty
+          facong x .x (case1 x₁) (case1 x₂) refl = fcong→ ab x x x₁ x₂ refl
+          facong x .x (case1 x₁) (case2 x₂) refl = ⊥-elim (¬x<0 (eq→  nac ⟪ x₁ , x₂ ⟫))
+          facong x .x (case2 x₁) (case1 x₂) refl = ⊥-elim (¬x<0 (eq→  nac ⟪ x₂ , x₁ ⟫))
+          facong x .x (case2 x₁) (case2 x₂) refl = fcong→ cd x x x₁ x₂ refl
+          fbcong : (x y : Ordinal) (ltx : odef (B ∪ D) x) (lty : odef (B ∪ D) y) → x ≡ y → fb x ltx ≡ fb y lty
+          fbcong x .x (case1 x₁) (case1 x₂) refl = fcong← ab x x x₁ x₂ refl
+          fbcong x .x (case1 x₁) (case2 x₂) refl = ⊥-elim (¬x<0 (eq→  nbd ⟪ x₁ , x₂ ⟫))
+          fbcong x .x (case2 x₁) (case1 x₂) refl = ⊥-elim (¬x<0 (eq→  nbd ⟪ x₂ , x₁ ⟫))
+          fbcong x .x (case2 x₁) (case2 x₂) refl = fcong← cd x x x₁ x₂ refl
 
 --
 --  f : A → B        OrdBijection A           (Image A f)
@@ -180,7 +199,7 @@
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* a) (* b)
 Bernstein {a} {b} ( fi @ record { i→ = f ; iB = b∋f ; inject = f-inject }) 
                   ( gi @ record { i→ = g ; iB = a∋g ; inject = g-inject })
-     = proj1 (==-bi (proj2 (==-bi (bi-∪  bi-UC  bi-fUC) ? ? ) (==-sym b=fUC∨b-fUC)) ? ? ) (==-sym a=UC∨a-UC) 
+     = proj1 (==-bi (proj2 (==-bi (bi-∪  bi-UC  bi-fUC ? ? ) ) (==-sym b=fUC∨b-fUC)) ) (==-sym a=UC∨a-UC) 
  where
       gf : Injection a a
       gf = record { i→ = λ x → g (f x ) ; iB = λ x ax → a∋g _ (b∋f x ax) 
@@ -230,8 +249,13 @@
            be01 {x} (case1 gfx) = a∋gfImage gfx
            be01 {x} (case2 ngfx) = proj1 ngfx
 
-      wld-a : (x : Ordinal) (lt1 lt2 : odef (UC ∪ a-UC) x) → ? -- fa bi-UC bi-fUC x lt1 ≡ fa bi-UC bi-fUC x lt2
-      wld-a = ?
+      exUC : (UC ∩ a-UC) =h= od∅
+      exUC = record { eq→ = be00 ; eq← = be01 } where
+           be00 : {x : Ordinal} → odef (UC ∩ a-UC) x → odef od∅ x
+           be00 {x} ⟪ a-g ax₁ ¬ib , ⟪ ax , nuc ⟫ ⟫ = ?
+           be00 {x} ⟪ next-gf ix uc , ⟪ ax , nuc ⟫ ⟫ = ?
+           be01 : {x : Ordinal} → odef od∅ x → odef (UC ∩ a-UC) x
+           be01 {x} lt = ⊥-elim ( ¬x<0 lt )
 
       FA : (x : Ordinal) → (ax : gfImage x) → Ordinal
       FA x ax = f x -- (a∋gfImage ax)
@@ -261,10 +285,10 @@
       ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) )
 
       f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → f x ≡ f y 
-      f-cong {x} {x} {ax} {ax1} refl = ? -- cong (λ k → f x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
+      f-cong {x} {x} {ax} {ax1} refl = refl 
 
       g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → g x ≡ g y 
-      g-cong {x} {x} {bx} {bx1} refl = ? -- cong (λ k → g x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
+      g-cong {x} {x} {bx} {bx1} refl = refl 
 
       g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → Ordinal
       g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = y
@@ -406,7 +430,7 @@
      f2 = f
      -- postulate   -- yes we have a proof but it is very slow
      b : HODBijection (Power S) S 
-     b = subst₂ (λ j k → HODBijection j k) ? ? ( Bernstein f2 f1)   -- this makes check very slow
+     b = ? -- subst₂ (λ j k → HODBijection j k) ? ? ( Bernstein f2 f1)   -- this makes check very slow
      --      but postulate makes check weak eg. irrerevance of ∋ 
 
      -- we have at least one element since Power S contains od∅