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

changeset 1175:7d2bae0ff36b

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 Tue, 21 Feb 2023 12:02:41 +0900
parents 375615f9d60f
children ae586d6275c2
files src/OD.agda src/Topology.agda src/Tychonoff.agda src/cardinal.agda src/logic.agda src/partfunc.agda
diffstat 6 files changed, 203 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/OD.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/OD.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -8,6 +8,7 @@
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.Nat.Properties
 open import Data.Empty
+open import Data.Unit
 open import Relation.Nullary
 open import Relation.Binary  hiding (_⇔_)
 open import Relation.Binary.Core hiding (_⇔_)
@@ -79,7 +80,7 @@
 
 -- Ordinals in OD , the maximum
 Ords : OD
-Ords = record { def = λ x → One }
+Ords = record { def = λ x → Lift n ⊤ }
 
 record HOD : Set (suc n) where
   field
@@ -120,7 +121,7 @@
 
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
 ¬OD-order : ( & : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( & x ) → & x o< & y) → ⊥
-¬OD-order & * c<→o< = o≤> <-osuc (c<→o< {Ords} OneObj )
+¬OD-order & * c<→o< = o≤> <-osuc (c<→o< {Ords} (lift tt) )
 
 -- Ordinal in OD ( and ZFSet ) Transitive Set
 Ord : ( a : Ordinal  ) → HOD
--- a/src/Topology.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/Topology.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -447,7 +447,38 @@
             fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
 
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
-Compact→FIP = ?
+Compact→FIP {L} top fip with trio< (& L) o∅
+... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
+... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } 
+... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
+   -- set of coset of X
+   OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
+   OX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
+   OOX : {X : Ordinal} → (cs :  * X ⊆ CS top) → * (OX cs) ⊆ OS top
+   OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox
+   ... | record { z = z ; az = az ; x=ψz = x=ψz } =  subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01))  where
+       comp01 : odef (* X) (& (* z))
+       comp01 = subst (λ k → odef (* X) k) (sym &iso) az
+   --
+   --   if all finite intersection of (OX X) contains something, 
+   --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
+   --     it means there is a limit
+   --
+   Intersection : (X : Ordinal ) →  HOD
+   Intersection X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = ? ; <odmax = ? }
+   has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
+      →  ¬ (  Intersection X  =h= od∅ )
+   has-intersection {X} CX fip i=0 = ? where
+       no-cover : ¬ ( (* (OX CX)) covers L ) 
+       no-cover = ?
+   limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
+      → Ordinal
+   limit = ?
+   fip00 : {X : Ordinal} (CX : * X ⊆ CS top)
+            (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
+            {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip )
+   fip00 = ?
+
 
 open Filter
 
--- a/src/Tychonoff.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/Tychonoff.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Ordinals
 module Tychonoff {n : Level } (O : Ordinals {n})   where
--- a/src/cardinal.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/cardinal.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Level
 open import Ordinals
 module cardinal {n : Level } (O : Ordinals {n}) where
@@ -59,6 +61,9 @@
 FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace A ( λ x → < x , (* (Func.func (FuncHOD→F fc) (& x))) > )
 FuncHOD=R {A} {B}  (felm F) = *iso
 
+--
+--  Set of All function from A to B
+--
 Funcs : (A B : HOD) → HOD
 Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (A ⊗ B)) 
        ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (A ⊗ B)) ) &iso (⊆→o≤ (lemma1 px)) } where
--- a/src/logic.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/logic.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -5,17 +5,15 @@
 open import Relation.Binary hiding (_⇔_ )
 open import Data.Empty
 
-data One {n : Level } : Set n where
-  OneObj : One
+
+data Bool : Set where
+    true : Bool
+    false : Bool
 
 data Two : Set where
    i0 : Two
    i1 : Two
 
-data Bool : Set where
-   true : Bool
-   false : Bool
-
 record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
    constructor ⟪_,_⟫
    field
@@ -29,6 +27,13 @@
 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
+∧-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∧ B → B ∧ A
+∧-exch p = ⟪ _∧_.proj2 p , _∧_.proj1 p ⟫
+
+∨-exch : {n m : Level} {A  : Set n} { B : Set m } → A ∨ B → B ∨ A
+∨-exch (case1 x) = case2 x
+∨-exch (case2 x) = case1 x
+
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
 
@@ -42,6 +47,10 @@
 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
 
