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

changeset 1374:51ccc9daa979

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 17:23:43 +0900
parents 1da09696a256
children 6210088c8f25
files src/bijection.agda
diffstat 1 files changed, 35 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Thu Jun 22 12:26:09 2023 +0900
+++ b/src/bijection.agda	Thu Jun 22 17:23:43 2023 +0900
@@ -733,14 +733,46 @@
     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 : ℕ) → 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 count-B m | inspect count-B m
-        ... | 0 | record { eq = eq2 } = record { b = Is.a isb ; cb = suc m ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 refl }
-        ... | suc cb | record { eq = eq2 } = lem03 0 m z≤n  (subst (λ k → _ < k ) (sym eq2) (x≤y→x<sy ?) )
+        ... | 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  = ?