Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/bijection.agda @ 266:e5cf49902db3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 17 Nov 2021 16:12:30 +0900 |
| parents | c47634c830f3 |
| children | cd91a9f313dd |
line wrap: on
line diff
--- a/automaton-in-agda/src/bijection.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/automaton-in-agda/src/bijection.agda Wed Nov 17 16:12:30 2021 +0900 @@ -98,13 +98,10 @@ open _∧_ -record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) (n→nxn : ℕ → ℕ ∧ ℕ) : Set where +record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) : Set where field - j k sum stage : ℕ - nn : j + k ≡ sum - ni : i ≡ j + stage -- not used + j k : ℕ 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 @@ -123,11 +120,11 @@ 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 zero = ⟪ 0 , 0 ⟫ - n→nxn (suc i) with n→nxn i - ... | ⟪ x , zero ⟫ = ⟪ zero , suc x ⟫ - ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫ + 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 ⟫ @@ -191,56 +188,64 @@ 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 + nni>j : {i : ℕ} → suc i > NN.j (nn i) ----- -- -- create the invariant NN for all n -- - 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)) + ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 ; sum = suc (sum ) ; stage = suc (sum ) + (stage ) ; nn = refl ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ; nn-unique = nn04 } where --- --- increment the stage --- - sum = NN.sum (nn i) - stage = NN.stage (nn i) + 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 + NNni : i ≡ NN.j (nn i) + stage + NNni = begin + i ≡⟨ sym (minus+n {i} {NN.j (nn i)} (nni>j {i} )) ⟩ + stage + NN.j (nn i) ≡⟨ +-comm stage _ ⟩ + NN.j (nn i) + stage ∎ where open ≡-Reasoning nn01 : suc i ≡ 0 + (suc sum + stage ) nn01 = begin - suc i ≡⟨ cong suc (NN.ni (nn i)) ⟩ + suc i ≡⟨ cong suc (NNni ) ⟩ 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)) ⟩ + suc ((NN.j (nn i) + NN.k (nn i)) + stage ) ≡⟨ cong (λ k → suc ( k + stage )) (NNnn ) ⟩ 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 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 - 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 : n→nxn (suc i) ≡ ⟪ 0 , suc (sum ) ⟫ -- 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 (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (cong proj1 refl) ⟩ ⟪ 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)) ⟩ + ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫ ) (NNnn ) ⟩ ⟪ 0 , suc sum ⟫ ∎ where open ≡-Reasoning - ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 (NN.k0 (nn i)))) (begin + ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 refl)) (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 : {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 @@ -252,7 +257,7 @@ 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) ⟩ + 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 @@ -264,18 +269,28 @@ 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 + ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = sum ; stage = stage ; nn = nn10 + ; ni = cong suc (NNni (nn i)) ; k1 = nn11 ; k0 = nn12 ; nn-unique = nn13 } where --- --- increment in a stage --- - nn10 : suc (NN.j (nn i)) + k ≡ NN.sum (nn i) + 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 + NNni : i ≡ NN.j (nn i) + stage + NNni = begin + i ≡⟨ sym (minus+n {i} {NN.j (nn i)} (nni>j {i} )) ⟩ + stage + NN.j (nn i) ≡⟨ +-comm stage _ ⟩ + NN.j (nn i) + stage ∎ where open ≡-Reasoning + 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) ≡⟨ NN.nn (nn i) ⟩ - NN.sum (nn i) ∎ where open ≡-Reasoning + 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) ⟩ @@ -291,13 +306,14 @@ ... | ⟪ 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)) ) ⟩ + NN.k (nn i) ≡⟨ cong proj2 (sym refl ) ⟩ 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) ⟩ + n→nxn i ≡⟨ refl ⟩ ⟪ 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 @@ -320,13 +336,21 @@ 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)) + n-id i = subst (λ k → nxn→n (proj1 k) (proj2 k) ≡ i ) (sym refl) (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)) ⟩ + 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 + nni>j {zero} = refl-≤ + nni>j {suc i} = {!!} + -- nni>j {i} {n} = begin + -- suc (NN.j n) ≤⟨ {!!} ⟩ + -- suc (nxn→n (NN.j n) (NN.k n)) ≡⟨ {!!} ⟩ + -- suc i ∎ where + -- open ≤-Reasoning + -- [] 0