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

changeset 1470:41a8df20cfea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bad pattern on fω→2-wld
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Jun 2024 11:39:35 +0900
parents 9d8fbfc5bf87
children e970149a6af5
files src/PFOD.agda
diffstat 1 files changed, 64 insertions(+), 48 deletions(-) [+]
line wrap: on
line diff
--- a/src/PFOD.agda	Sat Jun 22 09:24:52 2024 +0900
+++ b/src/PFOD.agda	Sat Jun 22 11:39:35 2024 +0900
@@ -48,15 +48,14 @@
 import filter 
 
 open import Relation.Nullary 
-open import Relation.Binary 
+-- open import Relation.Binary hiding ( _⇔_ )
 open import Data.Empty 
-open import Relation.Binary
-open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 import BAlgebra 
 
-open BAlgebra O
+-- open BAlgebra O
+open import ZProduct O HODAxiom ho<
 
 
 -------
@@ -67,7 +66,6 @@
 open import Data.List hiding (filter)
 open import Data.Maybe 
 
-open import ZProduct O
 
 data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
   hφ :  Hω2 0 o∅
@@ -85,61 +83,61 @@
 
 open Hω2r
 
-hw⊆POmega :  {x : Ordinal} → Hω2r x → odef (Power (Power Omega )) x
+hw⊆POmega :  {x : Ordinal} → Hω2r x → odef (Power (Power (Omega ho<))) x
 hw⊆POmega {x} r = odmax1 (Hω2r.count r) (Hω2r.hω2 r) where
-    odmax1 : {y : Ordinal} (i : Nat)  →  Hω2 i y → odef (Power (Power Omega )) y
-    odmax1 0 hφ z xz = ⊥-elim ( ¬x<0 (subst (λ k → odef k z) o∅≡od∅  xz ))
+    odmax1 : {y : Ordinal} (i : Nat)  →  Hω2 i y → odef (Power (Power (Omega ho<) )) y
+    odmax1 0 hφ z xz = ⊥-elim ( ¬x<0 (eq→  o∅==od∅  xz ))
     odmax1 (Suc i) (h0 {_} {y} hw) = pf01 where
-        pf00 : odef ( Power (Power Omega)) y
+        pf00 : odef ( Power (Power (Omega ho<))) y
         pf00 = odmax1 i hw
-        pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 0 > , * y)))
-        pf01 z xz with subst (λ k → odef k z ) *iso xz
+        pf01 : odef (Power (Power (Omega ho<))) (& (Union (< nat→ω i , nat→ω 0 > , * y)))
+        pf01 z xz with eq→  *iso xz
         ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where
              pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
-             pf02 w zw with subst (λ k → odef k z) *iso ox  
-             ... | case2 refl with subst (λ k → odef k w) *iso zw
+             pf02 w zw with eq→  *iso ox  
+             ... | case2 refl with eq→ *iso zw
              ... | case1 refl = ω∋nat→ω {i}
              ... | case2 refl = ω∋nat→ω {0}
-             pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw
+             pf02 w zw | case1 refl with eq→  *iso zw
              ... | case1 refl = ω∋nat→ω {i}
              ... | case2 refl = ω∋nat→ω {i} 
         ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where
-             pf03 : odef ( Power (Power Omega)) y
+             pf03 : odef ( Power (Power (Omega ho<))) y
              pf03 = odmax1 i hw
              pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
              pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox)  _ zw
     odmax1 (Suc i) (h1 {_} {y} hw) = pf01 where
-        pf00 : odef ( Power (Power Omega)) y
+        pf00 : odef ( Power (Power (Omega ho<))) y
         pf00 = odmax1 i hw
-        pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 1 > , * y)))
-        pf01 z xz with subst (λ k → odef k z ) *iso xz
+        pf01 : odef (Power (Power (Omega ho<))) (& (Union (< nat→ω i , nat→ω 1 > , * y)))
+        pf01 z xz with eq→ *iso xz
         ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where
              pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
-             pf02 w zw with subst (λ k → odef k z) *iso ox  
-             ... | case2 refl with subst (λ k → odef k w) *iso zw
+             pf02 w zw with eq→ *iso ox  
+             ... | case2 refl with eq→ *iso zw
              ... | case1 refl = ω∋nat→ω {i}
              ... | case2 refl = ω∋nat→ω {1}
