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

changeset 1304:f832e986427d

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 Wed, 07 Jun 2023 11:26:03 +0900
parents 66a6804d867b
children 81f66cec617e
files src/bijection.agda
diffstat 1 files changed, 36 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Wed Jun 07 09:42:58 2023 +0900
+++ b/src/bijection.agda	Wed Jun 07 11:26:03 2023 +0900
@@ -506,9 +506,6 @@
     f = InjectiveF.f fi
     g = InjectiveF.f gi
 
-    cbn : ℕ → ℕ
-    cbn n = fun→ cn (g (f (fun← an (suc n))))
-
     --
     -- count number of valid A and B in C
     --     the count of B is the numner of B in Bijection B ℕ
@@ -521,8 +518,6 @@
          ca≤cb : ca ≤ cb  
          na : {i : ℕ} → i < ca → A
          nb : {i : ℕ} → i < cb → B
-         ia : {i j : ℕ } → { i<c : i < ca } → {j<c : j < ca } → na i<c ≡ na j<c → i ≡ j
-         ib : {i j : ℕ } → { i<c : i < cb } → {j<c : j < cb } → nb i<c ≡ nb j<c → i ≡ j
 
     ¬isA∧isB : (y : C ) →  Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥
     ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where
@@ -534,25 +529,47 @@
 
     lb : (n : ℕ ) → CB n
     lb zero with is-A (fun← cn zero) | is-B (fun← cn zero)
-    ... | yes isA | yes isB =  record { ca = suc zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ≤-refl ; na = λ _ → Is.a isA ; nb = λ _ → Is.a isB ; ia = ? ; ib = ? } 
-    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = record { ca = zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ? ; na = λ () ; nb = ? ; ia = ? ; ib = ? } 
-    ... | no nisA | no nisB = record { ca = zero ; cb = zero ; cb≤n = ? ; ca≤cb = ? ; na = λ () ; nb = λ () ; ia = ? ; ib = ? } 
-    lb (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n))
-    ... | yes isA | yes isB =  record { ca = suc (CB.ca (lb n)) ; cb = suc (CB.cb (lb n)) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } 
+    ... | yes isA | yes isB =  record { ca = suc zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = ≤-refl ; na = λ _ → Is.a isA ; nb = λ _ → Is.a isB } 
     ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
-    ... | no nisA | yes isB = record { ca = CB.ca (lb n) ; cb = suc (CB.cb (lb n)) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } 
-    ... | no nisA | no nisB = record { ca = CB.ca (lb n) ; cb = CB.cb (lb n) ; cb≤n = ? ; ca≤cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } 
-    -- record { ca = ? ; cb = ? ; na = ? ; nb = ? ; ia = ? ; ib = ? } where
-    --    cbn : CB n
-    --    cbn = lb n
-    -- 
+    ... | no nisA | yes isB = record { ca = zero ; cb = suc zero ; cb≤n = ≤-refl ; ca≤cb = px≤x  ; na = λ () ; nb = λ _ → Is.a isB } 
+    ... | no nisA | no nisB = record { ca = zero ; cb = zero ; cb≤n = px≤x ; ca≤cb = ≤-refl ; na = λ () ; nb = λ () } 
+    lb (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n))
+    ... | yes isA | yes isB =  record { ca = suc (CB.ca (lb n)) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = s≤s (CB.ca≤cb (lb n)) 
+        ; na = na ; nb = nb } where
+           na : {i : ℕ} → i < suc (CB.ca (lb n)) → A
+           na {i} i<a with <-∨ i<a
+           ... | case1 refl = Is.a isA 
+           ... | case2 i<a = CB.na (lb n) i<a
+           nb : {i : ℕ} → i < suc (CB.cb (lb n)) → B
+           nb {i} i<a with <-∨ i<a
+           ... | case1 refl = Is.a isB 
+           ... | case2 i<a = CB.nb (lb n) i<a
+    ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB = record { ca = CB.ca (lb n) ; cb = suc (CB.cb (lb n)) ; cb≤n = s≤s (CB.cb≤n (lb n)) ; ca≤cb = ≤-trans (CB.ca≤cb (lb n)) px≤x 
+        ; na = CB.na (lb n)  ; nb = nb } where
+           nb : {i : ℕ} → i < suc (CB.cb (lb n)) → B
+           nb {i} i<a with <-∨ i<a
+           ... | case1 refl = Is.a isB 
+           ... | case2 i<a = CB.nb (lb n) i<a
+    ... | 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< : (n : ℕ) → CB.cb (lb (cbn n)) < CB.cb (lb (cbn (suc n)))
     cb< = ?
           
     n<cbn : (n : ℕ) →  n < CB.cb (lb (cbn n))
-    n<cbn zero = ?
+    n<cbn zero with is-A (fun← cn zero) | is-B (fun← cn zero) | inspect lb zero
+    ... | yes isA | yes isB | record { eq = eq1 } = subst (λ k → 1 ≤ CB.cb (lb k)) lem02 lem01  where
+         lem01 :  1 ≤ CB.cb (lb 0)
+         lem01 = subst (λ k → 1 ≤ k ) (sym (cong CB.cb eq1))  ≤-refl
+         lem02 : 0 ≡ fun→ cn (g (f (fun← an 0)))
+         lem02 = ?
+    ... | yes isA | no nisB | record { eq = eq1 } = ⊥-elim ( ¬isA∧isB _ isA nisB )
+    ... | no nisA | yes isB | record { eq = eq1 } = ?
+    ... | no nisA | no nisB | record { eq = eq1 } = ?
     n<cbn (suc n) = begin
        suc (suc n)  ≤⟨ s≤s (n<cbn n) ⟩  
        suc (CB.cb (lb (cbn n)))  ≤⟨ cb< n ⟩
@@ -562,9 +579,7 @@
     bton : B → ℕ
     bton b = CB.cb (lb (fun→ cn (g b)))
     ntob : ℕ → B
-    ntob n = CB.nb (lb (fun→ cn (g (f (fun← an (suc n)))))) {n} (n<cbn n)
-
-
+    ntob n = CB.nb (lb (fun→ cn (g (f (fun← an n))))) (n<cbn n)
 
 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 {