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

changeset 1038:dfbac4b59bae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mf< everywhere
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 03 Dec 2022 08:58:46 +0900
parents 23e185ef2737
children 4b22a2ece4e8
files src/zorn.agda
diffstat 1 files changed, 28 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Dec 02 19:14:41 2022 +0900
+++ b/src/zorn.agda	Sat Dec 03 08:58:46 2022 +0900
@@ -328,15 +328,14 @@
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫ 
 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫ 
 
-record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
+record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
         {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
    field
       supf :  Ordinal → Ordinal
 
       order : {x y w : Ordinal } → y o≤ z → x o< y → FClosure A f (supf x) w → w ≤ supf y
 
-      cfcs : (mf< : <-monotonic-f A f)
-         {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
+      cfcs : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b  → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
 
       asupf :  {x : Ordinal } → odef A (supf x)
       supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
@@ -354,6 +353,9 @@
    chain∋init : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) y
    chain∋init {x} x≤z = ⟪ ay , ch-init (init ay refl)  ⟫
 
+   mf : ≤-monotonic-f A f 
+   mf x ax = ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf x ax ) ⟫
+
    f-next : {a z : Ordinal} → odef (UnionCF A f ay supf z) a → odef (UnionCF A f ay supf z) (f a)
    f-next {a} ⟪ ua , ch-init fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-init (fsuc _ fc) ⟫ 
    f-next {a} ⟪ ua , ch-is-sup u su<x su=u fc ⟫ = ⟪ proj2 ( mf _ ua)  , ch-is-sup u su<x su=u (fsuc _ fc) ⟫ 
@@ -369,9 +371,8 @@
    supf<A : {x : Ordinal } → supf x o< & A
    supf<A = z09 asupf
 
-   csupf : (mf< : <-monotonic-f A f) {b : Ordinal } 
-      → supf b o< supf z → supf b o< z → odef (UnionCF A f ay supf z) (supf b) -- supf z is not an element of this chain
-   csupf mf< {b} sb<sz sb<z = cfcs mf< (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
+   csupf : {b : Ordinal } → supf b o< supf z → supf b o< z → odef (UnionCF A f ay supf z) (supf b) -- supf z is not an element of this chain
+   csupf {b} sb<sz sb<z = cfcs (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
 
    minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f ay supf x)
    minsup {x} x≤z = record { sup = supf x ; isMinSUP = is-minsup x≤z }
@@ -448,8 +449,8 @@
    supf-¬hp {x} x≤z <-mono hp = IsMinSUP→NotHasPrev asupf (λ {w} uw → 
        (subst (λ k → w ≤ k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
 
-   supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
-   supf-idem  mf< {b} b≤z sfb≤x = z52 where
+   supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
+   supf-idem {b} b≤z sfb≤x = z52 where
        z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
        z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
        z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z su<b fc where
@@ -461,8 +462,8 @@
    -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z  → ChainP A f supf (supf b)
    --    the condition of cfcs is satisfied, this is obvious
 
-record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
-        {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
+        {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
    supf = ZChain.supf zc
    field
       is-max :  {a b : Ordinal } → (ca : odef (UnionCF A f ay supf z) a ) → b o< z  → (ab : odef A b)
@@ -484,10 +485,10 @@
 --
 -- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup
 --
-supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
-        {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb ) 
+supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
+        {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb ) 
       → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z
-supf-unique A f mf {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
+supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa  where
        supfa = ZChain.supf za
        supfb = ZChain.supf zb
        ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x
@@ -640,7 +641,7 @@
      --     we have supf-unique now, it is provable in the first Tranfinte induction
 
      SZ1 : ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) (mf< : <-monotonic-f A f)
-        {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf ay zc x
+        {init : Ordinal} (ay : odef A init) (zc : ZChain A f mf< ay (& A)) (x : Ordinal) → x o≤ & A → ZChain1 A f mf< ay zc x
      SZ1 f mf mf< {y} ay zc x x≤A = zc1 x x≤A  where
         chain-mono1 :  {a b c : Ordinal} → a o≤ b
             → odef (UnionCF A f ay (ZChain.supf zc) a) c → odef (UnionCF A f ay (ZChain.supf zc) b) c
@@ -656,7 +657,7 @@
 
         supf = ZChain.supf zc
 
-        zc1 :  (x : Ordinal ) → x o≤ & A →   ZChain1 A f mf ay zc x
+        zc1 :  (x : Ordinal ) → x o≤ & A →   ZChain1 A f mf< ay zc x
         zc1 x x≤A with Oprev-p x  
         ... | yes op = record { is-max = is-max } where
                px = Oprev.oprev op
@@ -764,15 +765,15 @@
      -- create all ZChains under o< x
      --
 
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → ZChain A f mf ay z) → ZChain A f mf ay x
-     ind f mf {y} ay x prev with Oprev-p x
+     ind : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
+         → ((z : Ordinal) → z o< x → ZChain A f mf< ay z) → ZChain A f mf< ay x
+     ind f mf< {y} ay x prev with Oprev-p x
      ... | yes op = zc41 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
-          zc : ZChain A f mf ay (Oprev.oprev op)
+          zc : ZChain A f mf< ay (Oprev.oprev op)
           zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc
@@ -797,6 +798,9 @@
           ... | case1 eq = case2 eq
           ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x  ⟫ )
 
+          mf : ≤-monotonic-f A f 
+          mf x ax = ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf x ax ) ⟫
+
           --
           -- find the next value of supf
           --
@@ -855,7 +859,7 @@
              m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) sfpx≤sp1
              m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x fc) sfpx≤sp1
 
-          zc41 : ZChain A f mf ay x
+          zc41 : ZChain A f mf< ay x
           zc41 with zc43 x sp1
           zc41 | (case2 sp≤x ) =  record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono ; order = ?
               ; supfmax = ? ; is-minsup = ? ;  cfcs = cfcs  }  where
@@ -1061,7 +1065,7 @@
                             z27 : supf1 px ≡ px    --- sp1 o≤ x
                             z27 = trans (sf1=sf0 o≤-refl) ( ZChain.sup=u zc ? ? ? )
                             z29 : supf0 px o≤ z
-                            z29 = ? --    supf0 px ≡ supf1 px o≤ supf1 x o≤ x ≡ z
+                            z29 = ? --    supf0 px ≡ supf1 px o≤ supf1 x o≤ 
                             z28 : supf0 px o< z
                             z28 = ?
                         z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫
@@ -1236,6 +1240,9 @@
      ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf-mono ; order = ?
               ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs    }  where
 
+          mf : ≤-monotonic-f A f 
+          mf x ax = ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf x ax ) ⟫
+
           pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
           pzc {z} z<x = prev z z<x