-             pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw
+             pf02 w zw | case1 refl with eq→ *iso zw
              ... | case1 refl = ω∋nat→ω {i}
              ... | case2 refl = ω∋nat→ω {i}
         ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where
-             pf03 : odef ( Power (Power Omega)) y
+             pf03 : odef ( Power (Power (Omega ho<))) y
              pf03 = odmax1 i hw
              pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
              pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox)  _ zw
     odmax1 (Suc i) (he {_} {y} hw) = pf00 where
-        pf00 : odef ( Power (Power Omega)) y
+        pf00 : odef ( Power (Power (Omega ho<))) y
         pf00 = odmax1 i hw
 
 --
 -- Set of limited partial function of Omega
 --
 HODω2 :  HOD
-HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power (Power Omega))
+HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power (Power (Omega ho<)))
   ; <odmax = λ lt → odef< (hw⊆POmega  lt) } 
 
-HODω2⊆Omega : {x : HOD} → HODω2 ∋ x → x ⊆ Power  Omega 
-HODω2⊆Omega {x} hx {z} wz = hw⊆POmega hx _ (subst (λ k → odef k z) (sym *iso) wz)
+HODω2⊆Omega : {x : HOD} → HODω2 ∋ x → x ⊆ Power  (Omega ho<) 
+HODω2⊆Omega {x} hx {z} wz = hw⊆POmega hx _ (eq← *iso wz)
 
 record HwStep : Set n where
    field 
@@ -147,6 +145,10 @@
      i : Nat
      isHw : Hω2 i x
 
+data Two : Set where
+  i0 : Two
+  i1 : Two
+
 3→Hω2 : List (Maybe Two) → HOD
 3→Hω2 t = * (HwStep.x (list→hod t))  where
    list→hod : List (Maybe Two) → HwStep
@@ -172,55 +174,69 @@
    lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }
 
 ω→2 : HOD
-ω→2 = Power Omega
+ω→2 = Power (Omega ho<)
 
 ω2→f : (x : HOD) → ω→2 ∋ x → Nat → Two
-ω2→f x lt n with ODC.∋-p O x (nat→ω n)
+ω2→f x lt n with ∋-p x (nat→ω n)
 ω2→f x lt n | yes p = i1
 ω2→f x lt n | no ¬p = i0
 
 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
-fω→2-sel f x = (Omega ∋ x) ∧ ( (lt : odef Omega (&  x) ) → f (ω→nat x lt) ≡ i1 )
+fω→2-sel f x = (Omega ho< ∋ x) ∧ ( (lt : odef (Omega ho<) (&  x) ) → f (ω→nat x lt) ≡ i1 )
+
+open import zf
+
+fω→2-wld : ( f : Nat → Two ) → ZPred HOD _∋_ _=h=_ (fω→2-sel f)
+fω→2-wld f = record { ψ-cong = f00 } where
+     f01 : (x y : HOD) (ltx : odef (Omega ho<) (& x)) (lty : odef (Omega ho<) (& y)) → x =h= y →  f (ω→nat x ltx) ≡ i1  → f (ω→nat y lty) ≡ i1
+     f01 x y ltx lty x=y feq = subst (λ k → f k ≡ i1 ) (ω→nato-cong ltx lty (==→o≡ x=y) ) feq
+     f00 :  (x y : HOD) → x =h= y → (fω→2-sel f x ) ⇔ (fω→2-sel f y)
+     proj1 (f00 x y x=y) fs = ⟪ subst (λ k → odef (Omega ho<)  k) (==→o≡ x=y)       (proj1 fs)  , (λ lt → f01 x y (proj1 fs) lt x=y (proj2 fs (f02 _ _ lt))) ⟫ where
+         f02 : (y x : Ordinal ) → odef (Omega ho<) y → Omega-d x
+         f02 _ x OD.iφ = ?
+         f02 _ x (OD.isuc lt) = ?
+     proj2 (f00 x y x=y) fs = ⟪ subst (λ k → odef (Omega ho<)  k) (sym (==→o≡ x=y)) (proj1 fs)  , (λ lt → f01 y x (proj1 fs) lt (==-sym x=y) (proj2 fs ?)) ⟫
 
 fω→2 : (Nat → Two) → HOD
