Mercurial > hg > Members > kono > Proof > automaton

changeset 173:6835096cfa3a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bij
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Mar 2021 08:27:05 +0900
parents 684f53fb9b2c
children 0e87089e5de4
files agda/halt.agda
diffstat 1 files changed, 24 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/agda/halt.agda	Sun Mar 14 02:32:11 2021 +0900
+++ b/agda/halt.agda	Sun Mar 14 08:27:05 2021 +0900
@@ -115,6 +115,8 @@
 
 open import nat
 
+open ≡-Reasoning
+
 --   []     0
 --   0    → 1
 --   1    → 2
@@ -128,7 +130,7 @@
        fun←  = λ x → lton x 
      ; fun→  = λ n → ntol n 
      ; fiso← = lbiso0 
-     ; fiso→ = {!!}
+     ; fiso→ = lbisor
    } where
      lton1 : List Bool → ℕ
      lton1 [] = 0
@@ -149,13 +151,30 @@
      xx :   (x : ℕ ) → List Bool ∧ ℕ
      xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
      lbiso1 :  (x : ℕ) → suc (lton1 (ntol1 x)) ≡ suc x
-     lbiso1 = {!!}
+     lbiso1 zero = refl
+     lbiso1 (suc x) with div2 (suc x)
+     ... | ⟪ x1 , true ⟫ = begin
+         suc (suc (lton1 (ntol1 x1) + lton1 (ntol1 x1))) ≡⟨ {!!} ⟩
+         suc (lton1 (ntol1 x1)) + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + k ) (lbiso1 x1) ⟩
+         suc x1 + suc x1 ≡⟨ {!!} ⟩
+         suc (suc (x1 + x1)) ≡⟨ {!!} ⟩
+         suc (suc x) ∎ 
+     ... | ⟪ x1 , false ⟫ = {!!}
      lbiso0 :  (x : ℕ) → lton (ntol x)  ≡ x
      lbiso0 zero = refl
      lbiso0 (suc zero) = refl
-     lbiso0 (suc (suc x)) = subst (λ k → k ≡ suc (suc x)) {!!} ( lbiso1 (suc x)) where
-        hh : suc (lton1 (ntol1 (suc x))) ≡ lton (ntol (suc (suc x)))
-        hh = ?
+     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
+     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) = {!!}
 
 
 open import Axiom.Extensionality.Propositional