Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/bijection.agda @ 256:5aff0067b194
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Jul 2021 11:10:15 +0900 |
| parents | 3fa72793620b |
| children | 246da8456ad1 |
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda Thu Jul 01 19:07:19 2021 +0900 +++ b/automaton-in-agda/src/bijection.agda Mon Jul 05 11:10:15 2021 +0900 @@ -3,16 +3,17 @@ open import Level renaming ( zero to Zero ; suc to Suc ) open import Data.Nat open import Data.Maybe -open import Data.List hiding ([_]) +open import Data.List hiding ([_] ; sum ) open import Data.Nat.Properties open import Relation.Nullary open import Data.Empty -open import Data.Unit +open import Data.Unit hiding ( _≤_ ) 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 @@ -60,6 +61,229 @@ diag b n ∎ ) where open ≡-Reasoning + +open _∧_ + +record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) (n→nxn : ℕ → ℕ ∧ ℕ) : Set where + field + j k sum stage : ℕ + nn : j + k ≡ sum + ni : i ≡ j + stage + k1 : nxn→n j k ≡ i + k0 : n→nxn i ≡ ⟪ j , k ⟫ + 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← = n-id + ; 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)) + n→nxn : ℕ → ℕ ∧ ℕ + n→nxn zero = ⟪ 0 , 0 ⟫ + n→nxn (suc i) with n→nxn i + ... | ⟪ x , zero ⟫ = ⟪ zero , suc x ⟫ + ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫ + + 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} ) + + 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 + + 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 + + nn : ( i : ℕ) → NN i nxn→n n→nxn + nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = 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 (NN.sum (nn i)) ; j = 0 ; sum = suc (NN.sum (nn i)) ; stage = suc (NN.sum (nn i)) + (NN.stage (nn i)) + ; nn = refl + ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ; nn-unique = nn04 } where + sum = NN.sum (nn i) + stage = NN.stage (nn i) + j = NN.j (nn i) + nn01 : suc i ≡ 0 + (suc sum + stage ) + nn01 = begin + suc i ≡⟨ cong suc (NN.ni (nn i)) ⟩ + suc ((NN.j (nn i) ) + stage ) ≡⟨ cong (λ k → suc (k + stage )) (+-comm 0 _ ) ⟩ + suc ((NN.j (nn i) + 0 ) + stage ) ≡⟨ cong (λ k → suc ((NN.j (nn i) + k) + stage )) (sym eq) ⟩ + suc ((NN.j (nn i) + NN.k (nn i)) + stage ) ≡⟨ cong (λ k → suc ( k + stage )) (NN.nn (nn i)) ⟩ + 0 + (suc sum + stage ) ∎ where open ≡-Reasoning + 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 (NN.nn (nn i))) ⟩ + 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 + nn03 : n→nxn (suc i) ≡ ⟪ 0 , suc (NN.sum (nn i)) ⟫ -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫ + nn03 with n→nxn i | inspect n→nxn i + ... | ⟪ x , zero ⟫ | record { eq = eq1 } = begin + ⟪ zero , suc x ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (sym (cong proj1 eq1)) ⟩ + ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (cong proj1 (NN.k0 (nn i))) ⟩ + ⟪ zero , suc (NN.j (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (+-comm 0 _ ) ⟩ + ⟪ zero , suc (NN.j (nn i) + 0) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc (NN.j (nn i) + k) ⟫ ) (sym eq) ⟩ + ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫ ) (NN.nn (nn i)) ⟩ + ⟪ 0 , suc sum ⟫ ∎ where open ≡-Reasoning + ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 (NN.k0 (nn i)))) (begin + suc (NN.k (nn i)) ≡⟨ cong suc eq ⟩ + suc 0 ≤⟨ s≤s z≤n ⟩ + suc y ≡⟨ sym (cong proj2 eq1) ⟩ + proj2 (n→nxn i) ∎ )) where open ≤-Reasoning + -- nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j + nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (NN.sum (nn i)) ⟫ ≡ ⟪ 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) ≡⟨ NN.nn (nn i) ⟩ + 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)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = nn10 + ; ni = cong suc (NN.ni (nn i)) ; k1 = nn11 ; k0 = nn12 ; nn-unique = nn13 } where + nn10 : suc (NN.j (nn i)) + k ≡ NN.sum (nn i) + 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) ≡⟨ NN.nn (nn i) ⟩ + NN.sum (nn i) ∎ 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 + nn12 : n→nxn (suc i) ≡ ⟪ suc (NN.j (nn i)) , k ⟫ -- n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ + nn12 with n→nxn i | inspect n→nxn i + ... | ⟪ x , zero ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 eq1)) + (subst (λ k → 0 < k ) ( begin + suc k ≡⟨ sym eq ⟩ + NN.k (nn i) ≡⟨ cong proj2 (sym (NN.k0 (nn i)) ) ⟩ + proj2 (n→nxn i) ∎ ) (s≤s z≤n )) ) where open ≡-Reasoning -- eq1 n→nxn i ≡ ⟪ x , zero ⟫ + ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = begin -- n→nxn i ≡ ⟪ x , suc y ⟫ + ⟪ suc x , y ⟫ ≡⟨ refl ⟩ + ⟪ suc x , pred (suc y) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin + ⟪ x , suc y ⟫ ≡⟨ sym eq1 ⟩ + n→nxn i ≡⟨ NN.k0 (nn i) ⟩ + ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ∎ ) ⟩ + ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫) eq ⟩ + ⟪ suc (NN.j (nn i)) , k ⟫ ∎ 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 + + n-id : (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i + n-id i = subst (λ k → nxn→n (proj1 k) (proj2 k) ≡ i ) (sym (NN.k0 (nn i))) (NN.k1 (nn i)) + + nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫ + nn-id j k = begin + n→nxn (nxn→n j k) ≡⟨ NN.k0 (nn (nxn→n j k)) ⟩ + ⟪ 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 + + b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ b1 b = fun→ b (diag b)