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

changeset 1465:bd2b003e25ef

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 Fri, 05 Jan 2024 13:50:21 +0900
parents 484f83b04b5d
children e8c166541c86
files src/BAlgebra.agda
diffstat 1 files changed, 61 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgebra.agda	Wed Jan 03 19:29:23 2024 +0900
+++ b/src/BAlgebra.agda	Fri Jan 05 13:50:21 2024 +0900
@@ -30,8 +30,8 @@
 
 -- Ordinal Definable Set
 
-open HODBase.HOD 
-open HODBase.OD 
+open HODBase.HOD
+open HODBase.OD
 
 open _∧_
 open _∨_
@@ -39,7 +39,7 @@
 
 open  HODBase._==_
 
-open HODBase.ODAxiom HODAxiom  
+open HODBase.ODAxiom HODAxiom
 open OD O HODAxiom
 open AxiomOfChoice AC
 
@@ -47,7 +47,7 @@
 open _∨_
 open Bool
 
-L＼L=0 : { L  : HOD  } → (L ＼ L) =h= od∅ 
+L＼L=0 : { L  : HOD  } → (L ＼ L) =h= od∅
 L＼L=0 {L} = record { eq→ = lem0 ; eq← =  lem1 }  where
     lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
     lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx)
@@ -56,16 +56,16 @@
 
 L＼Lx=x : { L x : HOD  } → x ⊆ L   → (L ＼ ( L ＼ x )) =h= x
 L＼Lx=x {L} {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 }  where
-    lem03 :  {z : Ordinal} → odef (L ＼ (L ＼ x)) z → odef x z 
+    lem03 :  {z : Ordinal} → odef (L ＼ (L ＼ x)) z → odef x z
     lem03 {z} ⟪ Lz , Lxz ⟫ with ODC.∋-p O HODAxiom AC  x (* z)
-    ... | yes y = subst (λ k → odef x k ) &iso y 
+    ... | yes y = subst (λ k → odef x k ) &iso y
     ... | no n = ⊥-elim ( Lxz ⟪ Lz , ( subst (λ k → ¬ odef x k ) &iso n ) ⟫ )
-    lem04 :  {z : Ordinal} → odef x z → odef (L ＼ (L ＼ x)) z 
+    lem04 :  {z : Ordinal} → odef x z → odef (L ＼ (L ＼ x)) z
     lem04 {z} xz with ODC.∋-p O HODAxiom AC L (* z)
     ... | yes y = ⟪ subst (λ k → odef L k ) &iso y  , ( λ p → proj2 p xz )  ⟫
     ... | no  n = ⊥-elim ( n (subst (λ k → odef L k ) (sym &iso) ( x⊆L xz) ))
-     
-L＼0=L : { L  : HOD  } → (L ＼ od∅) =h= L 
+
+L＼0=L : { L  : HOD  } → (L ＼ od∅) =h= L
 L＼0=L {L} = record { eq→ = lem05 ; eq← = lem06 }  where
     lem05 : {x : Ordinal} → odef (L ＼ od∅) x → odef L x
     lem05 {x} ⟪ Lx , _ ⟫ = Lx
@@ -77,7 +77,7 @@
 ... | yes y = case1 ( subst (λ k → odef X k ) &iso y  )
 ... | no  n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫
 
-＼-⊆ : { P A B : HOD } →  A ⊆ P → ( A ⊆ B → ( P ＼ B ) ⊆ ( P ＼ A )) ∧ (( P ＼ B ) ⊆ ( P ＼ A ) → A ⊆ B ) 
+＼-⊆ : { P A B : HOD } →  A ⊆ P → ( A ⊆ B → ( P ＼ B ) ⊆ ( P ＼ A )) ∧ (( P ＼ B ) ⊆ ( P ＼ A ) → A ⊆ B )
 ＼-⊆ {P} {A} {B} A⊆P = ⟪ ( λ a<b {x} pbx → ⟪ proj1 pbx  , (λ ax → proj2 pbx (a<b ax))   ⟫ )  , lem07 ⟫ where
     lem07 : (P ＼ B) ⊆ (P ＼ A) → A ⊆ B
     lem07 pba {x} ax with ODC.p∨¬p O HODAxiom AC (odef B x)
