Mercurial > hg > Members > kono > Proof > automaton

changeset 181:9c63284d7695

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Mar 2021 09:39:10 +0900
parents 4c5d26c149fa
children 567754463810
files agda/bijection.agda agda/prime.agda
diffstat 2 files changed, 36 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/agda/bijection.agda	Thu Mar 18 07:47:39 2021 +0900
+++ b/agda/bijection.agda	Thu Mar 18 09:39:10 2021 +0900
@@ -117,7 +117,7 @@
      ntol1 : ℕ → List Bool 
      ntol1 0 = []
      ntol1 (suc x) with div2 (suc x)
-     ... | ⟪ x1 , true  ⟫ = true  ∷ ntol1 x1
+     ... | ⟪ x1 , true  ⟫ = true  ∷ ntol1 x1 -- non terminating
      ... | ⟪ x1 , false ⟫ = false ∷ ntol1 x1
      ntol : ℕ → List Bool 
      ntol 0 = []
@@ -125,32 +125,56 @@
      ntol (suc n) = ntol1 n
      xx :   (x : ℕ ) → List Bool ∧ ℕ
      xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
+     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)))
+     add12 : (x1 x : ℕ ) → suc x1 + x ≡ x1 + suc x
+     add12 zero x = refl
+     add12 (suc x1) x = cong suc (add12 x1 x)
      ---- div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
+     div20 : (x x1 : ℕ ) → div2 (suc x) ≡ ⟪ x1 , false ⟫ → x1 + x1 ≡ suc x
+     div20 x x1 eq = begin
+         x1 + x1 ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
+         div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
+         suc x ∎ 
+     div21 : (x x1 : ℕ ) → div2 (suc x) ≡ ⟪ x1 , true ⟫  → suc  (x1 + x1) ≡ suc x
+     div21 x x1 eq = begin
+         suc  (x1 + x1) ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
+         div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
+         suc x ∎ 
      lbiso1 :  (x : ℕ) → suc (lton1 (ntol1 x)) ≡ suc x
      lbiso1 zero = refl
      lbiso1 (suc x) with div2 (suc x) | inspect div2 (suc x)
      ... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin
-         suc (suc (lton1 (ntol1 x1) + lton1 (ntol1 x1))) ≡⟨ {!!} ⟩
+         suc (suc (lton1 (ntol1 x1) + lton1 (ntol1 x1))) ≡⟨ sym (add11 _) ⟩
          suc (lton1 (ntol1 x1)) + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + k ) (lbiso1 x1) ⟩
-         suc x1 + suc x1 ≡⟨ {!!} ⟩
-         suc (suc  (x1 + x1)) ≡⟨ cong (λ k → suc (suc (div2-rev k) )) {!!} ⟩
-         suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k )) (div2-eq x ) ⟩
+         suc x1 + suc x1 ≡⟨ add11 x1 ⟩
+         suc (suc  (x1 + x1)) ≡⟨ cong suc (div21 x x1 eq1) ⟩
          suc (suc x) ∎ 
-     ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = {!!}
+     ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
+         suc (lton1 (ntol1 x1) + lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + lton1 (ntol1 x1) ) (lbiso1 x1) ⟩
+         suc x1 + lton1 (ntol1 x1) ≡⟨ add12 _ _ ⟩
+         x1 + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → x1 + k )  (lbiso1 x1) ⟩
+         x1 + suc x1 ≡⟨ +-comm x1 _ ⟩
+         suc (x1 + x1) ≡⟨ cong suc (div20 x x1 eq1) ⟩
+         suc (suc x) ∎ 
      lbiso0 :  (x : ℕ) → lton (ntol x)  ≡ x
      lbiso0 zero = refl
      lbiso0 (suc zero) = refl
      lbiso0 (suc (suc x)) = subst (λ k → k ≡ suc (suc x)) (hh x) ( lbiso1 (suc x)) where
         hh : (x : ℕ ) → suc (lton1 (ntol1 (suc x))) ≡ lton (ntol (suc (suc x)))
         hh x with div2 (suc x)
-        ... | ⟪ proj3 , true ⟫ = refl
-        ... | ⟪ proj3 , false ⟫ = refl
+        ... | ⟪ _ , true ⟫ = refl
+        ... | ⟪ _ , false ⟫ = refl
+     lbisor0 :  (x : List Bool) → ntol1 (lton1 (true ∷ x))  ≡ true ∷ x
+     lbisor0 = {!!}
+     lbisor1 :  (x : List Bool) → ntol1 (lton1 (false ∷ x))  ≡ false ∷ x
+     lbisor1 = {!!}
      lbisor :  (x : List Bool) → ntol (lton x)  ≡ x
      lbisor [] = refl
      lbisor (false ∷ []) = refl
      lbisor (true ∷ []) = refl
-     lbisor (false ∷ true ∷ t) = {!!}
-     lbisor (false ∷ false ∷ t) = {!!}
-     lbisor (true ∷ x ∷ t) = {!!}
+     lbisor (false ∷ t) = trans {!!} ( lbisor1 t ) 
+     lbisor (true ∷  t) = trans {!!} ( lbisor0 t ) 
 
 
--- a/agda/prime.agda	Thu Mar 18 07:47:39 2021 +0900
+++ b/agda/prime.agda	Thu Mar 18 09:39:10 2021 +0900
@@ -24,7 +24,7 @@
       dividable : Dividable factor n
 
 isPrime : ( n : ℕ ) → Dec ( Prime n )
-isPrime = ?
+isPrime = {!!}
 
 nonPrime : ( n : ℕ ) → ¬ Prime n → NonPrime n
 nonPrime n np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where