+de-morgan∨ : {n  : Level } {A B : Set n} →  A ∨ B  → ¬ ( (¬ A ) ∧ (¬ B ) )
+de-morgan∨ {n} {A} {B} (case1 a) and = ⊥-elim (  _∧_.proj1 and a )
+de-morgan∨ {n} {A} {B} (case2 b) and = ⊥-elim (  _∧_.proj2 and b )
+
 dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
 dont-or {A} {B} (case2 b) ¬A = b
@@ -50,6 +59,150 @@
 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
 dont-orb {A} {B} (case1 a) ¬B = a
 
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+open import Relation.Binary.PropositionalEquality
+
+not-not-bool : { b : Bool } → not (not b) ≡ b
+not-not-bool {true} = refl
+not-not-bool {false} = refl
+
+record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
+   field
+       fun←  :  S → R
+       fun→  :  R → S
+       fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
+       fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x
+
+injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
+injection R S f = (x y : R) → f x ≡ f y → x ≡ y
+
+
+¬t=f : (t : Bool ) → ¬ ( not t ≡ t) 
+¬t=f true ()
+¬t=f false ()
+
+infixr  130 _\/_
+infixr  140 _/\_
+
+≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
+≡-Bool-func {true} {true} a→b b→a = refl
+≡-Bool-func {false} {true} a→b b→a with b→a refl
+... | ()
+≡-Bool-func {true} {false} a→b b→a with a→b refl
+... | ()
+≡-Bool-func {false} {false} a→b b→a = refl
+
+bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
+bool-≡-? true true = yes refl
+bool-≡-? true false = no (λ ())
+bool-≡-? false true = no (λ ())
+bool-≡-? false false = yes refl
+
+¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
+¬-bool-t {true} ne = ⊥-elim ( ne refl )
+¬-bool-t {false} ne = refl
+
+¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
+¬-bool-f {true} ne = refl
+¬-bool-f {false} ne = ⊥-elim ( ne refl )
+
+¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
+¬-bool refl ()
+
+lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
+lemma-∧-0 {true} {true} refl ()
+lemma-∧-0 {true} {false} ()
+lemma-∧-0 {false} {true} ()
+lemma-∧-0 {false} {false} ()
+
+lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
+lemma-∧-1 {true} {true} refl ()
+lemma-∧-1 {true} {false} ()
+lemma-∧-1 {false} {true} ()
+lemma-∧-1 {false} {false} ()
+
+bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
+bool-and-tt refl refl = refl
+
+bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
+bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {false} {_} ()
+
+bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
+bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {false} ()
+bool-∧→tt-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
+bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
+bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
+bool-or-41 {true} {b} refl = refl
+
+bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+
+open import Data.Nat
+open import Data.Nat.Properties
+
+_≥b_ : ( x y : ℕ) → Bool
+x ≥b y with <-cmp x y
+... | tri< a ¬b ¬c = false
+... | tri≈ ¬a b ¬c = true
+... | tri> ¬a ¬b c = true
+
+_>b_ : ( x y : ℕ) → Bool
+x >b y with <-cmp x y
+... | tri< a ¬b ¬c = false
+... | tri≈ ¬a b ¬c = false
+... | tri> ¬a ¬b c = true
+
+_≤b_ : ( x y : ℕ) → Bool
+x ≤b y  = y ≥b x
+
+_<b_ : ( x y : ℕ) → Bool
+x <b y  = y >b x
+
 open import Relation.Binary.PropositionalEquality
 
 ¬i0≡i1 : ¬ ( i0 ≡ i1 )
@@ -63,8 +216,3 @@
 ¬i1→i0 {i0} ne = refl
 ¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
 
-
-infixr  130 _∧_
-infixr  140 _∨_
-infixr  150 _⇔_
-
--- a/src/partfunc.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/partfunc.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -8,6 +8,7 @@
 open import logic
 open import Relation.Binary 
 open import Data.Empty 
+open import Data.Unit using ( ⊤ ; tt )
 open import Data.List hiding (filter)
 open import Data.Maybe  
 open import Relation.Binary
@@ -218,10 +219,10 @@
        dense-p :  { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) 
 
 
-Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_
+Dense-3 : F-Dense (List (Maybe Two) ) (λ x → ⊤ ) _3⊆_ _3∩_
 Dense-3 = record {
        dense =  λ x → Finite3b x ≡ true
-    ;  d⊆P = OneObj
+    ;  d⊆P = tt
     ;  dense-f = λ x → finite3cov x
     ;  dense-d = λ {p} d → lemma1 p
     ;  dense-p = λ {p} d → lemma2 p