|
141
|
1 module halt where
|
|
|
2
|
|
|
3 open import Level renaming ( zero to Zero ; suc to Suc )
|
|
|
4 open import Data.Nat
|
|
142
|
5 open import Data.Maybe
|
|
141
|
6 open import Data.List hiding ([_])
|
|
|
7 open import Data.Nat.Properties
|
|
|
8 open import Relation.Nullary
|
|
|
9 open import Data.Empty
|
|
|
10 open import Data.Unit
|
|
142
|
11 open import Relation.Binary.Core hiding (_⇔_)
|
|
141
|
12 open import Relation.Binary.Definitions
|
|
|
13 open import Relation.Binary.PropositionalEquality
|
|
|
14
|
|
|
15 open import logic
|
|
|
16
|
|
|
17 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
|
|
|
18 field
|
|
|
19 fun← : S → R
|
|
|
20 fun→ : R → S
|
|
|
21 fiso← : (x : R) → fun← ( fun→ x ) ≡ x
|
|
|
22 fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x
|
|
|
23
|
|
164
|
24 injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
|
|
|
25 injection R S f = (x y : R) → f x ≡ f y → x ≡ y
|
|
|
26
|
|
141
|
27 open Bijection
|
|
|
28
|
|
164
|
29 b→injection0 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection R S (fun→ b)
|
|
|
30 b→injection0 R S b x y eq = begin
|
|
|
31 x
|
|
|
32 ≡⟨ sym ( fiso← b x ) ⟩
|
|
|
33 fun← b ( fun→ b x )
|
|
|
34 ≡⟨ cong (λ k → fun← b k ) eq ⟩
|
|
|
35 fun← b ( fun→ b y )
|
|
|
36 ≡⟨ fiso← b y ⟩
|
|
|
37 y
|
|
|
38 ∎ where open ≡-Reasoning
|
|
|
39
|
|
|
40 b→injection1 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection S R (fun← b)
|
|
|
41 b→injection1 R S b x y eq = trans ( sym ( fiso→ b x ) ) (trans ( cong (λ k → fun→ b k ) eq ) ( fiso→ b y ))
|
|
|
42
|
|
|
43 -- ¬ A = A → ⊥
|
|
|
44
|
|
174
|
45 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool
|
|
164
|
46 diag b n = not (fun← b n n)
|
|
|
47
|
|
174
|
48 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S
|
|
|
49 diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
|
|
|
50 diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n )
|
|
164
|
51 diagn1 n dn = ¬t=f (diag b n ) ( begin
|
|
|
52 not (diag b n)
|
|
141
|
53 ≡⟨⟩
|
|
|
54 not (not fun← b n n)
|
|
|
55 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩
|
|
164
|
56 not (fun← b (fun→ b (diag b)) n)
|
|
141
|
57 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
|
|
|
58 not (fun← b n n)
|
|
|
59 ≡⟨⟩
|
|
164
|
60 diag b n
|
|
141
|
61 ∎ ) where open ≡-Reasoning
|
|
|
62
|
|
164
|
63 b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ
|
|
|
64 b1 b = fun→ b (diag b)
|
|
|
65
|
|
|
66 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
|
|
|
67 b-iso b = fiso← b _
|
|
|
68
|
|
|
69 postulate
|
|
|
70 utm : List Bool → List Bool → Maybe Bool
|
|
|
71
|
|
|
72 record TM : Set where
|
|
|
73 field
|
|
|
74 tm : List Bool → Maybe Bool
|
|
|
75 encode : List Bool
|
|
|
76 is-tm : utm encode ≡ tm
|
|
|
77
|
|
|
78 open TM
|
|
|
79
|
|
|
80 Halt1 : TM → List Bool → Bool -- ℕ → ( ℕ → Bool )
|
|
|
81 Halt1 = {!!}
|
|
|
82
|
|
|
83 record Halt1-is-tm : Set where
|
|
|
84 field
|
|
|
85 htm : TM
|
|
|
86 htm-is-Halt1 : (t : TM ) → (x : List Bool) → (Halt1 t x ≡ true) ⇔ ((tm htm (encode t ++ x)) ≡ just true)
|
|
|
87
|
|
|
88 Halt2 : (tm : TM ) → List Bool -- ( ℕ → Bool ) → ℕ
|
|
|
89 Halt2 tm = encode tm
|
|
|
90
|
|
|
91 not-halt : {!!}
|
|
|
92 not-halt = {!!}
|
|
|
93
|
|
141
|
94 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
|
|
|
95 to1 {n} {R} b = record {
|
|
|
96 fun← = to11
|
|
|
97 ; fun→ = to12
|
|
|
98 ; fiso← = to13
|
|
|
99 ; fiso→ = to14
|
|
|
100 } where
|
|
|
101 to11 : ⊤ ∨ R → ℕ
|
|
|
102 to11 (case1 tt) = 0
|
|
|
103 to11 (case2 x) = suc ( fun← b x )
|
|
|
104 to12 : ℕ → ⊤ ∨ R
|
|
|
105 to12 zero = case1 tt
|
|
|
106 to12 (suc n) = case2 ( fun→ b n)
|
|
|
107 to13 : (x : ℕ) → to11 (to12 x) ≡ x
|
|
|
108 to13 zero = refl
|
|
|
109 to13 (suc x) = cong suc (fiso← b x)
|
|
|
110 to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
|
|
|
111 to14 (case1 x) = refl
|
|
|
112 to14 (case2 x) = cong case2 (fiso→ b x)
|
|
|
113
|
|
|
114 open _∧_
|
|
|
115
|
|
172
|
116 open import nat
|
|
|
117
|
|
173
|
118 open ≡-Reasoning
|
|
|
119
|
|
172
|
120 -- [] 0
|
|
|
121 -- 0 → 1
|
|
|
122 -- 1 → 2
|
|
|
123 -- 01 → 3
|
|
|
124 -- 11 → 4
|
|
|
125 -- ...
|
|
141
|
126 --
|
|
172
|
127 {-# TERMINATING #-}
|
|
|
128 LBℕ : Bijection ℕ ( List Bool )
|
|
|
129 LBℕ = record {
|
|
|
130 fun← = λ x → lton x
|
|
|
131 ; fun→ = λ n → ntol n
|
|
|
132 ; fiso← = lbiso0
|
|
173
|
133 ; fiso→ = lbisor
|
|
172
|
134 } where
|
|
|
135 lton1 : List Bool → ℕ
|
|
|
136 lton1 [] = 0
|
|
|
137 lton1 (true ∷ t) = suc (lton1 t + lton1 t)
|
|
|
138 lton1 (false ∷ t) = lton1 t + lton1 t
|
|
|
139 lton : List Bool → ℕ
|
|
|
140 lton [] = 0
|
|
|
141 lton x = suc (lton1 x)
|
|
|
142 ntol1 : ℕ → List Bool
|
|
|
143 ntol1 0 = []
|
|
|
144 ntol1 (suc x) with div2 (suc x)
|
|
|
145 ... | ⟪ x1 , true ⟫ = true ∷ ntol1 x1
|
|
|
146 ... | ⟪ x1 , false ⟫ = false ∷ ntol1 x1
|
|
|
147 ntol : ℕ → List Bool
|
|
|
148 ntol 0 = []
|
|
|
149 ntol 1 = false ∷ []
|
|
|
150 ntol (suc n) = ntol1 n
|
|
|
151 xx : (x : ℕ ) → List Bool ∧ ℕ
|
|
|
152 xx x = ⟪ (ntol x) , lton ((ntol x)) ⟫
|
|
175
|
153 ---- div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
|
|
172
|
154 lbiso1 : (x : ℕ) → suc (lton1 (ntol1 x)) ≡ suc x
|
|
173
|
155 lbiso1 zero = refl
|
|
175
|
156 lbiso1 (suc x) with div2 (suc x) | inspect div2 (suc x)
|
|
|
157 ... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin
|
|
173
|
158 suc (suc (lton1 (ntol1 x1) + lton1 (ntol1 x1))) ≡⟨ {!!} ⟩
|
|
|
159 suc (lton1 (ntol1 x1)) + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + k ) (lbiso1 x1) ⟩
|
|
|
160 suc x1 + suc x1 ≡⟨ {!!} ⟩
|
|
|
161 suc (suc (x1 + x1)) ≡⟨ {!!} ⟩
|
|
|
162 suc (suc x) ∎
|
|
175
|
163 ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = {!!}
|
|
172
|
164 lbiso0 : (x : ℕ) → lton (ntol x) ≡ x
|
|
|
165 lbiso0 zero = refl
|
|
|
166 lbiso0 (suc zero) = refl
|
|
173
|
167 lbiso0 (suc (suc x)) = subst (λ k → k ≡ suc (suc x)) (hh x) ( lbiso1 (suc x)) where
|
|
|
168 hh : (x : ℕ ) → suc (lton1 (ntol1 (suc x))) ≡ lton (ntol (suc (suc x)))
|
|
|
169 hh x with div2 (suc x)
|
|
|
170 ... | ⟪ proj3 , true ⟫ = refl
|
|
|
171 ... | ⟪ proj3 , false ⟫ = refl
|
|
|
172 lbisor : (x : List Bool) → ntol (lton x) ≡ x
|
|
|
173 lbisor [] = refl
|
|
|
174 lbisor (false ∷ []) = refl
|
|
|
175 lbisor (true ∷ []) = refl
|
|
174
|
176 lbisor (false ∷ true ∷ t) = {!!}
|
|
|
177 lbisor (false ∷ false ∷ t) = {!!}
|
|
173
|
178 lbisor (true ∷ x ∷ t) = {!!}
|
|
141
|
179
|
|
|
180
|
|
|
181 open import Axiom.Extensionality.Propositional
|
|
|
182 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n
|
|
|
183 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
|
|
|
184
|
|
142
|
185 record Halt : Set where
|
|
|
186 field
|
|
|
187 htm : TM
|
|
|
188 is-halt : (t : TM ) → (x : List Bool ) → (tm htm (encode t ++ x) ≡ just true) ⇔ ((tm t x ≡ just true) ∨ (tm t x ≡ just false))
|
|
|
189 nhtm : TM
|
|
|
190 nhtm-is-negation : (t : TM ) → (x : List Bool ) → (tm htm (encode t ++ x) ≡ just true) ⇔ (tm nhtm (encode t ++ x) ≡ nothing )
|
|
|
191
|
|
|
192 open Halt
|
|
|
193
|
|
141
|
194 tm-cong : {x y : TM} → tm x ≡ tm y → encode x ≡ encode y → is-tm x ≅ is-tm y → x ≡ y
|
|
|
195 tm-cong refl refl refl = refl
|
|
|
196
|
|
|
197 tm-bij : Bijection TM (List Bool)
|
|
|
198 tm-bij = record {
|
|
|
199 fun← = λ x → record { tm = utm x ; encode = x ; is-tm = refl }
|
|
|
200 ; fun→ = λ tm → encode tm
|
|
|
201 ; fiso← = tmb1
|
|
|
202 ; fiso→ = λ x → refl
|
|
|
203 } where
|
|
|
204 tmb1 : (x : TM ) → record { tm = utm (encode x) ; encode = encode x ; is-tm = refl } ≡ x
|
|
|
205 tmb1 x with is-tm x | inspect is-tm x
|
|
|
206 ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
|
|
|
207
|
|
174
|
208 TNℕ : Halt → Bijection (TM → Bool) TM
|
|
164
|
209 TNℕ = {!!}
|
|
|
210
|
|
|
211 -- Halt1 (Halt2 x) ≡ x
|
|
|
212 -- Halt2 (Halt2 y) ≡ y
|
|
|
213
|
|
142
|
214 halting : ¬ Halt
|
|
|
215 halting h with tm (htm h) (encode (nhtm h) ++ encode (nhtm h))
|
|
|
216 ... | just true = ¬t=f {!!} {!!}
|
|
|
217 ... | nothing = {!!}
|
|
|
218 ... | just false = {!!}
|