@@ -89,7 +89,7 @@
     lemm : {x : HOD} → (L ＼ x) ⊆ Power (Union L )
     lemm {x} ⟪ Ly , nxy ⟫ z xz = record { owner = _ ; ao = Ly ; ox = xz }
     wdf : {x y : HOD} → od x == od y → (L ＼ x) =h= (L ＼ y)
-    wdf {x} {y} x=y = record { eq→ = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq← x=y yp) ) ⟫ 
+    wdf {x} {y} x=y = record { eq→ = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq← x=y yp) ) ⟫
                              ; eq← = λ {p} lxp → ⟪ proj1 lxp , (λ yp → proj2 lxp (eq→ x=y yp) ) ⟫  }
 
 
@@ -105,36 +105,43 @@
     ... | no  n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ )
 
 ∪-Union : { A B : HOD } → Union (A , B) =h= ( A ∪ B )
-∪-Union {A} {B} = ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
-    lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
-    lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) ? (sym ?) abo )
-    ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin 
-         * owner ≡⟨ cong (*) (sym a=o)  ⟩ 
-         * (& A) ≡⟨ ? ⟩ 
-         A ∎ ) ox ) where open ≡-Reasoning
-    ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) ?  ) ox)
+∪-Union {A} {B} = ( record { eq→ =  lemma4 ; eq← = lemma2 } )  where
+    lemma4 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
+    lemma4 {x} record { owner = owner ; ao = (case1 refl) ; ox = ox } = case1 (eq← *iso== ox)
+    lemma4 {x} record { owner = owner ; ao = (case2 refl) ; ox = ox } = case2 (eq← *iso== ox)
     lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
     lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) A
         ⟪ case1 refl , d→∋ A A∋x ⟫ )
     lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( union→ (A , B) (* x) B
         ⟪ case2 refl , d→∋ B B∋x ⟫ )
 
-∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )) ?  =h= ( A ∩ B )
+open import zf
+
+pred-in : (A B : HOD ) → ZPred HOD _∋_ _=h=_ (λ x → (A ∋ x) ∧ (B ∋ x))
+pred-in A B = record { ψ-cong = wdf } where
+ wdf : (x y : HOD) → x =h= y → ((A ∋ x) ∧ (B ∋ x)) ⇔ ((A ∋ y) ∧ (B ∋ y))
+ wdf = λ x y x=y
+   → ⟪ (λ p → ⟪ subst (λ k → odef A k) (==→o≡ x=y)       (proj1 p)
+              , subst (λ k → odef B k) (==→o≡ x=y)       (proj2 p)  ⟫ )
+     , (λ p → ⟪ subst (λ k → odef A k) (sym (==→o≡ x=y)) (proj1 p)
+              , subst (λ k → odef B k) (sym (==→o≡ x=y)) (proj2 p)  ⟫ ) ⟫  
+
+∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )) (pred-in A B)  =h= ( A ∩ B )
 ∩-Select {A} {B} =  record { eq→ =  lemma1 ; eq← = lemma2 }  where
-    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) ? ) x → odef (A ∩ B) x
+    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) (pred-in A B) ) x → odef (A ∩ B) x
     lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫
-    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) ? ) x
+    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁)) (pred-in A B) ) x
     lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫
 
 dist-ord : {p q r : HOD } → (p ∩ ( q ∪ r )) =h=  ( ( p ∩ q ) ∪ ( p ∩ r ))
 dist-ord {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 }  where
     lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
     lemma1 {x} lt with proj2 lt
-    lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ 
-    lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ 
+    lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫
+    lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫
     lemma2  : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
