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

changeset 1375:6210088c8f25

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 Thu, 22 Jun 2023 18:15:14 +0900
parents 51ccc9daa979
children aca9b1e67503
files src/bijection.agda
diffstat 1 files changed, 20 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Thu Jun 22 17:23:43 2023 +0900
+++ b/src/bijection.agda	Thu Jun 22 18:15:14 2023 +0900
@@ -733,49 +733,27 @@
     lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
     lem01 n i le = ? where
         -- starting from 0, if count B i ≡ suc n, this is it
-        lem05 : (i : ℕ) → 0 < count-B i → count-B i ≤ 1  → CountB 0
-        lem05 0 0<cb cb≤1 with is-B (fun← cn 0) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 refl }
-        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≤> 0<cb (s≤s z≤n) )
-        lem05 (suc i) 0<cb cb≤1 with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 lem06} where
-            lem06 : suc (count-B i) ≡ 1
-            lem06 with <-cmp (suc (count-B i)) 1
-            ... | tri< a ¬b ¬c = ⊥-elim (nat-≤> 0<cb a )
-            ... | tri≈ ¬a b ¬c = b
-            ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≤> cb≤1 c₁ )
-        ... | no nisb | record { eq = eq1 } = lem05 i (<-transˡ a<sa 0<cb) cb≤1
+        lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
+        lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq } 
+        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
+        lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq} 
+        ... | no nisb | record { eq = eq1 } = lem07 n i  eq
 
-        lem07 : (n i : ℕ) → n < count-B i → count-B i ≤ (suc n) → CountB n
-        lem07 n 0 0<cb cb≤1 with is-B (fun← cn 0) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 (sym lem06) } where
-            lem06 : suc n ≡ 1
-            lem06 with <-cmp 1 (suc n) 
-            ... | tri< a ¬b ¬c = ⊥-elim (nat-≤> 0<cb a )
-            ... | tri≈ ¬a b ¬c = sym b
-            ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≤> cb≤1 c₁ )
-        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≤> 0<cb (s≤s z≤n ) )
-        lem07 n (suc i) 0<cb cb≤1 with is-B (fun← cn (suc i)) | inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 lem06} where
-            lem06 : suc (count-B i) ≡ suc n
-            lem06 with <-cmp (suc (count-B i)) (suc n)
-            ... | tri< a ¬b ¬c = ⊥-elim (nat-≤> 0<cb a )
-            ... | tri≈ ¬a b ¬c = b
-            ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≤> cb≤1 c₁ )
-        ... | no nisb | record { eq = eq1 } = lem07 n i (<-transˡ a<sa 0<cb) cb≤1
-
-
-        lem03 : (i m : ℕ ) → i ≤ m → count-B i < count-B m → CountB i
-        lem03 0 0 i≤m ci<cm  = ⊥-elim ( nat-≡< refl ci<cm )
-        lem03 0 (suc m) i≤m ci<cm  with is-B (fun← cn (suc m)) | inspect count-B (suc m)
-        ... | yes isb | record { eq = eq1 } with <-cmp 0 (count-B m)
-        ... | tri≈ ¬a cb=0 ¬c = record { b = Is.a isb ; cb = suc m ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 (cong suc (sym cb=0)) }
-        ... | tri< 0<cb ¬b ¬c with ≤-∨ ci<cm
-        ... | case1 eq = record { b = Is.a isb ; cb = suc m ; b=cn = sym (Is.fa=c isb) ; cb=n = ? }
-        ... | case2 (s≤s lt) = lem03 0 m z≤n (<-transˡ a<sa lt)
-        lem03 zero (suc m) z≤n ci<cm | no nisb | record { eq = eq1 } = lem03 0 m z≤n (<-transˡ a<sa ci<cm)
-        lem03 (suc i) 0 i≤m ci<cm  = ?
-        lem03 (suc i) (suc m) i≤m ci<cm  = ?
+        lem08 : (i : ℕ) → suc n ≤ count-B i →  CountB n
+        lem08 0 n<cb with is-B (fun← cn i)| inspect count-B 0
+        ... | no nisb | record { eq = eq1 } = ?
+        ... | yes isb | record { eq = eq1 } with <-cmp (count-B i) 0
+        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (s≤s z≤n ))
+        ... | tri≈ ¬a b ¬c = record { b = Is.a isb ; cb = i ; b=cn = sym (Is.fa=c isb) ; cb=n = ? }
+        ... | tri> ¬a ¬b c₁ = ?
+        lem08 (suc i) n<cb with is-B (fun← cn (suc i))| inspect count-B (suc i)
+        ... | no nisb | record { eq = eq1 } = lem08 i n<cb
+        ... | yes isb | record { eq = eq1 } with <-cmp (count-B i) (suc n)
+        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a ?)
+        ... | tri≈ ¬a b ¬c = lem07 n i b
+        ... | tri> ¬a ¬b c₁ = lem08 i (≤-trans a≤sa c₁)
 
     ntob : (n : ℕ) → B
     ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ))