Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1372:4b7a756dae33
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 22 Jun 2023 09:20:17 +0900 |
parents | 8b66575d4939 |
children | 1da09696a256 |
files | src/bijection.agda |
diffstat | 1 files changed, 25 insertions(+), 26 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Thu Jun 22 07:38:29 2023 +0900 +++ b/src/bijection.agda Thu Jun 22 09:20:17 2023 +0900 @@ -678,8 +678,7 @@ any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl n<ca-list : (n : ℕ) → n < ca-list (clist (c n)) - n<ca-list zero = subst ( λ k → zero < k ) (a-list-ca zero (clist (c zero)) (clist-any zero zero ≤-refl)) ( <-transˡ a<sa (s≤s z≤n )) - n<ca-list (suc n) = lem06 where + n<ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le → clist-any n j le ) where -- -- we have ANY i on i ≤ n, so we can remove n element from clist (c n) -- induction on n is no good, because (ani (suc n)) may happen in clist (c n) @@ -704,25 +703,17 @@ → suc (ca-list (del i cl a)) ≡ ca-list cl del-ca i cl a = a-list-ca i cl (a i ≤-refl) - lem06 : suc n < ca-list (clist (c (suc n))) - lem06 = lem31 where - lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → suc i < ca-list cl - lem30 0 cl i≤n a = begin - 2 ≤⟨ s≤s (s≤s z≤n) ⟩ - suc (suc (ca-list (del 0 (del 1 cl a) (del-any 0 cl a)) )) ≡⟨ cong suc ( del-ca 0 (del 1 cl a) (del-any 0 cl a)) ⟩ - suc (ca-list (del 1 cl a) ) ≡⟨ del-ca 1 cl a ⟩ - ca-list cl ∎ where - open ≤-Reasoning - lem30 (suc i) cl i≤n a = begin - suc (suc (suc i)) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any (suc i) cl a) ) ⟩ - suc (ca-list (del (suc (suc i)) cl a)) ≡⟨ del-ca (suc (suc i)) cl a ⟩ - ca-list cl ∎ where - open ≤-Reasoning - lem31 : suc n < ca-list (clist (c (suc n))) - lem31 = lem30 n (clist (c (suc n))) a≤sa (λ j le → clist-any (suc n) j le ) - - n<ca0 : {n : ℕ} → n < count-A (c n) - n<ca0 = ? + lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl + lem30 0 cl i≤n a = begin + 1 ≤⟨ s≤s z≤n ⟩ + suc (ca-list (del 0 cl a) ) ≡⟨ del-ca 0 cl a ⟩ + ca-list cl ∎ where + open ≤-Reasoning + lem30 (suc i) cl i≤n a = begin + suc (suc i) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ + suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩ + ca-list cl ∎ where + open ≤-Reasoning record maxAC (n : ℕ) : Set where field @@ -730,24 +721,32 @@ n<ca : n < count-A ac lem02 : (n : ℕ) → maxAC n - lem02 n = record { ac = c n ; n<ca = ? } + lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) } record CountB (n : ℕ) : Set where field b : B cb : ℕ b=cn : fun← cn cb ≡ g b - cb=n : count-B cb ≡ n + cb=n : count-B cb ≡ suc n lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n - lem01 zero zero lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? } - lem01 zero (suc i) lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? } + lem01 zero zero le with is-B (fun← cn 0) | inspect count-B zero + ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = eq1 } + ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≤> le a<sa) + lem01 zero (suc i) le with ≤-∨ le + ... | case1 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 (sym eq) } + ... | no nisb | record { eq = eq1 } = lem01 zero i le + lem01 zero (suc i) le | case2 lt 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 ? } + ... | no nisb | record { eq = eq1 } = lem01 zero i le lem01 (suc n) zero () lem01 (suc n) (suc i) n≤i with is-B (fun← cn (suc i)) ... | no nisB = lem01 (suc n) i n≤i ... | yes isB with <-cmp (count-B (suc i)) (suc n) ... | tri< a ¬b ¬c = lem01 (suc n) i ? - ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = eq } + ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = ? } ... | tri> ¬a ¬b c = lem01 (suc n) i ?