Mercurial > hg > Members > kono > Proof > automaton

changeset 176:728cd6f7bf56

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 Sun, 14 Mar 2021 21:33:23 +0900
parents bf50676c77af
children 375e1dcba6aa
files agda/bijection.agda agda/halt.agda
diffstat 2 files changed, 166 insertions(+), 114 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/bijection.agda	Sun Mar 14 21:33:23 2021 +0900
@@ -0,0 +1,156 @@
+module bijection where
+
+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.Nat.Properties
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Unit
+open import  Relation.Binary.Core hiding (_⇔_)
+open import  Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+
+open import logic
+
+record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
+   field
+       fun←  :  S → R
+       fun→  :  R → S
+       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 
+
+b→injection0 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection R S (fun→ b)
+b→injection0 R S b x y eq = begin
+          x
+        ≡⟨ sym ( fiso← b x ) ⟩
+          fun← b ( fun→ b x )
+        ≡⟨ cong (λ k → fun← b k ) eq ⟩
+          fun← b ( fun→ b y )
+        ≡⟨  fiso← b y  ⟩
+          y  
+        ∎  where open ≡-Reasoning
+
+b→injection1 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection S R (fun← b)
+b→injection1 R S b x y eq = trans (  sym ( fiso→ b x ) ) (trans (  cong (λ k → fun→ b k ) eq ) ( fiso→ b y  ))
+
+--  ¬ A = A → ⊥ 
+
+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 (diag b) ) refl where
+    diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) 
+    diagn1 n dn = ¬t=f (diag b n ) ( begin
+           not (diag b n)
+        ≡⟨⟩
+           not (not fun← b n n)
+        ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
+           not (fun← b (fun→ b (diag b))  n)
+        ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
+           not (fun← b n n)
+        ≡⟨⟩
+           diag b n 
+        ∎ ) where open ≡-Reasoning
+
+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 _
+
+to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
+to1 {n} {R} b = record {
+       fun←  = to11
+     ; fun→  = to12
+     ; fiso← = to13
+     ; fiso→ = to14
+   } where
+       to11 : ⊤ ∨ R → ℕ
+       to11 (case1 tt) = 0
+       to11 (case2 x) = suc ( fun← b x )
+       to12 : ℕ → ⊤ ∨ R
+       to12 zero = case1 tt
+       to12 (suc n) = case2 ( fun→ b n)
+       to13 : (x : ℕ) → to11 (to12 x) ≡ x
+       to13 zero = refl
+       to13 (suc x) = cong suc (fiso← b x)
+       to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
+       to14 (case1 x) = refl
+       to14 (case2 x) = cong case2 (fiso→ b x)
+
+open _∧_
+
+open import nat
+
+open ≡-Reasoning
+
+--   []     0
+--   0    → 1
+--   1    → 2
+--   01   → 3
+--   11   → 4
+--   ...
+--
+{-# TERMINATING #-}
+LBℕ : Bijection ℕ ( List Bool ) 
+LBℕ = record {
+       fun←  = λ x → lton x 
+     ; fun→  = λ n → ntol n 
+     ; fiso← = lbiso0 
+     ; fiso→ = lbisor
+   } where
+     lton1 : List Bool → ℕ
+     lton1 [] = 0
+     lton1 (true ∷ t) = suc (lton1 t + lton1 t)
+     lton1 (false ∷ t) = lton1 t + lton1 t
+     lton : List Bool → ℕ
+     lton [] = 0
+     lton x  = suc (lton1 x)
+     ntol1 : ℕ → List Bool 
+     ntol1 0 = []
+     ntol1 (suc x) with div2 (suc x)
+     ... | ⟪ x1 , true  ⟫ = true  ∷ ntol1 x1
+     ... | ⟪ x1 , false ⟫ = false ∷ ntol1 x1
+     ntol : ℕ → List Bool 
+     ntol 0 = []
+     ntol 1 = false ∷ []
+     ntol (suc n) = ntol1 n
+     xx :   (x : ℕ ) → List Bool ∧ ℕ
+     xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
+     ---- div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ 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 (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 (suc x) ∎ 
+     ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = {!!}
+     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
+     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) = {!!}
+
+
--- a/agda/halt.agda	Sun Mar 14 19:18:51 2021 +0900
+++ b/agda/halt.agda	Sun Mar 14 21:33:23 2021 +0900
@@ -14,38 +14,23 @@
 
 open import logic
 
-record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
+record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
    field
        fun←  :  S → R
        fun→  :  R → S
        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
-       fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x 
+--  normal bijection required below, but we don't need this to show the inconsistency
+--     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 HBijection 
 
-b→injection0 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection R S (fun→ b)
-b→injection0 R S b x y eq = begin
-          x
-        ≡⟨ sym ( fiso← b x ) ⟩
-          fun← b ( fun→ b x )
-        ≡⟨ cong (λ k → fun← b k ) eq ⟩
-          fun← b ( fun→ b y )
-        ≡⟨  fiso← b y  ⟩
-          y  
-        ∎  where open ≡-Reasoning
-
-b→injection1 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection S R (fun← b)
-b→injection1 R S b x y eq = trans (  sym ( fiso→ b x ) ) (trans (  cong (λ k → fun→ b k ) eq ) ( fiso→ b y  ))
-
---  ¬ A = A → ⊥ 
-
-diag : {S : Set }  (b : Bijection  ( S → Bool ) S) → S → Bool
+diag : {S : Set }  (b : HBijection  ( S → Bool ) S) → S → Bool
 diag b n = not (fun← b n n)
 
-diagonal : { S : Set } → ¬ Bijection  ( S → Bool ) S
+diagonal : { S : Set } → ¬ HBijection  ( S → Bool ) S
 diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
     diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) 
     diagn1 n dn = ¬t=f (diag b n ) ( begin
@@ -60,12 +45,6 @@
            diag b n 
         ∎ ) where open ≡-Reasoning
 
