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

changeset 1387:003424a36fed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is this agda's bug?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 25 Jun 2023 15:58:16 +0900
parents 0afcd5b99548
children 2e53a8e6fa5f
files README.md src/bijection.agda src/cardinal.agda
diffstat 3 files changed, 94 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/README.md	Sat Jun 24 08:56:47 2023 +0900
+++ b/README.md	Sun Jun 25 15:58:16 2023 +0900
@@ -39,6 +39,8 @@
 
 [OPair](https://shinji-kono.github.io/zf-in-agda/html/OPair.html)   Orderd Pair and Direct Product
 
+[bijection](https://shinji-kono.github.io/zf-in-agda/html/bijection.html)   Bijection without HOD
+
 
 ```
 
--- a/src/bijection.agda	Sat Jun 24 08:56:47 2023 +0900
+++ b/src/bijection.agda	Sun Jun 25 15:58:16 2023 +0900
@@ -970,3 +970,33 @@
             lem01 with cong proj2 eq
             ... | refl = refl
 
+--
+--  (     Bool ∷      Bool ∷ [] )    (      Bool ∷      Bool ∷ []   )  (      Bool ∷ [] )
+--        true ∷      true ∷ false ∷        true ∷      true ∷ false ∷        true ∷ []
+
+-- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln)  fi gi dec0 dec1 where
+
+LBBℕ : Bijection (List (List Bool)) ℕ
+LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ))  
+        ? ? ? ? where
+
+    atob : List (List Bool) →  List Bool ∧ List Bool 
+    atob [] = ⟪ [] , [] ⟫
+    atob ( [] ∷  t ) = ⟪ false  ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫
+    atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true  ∷ proj2 ( atob t ) ⟫
+
+    btoa : List Bool ∧ List Bool → List (List Bool) 
+    btoa ⟪ [] , _ ⟫ = []
+    btoa ⟪ _ ∷ _  , [] ⟫ = []
+    btoa ⟪ _ ∷ t0 ,  false ∷ t1  ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ 
+    btoa ⟪ h ∷ t0 ,  true  ∷ t1  ⟫ with btoa ⟪ t0 , t1 ⟫
+    ... | [] = ( h ∷ [] ) ∷ []
+    ... | x ∷ y = (h ∷ x ) ∷ y
+
+Lℕ=ℕ : Bijection (List ℕ) ℕ
+Lℕ=ℕ = record {
+       fun→  = λ x → ?
+     ; fun←  = λ n → ?
+     ; fiso→ = ?
+     ; fiso← = ?
+     }
--- a/src/cardinal.agda	Sat Jun 24 08:56:47 2023 +0900
+++ b/src/cardinal.agda	Sun Jun 25 15:58:16 2023 +0900
@@ -1,6 +1,6 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 
-open import Level
+open import Level hiding (suc ; zero )
 open import Ordinals
 module cardinal {n : Level } (O : Ordinals {n}) where
 
@@ -9,7 +9,7 @@
 import OD hiding ( _⊆_ )
 
 import ODC
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
+open import Data.Nat 
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties
 open import Data.Empty
@@ -66,14 +66,18 @@
 
 record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
    field
-      ax : odef (* a) x
-      bx : odef (* b) (i→ iab _ ax)
+      y : Ordinal 
+      ay : odef (* a) y
+      x=fy : x ≡ i→ iab _ ay
 
 Image : { a b : Ordinal } → Injection a b → HOD
-Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = a ; <odmax = λ lt → ?  }
+Image {a} {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00  } where
+    im00 : {x : Ordinal } → IsImage a b iab x → x o< b
+    im00 {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ ( λ j k → j o< k) (trans &iso (sym x=fy)) &iso 
+         (c<→o< (subst ( λ k → odef (* b) k) (sym &iso) (iB iab y ay)) )
 
-image=a : ?
-image=a = ?
+Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image iab ⊆ * b 
+Image⊆b {a} {b} iab {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k) (sym x=fy) (iB iab y ay)
 
 _=c=_ : ( A B : HOD ) → Set n
 A =c= B = OrdBijection ( & A ) ( & B )
@@ -90,28 +94,67 @@
 a - b = & ( (* a) ＼ (* b) )
 
 -→<  : (a b : Ordinal ) → (a - b) o≤ a
--→< a b = ?
+-→< a b = subst₂ (λ j k → j o≤ k) &iso &iso ( ⊆→o≤ ( λ {x} a-b → proj1 (subst ( λ k → odef k x) *iso a-b) ) )
+
+b-a⊆b : {a b x : Ordinal } → odef (* (b - a)) x → odef (* b) x
+b-a⊆b {a} {b} {x} lt with subst (λ k → odef k x) *iso lt
+... | ⟪ bx , ¬ax ⟫ = bx
+
+open Data.Nat
 
 Bernstein1 : {a b : Ordinal } → a o< b → Injection a b ∧  Injection b a → Injection (b - a) b ∧  Injection b (b - a) 
-Bernstein1 = ?
+Bernstein1 {a} {b} a<b ⟪ f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject } , g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject } ⟫ 
+    = ⟪ record { i→ = f0 ; iB = b∋f0 ; inject = f0-inject } , record { i→ = f1 ; iB = b∋f1 ; inject = f1-inject } ⟫ where
+
+      C : ℕ → HOD
+      gf : (i : ℕ) → Injection (& (C i)) a
+      gf 0 = record { i→ = λ x cx  → fba x ?  ; iB = ? ; inject = ? }
+      gf (suc i) = record { i→ = be00 ; iB = ? ; inject = ? } where 
+          be00 : (x : Ordinal) → odef (* (& (C (suc i)))) x → Ordinal
+          be00 x lt with subst (λ k → odef k x) *iso lt | inspect C (suc i)
+          ... | t | record { eq = eq1 }  = ?
+      C 0 = (* a) ＼ Image g
+      C (suc i) = Image {& (C i)} {a} (gf i) 
+
+      record CN (x : Ordinal) : Set n where
+          field 
+             i : ℕ
+             cn=x : & (C i) ≡ x
+
+      UC : HOD
+      UC = record { od = record { def = λ x → CN x } ; odmax = a ; <odmax = ? }
+
+      -- Injection (b - a) b 
+      f0 : (x : Ordinal) → odef (* (b - a)) x → Ordinal
+      f0 x lt with subst (λ k → odef k x) *iso lt
+      ... | ⟪ bx , ¬ax ⟫ = fab (fba x bx) (a∋fba x bx)
+      b∋f0 : (x : Ordinal) (lt : odef (* (b - a)) x) → odef (* b) (f0 x lt)
+      b∋f0 x lt with subst (λ k → odef k x) *iso lt
+      ... | ⟪ bx , ¬ax ⟫ = b∋fab (fba x bx) (a∋fba x bx)
+      f0-inject : (x y : Ordinal) (ltx : odef (* (b - a)) x) (lty : odef (* (b - a)) y) → f0 x ltx ≡ f0 y lty → x ≡ y
+      f0-inject x y ltx lty eq = fba-inject _ _ (b-a⊆b ltx) (b-a⊆b lty) ( fab-inject _ _ (a∋fba x  (b-a⊆b ltx)) (a∋fba y (b-a⊆b lty)) eq )
+
+      -- Injection b (b - a) 
+      f1 : (x : Ordinal) → odef (* b) x → Ordinal
+      f1 x lt = ?
+      b∋f1 : (x : Ordinal) (lt : odef (* b) x) → odef (* (b - a)) (f1 x lt)
+      b∋f1 x lt = ?
+      f1-inject : (x y : Ordinal) (ltx : odef (* b) x) (lty : odef (* b) y) → f1 x ltx ≡ f1 y lty → x ≡ y
+      f1-inject x y ltx lty eq = ?
 
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
 Bernstein {a} {b} iab iba = be00 where
-    a⊆b : * a ⊆ * b
-    a⊆b {x} ax = subst (λ k → odef (* b) k) be01 ( iB iab _ ax ) where
-        be01 : i→ iab x ax ≡ x
-        be01 = ?
-        be02 : x ≡  i→ iba x ?
-        be02 = inject iab ? ? ax ( iB iba _ ? ) ? 
-    b⊆a : * b ⊆ * a
-    b⊆a bx = ?
     be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥ 
     be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥  } 
           ind a b a<b iab iba where
        ind :(x : Ordinal) →
             ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) →
             (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ 
-       ind x prev b x<b ixb ibx = ?
+       ind x prev b x<b ixb ibx = prev _ be01 _ be02 (proj1 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) (proj2 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) where
+           be01 : (b - x) o< x
+           be01 = ?
+           be02 : (b - x) o< b
+           be02 = ?
     be00 : OrdBijection a b
     be00 with trio< a b
     ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )
@@ -124,7 +167,7 @@
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection a x }
 
-record Cardinal (a : Ordinal ) : Set (suc n) where
+record Cardinal (a : Ordinal ) : Set (Level.suc n) where
    field
        card : Ordinal
        ciso : OrdBijection a card