module halt 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 

open Bijection 

diagonal : ¬ Bijection  ( ℕ → Bool ) ℕ
diagonal b = diagn1 (fun→ b diag) refl where
    diag :  ℕ → Bool
    diag n = not (fun← b n n)
    diagn1 : (n : ℕ ) → ¬ (fun→ b diag ≡ n ) 
    diagn1 n dn = ¬t=f (diag n ) ( begin
           not diag n 
        ≡⟨⟩
           not (not fun← b n n)
        ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
           not (fun← b (fun→ b diag)  n)
        ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
           not (fun← b n n)
        ≡⟨⟩
           diag n 
        ∎ ) where open ≡-Reasoning

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 _∧_

--   []     case1
--   0    → case2 10   
--   0111 → case2 10111
--
LBℕ : Bijection  ( List Bool ) ℕ
LBℕ = {!!}

postulate
   utm         : List Bool → List Bool → Maybe Bool

open import Axiom.Extensionality.Propositional
postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) 

record TM : Set where
   field
      tm : List Bool → Maybe Bool
      encode : List Bool
      is-tm : utm encode ≡ tm

open TM

record Halt : Set where
   field
      htm : TM
      is-halt :          (t : TM ) → (x : List Bool ) → (tm htm  (encode t ++ x) ≡ just true) ⇔ ((tm t x ≡ just true) ∨ (tm t x ≡ just false)) 
      nhtm : TM
      nhtm-is-negation : (t : TM ) → (x : List Bool ) → (tm htm (encode t ++ x) ≡ just true) ⇔ (tm nhtm (encode t ++ x) ≡ nothing )

open Halt

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 = 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

halting : ¬ Halt
halting h with tm (htm h) (encode (nhtm h) ++ encode (nhtm h))
... | just true = ¬t=f {!!} {!!}
... | nothing = {!!}
... | just false = {!!}