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

changeset 1308:f4bd059227f8

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, 09 Jun 2023 11:26:36 +0900
parents 71652ee117a7
children a93764db7c67
files src/bijection.agda src/nat.agda
diffstat 2 files changed, 41 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Fri Jun 09 07:42:31 2023 +0900
+++ b/src/bijection.agda	Fri Jun 09 11:26:36 2023 +0900
@@ -554,50 +554,49 @@
     ... | no nisA | no nisB = record { ca = CB.ca (lb n) ; cb = CB.cb (lb n) ; cb≤n = ≤-trans (CB.cb≤n (lb n)) px≤x  ; ca≤cb =  CB.ca≤cb (lb n)
         ; na = CB.na (lb n) ; nb = CB.nb (lb n) }
 
-    cbn : ℕ → ℕ
-    cbn n = fun→ cn (g (f (fun← an n)))
+    --   cb = count of B  monotonic    i ≤ j → CB.cb i ≤ CB.cb j ≤ j
+    --   ca = count of A  monotonic    i ≤ j → CB.ca i ≤ CB.ca j ≤ j
+    --      ca ≤ cb from CB 
+    --   cbn i : i ≡ fun← an n → i count of different B → some b ≥ i  
+    --   cbn 0     0 ≤ CB.cb (fun→ cn (g (f (fun→ an 0))))
+    --   cbn (suc i)     i < cbn i → cbn i 
+    --                   cbn i ≤ i → it contains all b ≤ i → f (fun← an n) is not in this → i < f (fun← an n) 
 
-    cb< : (n : ℕ) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
-    cb< n = cb00 (CB.cb (lb (cbn n))) ≤-refl  where
-        cb00 : (i : ℕ) → i ≤ CB.cb (lb (cbn n)) → i < CB.cb (lb (cbn (suc n))) 
-        cb00 zero le with is-A (fun← cn (cbn 0)) | is-B (fun← cn (cbn 0))
+    record CBN ( n : ℕ ) : Set where
+       field
+           cbn : ℕ
+           n<cbn : n < CB.cb (lb cbn )
+
+    cbn : (n : ℕ ) → CBN n
+    cbn 0 = record { cbn = j ; n<cbn = cb<0 _ refl  }  where
+        j =  CB.cb (lb (fun→ cn (g (f (fun← an zero))))) 
+        cb<0 : (i : ℕ) → i ≡ CB.cb (lb j) → 0 < i
+        cb<0 0 eq with is-A (fun← cn zero) | is-B (fun← cn zero)
         ... | yes isA | yes isB = ?
         ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-        ... | no nisA | yes isB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl )   } )
-        ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  refl )   } )
-        cb00 (suc c) le with is-A (fun← cn (suc c)) | is-B (fun← cn (suc c))
-        ... | yes isA | yes isB = ? where -- <-transʳ z≤n ≤-refl 
-             cb01 : c < CB.cb (lb (cbn (suc n))) 
-             cb01 = cb00 c (sx≤y→x≤y le)
-        ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
         ... | no nisA | yes isB = ?
-        ... | no nisA | no nisB = ?
-
-    cb<0 : 0 < CB.cb (lb (cbn 0))
-    cb<0 with cbn 0 | inspect cbn 0
-    ... | zero | record { eq = eq1 } with is-A (fun← cn zero) | is-B (fun← cn zero)
-    ... | yes isA | yes isB =  ≤-refl
-    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = ≤-refl
-    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1)   } )
-    cb<0 | suc t | record { eq = eq1 } with is-A (fun← cn (suc t)) | is-B (fun← cn (suc t))
-    ... | yes isA | yes isB = <-transʳ z≤n ≤-refl 
-    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = <-transʳ z≤n ≤-refl 
-    ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  eq1 )   } )
-
-    n<cbn : (n : ℕ) →  n < CB.cb (lb (cbn n))
-    n<cbn zero = cb<0
-    n<cbn (suc n) = begin
-       suc (suc n)  ≤⟨ s≤s (n<cbn n) ⟩
-       suc (CB.cb (lb (cbn n)))  ≤⟨ cb< n ⟩
-       CB.cb (lb (cbn (suc n)))  ∎  where
-          open ≤-Reasoning
+        ... | no nisA | no nisB = ⊥-elim ( nisA record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) ( cong (fun← cn)  ? )   } )
+        cb<0 (suc i) eq = 0<s
+    cbn (suc n) with <∨≤ (suc n) (CB.cb (lb (CBN.cbn (cbn n))))
+    ... | case1 lt = record { cbn = CBN.cbn (cbn n) ; n<cbn = lt }
+    ... | case2 le = ?
 
     bton : B → ℕ
     bton b = CB.cb (lb (fun→ cn (g b)))
     ntob : ℕ → B
-    ntob n = CB.nb (lb (fun→ cn (g (f (fun← an n))))) (n<cbn n)
+    ntob n = CB.nb (lb (CBN.cbn (cbn n))) (CBN.n<cbn (cbn n))
+
+    biso : (n : ℕ) → bton (ntob n) ≡ n
+    biso n = lem00 n where
+        lem00 : (n : ℕ) → CB.cb (lb (fun→ cn (g (CB.nb (lb (CBN.cbn (cbn n))) (CBN.n<cbn (cbn n)))))) ≡ n
+        lem00 zero = ?
+        lem00 (suc n) = ?
+
+    biso1 : (b : B) → ntob (bton b) ≡ b
+    biso1 b = lem01 _ _ b (CBN.n<cbn (cbn (CB.cb (lb (fun→ cn (g b)))))) refl where
+        lem01 : (i j : ℕ) → (b : B) → (lt : j < CB.cb (lb i)) → i ≡ (CBN.cbn (cbn (CB.cb (lb (fun→ cn (g b)))))) → CB.nb (lb i) lt ≡ b
+        lem01 zero j b lt eq = ?
+        lem01 (suc i) j b lt eq = ?
 
 bi-∧ : {A B C D : Set} → Bijection A B → Bijection C D → Bijection (A ∧ C) (B ∧ D)
 bi-∧ {A} {B} {C} {D} ab cd = record {
--- a/src/nat.agda	Fri Jun 09 07:42:31 2023 +0900
+++ b/src/nat.agda	Fri Jun 09 11:26:36 2023 +0900
@@ -209,6 +209,12 @@
 <to≤ {zero} {suc y} (s≤s z≤n) = z≤n
 <to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)
 
+<∨≤ : ( x y : ℕ ) →  (x < y ) ∨ (y ≤ x) 
+<∨≤ x y with <-cmp x y
+... | tri< a ¬b ¬c = case1 a
+... | tri≈ ¬a refl ¬c = case2 ≤-refl
+... | tri> ¬a ¬b c = case2 (<to≤ c)
+
 refl-≤s : {x : ℕ } → x ≤ suc x
 refl-≤s {zero} = z≤n
 refl-≤s {suc x} = s≤s (refl-≤s {x})