-fω→2 f = Select Omega (fω→2-sel f)
+fω→2 f = Select (Omega ho<) (fω→2-sel f) (fω→2-wld f) 
 
-open _==_
-
-import Axiom.Extensionality.Propositional
-postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
+-- import Axiom.Extensionality.Propositional
+-- postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
-ω2∋f f = power← Omega (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {Omega} )) lt))
+ω2∋f f = ? -- power← (Omega ho<) (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {(Omega ho<)} )) lt))
 
-ω→2f≡i1 : (X i : HOD) → (iω : Omega ∋ i) → (lt : ω→2 ∋ X ) → ω2→f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
-ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
-ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
+ω→2f≡i1 : (X i : HOD) → (iω : (Omega ho<) ∋ i) → (lt : ω→2 ∋ X ) → ω2→f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
+ω→2f≡i1 X i iω lt eq with ∋-p X (nat→ω (ω→nat i iω))
+ω→2f≡i1 X i iω lt eq | yes p = ? -- subst (λ k → X ∋ k ) (nat→ω-iso iω) p
 
 ω2→f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω2→f X lt )  =h= X
 eq→ (ω2→f-iso X lt) {x} ⟪ ωx , ⟪ ωx1 , iso ⟫ ⟫ = le00 where
     le00 : odef X x
     le00 = subst (λ k → odef X k) &iso ( ω→2f≡i1 _ _ ωx1 lt  (iso ωx1)  )
-eq← (ω2→f-iso X lt) {x} Xx = ⟪ subst (λ k → odef Omega k) &iso le02  , ⟪ le02 , le01 ⟫ ⟫ where
-    le02 : Omega ∋ * x
-    le02 = power→ Omega _ lt (subst (λ k → odef X k) (sym &iso) Xx) 
-    le01 : (wx : odef Omega (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1
-    le01 wx   with ODC.∋-p O X (nat→ω (ω→nat _ wx) )
+eq← (ω2→f-iso X lt) {x} Xx = ⟪ subst (λ k → odef (Omega ho<) k) &iso le02  , ⟪ le02 , le01 ⟫ ⟫ where
+    le02 : (Omega ho<) ∋ * x
+    le02 = power→ (Omega ho<) _ lt (subst (λ k → odef X k) (sym &iso) Xx) 
+    le01 : (wx : odef (Omega ho<) (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1
+    le01 wx   with ∋-p  X (nat→ω (ω→nat _ wx) )
     ... | yes p  = refl
     ... | no ¬p  = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where
         le03 :  x ≡ & (nat→ω (ω→nato wx))
-        le03 = subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) )
+        le03 = ? -- subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) )
+
+¬i1→i0 : ?
+¬i1→i0 = ?
 
 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f
-fω→2-iso f = f-extensionality (λ x → le01 x ) where
+fω→2-iso f = ? where -- f-extensionality (λ x → le01 x ) where
     le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x
-    le01 x with  ODC.∋-p O (fω→2 f) (nat→ω x) 
-    le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) (trans *iso *iso)) (sym ((proj2 (proj2 p)) le02)) where
+    le01 x with  ∋-p (fω→2 f) (nat→ω x) 
+    le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) ?) (sym ((proj2 (proj2 p)) le02)) where
         le02 :  Omega-d (& (* (& (nat→ω x))))
         le02 = proj1 (proj2 p )
     le01 x | no ¬p = sym ( ¬i1→i0 le04 ) where
         le04 : ¬ f x ≡ i1
         le04 fx=1 = ¬p ⟪ ω∋nat→ω {x} , ⟪ subst (λ k → Omega-d k) (sym &iso) (ω∋nat→ω {x})  , le05 ⟫ ⟫ where
             le05 : (lt : Omega-d (& (* (& (nat→ω x))))) → f (ω→nato lt) ≡ i1
-            le05 lt = trans (cong f (ω→nat-iso0 x lt (trans *iso *iso))) fx=1
+            le05 lt = trans (cong f (ω→nat-iso0 x lt ?)) fx=1