Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/bijection.agda @ 1354:3e14418230bc
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 18 Jun 2023 20:17:50 +0900 |
| parents | ddbc0726f9bb |
| children | db8229569750 |
line wrap: on
line source
{-# OPTIONS --allow-unsolved-metas #-} module bijection where open import Level renaming ( zero to Zero ; suc to Suc ) open import Data.Nat open import Data.Maybe open import Data.List hiding ([_] ; sum ) open import Data.Nat.Properties open import Relation.Nullary open import Data.Empty open import Data.Unit using ( tt ; ⊤ ) open import Relation.Binary.Core hiding (_⇔_) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality open import logic open import nat -- record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where -- field -- fun← : S → R -- fun→ : R → S -- fiso← : (x : R) → fun← ( fun→ x ) ≡ x -- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x -- -- injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) -- injection R S f = (x y : R) → f x ≡ f y → x ≡ y open Bijection bi-trans : {n m l : Level} (R : Set n) (S : Set m) (T : Set l) → Bijection R S → Bijection S T → Bijection R T bi-trans R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x ) ; fiso← = λ x → trans (cong (λ k → fun← rs k) (fiso← st (fun→ rs x))) ( fiso← rs x) ; fiso→ = λ x → trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) } bid : {n : Level} (R : Set n) → Bijection R R bid {n} R = record { fun← = λ x → x ; fun→ = λ x → x ; fiso← = λ _ → refl ; fiso→ = λ _ → refl } bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S → Bijection S R bi-sym R S eq = record { fun← = fun→ eq ; fun→ = fun← eq ; fiso← = fiso→ eq ; fiso→ = fiso← eq } bi-inject← : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : S} → fun← rs x ≡ fun← rs y → x ≡ y bi-inject← rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso→ rs _) (fiso→ rs _) (cong (fun→ rs) eq) bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso← rs _) (fiso← rs _) (cong (fun← rs) eq) open import Relation.Binary.Structures bijIsEquivalence : {n : Level } → IsEquivalence (Bijection {n} {n}) bijIsEquivalence = record { refl = λ {R} → bid R ; sym = λ {R} {S} → bi-sym R S ; trans = λ {R} {S} {T} → bi-trans R S T } -- ¬ A = A → ⊥ -- -- famous diagnostic function -- diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool diag b n = not (fun← b n n) diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) diagn1 n dn = ¬t=f (diag b n ) ( begin not (diag b n) ≡⟨⟩ not (not (fun← b n n)) ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ not (fun← b (fun→ b (diag b)) n) ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ not (fun← b n n) ≡⟨⟩ diag b n ∎ ) where open ≡-Reasoning b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ b1 b = fun→ b (diag b) b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b) b-iso b = fiso← b _ -- -- ℕ <=> ℕ + 1 -- to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) to1 {n} {R} b = record { fun← = to11 ; fun→ = to12 ; fiso← = to13 ; fiso→ = to14 } where to11 : ⊤ ∨ R → ℕ to11 (case1 tt) = 0 to11 (case2 x) = suc ( fun← b x ) to12 : ℕ → ⊤ ∨ R to12 zero = case1 tt to12 (suc n) = case2 ( fun→ b n) to13 : (x : ℕ) → to11 (to12 x) ≡ x to13 zero = refl to13 (suc x) = cong suc (fiso← b x) to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x to14 (case1 x) = refl to14 (case2 x) = cong case2 (fiso→ b x) open _∧_ record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) : Set where field j k : ℕ k1 : nxn→n j k ≡ i nn-unique : {j0 k0 : ℕ } → nxn→n j0 k0 ≡ i → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0 i≤0→i≡0 {0} z≤n = refl nxn : Bijection ℕ (ℕ ∧ ℕ) nxn = record { fun← = λ p → nxn→n (proj1 p) (proj2 p) ; fun→ = n→nxn ; fiso← = λ i → NN.k1 (nn i) ; fiso→ = λ x → nn-id (proj1 x) (proj2 x) } where nxn→n : ℕ → ℕ → ℕ nxn→n zero zero = zero nxn→n zero (suc j) = j + suc (nxn→n zero j) nxn→n (suc i) zero = suc i + suc (nxn→n i zero) nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j)) nn : ( i : ℕ) → NN i nxn→n n→nxn : ℕ → ℕ ∧ ℕ n→nxn n = ⟪ NN.j (nn n) , NN.k (nn n) ⟫ k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ k0 {i} = refl nxn→n0 : { j k : ℕ } → nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 ) nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫ nxn→n0 {zero} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → 0 < k) (+-comm _ k) (s≤s z≤n))) nxn→n0 {(suc j)} {zero} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) nxn→n0 {(suc j)} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) nid20 : (i : ℕ) → i + (nxn→n 0 i) ≡ nxn→n i 0 nid20 zero = refl -- suc (i + (i + suc (nxn→n 0 i))) ≡ suc (i + suc (nxn→n i 0)) nid20 (suc i) = begin suc (i + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (i + k)) (sym (+-assoc i 1 (nxn→n 0 i))) ⟩ suc (i + ((i + 1) + nxn→n 0 i)) ≡⟨ cong (λ k → suc (i + (k + nxn→n 0 i))) (+-comm i 1) ⟩ suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i) ⟩ suc (i + suc (nxn→n i 0)) ∎ where open ≡-Reasoning nid4 : {i j : ℕ} → i + 1 + j ≡ i + suc j nid4 {zero} {j} = refl nid4 {suc i} {j} = cong suc (nid4 {i} {j} ) nid5 : {i j k : ℕ} → i + suc (suc j) + suc k ≡ i + suc j + suc (suc k ) nid5 {zero} {j} {k} = begin suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩ 1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩ (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩ suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩ suc j + suc (suc k) ∎ where open ≡-Reasoning nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} ) -- increment in the same stage nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j nid2 zero zero = refl nid2 zero (suc j) = refl nid2 (suc i) zero = begin suc (nxn→n (suc i) 1) ≡⟨ refl ⟩ suc (suc (i + 1 + suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (suc k)) nid4 ⟩ suc (suc (i + suc (suc (nxn→n i 1)))) ≡⟨ cong (λ k → suc (suc (i + suc (suc k)))) (nid3 i) ⟩ suc (suc (i + suc (suc (i + suc (nxn→n i 0))))) ≡⟨ refl ⟩ nxn→n (suc (suc i)) zero ∎ where open ≡-Reasoning nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0) nid3 zero = refl nid3 (suc i) = begin suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩ suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (i + suc (suc k))) (nid3 i) ⟩ suc (i + suc (suc (i + suc (nxn→n i 0)))) ∎ nid2 (suc i) (suc j) = begin suc (nxn→n (suc i) (suc (suc j))) ≡⟨ refl ⟩ suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j))))) ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩ suc (suc (i + suc (suc j) + suc (i + suc j + suc (nxn→n i (suc j))))) ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩ suc (suc (i + suc j + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩ nxn→n (suc (suc i)) (suc j) ∎ where open ≡-Reasoning -- increment the stage nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) nid00 zero = refl nid00 (suc i) = begin suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩ suc (suc (i + (nxn→n 0 (suc i)))) ≡⟨ refl ⟩ suc (suc (i + (i + suc (nxn→n 0 i)))) ≡⟨ cong suc (sym ( +-assoc 1 i (i + suc (nxn→n 0 i)))) ⟩ suc ((1 + i) + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (k + (i + suc (nxn→n 0 i)))) (+-comm 1 i) ⟩ suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩ suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning ----- -- -- create the invariant NN for all n -- nn zero = record { j = 0 ; k = 0 ; k1 = refl ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } nn (suc i) with NN.k (nn i) | inspect NN.k (nn i) ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 ; k1 = nn02 ; nn-unique = nn04 } where --- --- increment the stage --- sum = NN.j (nn i) + NN.k (nn i) stage = minus i (NN.j (nn i)) j = NN.j (nn i) NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum NNnn = sym refl nn02 : nxn→n 0 (suc sum) ≡ suc i nn02 = begin sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩ (sum + 1) + nxn→n 0 sum ≡⟨ cong (λ k → k + nxn→n 0 sum ) (+-comm sum 1 )⟩ suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩ suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NNnn )) ⟩ suc (nxn→n (NN.j (nn i) + (NN.k (nn i)) ) 0) ≡⟨ cong₂ (λ j k → suc (nxn→n (NN.j (nn i) + j) k )) eq (sym eq) ⟩ suc (nxn→n (NN.j (nn i) + 0 ) (NN.k (nn i))) ≡⟨ cong (λ k → suc ( nxn→n k (NN.k (nn i)))) (+-comm (NN.j (nn i)) 0) ⟩ suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩ suc i ∎ where open ≡-Reasoning nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (sum ) ⟫ ≡ ⟪ j0 , k0 ⟫ nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- nn07 : nxn→n k0 0 ≡ i nn07 = cong pred ( begin suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩ nxn→n 0 (suc k0 ) ≡⟨ eq1 ⟩ suc i ∎ ) where open ≡-Reasoning nn08 : k0 ≡ sum nn08 = begin k0 ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩ NN.j (nn i) ≡⟨ +-comm 0 _ ⟩ NN.j (nn i) + 0 ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ sum ∎ where open ≡-Reasoning nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where nn05 : nxn→n j0 (suc k0) ≡ i nn05 = begin nxn→n j0 (suc k0) ≡⟨ cong pred ( begin suc (nxn→n j0 (suc k0)) ≡⟨ nid2 j0 k0 ⟩ nxn→n (suc j0) k0 ≡⟨ eq1 ⟩ suc i ∎ ) ⟩ i ∎ where open ≡-Reasoning nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ nn06 = NN.nn-unique (nn i) ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where --- --- increment in a stage --- sum = NN.j (nn i) + NN.k (nn i) stage = minus i (NN.j (nn i)) j = NN.j (nn i) NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum NNnn = sym refl nn10 : suc (NN.j (nn i)) + k ≡ sum nn10 = begin suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _) ⟩ (NN.j (nn i) + 1) + k ≡⟨ +-assoc (NN.j (nn i)) 1 k ⟩ NN.j (nn i) + suc k ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ sum ∎ where open ≡-Reasoning nn11 : nxn→n (suc (NN.j (nn i))) k ≡ suc i -- nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i nn11 = begin nxn→n (suc (NN.j (nn i))) k ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩ suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k → suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩ suc (nxn→n ( NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i)) ⟩ suc i ∎ where open ≡-Reasoning nn18 : zero < NN.k (nn i) nn18 = subst (λ k → 0 < k ) ( begin suc k ≡⟨ sym eq ⟩ NN.k (nn i) ∎ ) (s≤s z≤n ) where open ≡-Reasoning nn13 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫ nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where -- (nxn→n zero (suc k0)) ≡ suc i nn16 : nxn→n k0 zero ≡ i nn16 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid00 k0 )) eq1 ) nn17 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ k0 , zero ⟫ nn17 = NN.nn-unique (nn i) nn16 nn13 {suc j0} {k0} eq1 = begin ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩ ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡⟨ nn15 ⟩ ⟪ j0 , suc k0 ⟫ ∎ ) ⟩ ⟪ suc j0 , k0 ⟫ ∎ where -- nxn→n (suc j0) k0 ≡ suc i open ≡-Reasoning nn14 : nxn→n j0 (suc k0) ≡ i nn14 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid2 j0 k0 )) eq1 ) nn15 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ nn15 = NN.nn-unique (nn i) nn14 nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫ nn-id j k = begin n→nxn (nxn→n j k) ≡⟨ refl ⟩ ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩ ⟪ j , k ⟫ ∎ where open ≡-Reasoning -- [] 0 -- 0 → 1 -- 1 → 2 -- 01 → 3 -- 11 → 4 -- ... -- -- binary invariant -- record LB (n : ℕ) (lton : List Bool → ℕ ) : Set where field nlist : List Bool isBin : lton nlist ≡ n isUnique : (x : List Bool) → lton x ≡ n → nlist ≡ x lb+1 : List Bool → List Bool lb+1 [] = false ∷ [] lb+1 (false ∷ t) = true ∷ t lb+1 (true ∷ t) = false ∷ lb+1 t lb-1 : List Bool → List Bool lb-1 [] = [] lb-1 (true ∷ t) = false ∷ t lb-1 (false ∷ t) with lb-1 t ... | [] = true ∷ [] ... | x ∷ t1 = true ∷ x ∷ t1 LBℕ : Bijection ℕ ( List Bool ) LBℕ = record { fun← = λ x → lton x ; fun→ = λ n → LB.nlist (lb n) ; fiso← = λ n → LB.isBin (lb n) ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl } where lton1 : List Bool → ℕ lton1 [] = 1 lton1 (true ∷ t) = suc (lton1 t + lton1 t) lton1 (false ∷ t) = lton1 t + lton1 t lton : List Bool → ℕ lton x = pred (lton1 x) lton1>0 : (x : List Bool ) → 0 < lton1 x lton1>0 [] = a<sa lton1>0 (true ∷ x₁) = 0<s lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y 2lton1>0 : (t : List Bool ) → 0 < lton1 t + lton1 t 2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y lb=3 : {x y : ℕ} → 0 < x → 0 < y → 1 ≤ pred (x + y) lb=3 {suc x} {suc y} (s≤s 0<x) (s≤s 0<y) = subst (λ k → 1 ≤ k ) (+-comm (suc y) _ ) (s≤s z≤n) lton-cons>0 : {x : Bool} {y : List Bool } → 0 < lton (x ∷ y) lton-cons>0 {true} {[]} = refl-≤s lton-cons>0 {true} {x ∷ y} = ≤-trans ( lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y))) px≤x lton-cons>0 {false} {[]} = refl-≤ lton-cons>0 {false} {x ∷ y} = lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y)) lb=0 : {x y : ℕ } → pred x < pred y → suc (x + x ∸ 1) < suc (y + y ∸ 1) lb=0 {0} {suc y} lt = s≤s (subst (λ k → 0 < k ) (+-comm (suc y) y ) 0<s) lb=0 {suc x} {suc y} lt = begin suc (suc ((suc x + suc x) ∸ 1)) ≡⟨ refl ⟩ suc (suc x) + suc x ≡⟨ refl ⟩ suc (suc x + suc x) ≤⟨ <-plus (s≤s lt) ⟩ suc y + suc x <⟨ <-plus-0 {suc x} {suc y} {suc y} (s≤s lt) ⟩ suc y + suc y ≡⟨ refl ⟩ suc ((suc y + suc y) ∸ 1) ∎ where open ≤-Reasoning lb=2 : {x y : ℕ } → pred x < pred y → suc (x + x ) < suc (y + y ) lb=2 {zero} {suc y} lt = s≤s 0<s lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt) lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y lb=1 {x} {y} {true} eq with <-cmp (lton x) (lton y) ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=2 {lton1 x} {lton1 y} a)) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=2 {lton1 y} {lton1 x} c)) lb=1 {x} {y} {false} eq with <-cmp (lton x) (lton y) ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=0 {lton1 x} {lton1 y} a)) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c)) --- --- lton is unique in a head --- lb-tf : {x y : List Bool } → ¬ (lton (true ∷ x) ≡ lton (false ∷ y)) lb-tf {x} {y} eq with <-cmp (lton1 x) (lton1 y) ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (lb=01 a)) where lb=01 : {x y : ℕ } → x < y → x + x < (y + y ∸ 1) lb=01 {x} {y} x<y = begin suc (x + x) ≡⟨ refl ⟩ suc x + x ≤⟨ ≤-plus x<y ⟩ y + x ≡⟨ refl ⟩ pred (suc y + x) ≡⟨ cong (λ k → pred ( k + x)) (+-comm 1 y) ⟩ pred ((y + 1) + x ) ≡⟨ cong pred (+-assoc y 1 x) ⟩ pred (y + suc x) ≤⟨ px≤py (≤-plus-0 {suc x} {y} {y} x<y) ⟩ (y + y) ∸ 1 ∎ where open ≤-Reasoning ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (lb=02 c) ) where lb=02 : {x y : ℕ } → x < y → x + x ∸ 1 < y + y lb=02 {0} {y} lt = ≤-trans lt x≤x+y lb=02 {suc x} {y} lt = begin suc ( suc x + suc x ∸ 1 ) ≡⟨ refl ⟩ suc x + suc x ≤⟨ ≤-plus {suc x} (<to≤ lt) ⟩ y + suc x ≤⟨ ≤-plus-0 (<to≤ lt) ⟩ y + y ∎ where open ≤-Reasoning ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (sym eq) ( begin suc (lton1 y + lton1 y ∸ 1) ≡⟨ sucprd ( 2lton1>0 y) ⟩ lton1 y + lton1 y ≡⟨ cong (λ k → k + k ) (sym b) ⟩ lton1 x + lton1 x ∎ )) where open ≤-Reasoning --- --- lton injection --- lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y lb=b [] [] eq = refl lb=b [] (x ∷ y) eq = ⊥-elim ( nat-≡< eq (lton-cons>0 {x} {y} )) lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} )) lb=b (true ∷ x) (false ∷ y) eq = ⊥-elim ( lb-tf {x} {y} eq ) lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) ) lb=b (true ∷ x) (true ∷ y) eq = cong (λ k → true ∷ k ) (lb=b x y (lb=1 {x} {y} {true} eq)) lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq)) lb : (n : ℕ) → LB n lton lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x lb05 x eq = lb=b [] x (sym eq) lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where open ≡-Reasoning lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n lb10 = begin lton (false ∷ []) ≡⟨ refl ⟩ suc 0 ≡⟨ refl ⟩ suc (lton []) ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩ suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n) ) ⟩ suc n ∎ lb06 : (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x ... | false ∷ t | record { eq = eq } = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where lb01 : lton (true ∷ t) ≡ suc n lb01 = begin lton (true ∷ t) ≡⟨ refl ⟩ lton1 t + lton1 t ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩ suc (pred (lton1 t + lton1 t )) ≡⟨ refl ⟩ suc (lton (false ∷ t)) ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩ suc (lton (LB.nlist (lb n))) ≡⟨ cong suc (LB.isBin (lb n)) ⟩ suc n ∎ where open ≡-Reasoning lb09 : (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x ... | true ∷ t | record { eq = eq } = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where lb03 : lton (true ∷ t) ≡ n lb03 = begin lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩ n ∎ where open ≡-Reasoning add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc (x1 + x1)) add11 zero = refl add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x))) lb04 : (t : List Bool) → suc (lton1 t) ≡ lton1 (lb+1 t) lb04 [] = refl lb04 (false ∷ t) = refl lb04 (true ∷ []) = refl lb04 (true ∷ t0 @ (_ ∷ _)) = begin suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩ suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0 ) ⟩ lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎ where open ≡-Reasoning lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n lb02 [] refl = refl lb02 (t @ (_ ∷ _)) eq1 = begin lton (lb+1 t) ≡⟨ refl ⟩ pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩ pred (suc (lton1 t)) ≡⟨ sym (sucprd (lton1>0 t)) ⟩ suc (pred (lton1 t)) ≡⟨ refl ⟩ suc (lton t) ≡⟨ cong suc eq1 ⟩ suc n ∎ where open ≡-Reasoning lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1)) -- Bernstein is non constructive, so we cannot use this without some assumption -- but in case of ℕ, we can construct it directly. open import Data.Product open import Relation.Nary using (⌊_⌋) open import Relation.Nullary.Decidable hiding (⌊_⌋) open import Data.Unit.Base using (⊤ ; tt) open import Data.List.Fresh hiding ([_]) open import Data.List.Fresh.Relation.Unary.Any open import Data.List.Fresh.Relation.Unary.All record InjectiveF (A B : Set) : Set where field f : A → B inject : {x y : A} → f x ≡ f y → x ≡ y record Is (A C : Set) (f : A → C) (c : C) : Set where field a : A fa=c : f a ≡ c Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ → (fi : InjectiveF A B ) → (gi : InjectiveF B C ) → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c) ) → Bijection B ℕ Countable-Bernstein A B C an cn fi gi is-A is-B = record { fun→ = λ x → bton x ; fun← = λ n → ntob n ; fiso→ = λ n → ? ; fiso← = λ x → ? } where -- -- an f g cn -- ℕ ↔ A → B → C ↔ ℕ -- open Bijection f = InjectiveF.f fi g = InjectiveF.f gi -- -- count number of valid A and B in C -- the count of B is the numner of B in Bijection B ℕ -- if we have a , number a of A is larger than the numner of B C, so we have the inverse -- count-B : ℕ → ℕ count-B zero with is-B (fun← cn zero) ... | yes isb = 1 ... | no nisb = 0 count-B (suc n) with is-B (fun← cn (suc n)) ... | yes isb = suc (count-B n) ... | no nisb = count-B n bton : B → ℕ bton b = count-B (fun→ cn (g b)) count-A : ℕ → ℕ count-A zero with is-A (fun← cn zero) ... | yes isb = 1 ... | no nisb = 0 count-A (suc n) with is-A (fun← cn (suc n)) ... | yes isb = suc (count-A n) ... | no nisb = count-A n count-A-mono : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j count-A-mono {i} {j} i≤j with ≤-∨ i≤j ... | case1 refl = ≤-refl ... | case2 i<j = lem00 _ _ i<j where lem00 : (i j : ℕ) → i < j → count-A i ≤ count-A j lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-mono i<j) (lem01 j) where lem01 : (j : ℕ) → count-A j ≤ count-A (suc j) lem01 zero with is-A (fun← cn (suc zero)) ... | yes isb = refl-≤s ... | no nisb = ≤-refl lem01 (suc n) with is-A (fun← cn (suc (suc n))) ... | yes isb = refl-≤s ... | no nisb = ≤-refl count-A<i : (i : ℕ) → count-A i ≤ suc i count-A<i zero with is-A (fun← cn zero) | inspect ( count-A ) zero ... | yes isa | record { eq = eq1 } = ≤-refl ... | no nisa | record { eq = eq1 } = refl-≤s count-A<i (suc i) with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) ... | yes isa | record { eq = eq1 } = s≤s ( count-A<i i ) ... | no nisa | record { eq = eq1 } = ≤-trans (count-A<i i ) refl-≤s full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i) full-a zero i<ci with is-A (fun← cn zero) | inspect ( count-A ) zero ... | yes isa | record { eq = eq1 } = isa ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≡< refl i<ci ) full-a (suc i) i<ci with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) ... | yes isa | record { eq = eq1 } = isa ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans lem36 lem39) a<sa ) where lem36 : suc (suc i) ≤ count-A i lem36 = i<ci lem39 : count-A i ≤ suc i lem39 = count-A<i i ¬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 lem : g (f (Is.a isa)) ≡ y lem = begin g (f (Is.a isa)) ≡⟨ Is.fa=c isa ⟩ y ∎ where open ≡-Reasoning ca≤cb0 : (n : ℕ) → count-A n ≤ count-B n ca≤cb0 zero with is-A (fun← cn zero) | is-B (fun← cn zero) ... | yes isA | yes isB = ≤-refl ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) ... | no nisA | yes isB = px≤x ... | no nisA | no nisB = ≤-refl ca≤cb0 (suc n) with is-A (fun← cn (suc n)) | is-B (fun← cn (suc n)) ... | yes isA | yes isB = s≤s (ca≤cb0 n) ... | yes isA | no nisB = ⊥-elim ( ¬isA∧isB _ isA nisB ) ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x ... | no nisA | no nisB = ca≤cb0 n -- (c n) is -- fun→ c, where c contains all "a" less than n -- (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n) c : (n : ℕ) → ℕ c zero = fun→ cn (g (f (fun← an zero))) c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n) c< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n) c< zero zero (s≤s z≤n) = a<sa c< (suc i) zero (s≤s ()) c< zero (suc n) (s≤s z≤n) = ≤-trans (c< zero n (<-transʳ z≤n a<sa) ) (s≤s (y≤max (fun→ cn (g (f (fun← an (suc n))))) (c n))) c< (i @ (suc _)) (suc n) i≤n with ≤-∨ i≤n ... | case1 refl = s≤s (x≤max (fun→ cn (g (f (fun← an (suc n))))) (c n)) ... | case2 (s≤s (s≤s i<n)) = ≤-trans (c< i n (<-transʳ i<n a<sa)) (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (c n))) -- (c1 n i) is number of a which fun← an a ≤ n ∧ fun→ cn (g (f a)) < i ∧ g (f a) is A c1 : (n i : ℕ) → ℕ c1 zero i with <-cmp (fun→ cn (g (f (fun← an zero)))) i ... | tri< a ¬b ¬c = 1 ... | tri≈ ¬a b ¬c = 1 ... | tri> ¬a ¬b c₁ = 0 c1 (suc n) i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i ... | tri< a ¬b ¬c = suc (c1 n i) ... | tri≈ ¬a b ¬c = suc (c1 n i) ... | tri> ¬a ¬b c₁ = c1 n i c1-mono : {n i j : ℕ} → i ≤ j → (c1 n i ≡ c1 n j) ∨ (c1 n i < c1 n j) c1-mono {zero} {i} {j} le with <-cmp (fun→ cn (g (f (fun← an zero)))) i | <-cmp (fun→ cn (g (f (fun← an zero)))) j ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = case1 refl ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = case1 refl ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> le (<-trans c₁ a) ) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = case1 refl ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = case1 refl ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) le) c₁ ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = case2 ≤-refl ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = case2 ≤-refl ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = case1 refl c1-mono {suc n} {zero} {zero} z≤n = case1 refl c1-mono {suc n} {zero} {suc j} z≤n with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j) | c1-mono {n} {zero} {suc j} z≤n ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 ( s≤s le ) ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq) ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 ( s≤s le ) ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁) ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s ) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl ) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s ) ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case1 eq = case1 eq ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case2 le = case2 le c1-mono {suc n} {suc i} {suc j} (s≤s le) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j) | c1-mono {n} {suc i} {suc j} (s≤s le) ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case1 eq = case1 (cong suc eq) ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case2 le = case2 (s≤s le) ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case1 eq = case1 (cong suc eq) ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case2 le = case2 (s≤s le) ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> (s≤s le) (<-transˡ c₁ (≤-trans refl-≤s a ) )) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 (s≤s le) ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq) ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 (s≤s le) ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) (s≤s le)) c₁ ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s ) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl ) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s ) ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u c1-max : (n i : ℕ) → c n < i → c1 n i ≡ suc n c1-max zero i cn<i with <-cmp (fun→ cn (g (f (fun← an zero)))) i ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c₁ = ⊥-elim (c100 cn<i) where c100 : ¬ ( suc (fun→ cn (g ( f ( fun← an 0)))) ≤ i ) c100 f<i = nat-≤> (s≤s c₁) (<-transʳ f<i (<-trans a<sa a<sa)) c1-max (suc n) i cn<i = c101 where m<i : fun→ cn (g (f (fun← an (suc n)))) < i m<i = begin suc (fun→ cn (g (f (fun← an (suc n))))) ≤⟨ s≤s (x≤max _ _) ⟩ suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n)) ≤⟨ cn<i ⟩ i ∎ where open ≤-Reasoning c102 : c n < i c102 = begin suc (c n) ≤⟨ s≤s (y≤max _ _) ⟩ suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n)) ≤⟨ cn<i ⟩ i ∎ where open ≤-Reasoning c101 : c1 (suc n) i ≡ suc (suc n) c101 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i ... | tri< a ¬b ¬c = cong suc (c1-max n i c102 ) ... | tri≈ ¬a b ¬c = cong suc (c1-max n i c102 ) ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-<> c₁ m<i ) gf-is-a : (i : ℕ) → Is A C (λ i → g (f i)) (g (f (fun← an i))) gf-is-a i = record { a = fun← an i ; fa=c = refl } inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq ))) ani : (i : ℕ) → ℕ ani i = fun→ cn (g (f (fun← an i))) i-in-n : (i n : ℕ) → i ≤ n → Set i-in-n i n i≤n = c1 n (suc (c n)) ≤ i --- c1 n i c1+1P : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i))) → Set c1+1P n i isa with <-cmp n (fun→ an (Is.a isa)) ... | tri< n<an ¬b ¬c = c1 n i ≡ c1 n (suc i) ... | tri≈ ¬a n=an ¬c = suc (c1 n i) ≡ c1 n (suc i) ... | tri> ¬a ¬b an<n = suc (c1 n i) ≡ c1 n (suc i) c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i))) → c1+1P n i isa c1+1 0 i isa with <-cmp 0 (fun→ an (Is.a isa)) ... | tri< n<an ¬b ¬c = c123 where c123 : c1 zero i ≡ c1 zero (suc i) c123 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i) ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = refl ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> refl-≤s (<-trans c₁ a) ) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁ ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁)) ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< c126 n<an ) where open ≡-Reasoning c127 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ fun→ cn (g (f (fun← an 0))) c127 = begin fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩ fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩ fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩ suc i ≡⟨ sym b ⟩ fun→ cn (g (f (fun← an 0))) ∎ c126 : 0 ≡ fun→ an (Is.a isa) c126 = begin 0 ≡⟨ sym ( inject-cgf c127) ⟩ fun→ an (Is.a isa) ∎ ... | tri≈ ¬a n=an ¬c = c124 where open ≡-Reasoning c125 : fun→ cn (g (f (fun← an 0))) ≡ suc i c125 = begin fun→ cn (g (f (fun← an 0))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) n=an ⟩ fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩ fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩ fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩ suc i ∎ c124 : suc (c1 zero i) ≡ c1 zero (suc i) c124 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i) ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≤> a (<-trans a<sa (subst (λ k → suc i < suc k ) (sym c125) (s≤s a<sa) ))) ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (sym b) (subst (λ k → i < k) (sym c125) a<sa )) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = refl ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = refl ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⊥-elim ( ¬b₁ c125 ) c1+1 (suc n) i isa with <-cmp (suc n) (fun→ an (Is.a isa)) ... | tri< n<an ¬b ¬c = c115 where open ≡-Reasoning c110 : c1 n i ≡ c1 n (suc i) c110 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa ... | tri< a ¬b ¬c | s = s ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (<-trans a<sa n<an )) ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≤> c₁ (<-trans (<-trans a<sa a<sa) (<-transʳ n<an a<sa ) )) c115 : c1 (suc n) i ≡ c1 (suc n) (suc i) c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i) ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc c110 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc c110 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) )) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c110 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c110 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁ ) ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a)) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< c130 n<an) where c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i c118 = b c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ suc i c128 = begin fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩ fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩ fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩ suc i ∎ c130 : suc n ≡ fun→ an (Is.a isa) c130 = inject-cgf (trans c118 (sym c128 )) ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c110 ... | tri≈ ¬a n=an ¬c = c115 where c111 : c1 n i ≡ c1 n (suc i) c111 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa ... | tri< a ¬b ¬c | s = s ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (subst (λ k → n < k ) n=an a<sa )) ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≡< (sym n=an) (<-trans c₁ a<sa )) open ≡-Reasoning c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ suc i c128 = begin fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩ fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩ fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩ suc i ∎ c129 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i c129 = begin fun→ cn (g (f (fun← an (suc n)))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) n=an ⟩ fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩ fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩ fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩ suc i ∎ c115 : suc (c1 (suc n) i) ≡ c1 (suc n) (suc i) c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i) ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< c129 (<-trans a a<sa )) ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (trans (sym b) c129) a<sa ) ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a)) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = cong suc c111 ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⊥-elim ( nat-≡< (sym c129) c₂ ) ... | tri> ¬a ¬b an<n = c115 where c112 : suc (c1 n i) ≡ c1 n (suc i) c112 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa ... | tri< a ¬b ¬c | s = ⊥-elim (nat-≤> an<n (<-transʳ a a<sa) ) ... | tri≈ ¬a b ¬c | s = s ... | tri> ¬a ¬b c₁ | s = s open ≡-Reasoning c115 : suc (c1 (suc n) i) ≡ c1 (suc n) (suc i) c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i) ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc c112 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc c112 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) )) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c112 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c112 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁ ) ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a)) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym c130) an<n ) where c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i c118 = b c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ suc i c128 = begin fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩ fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩ fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩ suc i ∎ c130 : suc n ≡ fun→ an (Is.a isa) c130 = inject-cgf (trans c118 (sym c128 )) ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c112 c1+0 : {n i : ℕ} → ¬ Is A C (λ x → g (f x)) (fun← cn (suc i)) → c1 n i ≡ c1 n (suc i) c1+0 {zero} {i} nisa with <-cmp (fun→ cn (g (f (fun← an zero)))) i | <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i) ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = refl ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-trans c₁ a) ) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁ ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁)) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = c00 } ) where open ≡-Reasoning c00 : g (f (fun← an 0)) ≡ fun← cn (suc i) c00 = begin g (f (fun← an 0)) ≡⟨ sym (fiso← cn _) ⟩ fun← cn (fun→ cn (g (f (fun← an 0)))) ≡⟨ cong (fun← cn) b ⟩ fun← cn (suc i) ∎ ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl c1+0 {suc n} {zero} nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc zero) | c1+0 {n} {zero} nisa ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq = (cong suc eq) ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq = (cong suc eq) ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁) ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁)) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where open ≡-Reasoning c00 : g (f (fun← an (suc n))) ≡ fun← cn 1 c00 = begin g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩ fun← cn (fun→ cn (g (f (fun← an (suc n))))) ≡⟨ cong (fun← cn) b ⟩ fun← cn 1 ∎ ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | eq = eq c1+0 {suc n} {suc i} nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc (suc i)) | c1+0 {n} {suc i} nisa ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | eq = cong suc eq ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | eq = cong suc eq ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) )) ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq = cong suc eq ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq = cong suc eq ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁ ) ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁)) ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where open ≡-Reasoning c00 : g (f (fun← an (suc n))) ≡ fun← cn (suc (suc i)) c00 = begin g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩ fun← cn (fun→ cn (g (f (fun← an (suc n))))) ≡⟨ cong (fun← cn) b ⟩ fun← cn (suc (suc i)) ∎ ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u c1<count-A : (n i : ℕ) → c1 n i ≤ count-A i c1<count-A zero zero with is-A (fun← cn zero) | <-cmp (fun→ cn (g (f (fun← an zero)))) zero ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) }) ... | no nisa | tri> ¬a ¬b c₁ = ≤-refl ... | yes isa | tri≈ ¬a b ¬c = ≤-refl ... | yes isa | tri> ¬a ¬b c₁ = a≤sa c1<count-A (suc n) zero with is-A (fun← cn zero) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b ) } ) ... | no nisa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 0 lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero ... | tri> ¬a ¬b c₁ = ≤-refl ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } ) lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an (suc i) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } ) lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa) ... | yes isa | tri≈ ¬a b ¬c = lem01 n ≤-refl where lem01 : (i : ℕ) → i ≤ n → suc (c1 i 0) ≤ 1 lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero ... | tri> ¬a ¬b c₁ = ≤-refl ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa )) lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa )) lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa) ... | yes isa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 1 lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero ... | tri> ¬a ¬b c₁ = a≤sa ... | tri≈ ¬a bi ¬c = ≤-refl lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero ... | tri≈ ¬a bi ¬c = lem02 i ≤-refl where lem02 : (j : ℕ) → j ≤ i → suc (c1 j 0) ≤ 1 lem02 zero j≤i with <-cmp (fun→ cn (g (f (fun← an 0)))) zero ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ z≤n a<sa )) ... | tri> ¬a ¬b c₁ = ≤-refl lem02 (suc j) j≤i with <-cmp (fun→ cn (g (f (fun← an (suc j))))) zero ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ j≤i a<sa )) lem02 (suc j) (s≤s j≤i) | tri> ¬a ¬b c₁ = lem02 j (≤-trans j≤i a≤sa) lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa) c1<count-A zero (suc i) = ? c1<count-A (suc n) (suc i) with is-A (fun← cn (suc i)) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) ... | no nisa | tri< a ¬b ¬c = ? where -- subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where lem13 : c1 n i ≡ c1 n (suc i) lem13 = c1+0 {n} {i} nisa lem10 : c1 n i ≤ count-A i lem10 = c1<count-A n i lem12 : suc (c1 n (suc i)) ≤ count-A i -- becase count-A i contains (ani (suc n)) lem12 = ? ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim (nisa ? ) ... | no nisa | tri> ¬a ¬b c₁ = ? ... | yes isa | tri< a ¬b ¬c = ? -- count-A contains (suc i), so keep ≤-relation ... | yes isa | tri≈ ¬a b ¬c = ? ... | yes isa | tri> ¬a ¬b c₁ = ? record maxAC (n : ℕ) : Set where field ac : ℕ n<ca : n < count-A ac lem03 : (n : ℕ) → maxAC n lem03 n = record { ac = c1 n (suc (c n)) ; n<ca = ? } -- -- we have n C sequcence having n A which is less than c n as FList (c n) , so we have n -- c i = i th FL (c n) where -- ∃ j → i ≡ fun→ cn (g (f (fun← an j))) by FList n -- cm = count-A (c n) -- 0 < suc (count-A (c 0)) ≡ count-A (suc (c 0)) ≤ count-A (c 1) < ... < suc (count-A (c n)) ≤ count-A (c n) -- 0 < cm → 1 < cm → n < cm -- it means -- n < count-A (c n) -- cl07 : { i j : ℕ } → suc i < suc j → i < j cl07 {i} {j} (s≤s lt) = lt lem02 : (n : ℕ) → maxAC n lem02 n = record { ac = c n ; n<ca = n<ca n } where ca+1 : (i : ℕ) → i < fun→ cn (g (f (fun← an i))) → count-A i < count-A (fun→ cn (g (f (fun← an i)))) ca+1 i i<ca with fun→ cn (g (f (fun← an i))) | inspect (fun→ cn) (g (f (fun← an i))) ... | suc ca | record { eq = eq1 } with is-A (fun← cn (suc ca)) ... | yes isa = <-transʳ ( count-A-mono (px≤py i<ca)) cl22 where cl22 : count-A (pred (suc ca)) < suc (count-A ca) cl22 = ≤-refl ... | no nisa = ⊥-elim ( nisa record { a = fun← an i ; fa=c = cl21 } ) where cl21 : g (f ( fun← an i)) ≡ fun← cn (suc ca) cl21 = begin g (f ( fun← an i)) ≡⟨ sym (fiso← cn _) ⟩ fun← cn (fun→ cn (g (f ( fun← an i)))) ≡⟨ cong (fun← cn) eq1 ⟩ fun← cn (suc ca) ∎ where open ≡-Reasoning n<ca : (n : ℕ ) → n < count-A (c n) n<ca zero with fun→ cn (g (f (fun← an zero))) | inspect (fun→ cn) (g (f (fun← an zero))) ... | zero | record { eq = eq1 } = cl23 where cl23 : 1 ≤ count-A zero cl23 = ? ... | suc ca | record { eq = eq1 } = cl24 where cl24 : 1 ≤ count-A (suc ca) cl24 = ? n<ca (suc n) with <-cmp (c n) (fun→ cn (g (f (fun← an (suc n))))) ... | tri< ca<an ¬b ¬c = ? where cl26 : n < count-A (c n) cl26 = n<ca n cl25 : suc (suc n) ≤ count-A (fun→ cn (g (f (fun← an (suc n))))) cl25 = begin suc (suc n) ≤⟨ s≤s (n<ca n) ⟩ suc (count-A (c n)) ≤⟨ s≤s (count-A-mono ( sx≤py→x≤y ( begin suc (c n) ≤⟨ ca<an ⟩ fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))) ≤⟨ ? ⟩ suc (pred (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))))) ∎ ) )) ⟩ suc (count-A (pred (fun→ cn (g (f (fun← an (suc n))))))) ≡⟨ ? ⟩ count-A (fun→ cn (g (f (fun← an (suc n))))) ∎ where open ≤-Reasoning ... | tri≈ ¬a ca=an ¬c = ? ... | tri> ¬a ¬b an<ca = ? where cl25 : suc (suc n) ≤ count-A (max (fun→ cn (g (f (fun← an (suc n))))) (c n)) cl25 = ? cl27 : fun→ cn (g (f (fun← an (suc n) )) ) < c (suc n) cl27 = ? cl26 : fun→ cn (g (f (fun← an ? )) ) < fun→ cn (g (f (fun← an (suc n)))) cl26 = ? -- -- count-A (c m) < count (c (suc m)) ≤ count (c n) -- fun→ cn (g (f (fun← an i))) < suc (fun→ cn (g (f (fun← an (suc n))))) ≤ fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n -- c i c (suc i) c n -- fun→ cn (g (f (fun← an i))) < fun→ cn (g (f (fun← an (suc n)))) < fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n -- c i c (suc i) c (suc (suc i)) c (suc n) -- count-A (c m) = count-A (c (suc m)) count-A (c (suc m)) < count (c (suc (suc m)) ≤ count (c (suc n)) record CountB (n : ℕ) : Set where field b : B cb : ℕ b=cn : fun← cn cb ≡ g b cb=n : count-B cb ≡ 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 (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 ¬b c = lem01 (suc n) i ? 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))) )) biso : (n : ℕ) → bton (ntob n) ≡ n biso n = ? -- lem03 _ (≤-trans (maxAC.n<ca (lem02 n )) ?) refl biso1 : (b : B) → ntob (bton b) ≡ b biso1 b = ? 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 { fun← = λ x → ⟪ fun← ab (proj1 x) , fun← cd (proj2 x) ⟫ ; fun→ = λ n → ⟪ fun→ ab (proj1 n) , fun→ cd (proj2 n) ⟫ ; fiso← = lem0 ; fiso→ = lem1 } where open Bijection lem0 : (x : A ∧ C) → ⟪ fun← ab (fun→ ab (proj1 x)) , fun← cd (fun→ cd (proj2 x)) ⟫ ≡ x lem0 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso← ab x) (fiso← cd y) lem1 : (x : B ∧ D) → ⟪ fun→ ab (fun← ab (proj1 x)) , fun→ cd (fun← cd (proj2 x)) ⟫ ≡ x lem1 ⟪ x , y ⟫ = cong₂ ⟪_,_⟫ (fiso→ ab x) (fiso→ cd y) LM1 : (A : Set ) → Bijection (List A ) ℕ → Bijection (List A ∧ List Bool) ℕ LM1 A Ln = bi-trans (List A ∧ List Bool) (ℕ ∧ ℕ) ℕ (bi-∧ Ln (bi-sym _ _ LBℕ) ) (bi-sym _ _ nxn) open import Data.List.Properties open import Data.Maybe.Properties --- ℕ ⊆ List A ⊆ List (Maybe A) ⊆ List A ∧ List Bool ⊆ ℕ LMℕ : (A : Set ) → Bijection (List A) ℕ → Bijection (List (Maybe A)) ℕ LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi ? ? where f : List A → List (Maybe A) f [] = [] f (x ∷ t) = just x ∷ f t f-inject : {x y : List A} → f x ≡ f y → x ≡ y f-inject {[]} {[]} refl = refl f-inject {x ∷ xt} {y ∷ yt} eq = cong₂ (λ j k → j ∷ k ) (just-injective (∷-injectiveˡ eq)) (f-inject (∷-injectiveʳ eq) ) g : List (Maybe A) → List A ∧ List Bool g [] = ⟪ [] , [] ⟫ g (just h ∷ t) = ⟪ h ∷ proj1 (g t) , true ∷ proj2 (g t) ⟫ g (nothing ∷ t) = ⟪ proj1 (g t) , false ∷ proj2 (g t) ⟫ g⁻¹ : List A ∧ List Bool → List (Maybe A) g⁻¹ ⟪ [] , [] ⟫ = [] g⁻¹ ⟪ x ∷ xt , [] ⟫ = just x ∷ g⁻¹ ⟪ xt , [] ⟫ g⁻¹ ⟪ [] , true ∷ y ⟫ = [] g⁻¹ ⟪ x ∷ xt , true ∷ yt ⟫ = just x ∷ g⁻¹ ⟪ xt , yt ⟫ g⁻¹ ⟪ [] , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ [] , y ⟫ g⁻¹ ⟪ x ∷ x₁ , false ∷ y ⟫ = nothing ∷ g⁻¹ ⟪ x ∷ x₁ , y ⟫ g-iso : {x : List (Maybe A)} → g⁻¹ (g x) ≡ x g-iso {[]} = refl g-iso {just x ∷ xt} = cong ( λ k → just x ∷ k) ( g-iso ) g-iso {nothing ∷ []} = refl g-iso {nothing ∷ just x ∷ xt} = cong (λ k → nothing ∷ k ) ( g-iso {_} ) g-iso {nothing ∷ nothing ∷ xt} with g-iso {nothing ∷ xt} ... | t = trans (lemma01 (proj1 (g xt)) (proj2 (g xt)) ) ( cong (λ k → nothing ∷ k ) t ) where lemma01 : (x : List A) (y : List Bool ) → g⁻¹ ⟪ x , false ∷ false ∷ y ⟫ ≡ nothing ∷ g⁻¹ ⟪ x , false ∷ y ⟫ lemma01 [] y = refl lemma01 (x ∷ x₁) y = refl g-inject : {x y : List (Maybe A)} → g x ≡ g y → x ≡ y g-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) g-iso g-iso (cong g⁻¹ eq ) fi : InjectiveF (List A) (List (Maybe A)) fi = record { f = f ; inject = f-inject } gi : InjectiveF (List (Maybe A)) (List A ∧ List Bool ) gi = record { f = g ; inject = g-inject } -- open import Data.Fin -- --- LBFin : {n : ℕ } → Bijection (List (Meybe (Fin n))) ( List (Fin (suc n))) -- --- LBFin : {n : ℕ } → Bijection ℕ ( List (Fin n)) --- LBFin = ? --