-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 _
-
 postulate
    utm         : List Bool → List Bool → Maybe Bool
 
@@ -91,92 +70,10 @@
 not-halt : {!!}
 not-halt = {!!}
 
-to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
-to1 {n} {R} b = record {
-       fun←  = to11
-     ; fun→  = to12
-     ; fiso← = to13
-     ; fiso→ = to14
-   } where
-       to11 : ⊤ ∨ R → ℕ
-       to11 (case1 tt) = 0
-       to11 (case2 x) = suc ( fun← b x )
-       to12 : ℕ → ⊤ ∨ R
-       to12 zero = case1 tt
-       to12 (suc n) = case2 ( fun→ b n)
-       to13 : (x : ℕ) → to11 (to12 x) ≡ x
-       to13 zero = refl
-       to13 (suc x) = cong suc (fiso← b x)
-       to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
-       to14 (case1 x) = refl
-       to14 (case2 x) = cong case2 (fiso→ b x)
-
 open _∧_
 
-open import nat
-
 open ≡-Reasoning
 
---   []     0
---   0    → 1
---   1    → 2
---   01   → 3
---   11   → 4
---   ...
---
-{-# TERMINATING #-}
-LBℕ : Bijection ℕ ( List Bool ) 
-LBℕ = record {
-       fun←  = λ x → lton x 
-     ; fun→  = λ n → ntol n 
-     ; fiso← = lbiso0 
-     ; fiso→ = lbisor
-   } where
-     lton1 : List Bool → ℕ
-     lton1 [] = 0
-     lton1 (true ∷ t) = suc (lton1 t + lton1 t)
-     lton1 (false ∷ t) = lton1 t + lton1 t
-     lton : List Bool → ℕ
-     lton [] = 0
-     lton x  = suc (lton1 x)
-     ntol1 : ℕ → List Bool 
-     ntol1 0 = []
-     ntol1 (suc x) with div2 (suc x)
-     ... | ⟪ x1 , true  ⟫ = true  ∷ ntol1 x1
-     ... | ⟪ x1 , false ⟫ = false ∷ ntol1 x1
-     ntol : ℕ → List Bool 
-     ntol 0 = []
-     ntol 1 = false ∷ []
-     ntol (suc n) = ntol1 n
-     xx :   (x : ℕ ) → List Bool ∧ ℕ
-     xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
-     ---- div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ 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 (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 ⟫ | record { eq = eq1 } = {!!}
-     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
-     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
 postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
@@ -191,23 +88,22 @@
 
 open Halt
 
+TNℕ : Halt → HBijection (TM → Bool) TM
+TNℕ = {!!}
+
 tm-cong : {x y : TM} → tm x ≡ tm y → encode x ≡ encode y → is-tm x ≅ is-tm y → x ≡ y
 tm-cong refl refl refl  = refl
 
-tm-bij :  Bijection TM (List Bool)
+tm-bij :  HBijection TM (List Bool)
 tm-bij = record {
        fun←  = λ x → record { tm = utm x ; encode = x ; is-tm = refl }
      ; fun→  = λ tm → encode tm
      ; fiso← = tmb1
-     ; fiso→ = λ x → refl
     }  where
          tmb1 : (x : TM ) →  record { tm = utm (encode x) ; encode = encode x ; is-tm = refl } ≡ x
          tmb1 x with is-tm x | inspect is-tm x
          ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
 
-TNℕ : Halt → Bijection (TM → Bool) TM
-TNℕ = {!!}
-
 --  Halt1 (Halt2 x) ≡ x
 --  Halt2 (Halt2 y) ≡ y