Mercurial > hg > Members > kono > Proof > automaton
changeset 337:78e094559ceb
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Jul 2023 11:52:28 +0900 |
| parents | 1bf4163de311 |
| children | 78e57f261954 |
| files | automaton-in-agda/src/bijection.agda automaton-in-agda/src/derive.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/nat.agda |
| diffstat | 4 files changed, 801 insertions(+), 97 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda Sun Jul 09 16:03:43 2023 +0900 +++ b/automaton-in-agda/src/bijection.agda Mon Jul 10 11:52:28 2023 +0900 @@ -1,5 +1,8 @@ +{-# 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 @@ -7,7 +10,7 @@ open import Data.Nat.Properties open import Relation.Nullary open import Data.Empty -open import Data.Unit hiding ( _≤_ ) +open import Data.Unit using ( tt ; ⊤ ) open import Relation.Binary.Core hiding (_⇔_) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality @@ -19,13 +22,13 @@ -- field -- fun← : S → R -- fun→ : R → S --- fiso← : (x : R) → fun← ( fun→ x ) ≡ x --- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x --- +-- 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 +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 ) @@ -33,27 +36,40 @@ ; 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 } +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-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 → ⊥ +-- ¬ A = A → ⊥ -- -- famous diagnostic function -- +-- 1 1 0 1 0 ... +-- 0 1 0 1 0 ... +-- 1 0 0 1 0 ... +-- 1 1 1 1 0 ... + +-- 0 0 1 0 1 ... diag + 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 : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n ) diagn1 n dn = ¬t=f (diag b n ) ( begin not (diag b n) ≡⟨⟩ @@ -63,17 +79,17 @@ ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ not (fun← b n n) ≡⟨⟩ - diag b n + diag b n ∎ ) where open ≡-Reasoning -b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ +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 +-- ℕ <=> ℕ + 1 (infinite hotel) -- to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R ) to1 {n} {R} b = record { @@ -102,16 +118,23 @@ field j k : ℕ k1 : nxn→n j k ≡ i - nn-unique : {j0 k0 : ℕ } → nxn→n j0 k0 ≡ i → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ + 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 +---- +-- (0, 0) (0, 1) (0, 2) .... +-- (1, 0) (1, 1) (1, 2) .... +-- (2, 0) (2, 1) (2, 2) .... +-- : : : +-- : : : +-- nxn : Bijection ℕ (ℕ ∧ ℕ) nxn = record { fun← = λ p → nxn→n (proj1 p) (proj2 p) - ; fun→ = n→nxn + ; fun→ = n→nxn ; fiso← = λ i → NN.k1 (nn i) ; fiso→ = λ x → nn-id (proj1 x) (proj2 x) } where @@ -120,10 +143,10 @@ 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 + 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 : ℕ } → 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 ) @@ -153,7 +176,7 @@ 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 : (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 @@ -178,7 +201,7 @@ open ≡-Reasoning -- increment the stage - nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i) + 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) ⟩ @@ -192,10 +215,10 @@ -- -- create the invariant NN for all n -- - nn zero = record { j = 0 ; k = 0 ; k1 = refl + 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 + 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 @@ -216,28 +239,28 @@ 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 -- + 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 + 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 + 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 + 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 ⟫ + 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 --- @@ -248,23 +271,23 @@ 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 : 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 + 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 + 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 + 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 @@ -273,7 +296,7 @@ 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 + ⟪ 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 @@ -304,24 +327,24 @@ field nlist : List Bool isBin : lton nlist ≡ n - isUnique : (x : List Bool) → lton x ≡ n → nlist ≡ x + 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 [] = 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 (true ∷ t) = false ∷ t lb-1 (false ∷ t) with lb-1 t ... | [] = true ∷ [] ... | x ∷ t1 = true ∷ x ∷ t1 -LBℕ : Bijection ℕ ( List Bool ) +LBℕ : Bijection ℕ ( List Bool ) LBℕ = record { - fun← = λ x → lton x - ; fun→ = λ n → LB.nlist (lb n) + 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 @@ -332,7 +355,7 @@ lton : List Bool → ℕ lton x = pred (lton1 x) - lton1>0 : (x : List Bool ) → 0 < 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 @@ -361,7 +384,7 @@ 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 : 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 @@ -388,7 +411,7 @@ (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 {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) ⟩ @@ -408,60 +431,60 @@ 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=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) + 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 ∎ + 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)) ⟩ + 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) ⟩ + 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 : (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 ) ⟩ + 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 + 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)) ⟩ @@ -470,4 +493,525 @@ 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)) + 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.List hiding ([_]) +open import Data.List.Relation.Unary.Any + +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→ = biso + ; fiso← = biso1 + } where + -- + -- an f g cn + -- ℕ ↔ A → B → C ↔ ℕ + -- B = Image A f ∪ (B \ Image A f ) + -- + 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 + + 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 + + ¬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 : ℕ) → fun→ cn (g (f (fun← an i))) ≤ c i + c< zero = ≤-refl + c< (suc i) = x≤max _ _ + + c-mono1 : (i : ℕ) → c i ≤ c (suc i) + c-mono1 i = y≤max _ _ + c-mono : (i j : ℕ ) → i ≤ j → c i ≤ c j + c-mono i j i≤j with ≤-∨ i≤j + ... | case1 refl = ≤-refl + c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j) + c-mono (suc i) (suc j) (s≤s i≤j) | case2 (s≤s lt) = ≤-trans (c-mono (suc i) j lt ) (c-mono1 j) + + 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))) + + ncfi = λ n → (fun→ cn (g (f (fun← an n) ))) + cfi = λ n → (g (f (fun← an n) )) + + clist : (n : ℕ) → List C + clist 0 = fun← cn 0 ∷ [] + clist (suc n) = fun← cn (suc n) ∷ clist n + + clist-more : {i j : ℕ} → i ≤ j → {c : C} → Any (_≡_ c) (clist i) → Any (_≡_ c) (clist j) + clist-more {zero} {zero} z≤n a = a + clist-more {zero} {suc n} i≤n a = there (clist-more {zero} {n} z≤n a) + clist-more {suc i} {suc n} (s≤s le) {c} (there a) = there (clist-more {i} {n} le a) + clist-more {suc i} {suc n} (s≤s le) {c} (here px) with ≤-∨ le + ... | case1 refl = here px + ... | case2 lt = there (clist-more {suc i} {n} lt {c} (here px) ) + + clist-any : (n i : ℕ) → i ≤ n → Any (_≡_ (g (f (fun← an i)))) (clist (c n)) + clist-any n i i≤n = clist-more (c-mono _ _ i≤n) (lem00 (c i) (c< i)) where + lem00 : (j : ℕ ) → fun→ cn (g (f (fun← an i))) ≤ j → Any (_≡_ (g (f (fun← an i)))) (clist j) + lem00 0 f≤j with ≤-∨ f≤j + ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq )) + ... | case2 le = ⊥-elim (nat-≤> z≤n le ) + lem00 (suc j) f≤j with ≤-∨ f≤j + ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq )) + ... | case2 (s≤s le) = there (lem00 j le) + + ca-list : List C → ℕ + ca-list [] = 0 + ca-list (h ∷ t) with is-A h + ... | yes _ = suc (ca-list t) + ... | no _ = ca-list t + + ca-list=count-A : (n : ℕ) → ca-list (clist n) ≡ count-A n + ca-list=count-A n = lem02 n (clist n) refl where + lem02 : (n : ℕ) → (cl : List C) → cl ≡ clist n → ca-list cl ≡ count-A n + lem02 zero [] () + lem02 zero (h ∷ t) refl with is-A (fun← cn zero) + ... | yes _ = refl + ... | no _ = refl + lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n)) + ... | yes _ = cong suc (lem02 n t refl) + ... | no _ = lem02 n t refl + + -- remove (ani i) from clist (c n) + -- + a-list : (i : ℕ) → (cl : List C) → Any (_≡_ (g (f (fun← an i)))) cl → List C + a-list i (_ ∷ t) (here px) = t + a-list i (h ∷ t) (there a) = h ∷ ( a-list i t a ) + + -- count of a in a-list is one step reduced + -- + a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) + → suc (ca-list (a-list i cl a)) ≡ ca-list cl + a-list-ca i cl a = lem03 i cl _ a refl where + lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) → cal ≡ (a-list i cl a) → suc (ca-list cal) ≡ ca-list cl + lem03 i (h ∷ t) (h1 ∷ t1) (here px) refl with is-A h + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } ) + lem03 i (h ∷ t) (h ∷ t1) (there ah) refl with is-A h + ... | yes y = cong suc (lem03 i t t1 ah refl) + ... | no _ = lem03 i t t1 ah refl + lem03 i (x ∷ []) [] (here px) refl with is-A x + ... | yes y = refl + ... | no nisa = ⊥-elim ( nisa record { a = _ ; fa=c = px } ) + + -- reduced list still have all ani j < i + -- + a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) + → (j : ℕ) → j < i → Any (_≡_ (g (f (fun← an j)))) cl → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a) + a-list-any i cl a j j<i b = lem03 i cl _ a refl j j<i b where + lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) + → cal ≡ (a-list i cl a) + → (j : ℕ) → j < i → Any (_≡_ (g (f (fun← an j)))) cl → Any (_≡_ (g (f (fun← an j)))) cal + lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡< + ( bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) j<i ) + lem03 i (h ∷ t) cal (here px) eq j j<i (there b) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b + lem03 i (h ∷ t) cal (there a) eq j j<i (here px) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) (here px) + lem03 i (h ∷ t) (h1 ∷ cal) (there a) refl j j<i (there b) = there (lem03 i t cal a refl j j<i b) + + any-cl : (i : ℕ) → (cl : List C) → Set + 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 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) + -- 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 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 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 (del i cl a)) ≡ ca-list cl + del-ca i cl a = a-list-ca i cl (a i ≤-refl) + + 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 + ac : ℕ + n<ca : n < count-A ac + + lem02 : (n : ℕ) → maxAC n + lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) } + + -- + -- countB record create ℕ → B and its injection + -- + record CountB (n : ℕ) : Set where + field + b : B + cb : ℕ + b=cn : fun← cn cb ≡ g b + cb=n : count-B cb ≡ suc n + cb-inject : (cb1 : ℕ) → Is B C g (fun← cn cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1 + + count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j + count-B-mono {i} {j} i≤j with ≤-∨ i≤j + ... | case1 refl = ≤-refl + ... | case2 i<j = lem00 _ _ i<j where + lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j + lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where + lem01 : (j : ℕ) → count-B j ≤ count-B (suc j) + lem01 zero with is-B (fun← cn (suc zero)) + ... | yes isb = refl-≤s + ... | no nisb = ≤-refl + lem01 (suc n) with is-B (fun← cn (suc (suc n))) + ... | yes isb = refl-≤s + ... | no nisb = ≤-refl + + lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n + lem01 n i le = lem09 i (count-B i) le refl where + -- injection of count-B + --- + lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j + lem06 i j bi bj eq = lem08 where + lem20 : (i j : ℕ) → i < j → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥ + lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (suc j)) | inspect count-B (suc j) + ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) + ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) + ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where + lem22 : 1 ≡ count-B 0 + lem22 with is-B (fun← cn 0) | inspect count-B 0 + ... | yes _ | record { eq = eq1 } = refl + ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem24 : count-B j ≡ 0 + lem24 = cong pred le + lem25 : 1 ≤ 0 + lem25 = begin + 1 ≡⟨ lem22 ⟩ + count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩ + count-B j ≡⟨ lem24 ⟩ + 0 ∎ where open ≤-Reasoning + lem20 (suc i) zero () bi bj le + lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ⊥-elim ( nat-≡< lem24 lem21 ) where + -- + -- i < suc i ≤ j + -- cb i < suc (cb i) < cb (suc i) ≤ cb j + -- suc (cb i) ≡ suc (cb j) → cb i ≡ cb j + lem22 : suc (count-B i) ≡ count-B (suc i) + lem22 with is-B (fun← cn (suc i)) | inspect count-B (suc i) + ... | yes _ | record { eq = eq1 } = refl + ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem23 : suc (count-B j) ≡ count-B (suc j) + lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j) + ... | yes _ | record { eq = eq1 } = refl + ... | no nisa | _ = ⊥-elim ( nisa bj ) + lem24 : count-B i ≡ count-B j + lem24 with is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j) + ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) + ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) + ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le) + lem21 : suc (count-B i) ≤ count-B j + lem21 = begin + suc (count-B i) ≡⟨ lem22 ⟩ + count-B (suc i) ≤⟨ count-B-mono i<j ⟩ + count-B j ∎ where + open ≤-Reasoning + lem08 : i ≡ j + lem08 with <-cmp i j + ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) ) + ... | tri≈ ¬a b ¬c = b + ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq ) + + 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 + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → 1 ≡ count-B cb1 → 0 ≡ cb1 + lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) + ... | 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 + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 + lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq) + ... | no nisb | record { eq = eq1 } = lem07 n i eq + + -- starting from 0, if count B i ≡ suc n, this is it + + lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n + lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) + ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq )) + ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0 + ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) + ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n)) + lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le) + ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq )) + ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i) + ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq) + ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq + + bton : B → ℕ + bton b = pred (count-B (fun→ cn (g b))) + + 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 = begin + bton (ntob n) ≡⟨ refl ⟩ + pred (count-B (fun→ cn (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (fun→ cn k))) ( CountB.b=cn CB)) ⟩ + pred (count-B (fun→ cn (fun← cn (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (fiso→ cn _) ⟩ + pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩ + pred (suc n) ≡⟨ refl ⟩ + n ∎ where + open ≡-Reasoning + CB = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ) + + -- + -- uniqueness of ntob is proved by injection + -- + biso1 : (b : B) → ntob (bton b) ≡ b + biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) + ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where + lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero + lem20 = eq1 + lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B i + lem21 0 eq with is-B (fun← cn 0) | inspect count-B 0 + ... | yes isb | record { eq = eq1 } = ≤-refl + ... | no nisb | record{ eq = eq1 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) + lem21 (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i) + ... | yes isb | record{ eq = eq2 } = s≤s z≤n + ... | no nisb | record{ eq = eq2 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) + ... | suc n | record { eq = eq1 } = begin + CountB.b CB ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin + fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩ + fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩ + CountB.cb CB ≡⟨ CountB.cb-inject CB _ record { a = b ; fa=c = sym (fiso← cn _) } (trans (CountB.cb=n CB) (sym eq1)) ⟩ + fun→ cn (InjectiveF.f gi b) ∎ )) ⟩ + b ∎ where + open ≡-Reasoning + CB = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) ) + +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 dec0 dec1 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 } + dec0 : (c : List A ∧ List Bool) → Dec (Is (List A) (List A ∧ List Bool) (λ x → g (f x)) c) + dec0 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl } + dec0 ⟪ h ∷ t , [] ⟫ = no ( lem00 ) where + lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , [] ⟫ → ⊥ + lem00 record { a = [] ; fa=c = () } + lem00 record { a = (x ∷ a) ; fa=c = () } + dec0 ⟪ [] , true ∷ bt ⟫ = no lem00 where + lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , true ∷ bt ⟫ → ⊥ + lem00 record { a = [] ; fa=c = () } + dec0 ⟪ [] , false ∷ bt ⟫ = no lem00 where + lem00 : Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ [] , false ∷ bt ⟫ → ⊥ + lem00 record { a = [] ; fa=c = () } + dec0 ⟪ h ∷ t , (true ∷ bt) ⟫ with dec0 ⟪ t , bt ⟫ + ... | yes y = yes record { a = h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } + ... | no n = no lem00 where + lem00 : ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , true ∷ bt ⟫ + lem00 record { a = (x ∷ a) ; fa=c = refl } = ⊥-elim ( n record { a = a ; fa=c = refl } ) + dec0 ⟪ (h ∷ t) , (false ∷ bt) ⟫ = no lem00 where + lem00 : ¬ Is (List A) (List A ∧ List Bool) (λ x → g (f x)) ⟪ h ∷ t , false ∷ bt ⟫ + lem00 record { a = [] ; fa=c = () } + lem00 record { a = (x ∷ a) ; fa=c = () } + dec1 : (c : List A ∧ List Bool) → Dec (Is (List (Maybe A)) (List A ∧ List Bool) g c) + dec1 ⟪ [] , [] ⟫ = yes record { a = [] ; fa=c = refl } + dec1 ⟪ h ∷ t , [] ⟫ = no lem00 where + lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , [] ⟫ + lem00 record { a = (just x ∷ a) ; fa=c = () } + lem00 record { a = (nothing ∷ a) ; fa=c = () } + dec1 ⟪ [] , true ∷ bt ⟫ = no lem00 where + lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , true ∷ bt ⟫ + lem00 record { a = (just x ∷ a) ; fa=c = () } + lem00 record { a = (nothing ∷ a) ; fa=c = () } + dec1 ⟪ [] , false ∷ bt ⟫ with dec1 ⟪ [] , bt ⟫ + ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) } + ... | no n = no lem00 where + lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ [] , false ∷ bt ⟫ + lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where + lem01 : proj2 (g a) ≡ bt + lem01 with cong proj2 eq + ... | refl = refl + dec1 ⟪ h ∷ t , true ∷ bt ⟫ with dec1 ⟪ t , bt ⟫ + ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } + ... | no n = no lem00 where + lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , true ∷ bt ⟫ + lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl } + dec1 ⟪ h ∷ t , false ∷ bt ⟫ with dec1 ⟪ h ∷ t , bt ⟫ + ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) } + ... | no n = no lem00 where + lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , false ∷ bt ⟫ + lem00 record { a = (nothing ∷ a) ; fa=c = eq } = n record { a = a ; fa=c = cong₂ (λ j k → ⟪ j , k ⟫) (cong proj1 eq) lem01 } where + lem01 : proj2 (g a) ≡ bt + lem01 with cong proj2 eq + ... | refl = refl + +-- +-- ( Bool ∷ Bool ∷ [] ) ( Bool ∷ Bool ∷ [] ) ( Bool ∷ [] ) +-- true ∷ true ∷ false ∷ true ∷ true ∷ false ∷ true ∷ [] + +-- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where +-- someday ... + +LBBℕ : Bijection (List (List Bool)) ℕ +LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ)) + ? ? ? ? where + + atob : List (List Bool) → List Bool ∧ List Bool + atob [] = ⟪ [] , [] ⟫ + atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫ + atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫ + + btoa : List Bool ∧ List Bool → List (List Bool) + btoa ⟪ [] , _ ⟫ = [] + btoa ⟪ _ ∷ _ , [] ⟫ = [] + btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ + btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫ + ... | [] = ( h ∷ [] ) ∷ [] + ... | x ∷ y = (h ∷ x ) ∷ y + +Lℕ=ℕ : Bijection (List ℕ) ℕ +Lℕ=ℕ = record { + fun→ = λ x → ? + ; fun← = λ n → ? + ; fiso→ = ? + ; fiso← = ? + }
--- a/automaton-in-agda/src/derive.agda Sun Jul 09 16:03:43 2023 +0900 +++ b/automaton-in-agda/src/derive.agda Mon Jul 10 11:52:28 2023 +0900 @@ -81,6 +81,7 @@ -- term generate x & y for each * and & only once -- rank : Regex → ℕ -- r₀ & r₁ ... r +-- generated state is a subset of the term set open import Relation.Binary.Definitions
--- a/automaton-in-agda/src/finiteSetUtil.agda Sun Jul 09 16:03:43 2023 +0900 +++ b/automaton-in-agda/src/finiteSetUtil.agda Mon Jul 10 11:52:28 2023 +0900 @@ -13,7 +13,7 @@ open import nat open import finiteSet open import fin -open import Data.Nat.Properties as NatP hiding ( _≟_ ) +open import Data.Nat.Properties as NP hiding ( _≟_ ) open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) record Found ( Q : Set ) (p : Q → Bool ) : Set where @@ -55,14 +55,14 @@ next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false → End m p - next-end {m} p prev m<n np i m<i with NatP.<-cmp m (toℕ i) + next-end {m} p prev m<n np i m<i with NP.<-cmp m (toℕ i) next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c ) next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ< m<n ≡ i m<n=i i refl m<n = fromℕ<-toℕ i m<n found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true - found {p} q pt = found1 finite (NatP.≤-refl ) ( first-end p ) where + found {p} q pt = found1 finite (NP.≤-refl ) ( first-end p ) where found1 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → ((i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false ) → exists1 m m<n p ≡ true found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt ) found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true @@ -75,7 +75,7 @@ true ∎ where open ≡-Reasoning not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false - not-found {p} pn = not-found2 finite NatP.≤-refl where + not-found {p} pn = not-found2 finite NP.≤-refl where not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ finite ) → exists1 m m<n p ≡ false not-found2 zero _ = refl not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n)) @@ -87,7 +87,7 @@ false ∎ where open ≡-Reasoning found← : { p : Q → Bool } → exists p ≡ true → Found Q p - found← {p} exst = found2 finite NatP.≤-refl (first-end p ) where + found← {p} exst = found2 finite NP.≤-refl (first-end p ) where found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p → Found Q p found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q) z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where lemma : (λ z → p (Q←F (F←Q z))) ≡ p @@ -316,17 +316,17 @@ F2L : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n → Bool ) → Vec Bool n F2L {Q} {zero} fin _ Q→B = [] -F2L {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NatP.<-trans n<m a<sa ) qb1 where +F2L {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NP.<-trans n<m a<sa ) qb1 where lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m )) a<sa ) qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool - qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa) + qb1 q q<n = Q→B q (NP.<-trans q<n a<sa) List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → Q → Bool List2Func {Q} {zero} fin (s≤s z≤n) [] q = false List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m ... | yes _ = h -... | no _ = List2Func {Q} fin (NatP.<-trans n<m a<sa ) t q +... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q open import Level renaming ( suc to Suc ; zero to Zero) open import Axiom.Extensionality.Propositional @@ -344,21 +344,21 @@ lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m)) ≟ fromℕ< n<m lemma2 | yes p = refl lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) ) - lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NatP.<-trans n<m a<sa) t q + lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NP.<-trans n<m a<sa) t q lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl) lemma4 q _ | no ¬p = refl - lemma3f : F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t + lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t lemma3f = begin - F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) - ≡⟨ cong (λ k → F2L fin (NatP.<-trans n<m a<sa) ( λ q q<n → k q q<n )) + F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) + ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n )) (f-extensionality ( λ q → (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩ - F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NatP.<-trans n<m a<sa) t q ) - ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩ + F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q ) + ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩ t ∎ where open ≡-Reasoning @@ -375,7 +375,7 @@ lemma13 : {n nq : ℕ } → (n<m : n < m ) → ¬ ( nq ≡ n ) → nq ≤ n → nq < n lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl ) lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n - lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n) + lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n) lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt) lemma3f (s≤s lt) = refl lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m @@ -392,7 +392,7 @@ f q ∎ where open ≡-Reasoning - l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q) + l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q) fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) fin→ {A} fin = iso-fin fin2List iso where @@ -431,29 +431,29 @@ lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i} refl ) lemma10f : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n lemma10f refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl )) - lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c + lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NP.<-trans a<b b<c ≡ a<c lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl) - lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x + lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x lemma11f {n} {x} n<m = begin - toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) + toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡⟨ toℕ-fromℕ< _ ⟩ toℕ x ∎ where open ≡-Reasoning fun← iso (elm1 elm x) = fromℕ< x - fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m ))) to<n where + fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m ))) to<n where x<n : toℕ x < n x<n = toℕ<n x - to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m)))) < n - to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NatP.<-trans x<n n<m) )) x<n ) + to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m)))) < n + to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NP.<-trans x<n n<m) )) x<n ) fiso← iso x = lemma2 where lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym - (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) - (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x + (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) + (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x lemma2 = begin fromℕ< (subst (λ k → toℕ k < n) (sym - (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) - (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) + (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) + (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡⟨⟩ fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 ) ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩ @@ -464,8 +464,8 @@ x ∎ where open ≡-Reasoning - lemma6 : toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) < n - lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) + lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n + lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) fiso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm) lemma13 = begin @@ -473,13 +473,13 @@ ≡⟨ toℕ-fromℕ< _ ⟩ toℕ (FiniteSet.F←Q fa elm) ∎ where open ≡-Reasoning - lemma : FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm + lemma : FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm lemma = begin - FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) + FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡⟨⟩ - FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) + FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ - FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans x n<m)) + FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m)) ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) (HE.≅-to-≡ (lemma8 refl)) ⟩ FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm))) ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩ @@ -569,3 +569,92 @@ dl01 : fin-dup-in-list (F←Q finq (Q←F finq (FDup-in-list.dup dl))) (map (F←Q finq) qs) ≡ true dl01 = subst (λ k → fin-dup-in-list k (map (F←Q finq) qs) ≡ true ) (sym (finiso← finq _)) ( FDup-in-list.is-dup dl ) + +open import bijection using ( InjectiveF ; Is ) + +inject-fin : {A B : Set} (fa : FiniteSet A ) + → (fi : InjectiveF B A) + → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a) ) + → FiniteSet B +inject-fin {A} {B} fa fi is-B = B<n→B (inf00 (finite fa) NP.≤-refl ) where + f = InjectiveF.f fi + record B<n ( n : ℕ ) : Set where + field + b : B + b<n : toℕ (F←Q fa (f b)) < n + B<n→B : FiniteSet (B<n (finite fa)) → FiniteSet B + B<n→B b<n = record { + finite = finite b<n + ; Q←F = λ fb → B<n.b (Q←F b<n fb ) + ; F←Q = λ b → F←Q b<n record { b = b ; b<n = fin<n } + ; finiso→ = ? + ; finiso← = ? + } + inf00 : (n : ℕ ) → n ≤ finite fa → FiniteSet (B<n n) + inf00 zero lt = record { + finite = 0 + ; Q←F = inf03 + ; F←Q = inf01 + ; finiso→ = inf02 + ; finiso← = λ () + } where + inf03 : Fin 0 → B<n zero + inf03 () + inf01 : B<n zero → Fin 0 + inf01 b with B<n.b<n b + ... | le = ⊥-elim ( nat-≤> le (s≤s z≤n )) + inf02 : (b : B<n zero) → inf03 (inf01 b) ≡ b + inf02 b = ⊥-elim ( nat-≤> (B<n.b<n b) (s≤s z≤n ) ) + inf00 (suc n) le with is-B ( Q←F fa ( fromℕ< {n} ? )) + ... | yes isb = record { + finite = suc (finite bp) + ; Q←F = info05 + ; F←Q = ? + ; finiso→ = ? + ; finiso← = ? + } where + n≤fa : suc n ≤ finite fa + n≤fa = le + bp : FiniteSet (B<n n) + bp = inf00 n (NP.≤-trans a≤sa le ) + info05 : Fin (suc (finite bp)) → B<n (suc n) + info05 x with <-cmp (toℕ x) (finite bp) + ... | tri< a ¬b ¬c = record { b = B<n.b (Q←F bp ? ) ; b<n = ? } + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? + -- zero = record { b = Is.a isb ; b<n = ? } + -- info05 (suc x) = record { b = B<n.b (Q←F bp x) ; b<n = ? } + info06 : B<n (suc n) → Fin (suc (finite bp)) + info06 x with <-cmp (toℕ (F←Q fa (f (B<n.b x)))) n + ... | tri< a ¬b ¬c = fromℕ< {toℕ (F←Q fa (f (B<n.b x)))} ? + ... | tri≈ ¬a b ¬c = fromℕ< {n} ? + ... | tri> ¬a ¬b c = ? + ... | no nisb = record { + finite = finite bp + ; Q←F = λ x → record { b = B<n.b ( Q←F ? x) ; b<n = ? } + ; F←Q = ? + ; finiso→ = ? + ; finiso← = ? + } where + bp : FiniteSet (B<n n) + bp = inf00 n (NP.≤-trans a≤sa le ) + +-- record { +-- finite = ? +-- ; Q←F = ? +-- ; F←Q = ? +-- ; finiso→ = ? +-- ; finiso← = ? +-- } where +-- f = InjectiveF.f fi +-- f⁻¹ : (a : A ) → Is B A f a → B +-- f⁻¹ a isa = Is.a isa +-- +-- record CountB (b : B) : Set where +-- cb : ℕ +-- a : A +-- fb=a : InjectiveF.f fi b ≡ a +-- + + +
--- a/automaton-in-agda/src/nat.agda Sun Jul 09 16:03:43 2023 +0900 +++ b/automaton-in-agda/src/nat.agda Mon Jul 10 11:52:28 2023 +0900 @@ -45,12 +45,43 @@ <-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) <-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) +≤-∨ : { x y : ℕ } → x ≤ y → ( (x ≡ y ) ∨ (x < y) ) +≤-∨ {zero} {zero} z≤n = case1 refl +≤-∨ {zero} {suc y} z≤n = case2 (s≤s z≤n) +≤-∨ {suc x} {zero} () +≤-∨ {suc x} {suc y} (s≤s lt) with ≤-∨ {x} {y} lt +≤-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) +≤-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) + max : (x y : ℕ) → ℕ max zero zero = zero max zero (suc x) = (suc x) max (suc x) zero = (suc x) max (suc x) (suc y) = suc ( max x y ) +x≤max : (x y : ℕ) → x ≤ max x y +x≤max zero zero = ≤-refl +x≤max zero (suc x) = z≤n +x≤max (suc x) zero = ≤-refl +x≤max (suc x) (suc y) = s≤s( x≤max x y ) + +y≤max : (x y : ℕ) → y ≤ max x y +y≤max zero zero = ≤-refl +y≤max zero (suc x) = ≤-refl +y≤max (suc x) zero = z≤n +y≤max (suc x) (suc y) = s≤s( y≤max x y ) + +x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y +x≤y→max=y zero zero x≤y = refl +x≤y→max=y zero (suc y) x≤y = refl +x≤y→max=y (suc x) (suc y) (s≤s x≤y) = cong suc (x≤y→max=y x y x≤y ) + +y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x +y≤x→max=x zero zero y≤x = refl +y≤x→max=x zero (suc y) () +y≤x→max=x (suc x) zero lt = refl +y≤x→max=x (suc x) (suc y) (s≤s y≤x) = cong suc (y≤x→max=x x y y≤x ) + -- _*_ : ℕ → ℕ → ℕ -- _*_ zero _ = zero -- _*_ (suc n) m = m + ( n * m ) @@ -201,14 +232,25 @@ <to≤ {zero} {suc y} (s≤s z≤n) = z≤n <to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y} lt) +<∨≤ : ( x y : ℕ ) → (x < y ) ∨ (y ≤ x) +<∨≤ x y with <-cmp x y +... | tri< a ¬b ¬c = case1 a +... | tri≈ ¬a refl ¬c = case2 ≤-refl +... | tri> ¬a ¬b c = case2 (<to≤ c) + refl-≤s : {x : ℕ } → x ≤ suc x refl-≤s {zero} = z≤n refl-≤s {suc x} = s≤s (refl-≤s {x}) +a≤sa = refl-≤s + refl-≤ : {x : ℕ } → x ≤ x refl-≤ {zero} = z≤n refl-≤ {suc x} = s≤s (refl-≤ {x}) +refl-≤≡ : {x y : ℕ } → x ≡ y → x ≤ y +refl-≤≡ refl = refl-≤ + x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) @@ -226,6 +268,26 @@ px≤py {zero} {suc y} lt = z≤n px≤py {suc x} {suc y} (s≤s lt) = lt +sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x ≤ y +sx≤py→x≤y (s≤s lt) = lt + +sx<py→x<y : {x y : ℕ } → suc x < suc y → x < y +sx<py→x<y (s≤s lt) = lt + +sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x ≤ y +sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n +sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le) + +x<sy→x≤y : {x y : ℕ } → x < suc y → x ≤ y +x<sy→x≤y {zero} {suc y} (s≤s le) = z≤n +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 i-j=0→i=j : {i j : ℕ } → j ≤ i → i - j ≡ 0 → i ≡ j @@ -280,9 +342,16 @@ minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y) ≡ x - z minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z}) ++cancel<l : (x z : ℕ ) {y : ℕ} → y + x < y + z → x < z ++cancel<l x z {zero} lt = lt ++cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt + ++cancel<r : (x z : ℕ ) {y : ℕ} → x + y < z + y → x < z ++cancel<r x z {y} lt = +cancel<l x z (subst₂ (λ j k → j < k ) (+-comm x _) (+-comm z _) lt ) + y-x<y : {x y : ℕ } → 0 < x → 0 < y → y - x < y y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y) -... | tri< a ¬b ¬c = +-cancelʳ-< (y - x) _ ( begin +... | tri< a ¬b ¬c = +cancel<r (y - x) _ ( begin suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩ suc y ≡⟨ +-comm 1 _ ⟩ y + suc 0 ≤⟨ +-mono-≤ ≤-refl 0<x ⟩ @@ -681,3 +750,4 @@ ; ind = λ {p} prev → ind p prev } +