-    lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ 
-    lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ 
+    lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫
+    lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫
 
 dist-ord2 : {p q r : HOD } → (p ∪ ( q ∩ r )) =h=  ( ( p ∪ q ) ∩ ( p ∪ r ))
 dist-ord2 {p} {q} {r} = record { eq→ = lemma1 ; eq← = lemma2 }  where
@@ -144,63 +151,63 @@
     lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
     lemma2 {x} lt with proj1 lt | proj2 lt
     lemma2 {x} lt | case1 cp | _ = case1 cp
-    lemma2 {x} lt | _ | case1 cp = case1 cp 
-    lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ 
+    lemma2 {x} lt | _ | case1 cp = case1 cp
+    lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫
 
 record IsBooleanAlgebra {n m : Level} ( L : Set n)
-       ( _==_ : L → L → Set m )
+       ( _≈_ : L → L → Set m )
        ( b1 : L )
        ( b0 : L )
        ( -_ : L → L  )
        ( _+_ : L → L → L )
        ( _x_ : L → L → L ) : Set (n ⊔ m) where
    field
-       +-assoc : {a b c : L } → (a + ( b + c )) == ((a + b) + c)
-       x-assoc : {a b c : L } → (a x ( b x c )) == ((a x b) x c)
-       +-sym : {a b : L } → (a + b) == (b + a)
-       x-sym : {a b : L } → (a x b)  == (b x a)
-       +-aab : {a b : L } → (a + ( a x b )) == a
-       x-aab : {a b : L } → (a x ( a + b )) == a
-       +-dist : {a b c : L } → (a + ( b x c )) == (( a + b ) x ( a + c ))
-       x-dist : {a b c : L } → (a x ( b + c )) == (( a x b ) + ( a x c ))
-       a+0 : {a : L } → (a + b0) == a
-       ax1 : {a : L } → (a x b1) == a
-       a+-a1 : {a : L } → (a + ( - a )) == b1
-       ax-a0 : {a : L } → (a x ( - a )) == b0
+       +-assoc : {a b c : L } → (a + ( b + c )) ≈ ((a + b) + c)
+       x-assoc : {a b c : L } → (a x ( b x c )) ≈ ((a x b) x c)
+       +-sym : {a b : L } → (a + b) ≈ (b + a)
+       x-sym : {a b : L } → (a x b)  ≈ (b x a)
+       +-aab : {a b : L } → (a + ( a x b )) ≈ a
+       x-aab : {a b : L } → (a x ( a + b )) ≈ a
+       +-dist : {a b c : L } → (a + ( b x c )) ≈ (( a + b ) x ( a + c ))
+       x-dist : {a b c : L } → (a x ( b + c )) ≈ (( a x b ) + ( a x c ))
+       a+0 : {a : L } → (a + b0) ≈ a
+       ax1 : {a : L } → (a x b1) ≈ a
+       a+-a1 : {a : L } → (a + ( - a )) ≈ b1
+       ax-a0 : {a : L } → (a x ( - a )) ≈ b0
 
 record BooleanAlgebra {n m : Level} ( L : Set n) : Set (n ⊔ suc m) where
    field
-       _=b=_ : L → L → Set m 
+       _≈_ : L → L → Set m
        b1 : L
        b0 : L
-       -_ : L → L 
+       -_ : L → L
        _+_ : L → L → L
        _x_ : L → L → L
-       isBooleanAlgebra : IsBooleanAlgebra L _=b=_ b1 b0 -_ _+_ _x_
+       isBooleanAlgebra : IsBooleanAlgebra L _≈_ b1 b0 -_ _+_ _x_
 
 record PowerP (P : HOD) : Set (suc n) where
     constructor ⟦_,_⟧
     field
        hod : HOD
-       x⊆P : hod ⊆ P  
+       x⊆P : hod ⊆ P
 
 open PowerP
 
 HODBA : (P : HOD) → BooleanAlgebra {suc n} {n} (PowerP P)
