Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1371:8b66575d4939
lem06
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 22 Jun 2023 07:38:29 +0900 |
| parents | 3bcff593255e |
| children | 4b7a756dae33 |
| files | src/bijection.agda src/nat.agda |
| diffstat | 2 files changed, 23 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Wed Jun 21 17:05:15 2023 +0900 +++ b/src/bijection.agda Thu Jun 22 07:38:29 2023 +0900 @@ -685,26 +685,37 @@ -- induction on n is no good, because (ani (suc n)) may happen in clist (c n) -- so we cannot recurse on n<ca-list itself. -- + del : (i : ℕ) → (cl : List C) → any-cl i cl → List C -- del 0 contains ani 0 - del = ? + del i cl a = a-list i cl (a i ≤-refl) del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl) → any-cl i (del (suc i) cl a ) - del-any = ? + del-any i cl a j le = lem41 cl (del (suc i) cl a ) (a (suc i) ≤-refl ) (a j (≤-trans le a≤sa) ) refl where + lem41 : (cl dl : List C) + → (ai : Any (_≡_ (g (f (fun← an (suc i))))) cl) + → (aj : Any (_≡_ (g (f (fun← an j)))) cl) + → dl ≡ a-list (suc i) cl ai → Any (_≡_ (g (f (fun← an j)))) dl + lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡< + ( bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) (x≤y→x<sy le) ) + lem41 (h ∷ t) y (here px) (there b0) eq = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b0 + lem41 (h ∷ t) y (there a0) (here px) refl = here px + lem41 (h ∷ t) (x ∷ y) (there a0) (there b0) refl = there (lem41 t (a-list (suc i) t a0) a0 b0 refl) + del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl ) - → suc (ca-list cl) ≡ ca-list (del i cl a) - del-ca = ? + → 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 (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 (del (suc i) (del (suc (suc i)) cl a ) - (del-any (suc i) cl a) ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ - suc (ca-list (del (suc i) cl (del-any (suc i) cl a))) ≡⟨ del-ca (suc i) cl (del-any (suc i) cl a) ⟩ + 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)))
--- a/src/nat.agda Wed Jun 21 17:05:15 2023 +0900 +++ b/src/nat.agda Thu Jun 22 07:38:29 2023 +0900 @@ -280,6 +280,10 @@ x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le) x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl +x≤y→x<sy : {x y : ℕ } → x ≤ y → x < suc y +x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n) +x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le) + open import Data.Product