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

changeset 1438:5d69ed581269

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add comments
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Jul 2023 20:36:08 +0900
parents 6cac0f746c83
children 900c98ffde05
files src/bijection.agda src/cardinal.agda src/filter-util.agda
diffstat 3 files changed, 37 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jul 02 15:05:26 2023 +0900
+++ b/src/bijection.agda	Sun Jul 02 20:36:08 2023 +0900
@@ -724,6 +724,9 @@
     lem02 : (n : ℕ) → maxAC n
     lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) }
 
+    --
+    -- countB record create ℕ → B and its injection
+    --
     record CountB (n : ℕ) : Set where
        field
           b : B
@@ -845,6 +848,9 @@
            open ≡-Reasoning
            CB  = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )
 
+    --
+    -- uniqueness of ntob is proved by injection
+    --
     biso1 : (b : B) → ntob (bton b) ≡ b
     biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) 
     ... | zero  | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where
@@ -982,6 +988,7 @@
 --        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
+--    someday ...
 
 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ℕ))  
--- a/src/cardinal.agda	Sun Jul 02 15:05:26 2023 +0900
+++ b/src/cardinal.agda	Sun Jul 02 20:36:08 2023 +0900
@@ -64,11 +64,14 @@
 open Injection
 open HODBijection
 
-record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
+record IsImage0 (a b : HOD) (f : (x : Ordinal) → odef a x → Ordinal) (x : Ordinal ) : Set n where
    field
       y : Ordinal 
-      ay : odef (* a) y
-      x=fy : x ≡ i→ iab _ ay
+      ay : odef a y
+      x=fy : x ≡ f y ay
+
+IsImage : (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) → Set n 
+IsImage a b iab x = IsImage0 (* a) (* b) (i→ iab) x
 
 Image : (a : Ordinal) { b : Ordinal } → Injection a b → HOD
 Image a {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00  } where
@@ -76,12 +79,6 @@
     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)) )
 
-record IsImage0 (a b : HOD) (f : (x : Ordinal) → odef a x → Ordinal) (x : Ordinal ) : Set n where
-   field
-      y : Ordinal 
-      ay : odef a y
-      x=fy : x ≡ f y ay
-
 Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a 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)
 
@@ -111,6 +108,10 @@
 Injection-∙ {a} {b} {c} f g = record { i→ = λ x ax → i→ g (i→ f x ax) (iB f x ax) ; iB = λ x ax → iB g (i→ f x ax) (iB f x ax)
         ; inject = λ x y ix iy eq → inject f x y ix iy (inject g (i→ f x ix) (i→ f y iy) (iB f x ix) (iB f y iy) eq)   } 
 
+--
+-- Two injection can be joined
+--   A and C may overrap
+--
 bi-∪  : {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D )  
        → HODBijection (A ∪ C) (B ∪ D)
 bi-∪  {A} {B} {C} {D} ab cd = record { 
@@ -148,9 +149,12 @@
       gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) 
          ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } 
 
+      --
+      -- HOD UC is closure of g ∙ f starting from a - Image g
+      --
       data gfImage :  (x : Ordinal) → Set n where
           a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage  x
-          next-gf : {x : Ordinal} → (ix : IsImage a a gf x) → (gfiy : gfImage (IsImage.y ix) ) → gfImage  x
+          next-gf : {x : Ordinal} → (ix : IsImage a a gf x) → (gfiy : gfImage (IsImage0.y ix) ) → gfImage  x
 
       a∋gfImage : {x : Ordinal } → gfImage x → odef (* a) x
       a∋gfImage {x} (a-g ax ¬ib) = ax
@@ -224,7 +228,6 @@
       g⁻¹-eq {x} ax ax' {record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ }} {record { y = y ; ay = ay ; x=fy = x=fy }} 
            = inject g _ _ ay₁ ay (trans (sym x=fy₁) x=fy )
 
-
       cc11-case2 : {x : Ordinal} (ax : odef (* a) x) 
           → (ncn : ¬ gfImage x) 
           → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax))  (g⁻¹ ax (nimg ax ncn))
@@ -250,7 +253,6 @@
       Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal
       Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = y
 
-
       UC∋Uf1 : {x : Ordinal } → (lt : odef fUC x) → odef UC (Uf1 x lt )
       UC∋Uf1 {x} record { y = y ; ay = ay ; x=fy = x=fy } = ay
 
@@ -262,6 +264,13 @@
       fU-iso0 {x} (a-g ax ¬ib) = refl 
       fU-iso0 {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt) = refl
 
+      --
+      -- We cannot directly create h : * a → * b , because the cnoise of UC ∨  a-UC is non constructive and
+      -- even LEM cannot be used in positive context. The merging bi-UC and  bi-fUC uses also LEM but use it positively.
+      --
+      -- bijection on each side is easy, because these are images of f and g.
+      --    somehow we don't use injection of f.
+
       bi-UC : HODBijection UC fUC
       bi-UC = record { 
          fun←  = λ x lt → fU1 x lt
@@ -309,11 +318,11 @@
        ciso : HODBijection (* a) (* card)
        cmax : (x : Ordinal) → card o< x → ¬ HODBijection (* a) (* x)
 
-Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t
-Cardinal∈ = {!!}
+-- Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t
+-- Cardinal∈ = {!!}
 
-Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t )
-Cardinal⊆ = {!!}
+-- Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t )
+-- Cardinal⊆ = {!!}
 
 Cantor1 : { u : HOD } → u c< Power u
 Cantor1 = {!!}
--- a/src/filter-util.agda	Sun Jul 02 15:05:26 2023 +0900
+++ b/src/filter-util.agda	Sun Jul 02 20:36:08 2023 +0900
@@ -143,6 +143,11 @@
 rcq :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) Q (λ x fx → ZP-proj2 P Q x (filter-⊆ F fx))
 rcq {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP2.bb ly }
 
+--
+-- Proj2 can be dervie from symmetry of ZFP (Product)
+-- but it makes Agda very slow
+--   so we copy Proj1
+--
 Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
       →    Filter {Power Q} {Q} (λ x → x)