-HODBA P = record { _=b=_ = λ x y → hod x =h= hod y ; b1 = ⟦ P , (λ x → x) ⟧   ; b0 = ⟦ od∅ , (λ x →  ⊥-elim (¬x<0 x)) ⟧ 
+HODBA P = record { _≈_ = λ x y → hod x =h= hod y ; b1 = ⟦ P , (λ x → x) ⟧   ; b0 = ⟦ od∅ , (λ x →  ⊥-elim (¬x<0 x)) ⟧
   ; -_ = λ x → ⟦  P ＼ hod x , proj1 ⟧
-  ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt))  ⟧ 
+  ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt))  ⟧
    ; isBooleanAlgebra = record {
        +-assoc = λ {a} {b} {c} →  record { eq→ = ba01 a b c ; eq← = ba02 a b c  }
-     ; x-assoc = λ {a} {b} {c} →  
-        record { eq→ = λ lt → ⟪ ⟪ proj1 lt  , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt)  ⟫ 
-               ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt)  , proj2 lt ⟫ ⟫ } 
+     ; x-assoc = λ {a} {b} {c} →
+        record { eq→ = λ lt → ⟪ ⟪ proj1 lt  , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt)  ⟫
+               ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt)  , proj2 lt ⟫ ⟫ }
      ; +-sym = λ {a} {b} →  record { eq→ = λ {x} lt → ba05 {hod a} {hod b} lt  ; eq← = ba05 {hod b} {hod a} }
      ; x-sym = λ {a} {b} →  record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫  }
      ; +-aab = λ {a} {b} →  record { eq→ = ba03 a b ; eq← = case1  }
      ; x-aab = λ {a} {b} →  record { eq→ = proj1 ; eq← = λ ax →  ⟪ ax , case1 ax ⟫ }
-     ; +-dist = λ {p} {q} {r} → dist-ord2 {hod p} {hod q} {hod r} 
-     ; x-dist = λ {p} {q} {r} → dist-ord {hod p} {hod q} {hod r} 
+     ; +-dist = λ {p} {q} {r} → dist-ord2 {hod p} {hod q} {hod r}
+     ; x-dist = λ {p} {q} {r} → dist-ord {hod p} {hod q} {hod r}
      ; a+0 = λ {a} →  record { eq→ = ba04 (hod a) ; eq← = case1 }
      ; ax1 = λ {a} →  record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , x⊆P a ax ⟫ }
      ; a+-a1 = λ {a} →  record { eq→ = ba06 a ; eq← = ba07 a }
@@ -215,7 +222,7 @@
      ba01 a b c {x} (case2 (case1 bx)) = case1 (case2 bx)
      ba01 a b c {x} (case2 (case2 cx)) = case2 cx
      ba02 : (a b c : PowerP P) → {x : Ordinal} → odef (hod a ∪ hod b) x ∨ odef (hod c) x
-         → odef (hod a) x ∨ odef (hod b ∪ hod c) x 
+         → odef (hod a) x ∨ odef (hod b ∪ hod c) x
      ba02 a b c {x} (case1 (case1 ax)) = case1 ax
      ba02 a b c {x} (case1 (case2 bx)) = case2 (case1 bx)
      ba02 a b c {x} (case2 cx) = case2 (case2 cx)
@@ -232,7 +239,7 @@
      ba06 : (a : PowerP P ) → { x : Ordinal} → odef (hod a) x ∨ odef (P ＼ hod a) x → def (od P) x
      ba06 a {x} (case1 ax) = x⊆P a ax
      ba06 a {x} (case2 nax) = proj1 nax
-     ba07 : (a : PowerP P ) → { x : Ordinal} → def (od P) x → odef (hod a) x ∨ odef (P ＼ hod a) x 
+     ba07 : (a : PowerP P ) → { x : Ordinal} → def (od P) x → odef (hod a) x ∨ odef (P ＼ hod a) x
      ba07 a {x} px with ODC.∋-p O HODAxiom AC (hod a) (* x)
      ... | yes y = case1 (subst (λ k → odef (hod a) k) &iso y)
      ... | no n = case2 ⟪ px , subst (λ k → ¬ odef (hod a) k) &iso n ⟫